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.

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index dca61fe48c0564f51767efd9ced5f1286d67d01f..3fde52bbeb7ed36cd1da8d61dc7959a9004e436d 100644 (file)
--- 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 663be7f1f19881d9c0480900080667c20596ac00..d2577433e4efa60dd5256bb9983d65b8e32921c9 100644 (file)
--- 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 8447eb4dcb60b08888b4a0349893eca2de7c5b26..d4023620863f4fdf3016bbd2ccdcada0320f21c0 100644 (file)
--- 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 66831c0c477160dc8f10d1abad4722212ce97bd4..eca32cb837902177c012620b52b20d4b210f2f91 100644 (file)
--- 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 8c2b50b042723e9f71a73787b43e4f948b0ff989..42111f58175e36e71b7e4350083e3e7dd929dd60 100644 (file)
--- 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 954bca314d1adea6283d0d51de1aa0f1bd97d477..35ac781f5dc0903728d28003c0a10e7decc97bc5 100644 (file)
--- 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.
    *