type ascriptions (casts) for parameterized datatypes, e.g. "nil :: list[INT]

9 files changed, 122 insertions, 26 deletions

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 716e2a3b3..4cde0c624 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -238,7 +238,7 @@ void NodeManager::reclaimZombies() {
 }/* NodeManager::reclaimZombies() */
 
 TypeNode NodeManager::computeType(TNode n, bool check)
-  throw (TypeCheckingExceptionPrivate, AssertionException) {  
+  throw (TypeCheckingExceptionPrivate, AssertionException) {
   TypeNode typeNode;
 
   // Infer the type
@@ -444,6 +444,9 @@ TypeNode NodeManager::computeType(TNode n, bool check)
   case kind::APPLY_TESTER:
     typeNode = CVC4::theory::datatypes::DatatypeTesterTypeRule::computeType(this, n, check);
     break;
+  case kind::APPLY_TYPE_ASCRIPTION:
+    typeNode = CVC4::theory::datatypes::DatatypeAscriptionTypeRule::computeType(this, n, check);
+    break;
   default:
     Debug("getType") << "FAILURE" << std::endl;
     Unhandled(n.getKind());
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 8320a7053..077fc5ee2 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -537,6 +537,14 @@ bool DatatypeType::isParametric() const {
   return d_typeNode->isParametricDatatype();
 }
 
+bool DatatypeType::isInstantiated() const {
+  return d_typeNode->isInstantiatedDatatype();
+}
+
+bool DatatypeType::isParameterInstantiated(unsigned n) const {
+  return d_typeNode->isParameterInstantiatedDatatype(n);
+}
+
 size_t DatatypeType::getArity() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->getNumChildren() - 1;
diff --git a/src/expr/type.h b/src/expr/type.h
index 4b260185b..14ca3baf3 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -540,9 +540,22 @@ public:
   /** Get the underlying datatype */
   const Datatype& getDatatype() const;
 
-  /** Is this this datatype parametric? */
+  /** Is this datatype parametric? */
   bool isParametric() const;
 
+  /**
+   * Has this datatype been fully instantiated ?
+   *
+   * @return true if this datatype is not parametric or, if it is, it
+   * has been fully instantiated
+   */
+  bool isInstantiated() const;
+
+  /**
+   * Has this datatype been instantiated for parameter N ?
+   */
+  bool isParameterInstantiated(unsigned n) const;
+
   /** Get the parameter types */
   std::vector<Type> getParamTypes() const;
 
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index f77182d5d..7376b0080 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -199,6 +199,32 @@ bool TypeNode::isParametricDatatype() const {
   return getKind() == kind::PARAMETRIC_DATATYPE;
 }
 
+/** Is this an instantiated datatype type */
+bool TypeNode::isInstantiatedDatatype() const {
+  if(getKind() == kind::DATATYPE_TYPE) {
+    return true;
+  }
+  if(getKind() != kind::PARAMETRIC_DATATYPE) {
+    return false;
+  }
+  const Datatype& dt = (*this)[0].getConst<Datatype>();
+  unsigned n = dt.getNumParameters();
+  for(unsigned i = 0; i < n; ++i) {
+    if(TypeNode::fromType(dt.getParameter(i)) == (*this)[n + 1]) {
+      return false;
+    }
+  }
+  return true;
+}
+
+/** Is this an instantiated datatype parameter */
+bool TypeNode::isParameterInstantiatedDatatype(unsigned n) const {
+  AssertArgument(getKind() == kind::PARAMETRIC_DATATYPE, *this);
+  const Datatype& dt = (*this)[0].getConst<Datatype>();
+  AssertArgument(n < dt.getNumParameters(), *this);
+  return TypeNode::fromType(dt.getParameter(n)) != (*this)[n + 1];
+}
+
 /** Is this a constructor type */
 bool TypeNode::isConstructor() const {
   return getKind() == kind::CONSTRUCTOR_TYPE;
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 90fee7f1b..0f4b122db 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -488,6 +488,12 @@ public:
   /** Is this a parameterized datatype type */
   bool isParametricDatatype() const;
 
+  /** Is this a fully instantiated datatype type */
+  bool isInstantiatedDatatype() const;
+
+  /** Is this an instantiated datatype parameter */
+  bool isParameterInstantiatedDatatype(unsigned n) const;
+
   /** Is this a constructor type */
   bool isConstructor() const;
 
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 3c8d6e1ce..ca006daab 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -1461,9 +1461,16 @@ postfixTerm[CVC4::Expr& f]
           f = EXPR_MANAGER->mkVar(TupleType(f.getType()).getTypes()[k]); }
       )*/
     )*
-    (typeAscription[f, t] 
-     { //f = MK_EXPR(CVC4::kind::APPLY_TYPE_ANNOTATION, MK_CONST(t), f); 
-     } )? 
+    ( typeAscription[f, t]
+      { if(t.isDatatype()) {
+          f = MK_EXPR(CVC4::kind::APPLY_TYPE_ASCRIPTION, MK_CONST(AscriptionType(t)), f);
+        } else {
+          if(f.getType() != t) {
+            PARSER_STATE->parseError("Type ascription not satisfied.");
+          }
+        }
+      }
+    )?
   ;
 
 bvTerm[CVC4::Expr& f]
