add AscriptionType stuff to support nullary parameterized datatypes; also, review...

diff --git a/src/expr/declaration_scope.cpp b/src/expr/declaration_scope.cpp
index 79accf43a066f808e94efd0957812971d33d07a6..ae91efa686cf723457e96f4c1b1aad1adb0ff234 100644 (file)
--- 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 4cdb71ddcc5d3ec04a0d94b5e30e626628896fdd..d695a3bf848de42bc71833927784802bcbf6a9bf 100644 (file)
--- 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 c32dbbc7d14219b5dfcd3e23c3f9a728c757b2b3..038f58f95f6360b4c2ebc103b0fbd4af71f52a4a 100644 (file)
--- 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 2bcdcedfa513754f65a582661b79001d2ca9bb16..8320a70535ba94f71fd8c9a6aa9561f36dcbd12e 100644 (file)
--- 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 096336b0c5ed0e4804d27dfad795fd9c37c3381a..4b260185b0100e04dd96d1cfaaea8edd7fa4d1c3 100644 (file)
--- 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 9283da13abcb5e82d3f649dbb1757d2dc306e2c9..f77182d5d1f637ab5385bd8e3c06fb4fddb144cf 100644 (file)
--- 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 d6c685a7549acc51c459f33bc3544bfa10207e5a..90fee7f1b5fb3053f06fa20b97d22334477c9099 100644 (file)
--- 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;
 

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index efe01fb40adfecc8b2637c30482fae3095cca84a..78e70572a8ef50d0a74591ff31553ddf89e84bca 100644 (file)
--- 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 6d55e195ee8481f568524690a67f930b1cc7ea30..2e7e3ca3dd6d3421c3a0158e698801cf37b8fb14 100644 (file)
--- 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);
 

diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index df8cb6eb8df81a3978f5af47e3af5c90c919caad..b493b8c412f7bb0e8ef4a9474c3499d7dc100f40 100644 (file)
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -43,7 +43,6 @@ public:
         return RewriteResponse(REWRITE_DONE,
                                NodeManager::currentNM()->mkConst(result));
       } else {
-        //const Datatype& dt = in[0].getType().getConst<Datatype>();
         const Datatype& dt = DatatypeType(in[0].getType().toType()).getDatatype();
         if(dt.getNumConstructors() == 1) {
           // only one constructor, so it must be

diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index d08e3875cf400167958841049196528df24caf17..a119900754ddddc8f1b8f36e506b35895a0fd3f9 100644 (file)
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -61,5 +61,13 @@ well-founded PARAMETRIC_DATATYPE\
     "DatatypeType(%TYPE%.toType()).getDatatype().isWellFounded()" \
     "DatatypeType(%TYPE%.toType()).getDatatype().mkGroundTerm()" \
     "util/datatype.h"
-    
+
+parameterized APPLY_TYPE_ASCRIPTION ASCRIPTION_TYPE 1 \
+    "type ascription, for nullary, parameteric datatype constructors"
+constant ASCRIPTION_TYPE \
+    ::CVC4::AscriptionType \
+    ::CVC4::AscriptionTypeHashStrategy \
+    "util/ascription_type.h" \
+    "a type parameter for type ascription"
+
 endtheory

diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index dc2e95f9d5be9dc826c99e23be36d79de51552de..3fe43657f66a931288f7bb46c641ca6361c75c9e 100644 (file)
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -32,8 +32,7 @@ namespace expr {
 namespace theory {
 namespace datatypes {
 
-class Matcher
-{
+class Matcher {
 private:
   std::vector< TypeNode > d_types;
   std::vector< TypeNode > d_match;

diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 20806464d3149cc8ccf83408ebdeebf6c9e36e0f..5672d1eb2df509d32b375d97e79f6c128d257f11 100644 (file)
--- 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 (file)
index 0000000..85a51d8
--- /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 ecb0896580a81181e1c5b8213439a5de80b38b60..31b68c9a4e1a4d6345a5052f30851ee596dcae3e 100644 (file)
--- 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 abc9e3258c65679b5515e07813e7e271773ed17f..842be9b45788a9cf5f13b045b5f8c5634efb31f9 100644 (file)
--- 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;