added support for parametric datatypes, updated cvc parser to handle parametric datatypes, type ascriptions are not implemented yet

3 files changed, 94 insertions, 26 deletions

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index b3c253dab..3c8d6e1ce 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -1002,12 +1002,27 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t,
 }
     /* named types */
   : identifier[id,check,SYM_SORT]
-    parameterization[check]?
-    { if(check == CHECK_DECLARED ||
+    parameterization[check,types]?
+    { 
+      if(check == CHECK_DECLARED ||
          PARSER_STATE->isDeclared(id, SYM_SORT)) {
-        t = PARSER_STATE->getSort(id);
+        Debug("parser-param") << "param: getSort " << id << " " << types.size() << " " << PARSER_STATE->getArity( id ) 
+                              << " " << PARSER_STATE->isDeclared(id, SYM_SORT) << std::endl;
+        if( types.size()>0 ){
+          t = PARSER_STATE->getSort(id, types);
+        }else{
+          t = PARSER_STATE->getSort(id);
+        }
       } else {
-        t = PARSER_STATE->mkUnresolvedType(id);
+        if( types.empty() ){
+          t = PARSER_STATE->mkUnresolvedType(id);
+          Debug("parser-param") << "param: make unres type " << id << std::endl;
+        }else{
+          t = PARSER_STATE->mkUnresolvedTypeConstructor(id,types);
+          t = SortConstructorType(t).instantiate( types );
+          Debug("parser-param") << "param: make unres param type " << id << " " << types.size() << " " 
+                                << PARSER_STATE->getArity( id ) << std::endl;
+        }
       }
     }
 
@@ -1076,12 +1091,13 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t,
     }
   ;
 
-parameterization[CVC4::parser::DeclarationCheck check]
+parameterization[CVC4::parser::DeclarationCheck check, 
+                 std::vector<CVC4::Type>& params]
 @init {
   Type t;
 }
-  : LBRACKET restrictedType[t,check] ( COMMA restrictedType[t,check] )* RBRACKET
-    { UNSUPPORTED("parameterized types not yet supported"); }
+  : LBRACKET restrictedType[t,check] { Debug("parser-param") << "t = " << t << std::endl; params.push_back( t ); }
+    ( COMMA restrictedType[t,check] { Debug("parser-param") << "t = " << t << std::endl; params.push_back( t ); } )* RBRACKET
   ;
 
 bound returns [CVC4::parser::cvc::mySubrangeBound bound]
@@ -1267,6 +1283,7 @@ term[CVC4::Expr& f]
   std::vector<CVC4::Expr> expressions;
   std::vector<unsigned> operators;
   unsigned op;
+  Type t;
 }
   : storeTerm[f] { expressions.push_back(f); }
     ( arithmeticBinop[op] storeTerm[f] { operators.push_back(op); expressions.push_back(f); } )*
@@ -1374,6 +1391,7 @@ postfixTerm[CVC4::Expr& f]
   bool extract = false, left = false;
   std::vector<Expr> args;
   std::string id;
+  Type t;
 }
   : bvTerm[f]
     ( /* array select / bitvector extract */
@@ -1443,7 +1461,9 @@ postfixTerm[CVC4::Expr& f]
           f = EXPR_MANAGER->mkVar(TupleType(f.getType()).getTypes()[k]); }
       )*/
     )*
-    typeAscription[f]?
+    (typeAscription[f, t] 
+     { //f = MK_EXPR(CVC4::kind::APPLY_TYPE_ANNOTATION, MK_CONST(t), f); 
+     } )? 
   ;
 
 bvTerm[CVC4::Expr& f]
@@ -1642,20 +1662,19 @@ simpleTerm[CVC4::Expr& f]
  * Matches (and performs) a type ascription.
  * The f arg is the term to check (it is an input-only argument).
  */
-typeAscription[const CVC4::Expr& f]
+typeAscription[const CVC4::Expr& f, CVC4::Type& t]
 @init {
-  Type t;
 }
   : COLON COLON type[t,CHECK_DECLARED]
