More

Author: ajreynol

NEWS.md

@@ -5,7 +5,7 @@ ethos 0.1.2 prerelease
 
 - Change the execution semantics when a program takes an unevalated term as an argument. In particular, we do not call user provided programs and oracles when at least argument could not be evaluated. This change was made to make errors more intuitive. Note this changes the semantics of programs that previously relied on being called on unevaluated terms.
 - User programs, user oracles, and builtin operators that are unapplied are now considered unevaluated. This makes the type checker more strict and disallows passing them as arguments to other programs, which previously led to undefined behavior.
-- Changes the semantics of `declare-parameterized-const`. In particular, the parameters of a parameterized constants are no longer assumed to be implicit, and are explicit by default. The `:implicit` attribute can be used on all parameters to recover the previous behavior.
+- Changes the semantics of `declare-parameterized-const`. In particular, the parameters of a parameterized constants are no longer assumed to be implicit, and are explicit by default. The `:implicit` attribute can be used on all parameters to recover the previous behavior. Other attributes such as `:opaque` and `:requires` can be used on parameters to this command.
 - Remove support for the explicit parameter annotation `eo::_`, which was used to provide annotations for implicit arguments to parameterized constants.
 - Changed the semantics of pairwise and chainable operators for a single argument, which now reduces to the neutral element of the combining operator instead of a parse error.
 - The operator `eo::typeof` now fails to evaluate if the type of the given term is not ground.

src/expr_parser.cpp

@@ -795,7 +795,9 @@ std::vector<Expr> ExprParser::parseAndBindSortedVarList(
       bind(name, v);
       // parse attribute list
       AttrMap& attrs = amap[v.getValue()];
-      parseAttributeList(Kind::PARAM, v, attrs);
+      // all other parameter lists make fresh parameters, pass along the
+      // parameter list kind k
+      parseAttributeList(Kind::PARAM, v, attrs, k);
       if (attrs.find(Attr::IMPLICIT)!=attrs.end())
       {
         attrs.erase(Attr::IMPLICIT);
@@ -1112,7 +1114,7 @@ std::string ExprParser::parseStr(bool unescape)
   return s;
 }
 
-void ExprParser::parseAttributeList(Kind k, Expr& e, AttrMap& attrs, bool& pushedScope)
+void ExprParser::parseAttributeList(Kind k, Expr& e, AttrMap& attrs, bool& pushedScope, Kind plk)
 {
   std::map<std::string, Attr>::iterator its;
   // while the next token is KEYWORD, exit if RPAREN
@@ -1152,9 +1154,30 @@ void ExprParser::parseAttributeList(Kind k, Expr& e, AttrMap& attrs, bool& pushe
       case Kind::PARAM:
       {
         // attributes on parameters
-        if (a==Attr::LIST || a==Attr::IMPLICIT || a==Attr::OPAQUE)
+        // parameter lists of define and declare-parameterized-const
+        // allow for several attributes
+        if (plk==Kind::CONST || plk==Kind::LAMBDA)
         {
           handled = true;
+          switch (a)
+          {
+            case Attr::LIST:
+            case Attr::IMPLICIT:
+            case Attr::OPAQUE:
+              // requires no value
+              break;
+            case Attr::REQUIRES:
+              val = parseExprPair();
+              break;
+            default:
+              handled = false;
+              break;
+          }
+        }
+        else
+        {
+          // all others only allow for :list
+          handled = (a==Attr::LIST);
         }
       }
         break;
@@ -1271,10 +1294,10 @@ void ExprParser::parseAttributeList(Kind k, Expr& e, AttrMap& attrs, bool& pushe
   d_lex.reinsertToken(Token::RPAREN);
 }
 
-void ExprParser::parseAttributeList(Kind k, Expr& e, AttrMap& attrs)
+void ExprParser::parseAttributeList(Kind k, Expr& e, AttrMap& attrs, Kind plk)
 {
   bool pushedScope = false;
-  parseAttributeList(k, e, attrs, pushedScope);
+  parseAttributeList(k, e, attrs, pushedScope, plk);
   // pop the scope if necessary
   if (pushedScope)
   {

src/expr_parser.h

@@ -131,10 +131,12 @@ class ExprParser
    * @param pushedScope True if we pushed a scope while reading the list. This
    * is true when e.g. the attribute :var is read. The caller of this method
    * is responsible for popping the scope.
+   * @param plk If k is PARAM, this is the category of the parameter list
+   * which that parameter belongs to
    */
-  void parseAttributeList(Kind k, Expr& e, AttrMap& attrs, bool& pushedScope);
+  void parseAttributeList(Kind k, Expr& e, AttrMap& attrs, bool& pushedScope, Kind plk = Kind::NONE);
   /** Same as above, but ensures we pop the scope */
-  void parseAttributeList(Kind k, Expr& e, AttrMap& attrs);
+  void parseAttributeList(Kind k, Expr& e, AttrMap& attrs, Kind plk = Kind::NONE);
 
   /**
    * Parse literal kind.