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.

1 files changed, 72 insertions, 0 deletions

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: