Refactor type ascriptions in the parser (#3825)

Towards parser migration.

This consolidates two blocks of code (cvc/smt2) that do type ascriptions to a utility function in the parser. It updates this function to use the new API.

This code will be further refactored when the interface for parametric datatype constructors is further developed in the new API.

6 files changed, 108 insertions, 79 deletions

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index dca61fe48..3fde52bbe 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -1836,23 +1836,8 @@ postfixTerm[CVC4::Expr& f]
       { f = (args.size() == 1) ? MK_CONST(bool(true)) : MK_EXPR(CVC4::kind::DISTINCT, args); }
     )
     ( typeAscription[f, t]
-      { if(f.getKind() == CVC4::kind::APPLY_CONSTRUCTOR && t.isDatatype()) {
-          std::vector<CVC4::Expr> v;
-          Expr e = f.getOperator();
-          const DatatypeConstructor& dtc = Datatype::datatypeOf(e)[Datatype::indexOf(e)];
-          v.push_back(MK_EXPR( CVC4::kind::APPLY_TYPE_ASCRIPTION,
-                               MK_CONST(AscriptionType(dtc.getSpecializedConstructorType(t))), f.getOperator() ));
-          v.insert(v.end(), f.begin(), f.end());
-          f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, v);
-        } else if(f.getKind() == CVC4::kind::EMPTYSET && t.isSet()) {
-          f = MK_CONST(CVC4::EmptySet(t));
-        } else if(f.getKind() == CVC4::kind::UNIVERSE_SET && t.isSet()) {
-          f = EXPR_MANAGER->mkNullaryOperator(t, kind::UNIVERSE_SET);
-        } else {
-          if(f.getType() != t) {
-            PARSER_STATE->parseError("Type ascription not satisfied.");
-          }
-        }
+      {
+        f = PARSER_STATE->applyTypeAscription(f,t).getExpr();
       }
     )?
   ;
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 663be7f1f..d2577433e 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -515,6 +515,78 @@ Expr Parser::mkHoApply(Expr expr, std::vector<Expr>& args)
   return expr;
 }
 
