datatypes work

9 files changed, 262 insertions, 90 deletions

diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 286ddf611..7c2d02809 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -208,6 +208,62 @@ Type Expr::getType(bool check) const throw (TypeCheckingException) {
   return d_exprManager->getType(*this, check);
 }
 
+Expr::const_iterator::const_iterator() :
+  d_iterator(NULL) {
+}
+Expr::const_iterator::const_iterator(void* v) :
+  d_iterator(v) {
+}
+Expr::const_iterator::const_iterator(const const_iterator& it) {
+  if(it.d_iterator == NULL) {
+    d_iterator = NULL;
+  } else {
+    d_iterator = new Node::iterator(*reinterpret_cast<Node::iterator*>(it.d_iterator));
+  }
+}
+Expr::const_iterator& Expr::const_iterator::operator=(const const_iterator& it) {
+  if(d_iterator != NULL) {
+    delete reinterpret_cast<Node::iterator*>(d_iterator);
+  }
+  d_iterator = new Node::iterator(*reinterpret_cast<Node::iterator*>(it.d_iterator));
+  return *this;
+}
+Expr::const_iterator::~const_iterator() {
+  if(d_iterator != NULL) {
+    delete reinterpret_cast<Node::iterator*>(d_iterator);
+  }
+}
+bool Expr::const_iterator::operator==(const const_iterator& it) const {
+  if(d_iterator == NULL || it.d_iterator == NULL) {
+    return false;
+  }
+  return *reinterpret_cast<Node::iterator*>(d_iterator) ==
+    *reinterpret_cast<Node::iterator*>(it.d_iterator);
+}
+Expr::const_iterator& Expr::const_iterator::operator++() {
+  Assert(d_iterator != NULL);
+  ++*reinterpret_cast<Node::iterator*>(d_iterator);
+  return *this;
+}
+Expr::const_iterator Expr::const_iterator::operator++(int) {
+  Assert(d_iterator != NULL);
+  const_iterator it = *this;
+  ++*reinterpret_cast<Node::iterator*>(d_iterator);
+  return it;
+}
+Expr Expr::const_iterator::operator*() const {
+  Assert(d_iterator != NULL);
+  return (**reinterpret_cast<Node::iterator*>(d_iterator)).toExpr();
+}
+
+Expr::const_iterator Expr::begin() const {
+  return Expr::const_iterator(new Node::iterator(d_node->begin()));
+}
+
+Expr::const_iterator Expr::end() const {
+  return Expr::const_iterator(new Node::iterator(d_node->end()));
+}
+
 std::string Expr::toString() const {
   ExprManagerScope ems(*this);
   Assert(d_node != NULL, "Unexpected NULL expression pointer!");
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index b0157adbf..bffb37ddb 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -30,6 +30,7 @@ ${includes}
 
 #include <string>
 #include <iostream>
+#include <iterator>
 #include <stdint.h>
 
 #include "util/exception.h"
@@ -39,7 +40,7 @@ ${includes}
 // compiler directs the user to the template file instead of the
 // generated one.  We don't want the user to modify the generated one,
 // since it'll get overwritten on a later build.
-#line 43 "${template}"
+#line 44 "${template}"
 
 namespace CVC4 {
 
@@ -262,6 +263,46 @@ public:
   Expr operator[](unsigned i) const;
 
   /**
+   * Returns the children of this Expr.
+   */
+  std::vector<Expr> getChildren() const {
+    return std::vector<Expr>(begin(), end());
+  }
+
+  /**
+   * Iterator type for the children of an Expr.
+   */
+  class const_iterator : public std::iterator<std::input_iterator_tag, Expr> {
+    void* d_iterator;
+    explicit const_iterator(void*);
+
+    friend class Expr;// to access void* constructor
+
+  public:
+    const_iterator();
+    const_iterator(const const_iterator& it);
+    const_iterator& operator=(const const_iterator& it);
+    ~const_iterator();
+    bool operator==(const const_iterator& it) const;
+    bool operator!=(const const_iterator& it) const {
+      return !(*this == it);
+    }
+    const_iterator& operator++();
+    const_iterator operator++(int);
+    Expr operator*() const;
+  };/* class Expr::const_iterator */
+
+  /**
+   * Returns an iterator to the first child of this Expr.
+   */
+  const_iterator begin() const;
+
+  /**
+   * Returns an iterator to one-off-the-last child of this Expr.
+   */
+  const_iterator end() const;
+
+  /**
    * Check if this is an expression that has an operator.
    *
    * @return true if this expression has an operator
@@ -750,7 +791,7 @@ public:
 
 ${getConst_instantiations}
 
-#line 754 "${template}"
+#line 795 "${template}"
 
 namespace expr {
 
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index ca006daab..d6165b435 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -1462,8 +1462,14 @@ postfixTerm[CVC4::Expr& f]
       )*/
     )*
     ( typeAscription[f, t]
-      { if(t.isDatatype()) {
-          f = MK_EXPR(CVC4::kind::APPLY_TYPE_ASCRIPTION, MK_CONST(AscriptionType(t)), f);
+      { if(f.getKind() == CVC4::kind::APPLY_CONSTRUCTOR && t.isDatatype()) {
+          std::vector<CVC4::Expr> v;
+          Expr e = f.getOperator();
+          const Datatype::Constructor& dtc = Datatype::datatypeOf(e)[Datatype::indexOf(e)];
+          v.push_back(MK_EXPR( CVC4::kind::APPLY_TYPE_ASCRIPTION,
+                               MK_CONST(AscriptionType(dtc.getSpecializedConstructorType(t))), f.getOperator()[0] ));
+          v.insert(v.end(), f.begin(), f.end());
+          f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, v);
         } else {
           if(f.getType() != t) {
             PARSER_STATE->parseError("Type ascription not satisfied.");
diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index 1cdefa60b..47896b1e0 100644
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -34,7 +34,7 @@ cardinality TESTER_TYPE \
     "::CVC4::theory::builtin::FunctionProperties::computeCardinality(%TYPE%)" \
     "theory/builtin/theory_builtin_type_rules.h"
 
-parameterized APPLY_CONSTRUCTOR CONSTRUCTOR_TYPE 0: "constructor application"
+parameterized APPLY_CONSTRUCTOR APPLY_TYPE_ASCRIPTION 0: "constructor application"
 
 parameterized APPLY_SELECTOR SELECTOR_TYPE 1: "selector application"
 
@@ -63,7 +63,7 @@ well-founded PARAMETRIC_DATATYPE\
     "util/datatype.h"
 
 parameterized APPLY_TYPE_ASCRIPTION ASCRIPTION_TYPE 1 \
-    "type ascription, for nullary, parameteric datatype constructors"
+    "type ascription, for datatype constructor applications"
 constant ASCRIPTION_TYPE \
     ::CVC4::AscriptionType \
     ::CVC4::AscriptionTypeHashStrategy \
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index 270313e0f..5ff01924b 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -21,6 +21,8 @@
 #ifndef __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H
 #define __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H
 
+#include "util/matcher.h"
+
 namespace CVC4 {
 
 namespace expr {
@@ -32,81 +34,6 @@ namespace expr {
 namespace theory {
 namespace datatypes {
 
-class Matcher {
-private:
-  std::vector< TypeNode > d_types;
-  std::vector< TypeNode > d_match;
-public:
-  Matcher(){}
-  Matcher( DatatypeType dt ){
-    std::vector< Type > argTypes = dt.getParamTypes();
-    addTypes( argTypes );
-    Debug("typecheck-idt") << "instantiating matcher for " << dt << std::endl;
-    for(unsigned i = 0; i < argTypes.size(); ++i) {
-      if(dt.isParameterInstantiated(i)) {
-        Debug("typecheck-idt") << "++ instantiate param " << i << " : " << d_types[i] << std::endl;
-        d_match[i] = d_types[i];
-      }
-    }
-  }
-  ~Matcher(){}
-
-  void addType( Type t ){
-    d_types.push_back( TypeNode::fromType( t ) );
-    d_match.push_back( TypeNode::null() );
-  }
-  void addTypes( std::vector< Type > types ){
-    for( int i=0; i<(int)types.size(); i++ ){
-      addType( types[i] );
-    }
-  }
-
-  bool doMatching( TypeNode base, TypeNode match ){
-    Debug("typecheck-idt") << "doMatching() : " << base << " : " << match << std::endl;
-    std::vector< TypeNode >::iterator i = std::find( d_types.begin(), d_types.end(), base );
-    if( i!=d_types.end() ){
-      int index = i - d_types.begin();
-      Debug("typecheck-idt") << "++ match on " << index << " : " << d_match[index] << std::endl;
-      if( !d_match[index].isNull() && d_match[index]!=match ){
-        return false;
-      }else{
-        d_match[ i - d_types.begin() ] = match;
-        return true;
-      }
-    }else if( base==match ){
-      return true;
-    }else if( base.getKind()!=match.getKind() || base.getNumChildren()!=match.getNumChildren() ){
-      return false;
-    }else{
-      for( int i=0; i<(int)base.getNumChildren(); i++ ){
-        if( !doMatching( base[i], match[i] ) ){
-          return false;
-        }
-      }
-      return true;
-    }
-  }
-
-  TypeNode getMatch( unsigned int i ){ return d_match[i]; }
-  void getTypes( std::vector<Type>& types ) {
-    types.clear();
-    for( int i=0; i<(int)d_match.size(); i++ ){
-      types.push_back( d_types[i].toType() );
-    }
-  }
-  void getMatches( std::vector<Type>& types ) {
-    types.clear();
-    for( int i=0; i<(int)d_match.size(); i++ ){
-      if(d_match[i].isNull()) {
-        types.push_back( d_types[i].toType() );
-      } else {
-        types.push_back( d_match[i].toType() );
-      }
-    }
-  }
-};/* class Matcher */
-
-
 typedef expr::Attribute<expr::attr::DatatypeConstructorTypeGroundTermTag, Node> GroundTermAttr;
 
 struct DatatypeConstructorTypeRule {
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index b8f336f2d..dc1da0659 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -41,6 +41,7 @@ libutil_la_SOURCES = \
 	ascription_type.h \
 	datatype.h \
 	datatype.cpp \
+	matcher.h \
 	gmp_util.h \
 	sexpr.h \
 	stats.h \
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index 4b84d2955..a06a7c2b5 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -27,6 +27,7 @@
 #include "expr/node_manager.h"
 #include "expr/node.h"
 #include "util/recursion_breaker.h"
+#include "util/matcher.h"
 
 using namespace std;
 
@@ -261,7 +262,7 @@ Expr Datatype::mkGroundTerm( Type t ) const throw(AssertionException) {
     CheckArgument(false, *this, "this datatype is not well-founded, cannot construct a ground term!");
   }else{
     if( t!=groundTerm.getType() ){
-      groundTerm = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, 
+      groundTerm = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION,
                                                     NodeManager::currentNM()->mkConst(AscriptionType(t)), groundTerm).toExpr();
     }
     return groundTerm;
@@ -511,6 +512,19 @@ Expr Datatype::Constructor::getConstructor() const {
   return d_constructor;
 }
 
+Type Datatype::Constructor::getSpecializedConstructorType(Type returnType) const {
+  CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+  const Datatype& dt = Datatype::datatypeOf(d_constructor);
+  CheckArgument(dt.isParametric(), this, "this datatype constructor is not yet resolved");
+  DatatypeType dtt = DatatypeType(dt.d_self);
+  Matcher m(dtt);
+  m.doMatching( TypeNode::fromType(dtt), TypeNode::fromType(returnType) );
+  vector<Type> subst;
+  m.getMatches(subst);
+  vector<Type> params = dt.getParameters();
+  return d_constructor.getType().substitute(subst, params);
+}
+
 Expr Datatype::Constructor::getTester() const {
   CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
   return d_tester;
@@ -625,9 +639,10 @@ Expr Datatype::Constructor::mkGroundTerm( Type t ) const throw(AssertionExceptio
 
   // for each selector, get a ground term
   Assert( t.isDatatype() );
-  std::vector< Type > instTypes; 
-  std::vector< Type > paramTypes = DatatypeType(t).getDatatype().getParameters();
+  std::vector< Type > instTypes;
+  std::vector< Type > paramTypes;
   if( DatatypeType(t).isParametric() ){
+    paramTypes = DatatypeType(t).getDatatype().getParameters();
     instTypes = DatatypeType(t).getParamTypes();
   }
   for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
diff --git a/src/util/datatype.h b/src/util/datatype.h
index 3506616d6..477b16f66 100644
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -169,8 +169,8 @@ public:
       Expr getSelector() const;
 
       /**
-       * Get the associated constructor for this constructor argument; this call is
-       * only permitted after resolution.
+       * Get the associated constructor for this constructor argument;
+       * this call is only permitted after resolution.
        */
       Expr getConstructor() const;
 
@@ -216,10 +216,10 @@ public:
       throw(AssertionException, DatatypeResolutionException);
     friend class Datatype;
 
-    /** */
-    Type doParametricSubstitution( Type range, 
-                                   const std::vector< SortConstructorType >& paramTypes, 
-                                   const std::vector< DatatypeType >& paramReplacements );
+    /** @FIXME document this! */
+    Type doParametricSubstitution(Type range,
+                                  const std::vector< SortConstructorType >& paramTypes,
+                                  const std::vector< DatatypeType >& paramReplacements);
   public:
     /**
      * Create a new Datatype constructor with the given name for the
@@ -273,6 +273,12 @@ public:
     inline size_t getNumArgs() const throw();
 
     /**
+     * Get the specialized constructor type for a parametric
+     * constructor; this call is only permitted after resolution.
+     */
+    Type getSpecializedConstructorType(Type returnType) const;
+
+    /**
      * Return the cardinality of this constructor (the product of the
      * cardinalities of its arguments).
      */
@@ -369,6 +375,9 @@ public:
   /** Get the number of constructors (so far) for this Datatype. */
   inline size_t getNumConstructors() const throw();
 
+  /** Is this datatype parametric? */
+  inline bool isParametric() const throw();
+
   /** Get the nubmer of type parameters */
   inline size_t getNumParameters() const throw();
 
@@ -527,15 +536,22 @@ inline size_t Datatype::getNumConstructors() const throw() {
   return d_constructors.size();
 }
 
+inline bool Datatype::isParametric() const throw() {
+  return d_params.size() > 0;
+}
+
 inline size_t Datatype::getNumParameters() const throw() {
   return d_params.size();
 }
 
 inline Type Datatype::getParameter( unsigned int i ) const {
+  CheckArgument(isParametric(), this, "cannot get type parameter of a non-parametric datatype");
+  CheckArgument(i < d_params.size(), i, "type parameter index out of range for datatype");
   return d_params[i];
 }
 
 inline std::vector<Type> Datatype::getParameters() const {
+  CheckArgument(isParametric(), this, "cannot get type parameters of a non-parametric datatype");
   return d_params;
 }
 
diff --git a/src/util/matcher.h b/src/util/matcher.h
new file mode 100644
index 000000000..2c55309d3
--- /dev/null
+++ b/src/util/matcher.h
@@ -0,0 +1,110 @@
+/*********************                                                        */
+/*! \file matcher.h
+ ** \verbatim
+ ** Original author: ajreynol
+ ** 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 matcher
+ **
+ ** A class representing a type matcher.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__MATCHER_H
+#define __CVC4__MATCHER_H
+
+#include <iostream>
+#include <string>
+#include <vector>
+#include <map>
+#include "util/Assert.h"
+#include "expr/node.h"
+#include "expr/type_node.h"
+
+namespace CVC4 {
+
+class Matcher {
+private:
+  std::vector< TypeNode > d_types;
+  std::vector< TypeNode > d_match;
+public:
+  Matcher(){}
+  Matcher( DatatypeType dt ){
+    std::vector< Type > argTypes = dt.getParamTypes();
+    addTypes( argTypes );
+    Debug("typecheck-idt") << "instantiating matcher for " << dt << std::endl;
+    for(unsigned i = 0; i < argTypes.size(); ++i) {
+      if(dt.isParameterInstantiated(i)) {
+        Debug("typecheck-idt") << "++ instantiate param " << i << " : " << d_types[i] << std::endl;
+        d_match[i] = d_types[i];
+      }
+    }
+  }
+  ~Matcher(){}
+
+  void addType( Type t ){
+    d_types.push_back( TypeNode::fromType( t ) );
+    d_match.push_back( TypeNode::null() );
+  }
+  void addTypes( std::vector< Type > types ){
+    for( int i=0; i<(int)types.size(); i++ ){
+      addType( types[i] );
+    }
+  }
+
+  bool doMatching( TypeNode base, TypeNode match ){
+    Debug("typecheck-idt") << "doMatching() : " << base << " : " << match << std::endl;
+    std::vector< TypeNode >::iterator i = std::find( d_types.begin(), d_types.end(), base );
+    if( i!=d_types.end() ){
+      int index = i - d_types.begin();
+      Debug("typecheck-idt") << "++ match on " << index << " : " << d_match[index] << std::endl;
+      if( !d_match[index].isNull() && d_match[index]!=match ){
+        return false;
+      }else{
+        d_match[ i - d_types.begin() ] = match;
+        return true;
+      }
+    }else if( base==match ){
+      return true;
+    }else if( base.getKind()!=match.getKind() || base.getNumChildren()!=match.getNumChildren() ){
+      return false;
+    }else{
+      for( int i=0; i<(int)base.getNumChildren(); i++ ){
+        if( !doMatching( base[i], match[i] ) ){
+          return false;
+        }
+      }
+      return true;
+    }
+  }
+
+  TypeNode getMatch( unsigned int i ){ return d_match[i]; }
+  void getTypes( std::vector<Type>& types ) {
+    types.clear();
+    for( int i=0; i<(int)d_match.size(); i++ ){
+      types.push_back( d_types[i].toType() );
+    }
+  }
+  void getMatches( std::vector<Type>& types ) {
+    types.clear();
+    for( int i=0; i<(int)d_match.size(); i++ ){
+      if(d_match[i].isNull()) {
+        types.push_back( d_types[i].toType() );
+      } else {
+        types.push_back( d_match[i].toType() );
+      }
+    }
+  }
+};/* class Matcher */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__MATCHER_H */