Merge branch 'main' into progTypes

Author: ajreynol

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,19 +137,21 @@ 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;
       if (tok == Token::DECLARE_FUN || tok == Token::DECLARE_ORACLE_FUN)
       {
         sorts = d_eparser.parseTypeList();
       }
       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;
@@ -171,7 +173,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;
@@ -189,6 +191,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)
@@ -329,7 +369,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;
@@ -489,9 +529,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
@@ -507,6 +549,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)
       {
@@ -683,7 +727,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.cpp

@@ -236,8 +236,7 @@ std::string quoteSymbol(const std::string& s)
 std::map<const ExprValue*, size_t> Expr::computeLetBinding(
     const Expr& e, std::vector<Expr>& ll)
 {
-  size_t idc = 0;
-  std::map<const ExprValue*, size_t> lbind;
+  std::map<const ExprValue*, size_t> lcount;
   std::unordered_set<const ExprValue*> visited;
   std::vector<Expr> visit;
   std::vector<Expr> llv;
@@ -246,35 +245,41 @@ std::map<const ExprValue*, size_t> Expr::computeLetBinding(
   do
   {
     cur = visit.back();
-    visit.pop_back();
     if (cur.getNumChildren() == 0)
     {
+      visit.pop_back();
       continue;
     }
     const ExprValue* cv = cur.getValue();
     if (visited.find(cv) == visited.end())
     {
       visited.insert(cv);
-      llv.push_back(cur);
       for (size_t i = 0, nchildren = cur.getNumChildren(); i < nchildren; i++)
       {
         visit.push_back(cur[i]);
       }
       continue;
     }
-    if (lbind.find(cv) == lbind.end())
+    visit.pop_back();
+    // add to vector, which is done after all subterms of cv are added to llv
+    if (lcount.find(cv) == lcount.end())
     {
-      lbind[cv] = idc;
-      idc++;
+      llv.push_back(cur);
     }
+    lcount[cv]++;
   }while(!visit.empty());
+  // go back and only keep the ones that were found more than once.
+  std::map<const ExprValue*, size_t> lbind;
+  size_t idc = 0;
   for (size_t i=0, lsize = llv.size(); i<lsize; i++)
   {
-    const Expr& l = llv[lsize - 1 - i];
+    const Expr& l = llv[i];
     const ExprValue* lv = l.getValue();
-    if (lbind.find(lv) != lbind.end())
+    if (lcount[lv] > 1)
     {
       ll.push_back(l);
+      lbind[lv] = idc;
+      idc++;
     }
   }
   return lbind;

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,