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/node_manager.cpp | |
| parent | 46a299aa48bcb0bff64bdb607f61f75a05987962 (diff) | |
type ascriptions (casts) for parameterized datatypes, e.g. "nil :: list[INT]
Diffstat (limited to 'src/expr/node_manager.cpp')
| -rw-r--r-- | src/expr/node_manager.cpp | 5 |
1 files changed, 4 insertions, 1 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()); |