Refactor declare-parameterized-const in preparation for deprecating :var

NEWS.md

@@ -5,14 +5,19 @@ 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 interface 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.
+
 - Adds support for the SMT-LIB `as` annotations for ambiguous datatype constructors, i.e. those whose return type cannot be inferred from its argument types. Following SMT-LIB convention, ambiguous datatype constructors are expected to be annotated with their *return* type using `as`, which internally is treated as a type argument to the constructor.
 - The semantics for `eo::dt_constructors` is extended for instantiated parametric datatypes. For example calling `eo::dt_constructors` on `(List Int)` returns the list containing `cons` and `(as nil (List Int))`.
 - The semantics for `eo::dt_selectors` is extended for annotated constructors. For example calling `eo::dt_selectors` on `(as nil (List Int))` returns the empty list.
-- 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.
+
 - Added the option `--stats-all` to track the number of times side conditions are invoked.
 - The option `--print-let` has been renamed to `--print-dag` and is now enabled by default. The printer is changed to use `eo::define` instead of `let`.
 - Ethos now explicitly forbids `:var`, `:implicit`, and `:opaque` on return types.
-- The operator `eo::typeof` now fails to evaluate if the type of the given term is not ground.
+- The option `--binder-fresh`, which specified for fresh variables to be constructed when parsing binders, has been removed.
 
 ethos 0.1.1
 ===========

src/cmd_parser.cpp

@@ -137,11 +137,13 @@ bool CmdParser::parseNextCommand()
     case Token::DECLARE_PARAMETERIZED_CONST:
     case Token::DECLARE_ORACLE_FUN:
     {
-      //d_state.checkThatLogicIsSet();
       std::string name = d_eparser.parseSymbol();
       //d_state.checkUserSymbol(name);
       std::vector<Expr> sorts;
+      // the parameters, if declare-parameterized-const
       std::vector<Expr> params;
+      // attributes marked on variables
+      std::map<ExprValue*, AttrMap> pattrMap;
       bool flattenFunction = (tok != Token::DECLARE_ORACLE_FUN);
       if (tok == Token::DECLARE_FUN || tok == Token::DECLARE_ORACLE_FUN)
       {
@@ -150,7 +152,7 @@ bool CmdParser::parseNextCommand()
       else if (tok == Token::DECLARE_PARAMETERIZED_CONST)
       {
         d_state.pushScope();
-        params = d_eparser.parseAndBindSortedVarList();
+        params = d_eparser.parseAndBindSortedVarList(Kind::CONST, pattrMap);
       }
       Expr ret = d_eparser.parseType();
       Attr ck = Attr::NONE;
@@ -172,7 +174,7 @@ bool CmdParser::parseNextCommand()
         AttrMap attrs;
         d_eparser.parseAttributeList(Kind::CONST, t, attrs);
         // determine if an attribute specified a constructor kind
-        d_eparser.processAttributeMap(attrs, ck, cons, params);
+        d_eparser.processAttributeMap(attrs, ck, cons);
       }
       // declare-fun does not parse attribute list, as it is only in smt2
       t = ret;
@@ -188,6 +190,44 @@ bool CmdParser::parseNextCommand()
         opaqueArgs.push_back(t[0][0]);
         t = t[1];
       }
+      // process the parameter list
+      if (!params.empty())
+      {
+        // explicit parameters are quote arrows
+        std::map<ExprValue*, AttrMap>::iterator itp;
+        AttrMap::iterator itpa;
+        for (size_t i = 0, nparams = params.size(); i < nparams; i++)
+        {
+          size_t ii = nparams - i - 1;
+          Expr qt = d_state.mkQuoteType(params[ii]);
+          itp = pattrMap.find(params[ii].getValue());
+          if (itp != pattrMap.end())
+          {
+            itpa = itp->second.find(Attr::REQUIRES);
+            if (itpa != itp->second.end())
+            {
+              // requires adds to return type
+              t = d_state.mkRequires(itpa->second, t);
+              itp->second.erase(itpa);
+            }
+            itpa = itp->second.find(Attr::OPAQUE);
+            if (itpa != itp->second.end())
+            {
+              // if marked opaque, it is an opaque argument
+              opaqueArgs.insert(opaqueArgs.begin(), qt);
+              itp->second.erase(itpa);
+              continue;
+            }
+          }
+          if (!opaqueArgs.empty())
+          {
+            d_lex.parseError("Opaque arguments must be a prefix of arguments.");
+          }
+          t = d_state.mkFunctionType({qt}, t);
+        }
+      }
+      // now process remainder of map
+      d_eparser.processAttributeMaps(pattrMap);
       if (!opaqueArgs.empty())
       {
         if (ck!=Attr::NONE)
@@ -328,7 +368,7 @@ bool CmdParser::parseNextCommand()
         }
       }
       std::vector<Expr> vs =
