diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-05-14 00:15:43 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-05-14 00:15:43 +0000 |
commit | 11bb98ba5b1e9e88053a7bd6adc1d48d48a4bb21 (patch) | |
tree | 1c975ba91df4f5ffcee6b53d164d00e1181b83c8 /src/parser/parser.cpp | |
parent | 8d54316e7ff784a8d66da9ecc2d289ab463761c2 (diff) |
add AscriptionType stuff to support nullary parameterized datatypes; also, review of Andy's earlier commit, with some minor code clean-up and documentation
Diffstat (limited to 'src/parser/parser.cpp')
-rw-r--r-- | src/parser/parser.cpp | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index efe01fb40..78e70572a 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -242,15 +242,17 @@ SortType Parser::mkUnresolvedType(const std::string& name) { return unresolved; } -SortConstructorType Parser::mkUnresolvedTypeConstructor(const std::string& name, - size_t arity) -{ +SortConstructorType +Parser::mkUnresolvedTypeConstructor(const std::string& name, + size_t arity) { SortConstructorType unresolved = mkSortConstructor(name,arity); d_unresolved.insert(unresolved); return unresolved; } -SortConstructorType Parser::mkUnresolvedTypeConstructor(const std::string& name, - const std::vector<Type>& params){ + +SortConstructorType +Parser::mkUnresolvedTypeConstructor(const std::string& name, + const std::vector<Type>& params) { Debug("parser") << "newSortConstructor(P)(" << name << ", " << params.size() << ")" << std::endl; SortConstructorType unresolved = d_exprManager->mkSortConstructor(name, params.size()); @@ -283,10 +285,10 @@ Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) { if(isDeclared(name, SYM_SORT)) { throw ParserException(name + " already declared"); } - if( t.isParametric() ){ + if( t.isParametric() ) { std::vector< Type > paramTypes = t.getParamTypes(); defineType(name, paramTypes, t ); - }else{ + } else { defineType(name, t); } for(Datatype::const_iterator j = dt.begin(), |