add AscriptionType stuff to support nullary parameterized datatypes; also, review of Andy's earlier commit, with some minor code clean-up and documentation

2 files changed, 15 insertions, 8 deletions

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index efe01fb40..78e70572a 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -242,15 +242,17 @@ SortType Parser::mkUnresolvedType(const std::string& name) {
   return unresolved;
 }
 
-SortConstructorType Parser::mkUnresolvedTypeConstructor(const std::string& name, 
-                                                        size_t arity)
-{
+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){
+
+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());
@@ -283,10 +285,10 @@ Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
     if(isDeclared(name, SYM_SORT)) {
       throw ParserException(name + " already declared");
     }
-    if( t.isParametric() ){
+    if( t.isParametric() ) {
       std::vector< Type > paramTypes = t.getParamTypes();
       defineType(name, paramTypes, t );
-    }else{
+    } else {
       defineType(name, t);
     }
     for(Datatype::const_iterator j = dt.begin(),
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 6d55e195e..2e7e3ca3d 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -373,10 +373,15 @@ public:
   SortType mkUnresolvedType(const std::string& name);
 
   /**
-   * Creates a new "unresolved type," used only during parsing.
+   * Creates a new unresolved (parameterized) type constructor of the given
+   * arity.
    */
   SortConstructorType mkUnresolvedTypeConstructor(const std::string& name, 
                                                   size_t arity);
+  /**
+   * Creates a new unresolved (parameterized) type constructor given the type
+   * parameters.
+   */
   SortConstructorType mkUnresolvedTypeConstructor(const std::string& name, 
                                                   const std::vector<Type>& params);