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

7 files changed, 29 insertions, 28 deletions

diff --git a/src/expr/declaration_scope.cpp b/src/expr/declaration_scope.cpp
index 79accf43a..ae91efa68 100644
--- a/src/expr/declaration_scope.cpp
+++ b/src/expr/declaration_scope.cpp
@@ -144,10 +144,10 @@ Type DeclarationScope::lookupType(const std::string& name,
     Debug("sort") << "instance is  " << instantiation << endl;
 
     return instantiation;
-  }else if( p.second.isDatatype() ){
-    Assert( DatatypeType( p.second ).isParametric() );
+  } else if(p.second.isDatatype()) {
+    Assert( DatatypeType(p.second).isParametric() );
     return DatatypeType(p.second).instantiate(params);
-  }else {
+  } else {
     if(Debug.isOn("sort")) {
       Debug("sort") << "instantiating using a sort substitution" << endl;
       Debug("sort") << "have formals [";
@@ -170,7 +170,7 @@ Type DeclarationScope::lookupType(const std::string& name,
   }
 }
 
-size_t DeclarationScope::lookupArity( const std::string& name ){
+size_t DeclarationScope::lookupArity(const std::string& name) {
   pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second;
   return p.first.size();
 }
diff --git a/src/expr/declaration_scope.h b/src/expr/declaration_scope.h
index 4cdb71ddc..d695a3bf8 100644
--- a/src/expr/declaration_scope.h
+++ b/src/expr/declaration_scope.h
@@ -177,7 +177,7 @@ public:
   /**
    * Lookup the arity of a bound parameterized type.
    */
-  size_t lookupArity( const std::string& name );
+  size_t lookupArity(const std::string& name);
 
   /**
    * Pop a scope level. Deletes all bindings since the last call to
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index c32dbbc7d..038f58f95 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -506,16 +506,17 @@ ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
       i != i_end;
       ++i) {
     TypeNode* typeNode;
-    if( (*i).getNumParameters()==0 ){
+    if( (*i).getNumParameters() == 0 ) {
       typeNode = new TypeNode(d_nodeManager->mkTypeConst(*i));
-    }else{
+    } else {
       TypeNode cons = d_nodeManager->mkTypeConst(*i);
       std::vector< TypeNode > params;
       params.push_back( cons );
-      for( unsigned int ip=0; ip<(*i).getNumParameters(); ip++ ){
+      for( unsigned int ip = 0; ip < (*i).getNumParameters(); ++ip ) {
         params.push_back( TypeNode::fromType( (*i).getParameter( ip ) ) );
       }
-      typeNode = new TypeNode( d_nodeManager->mkTypeNode( kind::PARAMETRIC_DATATYPE, params ) );
+
+      typeNode = new TypeNode(d_nodeManager->mkTypeNode(kind::PARAMETRIC_DATATYPE, params));
     }
     Type type(d_nodeManager, typeNode);
     DatatypeType dtt(type);
@@ -546,9 +547,9 @@ ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
       i != i_end;
       ++i) {
     std::string name;
-    if( (*i).isSort() ){
+    if( (*i).isSort() ) {
       name = SortType(*i).getName();
-    }else{
+    } else {
       Assert( (*i).isSortConstructor() );
       name = SortConstructorType(*i).getName();
     }
@@ -562,10 +563,10 @@ ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
     // unresolved SortType used as a placeholder in complex types)
     // with "(*resolver).second" (the DatatypeType we created in the
     // first step, above).
-    if( (*i).isSort() ){
+    if( (*i).isSort() ) {
       placeholders.push_back(*i);
       replacements.push_back( (*resolver).second );
-    }else{
+    } else {
       Assert( (*i).isSortConstructor() );
       paramTypes.push_back( SortConstructorType(*i) );
       paramReplacements.push_back( (*resolver).second );
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 2bcdcedfa..8320a7053 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -222,7 +222,7 @@ Type::operator DatatypeType() const throw(AssertionException) {
   return DatatypeType(*this);
 }
 
-/** Is this the Datatype type? */
+/** Is this a datatype type? */
 bool Type::isDatatype() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->isDatatype() || d_typeNode->isParametricDatatype();
@@ -388,14 +388,12 @@ string SortType::getName() const {
   return d_typeNode->getAttribute(expr::VarNameAttr());
 }
 
-bool SortType::isParameterized() const
-{
+bool SortType::isParameterized() const {
   return false;
 }
 
 /** Get the parameter types */
-std::vector<Type> SortType::getParamTypes() const
-{
+std::vector<Type> SortType::getParamTypes() const {
   vector<Type> params;
   return params;
 }
@@ -526,11 +524,11 @@ std::vector<Type> ConstructorType::getArgTypes() const {
 }
 
 const Datatype& DatatypeType::getDatatype() const {
-  if( d_typeNode->isParametricDatatype() ){
-    Assert( (*d_typeNode)[0].getKind()==kind::DATATYPE_TYPE );
+  if( d_typeNode->isParametricDatatype() ) {
+    Assert( (*d_typeNode)[0].getKind() == kind::DATATYPE_TYPE );
     const Datatype& dt = (*d_typeNode)[0].getConst<Datatype>();
     return dt;
-  }else{
+  } else {
     return d_typeNode->getConst<Datatype>();
   }
 }
@@ -544,13 +542,13 @@ size_t DatatypeType::getArity() const {
   return d_typeNode->getNumChildren() - 1;
 }
 
-std::vector<Type> DatatypeType::getParamTypes() const{
+std::vector<Type> DatatypeType::getParamTypes() const {
   NodeManagerScope nms(d_nodeManager);
   vector<Type> params;
   vector<TypeNode> paramNodes = d_typeNode->getParamTypes();
   vector<TypeNode>::iterator it = paramNodes.begin();
   vector<TypeNode>::iterator it_end = paramNodes.end();
-  for(; it != it_end; ++ it) {
+  for(; it != it_end; ++it) {
     params.push_back(makeType(*it));
   }
   return params;
diff --git a/src/expr/type.h b/src/expr/type.h
index 096336b0c..4b260185b 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -470,11 +470,12 @@ public:
   /** Get the name of the sort */
   std::string getName() const;
 
-  /** is parameterized */
+  /** Is this type parameterized? */
   bool isParameterized() const;
 
   /** Get the parameter types */
   std::vector<Type> getParamTypes() const;
+
 };/* class SortType */
 
 /**
@@ -539,7 +540,7 @@ public:
   /** Get the underlying datatype */
   const Datatype& getDatatype() const;
 
-  /** is parameterized */
+  /** Is this this datatype parametric? */
   bool isParametric() const;
 
   /** Get the parameter types */
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 9283da13a..f77182d5d 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -138,7 +138,7 @@ std::vector<TypeNode> TypeNode::getArgTypes() const {
 
 std::vector<TypeNode> TypeNode::getParamTypes() const {
   vector<TypeNode> params;
-  Assert( isParametricDatatype() );
+  Assert(isParametricDatatype());
   for(unsigned i = 1, i_end = getNumChildren(); i < i_end; ++i) {
     params.push_back((*this)[i]);
   }
@@ -194,7 +194,7 @@ bool TypeNode::isDatatype() const {
   return getKind() == kind::DATATYPE_TYPE;
 }
 
-/** Is this a datatype type */
+/** Is this a parametric datatype type */
 bool TypeNode::isParametricDatatype() const {
   return getKind() == kind::PARAMETRIC_DATATYPE;
 }
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index d6c685a75..90fee7f1b 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -452,7 +452,8 @@ public:
   std::vector<TypeNode> getArgTypes() const;
 
   /**
-   * Get the paramater types of a parameterized datatype.
+   * Get the paramater types of a parameterized datatype.  Fails an
+   * assertion if this type is not a parametric datatype.
    */
   std::vector<TypeNode> getParamTypes() const;