fixed various bugs related to ambiguous parametric datatype constructors, parametric datatype versions of paper benchmarks are now working

2 files changed, 35 insertions, 22 deletions

diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index a06a7c2b5..926f31847 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -52,6 +52,7 @@ typedef expr::Attribute<expr::attr::DatatypeWellFoundedComputedTag, bool> Dataty
 typedef expr::Attribute<expr::attr::DatatypeGroundTermTag, Node> DatatypeGroundTermAttr;
 
 const Datatype& Datatype::datatypeOf(Expr item) {
+  ExprManagerScope ems(item);
   TypeNode t = Node::fromExpr(item).getType();
   switch(t.getKind()) {
   case kind::CONSTRUCTOR_TYPE:
@@ -65,14 +66,19 @@ const Datatype& Datatype::datatypeOf(Expr item) {
 }
 
 size_t Datatype::indexOf(Expr item) {
+  ExprManagerScope ems(item);
   AssertArgument(item.getType().isConstructor() ||
                  item.getType().isTester() ||
                  item.getType().isSelector(),
                  item,
                  "arg must be a datatype constructor, selector, or tester");
   TNode n = Node::fromExpr(item);
-  Assert(n.hasAttribute(DatatypeIndexAttr()));
-  return n.getAttribute(DatatypeIndexAttr());
+  if( item.getKind()==kind::APPLY_TYPE_ASCRIPTION ){
+    return indexOf( item[0] );
+  }else{
+    Assert(n.hasAttribute(DatatypeIndexAttr()));
+    return n.getAttribute(DatatypeIndexAttr());
+  }
 }
 
 void Datatype::resolve(ExprManager* em,
@@ -201,7 +207,8 @@ Expr Datatype::mkGroundTerm( Type t ) const throw(AssertionException) {
     for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
       // prefer the nullary constructor
       if( groundTerm.isNull() && (*i).getNumArgs() == 0) {
-        groundTerm = (*i).getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, (*i).getConstructor());
+        groundTerm = d_constructors[indexOf((*i).getConstructor())].mkGroundTerm( t );
+        //groundTerm = (*i).getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, (*i).getConstructor());
         self.setAttribute(DatatypeGroundTermAttr(), groundTerm);
         Debug("datatypes-gt") << "constructed nullary: " << getName() << " => " << groundTerm << std::endl;
       }
@@ -261,10 +268,6 @@ Expr Datatype::mkGroundTerm( Type t ) const throw(AssertionException) {
     // if we get all the way here, we aren't well-founded
     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,
-                                                    NodeManager::currentNM()->mkConst(AscriptionType(t)), groundTerm).toExpr();
-    }
     return groundTerm;
   }
 }
@@ -522,7 +525,7 @@ Type Datatype::Constructor::getSpecializedConstructorType(Type returnType) const
   vector<Type> subst;
   m.getMatches(subst);
   vector<Type> params = dt.getParameters();
-  return d_constructor.getType().substitute(subst, params);
+  return d_constructor.getType().substitute(params, subst);
 }
 
 Expr Datatype::Constructor::getTester() const {
@@ -615,7 +618,6 @@ bool Datatype::Constructor::isWellFounded() const throw(AssertionException) {
 Expr Datatype::Constructor::mkGroundTerm( Type t ) const throw(AssertionException) {
   CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 
-  Debug("datatypes-gt") << "mkGroundTerm " << t << std::endl;
   // we're using some internals, so we have to set up this library context
   ExprManagerScope ems(d_constructor);
 
@@ -652,8 +654,17 @@ Expr Datatype::Constructor::mkGroundTerm( Type t ) const throw(AssertionExceptio
     }
     groundTerms.push_back(selType.mkGroundTerm());
   }
-
+  
   groundTerm = getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, groundTerms);
+  if( groundTerm.getType()!=t ){
+    Assert( Datatype::datatypeOf( d_constructor ).isParametric() );
+    //type is ambiguous, must apply type ascription
+    Debug("datatypes-gt") << "ambiguous type for " << groundTerm << ", ascribe to " << t << std::endl;
+    groundTerms[0] = getConstructor().getExprManager()->mkExpr(kind::APPLY_TYPE_ASCRIPTION,
+                       getConstructor().getExprManager()->mkConst(AscriptionType(getSpecializedConstructorType(t))),
+                       groundTerms[0]);
+    groundTerm = getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, groundTerms);
+  }
   self.setAttribute(DatatypeGroundTermAttr(), groundTerm);
   return groundTerm;
 }
diff --git a/src/util/matcher.h b/src/util/matcher.h
index 2c55309d3..5dc511bc2 100644
--- a/src/util/matcher.h
+++ b/src/util/matcher.h
@@ -38,6 +38,11 @@ private:
 public:
   Matcher(){}
   Matcher( DatatypeType dt ){
+    addTypesFromDatatype( dt );
+  }
+  ~Matcher(){}
+
+  void addTypesFromDatatype( DatatypeType dt ){
     std::vector< Type > argTypes = dt.getParamTypes();
     addTypes( argTypes );
     Debug("typecheck-idt") << "instantiating matcher for " << dt << std::endl;
@@ -48,8 +53,6 @@ public:
       }
     }
   }
-  ~Matcher(){}
-
   void addType( Type t ){
     d_types.push_back( TypeNode::fromType( t ) );
     d_match.push_back( TypeNode::null() );
@@ -60,25 +63,24 @@ public:
     }
   }
 
-  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 );
+  bool doMatching( TypeNode pattern, TypeNode tn ){
+    Debug("typecheck-idt") << "doMatching() : " << pattern << " : " << tn << std::endl;
+    std::vector< TypeNode >::iterator i = std::find( d_types.begin(), d_types.end(), pattern );
     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 ){
+      if( !d_match[index].isNull() && d_match[index]!=tn ){
         return false;
       }else{
-        d_match[ i - d_types.begin() ] = match;
+        d_match[ i - d_types.begin() ] = tn;
         return true;
       }
-    }else if( base==match ){
+    }else if( pattern==tn ){
       return true;
-    }else if( base.getKind()!=match.getKind() || base.getNumChildren()!=match.getNumChildren() ){
+    }else if( pattern.getKind()!=tn.getKind() || pattern.getNumChildren()!=tn.getNumChildren() ){
       return false;
     }else{
-      for( int i=0; i<(int)base.getNumChildren(); i++ ){
-        if( !doMatching( base[i], match[i] ) ){
+      for( int i=0; i<(int)pattern.getNumChildren(); i++ ){
+        if( !doMatching( pattern[i], tn[i] ) ){
           return false;
         }
       }