More

Author: ajreynol

NEWS.md

@@ -5,12 +5,12 @@ 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.
+- 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 now 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.
+- Adds support for the SMT-LIB `as` annotations for ambiguous functions and constants, i.e. those whose return type cannot be inferred from their argument types. Following SMT-LIB convention, ambiguous functions and constants are expected to be annotated with their *return* type using `as`, which internally is treated as a type argument to the function. This policy is applied both for ambiguous datatype constructors and ambiguous functions and constants declared with `declare-parameterized-const`.
 - 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.
 

src/cmd_parser.cpp

@@ -230,30 +230,32 @@ bool CmdParser::parseNextCommand()
           }
           t = d_state.mkFunctionType({qt}, t);
         }
-        if (tok==Token::DECLARE_PARAMETERIZED_CONST)
+      }
+      if (tok==Token::DECLARE_PARAMETERIZED_CONST)
+      {
+        // If this is an ambiguous function, we add (Quote T)
+        // as the first argument type. We only need to test if we are parsing
+        // the command declare-parameterized-const.
+        std::pair<std::vector<Expr>, Expr> ft = t.getFunctionType();
+        std::vector<Expr> argTypes = ft.first;
+        argTypes.insert(argTypes.end(), opaqueArgs.begin(), opaqueArgs.end());
+        Expr tup = d_state.mkExpr(Kind::TUPLE, argTypes);
+        std::vector<Expr> pargs = Expr::getVariables(tup);
+        Expr fv = d_eparser.findFreeVar(ft.second, pargs);
+        Trace("ajr-temp") << "Looking for free variable in " << ft.second << " returned " << fv << std::endl;
+        if (!fv.isNull())
         {
-          // if this is an ambiguous datatype constructor, we add (Quote T)
-          // as the first argument type.
-          std::pair<std::vector<Expr>, Expr> ft = t.getFunctionType();
-          std::vector<Expr> argTypes = ft.first;
-          argTypes.insert(argTypes.end(), opaqueArgs.begin(), opaqueArgs.end());
-          Expr tup = d_state.mkExpr(Kind::TUPLE, argTypes);
-          std::vector<Expr> pargs = Expr::getVariables(tup);
-          Expr fv = d_eparser.findFreeVar(ft.second, pargs);
-          if (!fv.isNull())
+          if (ck!=Attr::NONE)
           {
-            if (ck!=Attr::NONE)
-            {
-              d_lex.parseError("Ambiguous functions cannot have attributes");
-            }
-            else if(!opaqueArgs.empty())
-            {
-              d_lex.parseError("Ambiguous functions cannot have opaque arguments");
-            }
-            Expr qt = d_state.mkQuoteType(ft.second);
-            t = d_state.mkFunctionType({qt}, t);
-            ck = Attr::AMB;
+            d_lex.parseError("Ambiguous functions cannot have attributes");
+          }
+          else if(!opaqueArgs.empty())
+          {
+            d_lex.parseError("Ambiguous functions cannot have opaque arguments");
           }
+          Expr qt = d_state.mkQuoteType(ft.second);
+          t = d_state.mkFunctionType({qt}, t);
+          ck = Attr::AMB;
         }
       }
       // now process remainder of map