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

1 files changed, 14 insertions, 1 deletions

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);