From 471352e0956d1e9e1f0636933e792ed8650d5526 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 1 Jun 2011 00:49:37 +0000 Subject: type ascriptions (casts) for parameterized datatypes, e.g. "nil :: list[INT] --- src/expr/node_manager.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'src/expr/node_manager.cpp') 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()); -- cgit v1.2.3