From 11bb98ba5b1e9e88053a7bd6adc1d48d48a4bb21 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Sat, 14 May 2011 00:15:43 +0000
Subject: add AscriptionType stuff to support nullary parameterized datatypes;
 also, review of Andy's earlier commit, with some minor code clean-up and
 documentation

---
 src/parser/parser.cpp | 16 +++++++++-------
 src/parser/parser.h   |  7 ++++++-
 2 files changed, 15 insertions(+), 8 deletions(-)

(limited to 'src/parser')

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);
 
-- 
cgit v1.2.3