-          d_eparser.parseAndBindSortedVarList();
+          d_eparser.parseAndBindSortedVarList(Kind::PROOF_RULE);
       Expr assume;
       Expr plCons;
       std::vector<Expr> premises;
@@ -488,9 +528,11 @@ bool CmdParser::parseNextCommand()
       std::string name = d_eparser.parseSymbol();
       //d_state.checkUserSymbol(name);
       std::vector<Expr> impls;
+      std::vector<Expr> opaques;
+      std::map<ExprValue*, AttrMap> pattrMap;
       std::vector<Expr> vars =
-          d_eparser.parseAndBindSortedVarList(impls);
-      if (!impls.empty())
+          d_eparser.parseAndBindSortedVarList(Kind::LAMBDA, pattrMap);
+      if (vars.size() < pattrMap.size())
       {
         // If there were implicit variables, we go back and refine what is
         // bound in the body to only include the explicit arguments. This
@@ -506,6 +548,8 @@ bool CmdParser::parseNextCommand()
           d_state.bind(e.getSymbol(), e);
         }
       }
+      // now process remainder of map
+      d_eparser.processAttributeMaps(pattrMap);
       Expr ret;
       if (tok == Token::DEFINE_FUN)
       {
@@ -682,7 +726,8 @@ bool CmdParser::parseNextCommand()
       }
       // push the scope
       d_state.pushScope();
-      std::vector<Expr> vars = d_eparser.parseAndBindSortedVarList();
+      std::vector<Expr> vars =
+          d_eparser.parseAndBindSortedVarList(Kind::PROGRAM);
       std::vector<Expr> argTypes = d_eparser.parseTypeList();
       Expr retType = d_eparser.parseType();
       Expr progType = retType;

src/expr.h

@@ -118,9 +118,9 @@ class Expr
   explicit Expr(const ExprValue* ev);
   Expr(const Expr& e);
   ~Expr();
-  /** Get the free symbols */
+  /** Get the free parameters in expression e */
   static std::vector<Expr> getVariables(const Expr& e);
