diff options
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/parser.cpp | 110 |
1 files changed, 57 insertions, 53 deletions
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 10ca16001..57589ec9c 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -277,66 +277,70 @@ bool Parser::isUnresolvedType(const std::string& name) { std::vector<DatatypeType> Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) { - std::vector<DatatypeType> types = - d_exprManager->mkMutualDatatypeTypes(datatypes, d_unresolved); - - assert(datatypes.size() == types.size()); - - for(unsigned i = 0; i < datatypes.size(); ++i) { - DatatypeType t = types[i]; - const Datatype& dt = t.getDatatype(); - const std::string& name = dt.getName(); - Debug("parser-idt") << "define " << name << " as " << t << std::endl; - if(isDeclared(name, SYM_SORT)) { - throw ParserException(name + " already declared"); - } - if( t.isParametric() ) { - std::vector< Type > paramTypes = t.getParamTypes(); - defineType(name, paramTypes, t ); - } else { - defineType(name, t); - } - for(Datatype::const_iterator j = dt.begin(), - j_end = dt.end(); - j != j_end; - ++j) { - const DatatypeConstructor& ctor = *j; - Expr::printtypes::Scope pts(Debug("parser-idt"), true); - Expr constructor = ctor.getConstructor(); - Debug("parser-idt") << "+ define " << constructor << std::endl; - string constructorName = ctor.getName(); - if(isDeclared(constructorName, SYM_VARIABLE)) { - throw ParserException(constructorName + " already declared"); + try { + std::vector<DatatypeType> types = + d_exprManager->mkMutualDatatypeTypes(datatypes, d_unresolved); + + assert(datatypes.size() == types.size()); + + for(unsigned i = 0; i < datatypes.size(); ++i) { + DatatypeType t = types[i]; + const Datatype& dt = t.getDatatype(); + const std::string& name = dt.getName(); + Debug("parser-idt") << "define " << name << " as " << t << std::endl; + if(isDeclared(name, SYM_SORT)) { + throw ParserException(name + " already declared"); } - defineVar(constructorName, constructor); - Expr tester = ctor.getTester(); - Debug("parser-idt") << "+ define " << tester << std::endl; - string testerName = ctor.getTesterName(); - if(isDeclared(testerName, SYM_VARIABLE)) { - throw ParserException(testerName + " already declared"); + if( t.isParametric() ) { + std::vector< Type > paramTypes = t.getParamTypes(); + defineType(name, paramTypes, t ); + } else { + defineType(name, t); } - defineVar(testerName, tester); - for(DatatypeConstructor::const_iterator k = ctor.begin(), - k_end = ctor.end(); - k != k_end; - ++k) { - Expr selector = (*k).getSelector(); - Debug("parser-idt") << "+++ define " << selector << std::endl; - string selectorName = (*k).getName(); - if(isDeclared(selectorName, SYM_VARIABLE)) { - throw ParserException(selectorName + " already declared"); + for(Datatype::const_iterator j = dt.begin(), + j_end = dt.end(); + j != j_end; + ++j) { + const DatatypeConstructor& ctor = *j; + Expr::printtypes::Scope pts(Debug("parser-idt"), true); + Expr constructor = ctor.getConstructor(); + Debug("parser-idt") << "+ define " << constructor << std::endl; + string constructorName = ctor.getName(); + if(isDeclared(constructorName, SYM_VARIABLE)) { + throw ParserException(constructorName + " already declared"); + } + defineVar(constructorName, constructor); + Expr tester = ctor.getTester(); + Debug("parser-idt") << "+ define " << tester << std::endl; + string testerName = ctor.getTesterName(); + if(isDeclared(testerName, SYM_VARIABLE)) { + throw ParserException(testerName + " already declared"); + } + defineVar(testerName, tester); + for(DatatypeConstructor::const_iterator k = ctor.begin(), + k_end = ctor.end(); + k != k_end; + ++k) { + Expr selector = (*k).getSelector(); + Debug("parser-idt") << "+++ define " << selector << std::endl; + string selectorName = (*k).getName(); + if(isDeclared(selectorName, SYM_VARIABLE)) { + throw ParserException(selectorName + " already declared"); + } + defineVar(selectorName, selector); } - defineVar(selectorName, selector); } } - } - // These are no longer used, and the ExprManager would have - // complained of a bad substitution if anything is left unresolved. - // Clear out the set. - d_unresolved.clear(); + // These are no longer used, and the ExprManager would have + // complained of a bad substitution if anything is left unresolved. + // Clear out the set. + d_unresolved.clear(); - return types; + return types; + } catch(IllegalArgumentException& ie) { + throw ParserException(ie.getMessage()); + } } bool Parser::isDeclared(const std::string& name, SymbolType type) { |