@@ -1666,16 +1673,6 @@ typeAscription[const CVC4::Expr& f, CVC4::Type& t]
 @init {
 }
   : COLON COLON type[t,CHECK_DECLARED]
-    { //if(f.getType() != t) {
-      //  std::stringstream ss;
-      //  ss << Expr::setlanguage(language::output::LANG_CVC4)
-      //     << "type ascription not satisfied\n"
-      //     << "term:     " << f << '\n'
-      //     << "has type: " << f.getType() << '\n'
-      //     << "ascribed: " << t;
-      //  PARSER_STATE->parseError(ss.str());
-      //}
-    }
   ;
 
 /**
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index 3fe43657f..c9c76a15b 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -41,6 +41,13 @@ public:
   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(){}
 
@@ -55,9 +62,11 @@ 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 );
     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{
@@ -79,20 +88,23 @@ public:
   }
 
   TypeNode getMatch( unsigned int i ){ return d_match[i]; }
-  void getTypes( std::vector<Type>& types ) { 
+  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 ) { 
+  void getMatches( std::vector<Type>& types ) {
     types.clear();
     for( int i=0; i<(int)d_match.size(); i++ ){
-      Assert( !d_match[i].isNull() ); //verify that all types have been set
-      types.push_back( d_match[i].toType() );
+      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;
@@ -157,6 +169,9 @@ struct DatatypeSelectorTypeRule {
       Debug("typecheck-idt") << "typecheck parameterized sel: " << n << std::endl;
       Matcher m( dt );
       TypeNode childType = n[0].getType(check);
+      if(! childType.isInstantiatedDatatype()) {
+        throw TypeCheckingExceptionPrivate(n, "Datatype type not fully instantiated");
+      }
       if( !m.doMatching( selType[0], childType ) ){
         throw TypeCheckingExceptionPrivate(n, "matching failed for selector argument of parameterized datatype");
       }
@@ -211,7 +226,36 @@ struct DatatypeTesterTypeRule {
     }
     return nodeManager->booleanType();
   }
-};/* struct DatatypeSelectorTypeRule */
+};/* struct DatatypeTesterTypeRule */
+
+struct DatatypeAscriptionTypeRule {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+    throw(TypeCheckingExceptionPrivate) {
+    Debug("typecheck-idt") << "typechecking ascription: " << n << std::endl;
+    Assert(n.getKind() == kind::APPLY_TYPE_ASCRIPTION);
+    TypeNode t = TypeNode::fromType(n.getOperator().getConst<AscriptionType>().getType());
+    if(check) {
+      TypeNode childType = n[0].getType(check);
+      if(!t.getKind() == kind::DATATYPE_TYPE) {
+        throw TypeCheckingExceptionPrivate(n, "bad type for datatype type ascription");
+      }
+      DatatypeType dt = DatatypeType(childType.toType());
+      if( dt.isParametric() ){
+        Debug("typecheck-idt") << "typecheck parameterized ascription: " << n << std::endl;
+        Matcher m( dt );
+        if( !m.doMatching( childType, t ) ){
+          throw TypeCheckingExceptionPrivate(n, "matching failed for type ascription argument of parameterized datatype");
+        }
+      }else{
+        Debug("typecheck-idt") << "typecheck test: " << n << std::endl;
+        if(t != childType) {
+          throw TypeCheckingExceptionPrivate(n, "bad type for type ascription argument");
+        }
+      }
+    }
+    return t;
+  }
+};/* struct DatatypeAscriptionTypeRule */
 
 struct ConstructorProperties {
   inline static Cardinality computeCardinality(TypeNode type) {
diff --git a/src/util/ascription_type.h b/src/util/ascription_type.h
index 85a51d8a4..81289572c 100644
--- a/src/util/ascription_type.h
+++ b/src/util/ascription_type.h
@@ -18,8 +18,8 @@
 
 #include "cvc4_public.h"
 
-#ifndef __CVC4__TYPE_ASCRIPTION_H
-#define __CVC4__TYPE_ASCRIPTION_H
+#ifndef __CVC4__ASCRIPTION_TYPE_H
+#define __CVC4__ASCRIPTION_TYPE_H
 
 #include "expr/type.h"
 
@@ -62,5 +62,4 @@ inline std::ostream& operator<<(std::ostream& out, AscriptionType at) {
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__TYPE_ASCRIPTION_H */
-
+#endif /* __CVC4__ASCRIPTION_TYPE_H */
diff --git a/src/util/datatype.h b/src/util/datatype.h
index 6aeb93bcf..90dd8775f 100644
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -369,7 +369,7 @@ public:
   /** Get the number of constructors (so far) for this Datatype. */
   inline size_t getNumConstructors() const throw();
 
-  /** Get the nubmer of parameters */
+  /** Get the nubmer of type parameters */
   inline size_t getNumParameters() const throw();
 
   /** Get parameter */