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

5 files changed, 58 insertions, 2 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;