Use PROGRAM_TYPE for programs and oracles (#127)

Author: ajreynol

src/cmd_parser.cpp

@@ -144,7 +144,6 @@ bool CmdParser::parseNextCommand()
       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)
       {
         sorts = d_eparser.parseTypeList();
@@ -180,7 +179,9 @@ bool CmdParser::parseNextCommand()
       t = ret;
       if (!sorts.empty())
       {
-        t = d_state.mkFunctionType(sorts, ret, flattenFunction);
+        t = (tok == Token::DECLARE_ORACLE_FUN)
+                ? d_state.mkProgramType(sorts, ret)
+                : d_state.mkFunctionType(sorts, ret);
       }
       std::vector<Expr> opaqueArgs;
       while (t.getKind()==Kind::FUNCTION_TYPE && t[0].getKind()==Kind::OPAQUE_TYPE)
@@ -733,7 +734,7 @@ bool CmdParser::parseNextCommand()
       Expr progType = retType;
       if (!argTypes.empty())
       {
-        progType = d_state.mkFunctionType(argTypes, retType, false);
+        progType = d_state.mkProgramType(argTypes, retType);
       }
       // it may have been forward declared
       Expr pprev = d_state.getVar(name);

src/expr_parser.cpp

@@ -597,7 +597,7 @@ Expr ExprParser::parseExpr()
               Trace("parser") << "Binder is " << vl << std::endl;
               Trace("parser") << "Env is " << env << std::endl;
               // make the program variable, whose type is abstract
-              Expr ftype = d_state.mkFunctionType(fargTypes, atype, false);
+              Expr ftype = d_state.mkProgramType(fargTypes, atype);
               std::stringstream pvname;
               pvname << "eo::match_" << hd;
               Expr pv = d_state.mkSymbol(Kind::PROGRAM_CONST, pvname.str(), ftype);

src/kind.cpp

@@ -19,6 +19,7 @@ std::ostream& operator<<(std::ostream& o, Kind k)
     case Kind::NONE: o << "NONE"; break;
     case Kind::TYPE: o << "TYPE"; break;
     case Kind::FUNCTION_TYPE: o << "FUNCTION_TYPE"; break;
+    case Kind::PROGRAM_TYPE: o << "PROGRAM_TYPE"; break;
     case Kind::PROOF_TYPE: o << "PROOF_TYPE"; break;
     case Kind::ABSTRACT_TYPE: o << "ABSTRACT_TYPE"; break;
     case Kind::BOOL_TYPE: o << "BOOL_TYPE"; break;
@@ -110,6 +111,7 @@ std::string kindToTerm(Kind k)
   {
     case Kind::TYPE: ss << "Type"; break;
     case Kind::FUNCTION_TYPE: ss << "->"; break;
+    case Kind::PROGRAM_TYPE: ss << "eo::arrow"; break;
     case Kind::PROOF_TYPE: ss << "Proof"; break;
     case Kind::ABSTRACT_TYPE: ss << "?"; break;
     case Kind::BOOL_TYPE: ss << "Bool"; break;

src/kind.h

@@ -23,12 +23,13 @@ enum class Kind
   // types
   TYPE,
   FUNCTION_TYPE,
+  PROGRAM_TYPE,
   PROOF_TYPE,
   ABSTRACT_TYPE,
   BOOL_TYPE,
   QUOTE_TYPE,
   OPAQUE_TYPE,  // an argument marked :opaque, temporary during parsing
-  NULL_TYPE,         // an argument marked :implicit, temporary during parsing
+  NULL_TYPE,    // an argument marked :implicit, temporary during parsing
 
   // terms
   APPLY,
@@ -43,7 +44,8 @@ enum class Kind
   // symbols
   PARAM,
   CONST,
-  BUILTIN_CONST,    // used for e.g. _, ->, eo::*, as, etc. which are temporary during parsing only
+  BUILTIN_CONST,  // used for e.g. _, ->, eo::*, as, etc. which are temporary
+                  // during parsing only
   PROGRAM_CONST,
   PROOF_RULE,
   VARIABLE,

src/state.cpp

@@ -556,6 +556,18 @@ Expr State::mkFunctionType(const std::vector<Expr>& args, const Expr& ret, bool
   return curr;
 }
 
+Expr State::mkProgramType(const std::vector<Expr>& args, const Expr& ret)
+{
+  Assert(!args.empty());
+  std::vector<ExprValue*> atypes;
+  for (size_t i = 0, nargs = args.size(); i < nargs; i++)
+  {
+    atypes.push_back(args[i].getValue());
+  }
+  atypes.push_back(ret.getValue());
+  return Expr(mkExprInternal(Kind::PROGRAM_TYPE, atypes));
+}
+
 Expr State::mkRequires(const std::vector<Expr>& args, const Expr& ret)
 {
   Expr curr = ret;

src/state.h

@@ -98,6 +98,8 @@ class State
   Expr mkTypeConstant(const std::string& name, size_t arity);
   /** (-> <type>+ <type>) */
   Expr mkFunctionType(const std::vector<Expr>& args, const Expr& ret, bool flatten = true);
+  /** (-> <type>+ <type>) */
+  Expr mkProgramType(const std::vector<Expr>& args, const Expr& ret);
   /** ? */
   Expr mkAbstractType();
   /** Bool */

src/type_checker.cpp

@@ -241,7 +241,7 @@ Expr TypeChecker::getTypeInternal(ExprValue* e, std::ostream* out)
     case Kind::ABSTRACT_TYPE:
     case Kind::BOOL_TYPE:
     case Kind::FUNCTION_TYPE:
-      return d_state.mkType();
+    case Kind::PROGRAM_TYPE: return d_state.mkType();
     case Kind::PROOF_TYPE:
     {
       ExprValue* ctype = d_state.lookupType(e->d_children[0]);
@@ -343,7 +343,8 @@ Expr TypeChecker::getTypeAppInternal(std::vector<ExprValue*>& children,
   ExprValue* hd = children[0];
   ExprValue* hdType = d_state.lookupType(hd);
   Assert(hdType != nullptr) << "No type for " << Expr(hd);
-  if (hdType->getKind()!=Kind::FUNCTION_TYPE)
+  Kind hk = hdType->getKind();
+  if (hk != Kind::FUNCTION_TYPE && hk != Kind::PROGRAM_TYPE)
   {
     // non-function at head
     if (out)