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

4 files changed, 82 insertions, 21 deletions

diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 20806464d..5672d1eb2 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -37,6 +37,7 @@ libutil_la_SOURCES = \
 	configuration_private.h \
 	configuration.cpp \
 	bitvector.h \
+	ascription_type.h \
 	datatype.h \
 	datatype.cpp \
 	gmp_util.h \
diff --git a/src/util/ascription_type.h b/src/util/ascription_type.h
new file mode 100644
index 000000000..85a51d8a4
--- /dev/null
+++ b/src/util/ascription_type.h
@@ -0,0 +1,66 @@
+/*********************                                                        */
+/*! \file ascription_type.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief A class representing a type ascription
+ **
+ ** A class representing a parameter for the type ascription operator.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__TYPE_ASCRIPTION_H
+#define __CVC4__TYPE_ASCRIPTION_H
+
+#include "expr/type.h"
+
+namespace CVC4 {
+
+/**
+ * A class used to parameterize a type ascription.  For example,
+ * "nil :: list<nat>" is an expression of kind APPLY_TYPE_ASCRIPTION.
+ * The parameter is an ASCRIPTION_TYPE-kinded expression with an
+ * AscriptionType payload.  (Essentially, all of this is a way to
+ * coerce a Type into the expression tree.)
+ */
+class CVC4_PUBLIC AscriptionType {
+  Type d_type;
+public:
+  AscriptionType(Type t) throw() : d_type(t) {}
+  Type getType() const throw() { return d_type; }
+  bool operator==(const AscriptionType& other) const throw() {
+    return d_type == other.d_type;
+  }
+  bool operator!=(const AscriptionType& other) const throw() {
+    return d_type != other.d_type;
+  }
+};/* class AscriptionType */
+
+/**
+ * A hash strategy for type ascription operators.
+ */
+struct CVC4_PUBLIC AscriptionTypeHashStrategy {
+  static inline size_t hash(const AscriptionType& at) {
+    return TypeHashFunction()(at.getType());
+  }
+};/* struct AscriptionTypeHashStrategy */
+
+/** An output routine for AscriptionTypes */
+inline std::ostream& operator<<(std::ostream& out, AscriptionType at) {
+  out << at.getType();
+  return out;
+}
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__TYPE_ASCRIPTION_H */
+
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index ecb089658..31b68c9a4 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -54,15 +54,13 @@ const Datatype& Datatype::datatypeOf(Expr item) {
   TypeNode t = Node::fromExpr(item).getType();
   switch(t.getKind()) {
   case kind::CONSTRUCTOR_TYPE:
-    //return t[t.getNumChildren() - 1].getConst<Datatype>();
     return DatatypeType(t[t.getNumChildren() - 1].toType()).getDatatype();
   case kind::SELECTOR_TYPE:
   case kind::TESTER_TYPE:
-    //return t[0].getConst<Datatype>();
     return DatatypeType(t[0].toType()).getDatatype();
   default:
     Unhandled("arg must be a datatype constructor, selector, or tester");
-  } 
+  }
 }
 
 size_t Datatype::indexOf(Expr item) {
@@ -84,7 +82,6 @@ void Datatype::resolve(ExprManager* em,
                        const std::vector< DatatypeType >& paramReplacements)
   throw(AssertionException, DatatypeResolutionException) {
 
-  //cout << "resolve " << *this << "..." << std::endl;
   AssertArgument(em != NULL, "cannot resolve a Datatype with a NULL expression manager");
   CheckArgument(!d_resolved, "cannot resolve a Datatype twice");
   AssertArgument(resolutions.find(d_name) != resolutions.end(),
@@ -104,8 +101,6 @@ void Datatype::resolve(ExprManager* em,
   }
   d_self = self;
   Assert(index == getNumConstructors());
-
-  //cout << "done resolve " << *this << std::endl;
 }
 
 void Datatype::addConstructor(const Constructor& c) {
@@ -274,7 +269,8 @@ DatatypeType Datatype::getDatatypeType() const throw(AssertionException) {
   return DatatypeType(d_self);
 }
 
-DatatypeType Datatype::getDatatypeType(const std::vector<Type>& params) const throw(AssertionException) {
+DatatypeType Datatype::getDatatypeType(const std::vector<Type>& params)
+  const throw(AssertionException) {
   CheckArgument(isResolved(), *this, "Datatype must be resolved to get its DatatypeType");
   Assert(!d_self.isNull() && DatatypeType(d_self).isParametric());
   return DatatypeType(d_self).instantiate(params);
@@ -367,8 +363,6 @@ void Datatype::Constructor::resolve(ExprManager* em, DatatypeType self,
                                     const std::vector< DatatypeType >& paramReplacements)
   throw(AssertionException, DatatypeResolutionException) {
 
-  //cout << "resolve " << *this << "..." << std::endl;
-
   AssertArgument(em != NULL, "cannot resolve a Datatype with a NULL expression manager");
   CheckArgument(!isResolved(),
                 "cannot resolve a Datatype constructor twice; "
@@ -401,7 +395,7 @@ void Datatype::Constructor::resolve(ExprManager* em, DatatypeType self,
       if(!placeholders.empty()) {
         range = range.substitute(placeholders, replacements);
       }
-      if(!paramTypes.empty() ){
+      if(!paramTypes.empty() ) {
         range = doParametricSubstitution( range, paramTypes, paramReplacements );
       }
       (*i).d_selector = em->mkVar((*i).d_name, em->mkSelectorType(self, range));
@@ -424,13 +418,11 @@ void Datatype::Constructor::resolve(ExprManager* em, DatatypeType self,
   for(iterator i = begin(), i_end = end(); i != i_end; ++i) {
     (*i).d_constructor = d_constructor;
   }
-
-  //cout << "done resolve " << *this << std::endl;
 }
 
-Type Datatype::Constructor::doParametricSubstitution( Type range, 
-                                  const std::vector< SortConstructorType >& paramTypes, 
-                                  const std::vector< DatatypeType >& paramReplacements ){
+Type Datatype::Constructor::doParametricSubstitution( Type range,
+                                  const std::vector< SortConstructorType >& paramTypes,
+                                  const std::vector< DatatypeType >& paramReplacements ) {
   TypeNode typn = TypeNode::fromType( range );
   if(typn.getNumChildren() == 0) {
     return range;
@@ -441,16 +433,16 @@ Type Datatype::Constructor::doParametricSubstitution( Type range,
       origChildren.push_back( (*i).toType() );
       children.push_back( doParametricSubstitution( (*i).toType(), paramTypes, paramReplacements ) );
     }
-    for( int i=0; i<(int)paramTypes.size(); i++ ){
-      if( paramTypes[i].getArity()==origChildren.size() ){
+    for( int i=0; i<(int)paramTypes.size(); i++ ) {
+      if( paramTypes[i].getArity()==origChildren.size() ) {
         Type tn = paramTypes[i].instantiate( origChildren );
-        if( range==tn ){
+        if( range==tn ) {
           return paramReplacements[i].instantiate( children );
         }
       }
     }
     NodeBuilder<> nb(typn.getKind());
-    for( int i=0; i<(int)children.size(); i++ ){
+    for( int i=0; i<(int)children.size(); i++ ) {
       nb << TypeNode::fromType( children[i] );
     }
     return nb.constructTypeNode().toType();
@@ -662,12 +654,12 @@ Expr Datatype::Constructor::Arg::getSelector() const {
 }
 
 Expr Datatype::Constructor::Arg::getConstructor() const {
-  CheckArgument(isResolved(), this, 
+  CheckArgument(isResolved(), this,
                 "cannot get a associated constructor for argument of an unresolved datatype constructor");
   return d_constructor;
 }
 
-Type Datatype::Constructor::Arg::getSelectorType() const{
+Type Datatype::Constructor::Arg::getSelectorType() const {
   return getSelector().getType();
 }
 
diff --git a/src/util/datatype.h b/src/util/datatype.h
index abc9e3258..842be9b45 100644
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -359,11 +359,13 @@ public:
 
   /** Get the name of this Datatype. */
   inline std::string getName() const throw();
+
   /** Get the number of constructors (so far) for this Datatype. */
   inline size_t getNumConstructors() const throw();
 
   /** Get the nubmer of parameters */
   inline size_t getNumParameters() const throw();
+
   /** Get parameter */
   inline Type getParameter( unsigned int i ) const;