+api::Term Parser::applyTypeAscription(api::Term t, api::Sort s)
+{
+  api::Kind k = t.getKind();
+  if (k == api::EMPTYSET)
+  {
+    t = d_solver->mkEmptySet(s);
+  }
+  else if (k == api::UNIVERSE_SET)
+  {
+    t = d_solver->mkUniverseSet(s);
+  }
+  else if (k == api::SEP_NIL)
+  {
+    t = d_solver->mkSepNil(s);
+  }
+  else if (k == api::APPLY_CONSTRUCTOR)
+  {
+    std::vector<api::Term> children(t.begin(), t.end());
+    // apply type ascription to the operator and reconstruct
+    children[0] = applyTypeAscription(children[0], s);
+    t = d_solver->mkTerm(api::APPLY_CONSTRUCTOR, children);
+  }
+  // !!! temporary until datatypes are refactored in the new API
+  api::Sort etype = t.getSort();
+  if (etype.isConstructor())
+  {
+    api::Sort etype = t.getSort();
+    // get the datatype that t belongs to
+    api::Sort etyped = etype.getConstructorCodomainSort();
+    api::Datatype d = etyped.getDatatype();
+    // lookup by name
+    api::DatatypeConstructor dc = d.getConstructor(t.toString());
+
+    // Type ascriptions only have an effect on the node structure if this is a
+    // parametric datatype.
+    if (s.isParametricDatatype())
+    {
+      ExprManager* em = getExprManager();
+      // apply type ascription to the operator
+      Expr e = t.getExpr();
+      const DatatypeConstructor& dtc =
+          Datatype::datatypeOf(e)[Datatype::indexOf(e)];
+      t = api::Term(em->mkExpr(
+          kind::APPLY_TYPE_ASCRIPTION,
+          em->mkConst(
+              AscriptionType(dtc.getSpecializedConstructorType(s.getType()))),
+          e));
+    }
+    // the type of t does not match the sort s by design (constructor type
+    // vs datatype type), thus we use an alternative check here.
+    if (t.getSort().getConstructorCodomainSort() != s)
+    {
+      std::stringstream ss;
+      ss << "Type ascription on constructor not satisfied, term " << t
+         << " expected sort " << s << " but has sort "
+         << t.getSort().getConstructorCodomainSort();
+      parseError(ss.str());
+    }
+    return t;
+  }
+  // otherwise, nothing to do
+  // check that the type is correct
+  if (t.getSort() != s)
+  {
+    std::stringstream ss;
+    ss << "Type ascription not satisfied, term " << t << " expected sort " << s
+       << " but has sort " << t.getSort();
+    parseError(ss.str());
+  }
+  return t;
+}
+
 bool Parser::isDeclared(const std::string& name, SymbolType type) {
   switch (type) {
     case SYM_VARIABLE:
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 8447eb4dc..d40236208 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -678,6 +678,30 @@ public:
    */
   Expr mkHoApply(Expr expr, std::vector<Expr>& args);
 
+  /** Apply type ascription
+   *
+   * Return term t with a type ascription applied to it. This is used for
+   * syntax like (as t T) in smt2 and t::T in the CVC language. This includes:
+   * - (as emptyset (Set T))
+   * - (as univset (Set T))
+   * - (as sep.nil T)
+   * - (cons T)
+   * - ((as cons T) t1 ... tn) where cons is a parametric datatype constructor.
+   *
+   * The term to ascribe t is a term whose kind and children (but not type)
+   * are equivalent to that of the term returned by this method.
+   *
+   * Notice that method is not necessarily a cast. In actuality, the above terms
+   * should be understood as symbols indexed by types. However, SMT-LIB does not
+   * permit types as indices, so we must use, e.g. (as emptyset (Set T))
+   * instead of (_ emptyset (Set T)).
+   *
+   * @param t The term to ascribe a type
+   * @param s The sort to ascribe
+   * @return Term t with sort s ascribed.
+   */
+  api::Term applyTypeAscription(api::Term t, api::Sort s);
+
   /**
    * Add an operator to the current legal set.
    *
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 66831c0c4..eca32cb83 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1931,12 +1931,12 @@ qualIdentifier[CVC4::ParseOp& p]
     ( CONST_TOK sortSymbol[type, CHECK_DECLARED]
       {
         p.d_kind = kind::STORE_ALL;
-        PARSER_STATE->applyTypeAscription(p, type);
+        PARSER_STATE->parseOpApplyTypeAscription(p, type);
       }
     | identifier[p]
       sortSymbol[type, CHECK_DECLARED]
       {
-        PARSER_STATE->applyTypeAscription(p, type);
+        PARSER_STATE->parseOpApplyTypeAscription(p, type);
       }
     )
     RPAREN_TOK
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 8c2b50b04..42111f581 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -1578,8 +1578,10 @@ InputLanguage Smt2::getLanguage() const
   return em->getOptions().getInputLanguage();
 }
 
-void Smt2::applyTypeAscription(ParseOp& p, Type type)
+void Smt2::parseOpApplyTypeAscription(ParseOp& p, Type type)
 {
+  Debug("parser") << "parseOpApplyTypeAscription : " << p << " " << type
+                  << std::endl;
   // (as const (Array T1 T2))
   if (p.d_kind == kind::STORE_ALL)
   {
@@ -1612,66 +1614,12 @@ void Smt2::applyTypeAscription(ParseOp& p, Type type)
       parseError(ss.str());
     }
   }
-  ExprManager* em = getExprManager();
-  Type etype = p.d_expr.getType();
-  Kind ekind = p.d_expr.getKind();
   Trace("parser-qid") << "Resolve ascription " << type << " on " << p.d_expr;
-  Trace("parser-qid") << " " << ekind << " " << etype;
+  Trace("parser-qid") << " " << p.d_expr.getKind() << " " << p.d_expr.getType();
   Trace("parser-qid") << std::endl;
-  if (ekind == kind::APPLY_CONSTRUCTOR && type.isDatatype())
-  {
-    // nullary constructors with a type ascription
-    // could be a parametric constructor or just an overloaded constructor
-    DatatypeType dtype = static_cast<DatatypeType>(type);
-    if (dtype.isParametric())
-    {
-      std::vector<Expr> v;
-      Expr e = p.d_expr.getOperator();
-      const DatatypeConstructor& dtc =
-          Datatype::datatypeOf(e)[Datatype::indexOf(e)];
-      v.push_back(em->mkExpr(
-          kind::APPLY_TYPE_ASCRIPTION,
-          em->mkConst(AscriptionType(dtc.getSpecializedConstructorType(type))),
-          p.d_expr.getOperator()));
-      v.insert(v.end(), p.d_expr.begin(), p.d_expr.end());
-      p.d_expr = em->mkExpr(kind::APPLY_CONSTRUCTOR, v);
-    }
-  }
-  else if (etype.isConstructor())
-  {
-    // a non-nullary constructor with a type ascription
-    DatatypeType dtype = static_cast<DatatypeType>(type);
-    if (dtype.isParametric())
-    {
-      const DatatypeConstructor& dtc =
-          Datatype::datatypeOf(p.d_expr)[Datatype::indexOf(p.d_expr)];
-      p.d_expr = em->mkExpr(
-          kind::APPLY_TYPE_ASCRIPTION,
-          em->mkConst(AscriptionType(dtc.getSpecializedConstructorType(type))),
-          p.d_expr);
-    }
-  }
-  else if (ekind == kind::EMPTYSET)
-  {
-    Debug("parser") << "Empty set encountered: " << p.d_expr << " " << type
-                    << std::endl;
-    p.d_expr = em->mkConst(EmptySet(type));
-  }
-  else if (ekind == kind::UNIVERSE_SET)
-  {
-    p.d_expr = em->mkNullaryOperator(type, kind::UNIVERSE_SET);
-  }
-  else if (ekind == kind::SEP_NIL)
-  {
-    // We don't want the nil reference to be a constant: for instance, it
-    // could be of type Int but is not a const rational. However, the
-    // expression has 0 children. So we convert to a SEP_NIL variable.
-    p.d_expr = em->mkNullaryOperator(type, kind::SEP_NIL);
-  }
-  else if (etype != type)
-  {
-    parseError("Type ascription not satisfied.");
-  }
+  // otherwise, we process the type ascription
+  p.d_expr =
+      applyTypeAscription(api::Term(p.d_expr), api::Sort(type)).getExpr();
 }
 
 Expr Smt2::parseOpToExpr(ParseOp& p)
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 954bca314..35ac781f5 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -516,7 +516,7 @@ class Smt2 : public Parser
    * - If p's expression field is set, then we leave p unchanged, check if
    * that expression has the given type and throw a parse error otherwise.
    */
-  void applyTypeAscription(ParseOp& p, Type type);
+  void parseOpApplyTypeAscription(ParseOp& p, Type type);
   /**
    * This converts a ParseOp to expression, assuming it is a standalone term.
    *