-  /** Get the free symbols in vector es */
+  /** Get the free parameters in vector es */
   static std::vector<Expr> getVariables(const std::vector<Expr>& es);
   /** Get the free symbols */
   static bool hasVariable(const Expr& e,

src/expr_parser.cpp

@@ -161,7 +161,7 @@ Expr ExprParser::parseExpr()
           {
             // parse the variable list
             d_state.pushScope();
-            std::vector<Expr> vs = parseAndBindSortedVarList();
+            std::vector<Expr> vs = parseAndBindSortedVarList(Kind::PROGRAM);
             std::vector<Expr> args;
             args.emplace_back(d_state.mkExpr(Kind::TUPLE, vs));
             pstack.emplace_back(ParseCtx::MATCH_HEAD, 1, args);
@@ -194,10 +194,8 @@ Expr ExprParser::parseExpr()
             if (ck==Attr::BINDER || ck==Attr::LET_BINDER)
             {
               // If it is a binder, immediately read the bound variable list.
-              // If option d_binderFresh is true, we parse and bind fresh
-              // variables. Otherwise, we make calls to State::getBoundVar
-              // meaning the bound variables are unique for each (name, type)
-              // pair.
+              // We make calls to State::getBoundVar meaning the bound variables
+              // are unique for each (name, type) pair.
               // We only do this if there are two left parentheses. Otherwise we
               // will parse a tuple term that stands for a symbolic bound
               // variable list. We do this because there are no terms that
@@ -213,10 +211,9 @@ Expr ExprParser::parseExpr()
                   if (ck==Attr::BINDER)
                   {
                     nscopes = 1;
-                    // we always do lookups if parsing signature
-                    bool isLookup = d_isSignature || !d_state.getOptions().d_binderFresh;
                     d_state.pushScope();
-                    std::vector<Expr> vs = parseAndBindSortedVarList(isLookup);
+                    std::vector<Expr> vs =
+                        parseAndBindSortedVarList(Kind::NONE);
                     if (vs.empty())
                     {
                       d_lex.parseError("Expected non-empty sorted variable list");
@@ -764,29 +761,29 @@ std::vector<Expr> ExprParser::parseExprPairList()
   return terms;
 }
 
-std::vector<Expr> ExprParser::parseAndBindSortedVarList(bool isLookup)
+std::vector<Expr> ExprParser::parseAndBindSortedVarList(Kind k)
 {
-  std::vector<Expr> impls;
-  return parseAndBindSortedVarList(impls, isLookup);
+  std::map<ExprValue*, AttrMap> amap;
+  std::vector<Expr> vars = parseAndBindSortedVarList(k, amap);
+  processAttributeMaps(amap);
+  return vars;
 }
 
 std::vector<Expr> ExprParser::parseAndBindSortedVarList(
-                     std::vector<Expr>& impls, bool isLookup)
+    Kind k, std::map<ExprValue*, AttrMap>& amap)
 {
   std::vector<Expr> varList;
   d_lex.eatToken(Token::LPAREN);
   std::string name;
   Expr t;
-  Attr ck = Attr::NONE;
-  Expr cons;
   // while the next token is LPAREN, exit if RPAREN
   while (d_lex.eatTokenChoice(Token::LPAREN, Token::RPAREN))
   {
     name = parseSymbol();
     t = parseType();
     Expr v;
     bool isImplicit = false;
-    if (isLookup)
+    if (k == Kind::NONE)
     {
       // lookup and type check
       v = d_state.getBoundVar(name, t);
@@ -798,21 +795,14 @@ std::vector<Expr> ExprParser::parseAndBindSortedVarList(
       v = d_state.mkSymbol(Kind::PARAM, name, t);
       bind(name, v);
       // parse attribute list
-      AttrMap attrs;
-      parseAttributeList(Kind::PARAM, v, attrs);
+      AttrMap& attrs = amap[v.getValue()];
+      // 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);
         isImplicit = true;
-        impls.push_back(v);
-      }
-      // process the attribute map, which may mark the parameter as a list
-      processAttributeMap(attrs, ck, cons, {});
-      if (ck!=Attr::NONE)
-      {
-        d_state.markConstructorKind(v, ck, cons);
-        ck = Attr::NONE;
-        cons = d_null;
       }
     }
     d_lex.eatToken(Token::RPAREN);
@@ -1125,7 +1115,8 @@ 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
@@ -1165,9 +1156,26 @@ void ExprParser::parseAttributeList(Kind k, Expr& e, AttrMap& attrs, bool& pushe
       case Kind::PARAM:
       {
         // attributes on parameters
-        if (a==Attr::LIST || a==Attr::IMPLICIT)
+        // 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;
@@ -1284,10 +1292,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)
   {
@@ -1466,10 +1474,23 @@ void ExprParser::ensureBound(const Expr& e, const std::vector<Expr>& bvs)
   }
 }
 
-void ExprParser::processAttributeMap(const AttrMap& attrs,
-                                     Attr& ck,
-                                     Expr& cons,
-                                     const std::vector<Expr>& params)
+void ExprParser::processAttributeMaps(const std::map<ExprValue*, AttrMap>& amap)
+{
+  // process the attribute map, which may mark the parameter as a list
+  for (const std::pair<ExprValue* const, AttrMap>& as : amap)
+  {
+    Attr ck = Attr::NONE;
+    Expr cons;
+    processAttributeMap(as.second, ck, cons);
+    if (ck != Attr::NONE)
+    {
+      Expr v(as.first);
+      d_state.markConstructorKind(v, ck, cons);
+    }
+  }
+}
+
+void ExprParser::processAttributeMap(const AttrMap& attrs, Attr& ck, Expr& cons)
 {
   ck = Attr::NONE;
   for (const std::pair<const Attr, std::vector<Expr>>& a : attrs)
@@ -1490,18 +1511,13 @@ void ExprParser::processAttributeMap(const AttrMap& attrs,
         // if the constructor spec is non-ground, make a lambda
         if (!av.isNull() && !av.isGround())
         {
+          std::vector<Expr> params = Expr::getVariables(av);
           Assert (!params.empty());
           cons = d_state.mkParameterized(av.getValue(), params);
         }
         else
         {
           cons = av;
-          // if the nil constructor doesn't use parameters, just ignore
-          if (!params.empty())
-          {
-            Warning() << "Ignoring unused parameters for definition of "
-                      << "symbol with nil constructor " << av << std::endl;
-          }
         }
         ck = a.first;
       }