-    { if(f.getType() != t) {
-        std::stringstream ss;
-        ss << Expr::setlanguage(language::output::LANG_CVC4)
-           << "type ascription not satisfied\n"
-           << "term:     " << f << '\n'
-           << "has type: " << f.getType() << '\n'
-           << "ascribed: " << t;
-        PARSER_STATE->parseError(ss.str());
-      }
+    { //if(f.getType() != t) {
+      //  std::stringstream ss;
+      //  ss << Expr::setlanguage(language::output::LANG_CVC4)
+      //     << "type ascription not satisfied\n"
+      //     << "term:     " << f << '\n'
+      //     << "has type: " << f.getType() << '\n'
+      //     << "ascribed: " << t;
+      //  PARSER_STATE->parseError(ss.str());
+      //}
     }
   ;
 
@@ -1706,16 +1725,23 @@ iteElseTerm[CVC4::Expr& f]
 datatypeDef[std::vector<CVC4::Datatype>& datatypes]
 @init {
   std::string id, id2;
+  Type t;
+  std::vector< Type > params;
 }
     /* This really needs to be CHECK_NONE, or mutually-recursive datatypes
      * won't work, because this type will already be "defined" as an
      * unresolved type; don't worry, we check below. */
-  : identifier[id,CHECK_NONE,SYM_SORT]
-    ( LBRACKET identifier[id2,CHECK_NONE,SYM_SORT]
-      ( COMMA identifier[id2,CHECK_NONE,SYM_SORT] )* RBRACKET
-      { UNSUPPORTED("parameterized datatypes not yet supported"); }
+  : identifier[id,CHECK_NONE,SYM_SORT] { PARSER_STATE->pushScope(); }
+    ( LBRACKET identifier[id2,CHECK_UNDECLARED,SYM_SORT] { 
+        t = PARSER_STATE->mkSort(id2);
+        params.push_back( t ); 
+      }
+      ( COMMA identifier[id2,CHECK_UNDECLARED,SYM_SORT] { 
+        t = PARSER_STATE->mkSort(id2);
+        params.push_back( t ); } 
+      )* RBRACKET
     )?
-    { datatypes.push_back(Datatype(id));
+    { datatypes.push_back(Datatype(id,params));
       if(!PARSER_STATE->isUnresolvedType(id)) {
         // if not unresolved, must be undeclared
         PARSER_STATE->checkDeclaration(id, CHECK_UNDECLARED, SYM_SORT);
@@ -1723,6 +1749,7 @@ datatypeDef[std::vector<CVC4::Datatype>& datatypes]
     }
     EQUAL_TOK constructorDef[datatypes.back()]
     ( BAR constructorDef[datatypes.back()] )*
+    { PARSER_STATE->popScope(); }
   ;
 
 /**
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 29ade43c1..efe01fb40 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -95,6 +95,11 @@ Type Parser::getSort(const std::string& name,
   return t;
 }
 
+size_t Parser::getArity(const std::string& sort_name){
+  Assert( isDeclared(sort_name, SYM_SORT) );
+  return d_declScope->lookupArity(sort_name);
+}
+
 /* Returns true if name is bound to a boolean variable. */
 bool Parser::isBoolean(const std::string& name) {
   return isDeclared(name, SYM_VARIABLE) && getType(name).isBoolean();
@@ -237,6 +242,24 @@ SortType Parser::mkUnresolvedType(const std::string& name) {
   return unresolved;
 }
 
+SortConstructorType Parser::mkUnresolvedTypeConstructor(const std::string& name, 
+                                                        size_t arity)
+{
+  SortConstructorType unresolved = mkSortConstructor(name,arity);
+  d_unresolved.insert(unresolved);
+  return unresolved;
+}
+SortConstructorType Parser::mkUnresolvedTypeConstructor(const std::string& name, 
+                                                        const std::vector<Type>& params){
+  Debug("parser") << "newSortConstructor(P)(" << name << ", " << params.size() << ")"
+                  << std::endl;
+  SortConstructorType unresolved = d_exprManager->mkSortConstructor(name, params.size());
+  defineType(name, params, unresolved);
+  Type t = getSort( name, params );
+  d_unresolved.insert(unresolved);
+  return unresolved;
+}
+
 bool Parser::isUnresolvedType(const std::string& name) {
   if(!isDeclared(name, SYM_SORT)) {
     return false;
@@ -260,7 +283,12 @@ Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
     if(isDeclared(name, SYM_SORT)) {
       throw ParserException(name + " already declared");
     }
-    defineType(name, t);
+    if( t.isParametric() ){
+      std::vector< Type > paramTypes = t.getParamTypes();
+      defineType(name, paramTypes, t );
+    }else{
+      defineType(name, t);
+    }
     for(Datatype::const_iterator j = dt.begin(),
           j_end = dt.end();
         j != j_end;
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 6509b192b..6d55e195e 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -150,7 +150,7 @@ class CVC4_PUBLIC Parser {
    * depend on mkMutualDatatypeTypes() to check everything and clear
    * this out.
    */
-  std::set<SortType> d_unresolved;
+  std::set<Type> d_unresolved;
 
   /**
    * "Preemption commands": extra commands implied by subterms that
@@ -255,6 +255,11 @@ public:
                const std::vector<Type>& params);
 
   /**
+   * Returns arity of a (parameterized) sort, given a name and args.
+   */
+  size_t getArity(const std::string& sort_name);
+
+  /**
    * Checks if a symbol has been declared.
    * @param name the symbol name
    * @param type the symbol type
@@ -368,6 +373,14 @@ public:
   SortType mkUnresolvedType(const std::string& name);
 
   /**
+   * Creates a new "unresolved type," used only during parsing.
+   */
+  SortConstructorType mkUnresolvedTypeConstructor(const std::string& name, 
+                                                  size_t arity);
+  SortConstructorType mkUnresolvedTypeConstructor(const std::string& name, 
+                                                  const std::vector<Type>& params);
+
+  /**
    * Returns true IFF name is an unresolved type.
    */
   bool isUnresolvedType(const std::string& name);