added (temporary) support for ensuring that all ambiguously typed constructor nodes created internally are given a type ascription

5 files changed, 30 insertions, 7 deletions

diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index b493b8c41..b4ff7e135 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -75,11 +75,18 @@ public:
                                    << std::endl;
         return RewriteResponse(REWRITE_DONE, in[0][selectorIndex]);
       } else {
+        TNode gt = in.getType().mkGroundTerm();
+        TypeNode gtt = gt.getType();
+        Assert( gtt.isDatatype() || gtt.isParametricDatatype() );
+        if( !gtt.isInstantiatedDatatype() ){
+          gt = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, 
+                                                NodeManager::currentNM()->mkConst(AscriptionType(in.getType().toType())), gt);
+        }
         Debug("datatypes-rewrite") << "DatatypesRewriter::postRewrite: "
                                    << "Rewrite trivial selector " << in
                                    << " to distinguished ground term "
                                    << in.getType().mkGroundTerm() << std::endl;
-        return RewriteResponse(REWRITE_DONE,in.getType().mkGroundTerm() );
+        return RewriteResponse(REWRITE_DONE,gt );
       }
     }
 
diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index a11990075..1cdefa60b 100644
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -50,7 +50,7 @@ cardinality DATATYPE_TYPE \
     "util/datatype.h"
 well-founded DATATYPE_TYPE \
     "%TYPE%.getConst<Datatype>().isWellFounded()" \
-    "%TYPE%.getConst<Datatype>().mkGroundTerm()" \
+    "%TYPE%.getConst<Datatype>().mkGroundTerm(%TYPE%.toType())" \
     "util/datatype.h"
 
 operator PARAMETRIC_DATATYPE 1: "parametric datatype"
@@ -59,7 +59,7 @@ cardinality PARAMETRIC_DATATYPE \
     "util/datatype.h"
 well-founded PARAMETRIC_DATATYPE\
     "DatatypeType(%TYPE%.toType()).getDatatype().isWellFounded()" \
-    "DatatypeType(%TYPE%.toType()).getDatatype().mkGroundTerm()" \
+    "DatatypeType(%TYPE%.toType()).getDatatype().mkGroundTerm(%TYPE%.toType())" \
     "util/datatype.h"
 
 parameterized APPLY_TYPE_ASCRIPTION ASCRIPTION_TYPE 1 \
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 2f0b82f7c..20668a5ff 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -474,6 +474,7 @@ bool TheoryDatatypes::checkInstantiate( Node te, Node cons )
       d_inst_map[ te ] = true;
       //instantiate, add equality
       Node val = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, selectorVals );
+      val = doTypeAscription( val, te.getType() );      //IDT-param
       if( find( val ) != find( te ) ) {
         //build explaination
         NodeBuilder<> nb(kind::AND);
@@ -518,6 +519,7 @@ bool TheoryDatatypes::checkInstantiate( Node te, Node cons )
 bool TheoryDatatypes::collapseSelector( Node t ) {
   if( !hasConflict() && t.getKind() == APPLY_SELECTOR ) {
     //collapse constructor
+    TypeNode retTyp = t.getType(); 
     TypeNode typ = t[0].getType();
     Node sel = t.getOperator();
     TypeNode selType = sel.getType();
@@ -531,7 +533,8 @@ bool TheoryDatatypes::collapseSelector( Node t ) {
         retNode = tmp[ Datatype::indexOf( sel.toExpr() ) ];
       } else {
         Debug("datatypes") << "Applied selector " << t << " to wrong constructor." << endl;
-        retNode = selType[1].mkGroundTerm();
+        retNode = doTypeAscription( retTyp.mkGroundTerm(), selType[1] );    //IDT-param
+        //retNode = selType[1].mkGroundTerm();
       }
       if( tmp!=t[0] ){
         t = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, t.getOperator(), tmp );
@@ -548,7 +551,7 @@ bool TheoryDatatypes::collapseSelector( Node t ) {
       unsigned r;
       checkTester( tester, conflict, r );
       if( !conflict.isNull() ) {
-        Debug("datatypes") << "Applied selector " << t << " to provably wrong constructor." << endl;
+        Debug("datatypes") << "Applied selector " << t << " to provably wrong constructor. " << retTyp << endl;
         //conflict is c ^ tester, where conflict => false, but we want to say c => ~tester
         //must remove tester from conflict
         if( conflict.getKind()==kind::AND ){
@@ -574,7 +577,8 @@ bool TheoryDatatypes::collapseSelector( Node t ) {
           tester = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( cn.getTester() ), t[0] );
           d_em.addNode( tester.notNode(), exp, Reason::idt_tcong );
         }
-        retNode = selType[1].mkGroundTerm();
+        retNode = doTypeAscription( retTyp.mkGroundTerm(), retTyp );    //IDT-param
+        //retNode = selType[1].mkGroundTerm();
         Node neq = NodeManager::currentNM()->mkNode( EQUAL, retNode, t );
 
         d_em.addNode( neq, tester.notNode(), Reason::idt_collapse2 );
@@ -1044,3 +1048,14 @@ bool TheoryDatatypes::searchForCycle( Node n, Node on,
   }
   return false;
 }
+
+Node TheoryDatatypes::doTypeAscription( Node t, TypeNode typ )
+{
+  TypeNode tt = t.getType();
+  if( (tt.isDatatype() || tt.isParametricDatatype()) && !tt.isInstantiatedDatatype() ){
+    return NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, 
+                                            NodeManager::currentNM()->mkConst(AscriptionType(typ.toType())), t);
+  }else{
+    return t;
+  }
+}
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 1b9e357ed..9dfb8c818 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -178,6 +178,7 @@ private:
   bool searchForCycle( Node n, Node on,
                        std::map< Node, bool >& visited,
                        NodeBuilder<>& explanation );
+  Node doTypeAscription( Node t, TypeNode typ );
 };/* class TheoryDatatypes */
 
 inline bool TheoryDatatypes::hasConflict() { 
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index c9c76a15b..270313e0f 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -304,7 +304,7 @@ struct ConstructorProperties {
         i != i_end;
         ++i) {
       if(TypeNode::fromType((*i).getConstructor().getType()) == type) {
-        groundTerm = Node::fromExpr((*i).mkGroundTerm());
+        groundTerm = Node::fromExpr((*i).mkGroundTerm( type.toType() ));
         type.setAttribute(GroundTermAttr(), groundTerm);
         return groundTerm;
       }