diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-06-01 00:49:37 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-06-01 00:49:37 +0000 |
commit | 471352e0956d1e9e1f0636933e792ed8650d5526 (patch) | |
tree | dfacaaf551794af187b9b70ef59a82b42b68d45a /src/expr | |
parent | 46a299aa48bcb0bff64bdb607f61f75a05987962 (diff) |
type ascriptions (casts) for parameterized datatypes, e.g. "nil :: list[INT]
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/node_manager.cpp | 5 | ||||
-rw-r--r-- | src/expr/type.cpp | 8 | ||||
-rw-r--r-- | src/expr/type.h | 15 | ||||
-rw-r--r-- | src/expr/type_node.cpp | 26 | ||||
-rw-r--r-- | src/expr/type_node.h | 6 |
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; |