diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2011-05-13 22:02:52 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2011-05-13 22:02:52 +0000 |
commit | 8d54316e7ff784a8d66da9ecc2d289ab463761c2 (patch) | |
tree | c7b5351b372cb360780ce62935fb2cfb5792299a /src/expr/declaration_scope.cpp | |
parent | 69c9ec0e1e42f3f2f2f79d3e98398c5cd1559c66 (diff) |
added support for parametric datatypes, updated cvc parser to handle parametric datatypes, type ascriptions are not implemented yet
Diffstat (limited to 'src/expr/declaration_scope.cpp')
-rw-r--r-- | src/expr/declaration_scope.cpp | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/src/expr/declaration_scope.cpp b/src/expr/declaration_scope.cpp index 8dd329b83..79accf43a 100644 --- a/src/expr/declaration_scope.cpp +++ b/src/expr/declaration_scope.cpp @@ -144,7 +144,10 @@ Type DeclarationScope::lookupType(const std::string& name, Debug("sort") << "instance is " << instantiation << endl; return instantiation; - } else { + }else if( p.second.isDatatype() ){ + Assert( DatatypeType( p.second ).isParametric() ); + return DatatypeType(p.second).instantiate(params); + }else { if(Debug.isOn("sort")) { Debug("sort") << "instantiating using a sort substitution" << endl; Debug("sort") << "have formals ["; @@ -167,6 +170,11 @@ Type DeclarationScope::lookupType(const std::string& name, } } +size_t DeclarationScope::lookupArity( const std::string& name ){ + pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second; + return p.first.size(); +} + void DeclarationScope::popScope() throw(ScopeException) { if( d_context->getLevel() == 0 ) { throw ScopeException(); |