diff options
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/cvc/Cvc.g | 75 | ||||
-rw-r--r-- | src/parser/parser.cpp | 30 | ||||
-rw-r--r-- | src/parser/parser.h | 15 |
3 files changed, 94 insertions, 26 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index b3c253dab..3c8d6e1ce 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1002,12 +1002,27 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t, } /* named types */ : identifier[id,check,SYM_SORT] - parameterization[check]? - { if(check == CHECK_DECLARED || + parameterization[check,types]? + { + if(check == CHECK_DECLARED || PARSER_STATE->isDeclared(id, SYM_SORT)) { - t = PARSER_STATE->getSort(id); + Debug("parser-param") << "param: getSort " << id << " " << types.size() << " " << PARSER_STATE->getArity( id ) + << " " << PARSER_STATE->isDeclared(id, SYM_SORT) << std::endl; + if( types.size()>0 ){ + t = PARSER_STATE->getSort(id, types); + }else{ + t = PARSER_STATE->getSort(id); + } } else { - t = PARSER_STATE->mkUnresolvedType(id); + if( types.empty() ){ + t = PARSER_STATE->mkUnresolvedType(id); + Debug("parser-param") << "param: make unres type " << id << std::endl; + }else{ + t = PARSER_STATE->mkUnresolvedTypeConstructor(id,types); + t = SortConstructorType(t).instantiate( types ); + Debug("parser-param") << "param: make unres param type " << id << " " << types.size() << " " + << PARSER_STATE->getArity( id ) << std::endl; + } } } @@ -1076,12 +1091,13 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t, } ; -parameterization[CVC4::parser::DeclarationCheck check] +parameterization[CVC4::parser::DeclarationCheck check, + std::vector<CVC4::Type>& params] @init { Type t; } - : LBRACKET restrictedType[t,check] ( COMMA restrictedType[t,check] )* RBRACKET - { UNSUPPORTED("parameterized types not yet supported"); } + : LBRACKET restrictedType[t,check] { Debug("parser-param") << "t = " << t << std::endl; params.push_back( t ); } + ( COMMA restrictedType[t,check] { Debug("parser-param") << "t = " << t << std::endl; params.push_back( t ); } )* RBRACKET ; bound returns [CVC4::parser::cvc::mySubrangeBound bound] @@ -1267,6 +1283,7 @@ term[CVC4::Expr& f] std::vector<CVC4::Expr> expressions; std::vector<unsigned> operators; unsigned op; + Type t; } : storeTerm[f] { expressions.push_back(f); } ( arithmeticBinop[op] storeTerm[f] { operators.push_back(op); expressions.push_back(f); } )* @@ -1374,6 +1391,7 @@ postfixTerm[CVC4::Expr& f] bool extract = false, left = false; std::vector<Expr> args; std::string id; + Type t; } : bvTerm[f] ( /* array select / bitvector extract */ @@ -1443,7 +1461,9 @@ postfixTerm[CVC4::Expr& f] f = EXPR_MANAGER->mkVar(TupleType(f.getType()).getTypes()[k]); } )*/ )* - typeAscription[f]? + (typeAscription[f, t] + { //f = MK_EXPR(CVC4::kind::APPLY_TYPE_ANNOTATION, MK_CONST(t), f); + } )? ; bvTerm[CVC4::Expr& f] @@ -1642,20 +1662,19 @@ simpleTerm[CVC4::Expr& f] * Matches (and performs) a type ascription. * The f arg is the term to check (it is an input-only argument). */ -typeAscription[const CVC4::Expr& f] +typeAscription[const CVC4::Expr& f, CVC4::Type& t] @init { - Type t; } : COLON COLON type[t,CHECK_DECLARED] - { if(f.getType() != t) { - std::stringstream ss; - ss << Expr::setlanguage(language::output::LANG_CVC4) - << "type ascription not satisfied\n" - << "term: " << f << '\n' - << "has type: " << f.getType() << '\n' - << "ascribed: " << t; - PARSER_STATE->parseError(ss.str()); - } + { //if(f.getType() != t) { + // std::stringstream ss; + // ss << Expr::setlanguage(language::output::LANG_CVC4) + // << "type ascription not satisfied\n" + // << "term: " << f << '\n' + // << "has type: " << f.getType() << '\n' + // << "ascribed: " << t; + // PARSER_STATE->parseError(ss.str()); + //} } ; @@ -1706,16 +1725,23 @@ iteElseTerm[CVC4::Expr& f] datatypeDef[std::vector<CVC4::Datatype>& datatypes] @init { std::string id, id2; + Type t; + std::vector< Type > params; } /* This really needs to be CHECK_NONE, or mutually-recursive datatypes * won't work, because this type will already be "defined" as an * unresolved type; don't worry, we check below. */ - : identifier[id,CHECK_NONE,SYM_SORT] - ( LBRACKET identifier[id2,CHECK_NONE,SYM_SORT] - ( COMMA identifier[id2,CHECK_NONE,SYM_SORT] )* RBRACKET - { UNSUPPORTED("parameterized datatypes not yet supported"); } + : identifier[id,CHECK_NONE,SYM_SORT] { PARSER_STATE->pushScope(); } + ( LBRACKET identifier[id2,CHECK_UNDECLARED,SYM_SORT] { + t = PARSER_STATE->mkSort(id2); + params.push_back( t ); + } + ( COMMA identifier[id2,CHECK_UNDECLARED,SYM_SORT] { + t = PARSER_STATE->mkSort(id2); + params.push_back( t ); } + )* RBRACKET )? - { datatypes.push_back(Datatype(id)); + { datatypes.push_back(Datatype(id,params)); if(!PARSER_STATE->isUnresolvedType(id)) { // if not unresolved, must be undeclared PARSER_STATE->checkDeclaration(id, CHECK_UNDECLARED, SYM_SORT); @@ -1723,6 +1749,7 @@ datatypeDef[std::vector<CVC4::Datatype>& datatypes] } EQUAL_TOK constructorDef[datatypes.back()] ( BAR constructorDef[datatypes.back()] )* + { PARSER_STATE->popScope(); } ; /** diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 29ade43c1..efe01fb40 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -95,6 +95,11 @@ Type Parser::getSort(const std::string& name, return t; } +size_t Parser::getArity(const std::string& sort_name){ + Assert( isDeclared(sort_name, SYM_SORT) ); + return d_declScope->lookupArity(sort_name); +} + /* Returns true if name is bound to a boolean variable. */ bool Parser::isBoolean(const std::string& name) { return isDeclared(name, SYM_VARIABLE) && getType(name).isBoolean(); @@ -237,6 +242,24 @@ SortType Parser::mkUnresolvedType(const std::string& name) { return unresolved; } +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){ + Debug("parser") << "newSortConstructor(P)(" << name << ", " << params.size() << ")" + << std::endl; + SortConstructorType unresolved = d_exprManager->mkSortConstructor(name, params.size()); + defineType(name, params, unresolved); + Type t = getSort( name, params ); + d_unresolved.insert(unresolved); + return unresolved; +} + bool Parser::isUnresolvedType(const std::string& name) { if(!isDeclared(name, SYM_SORT)) { return false; @@ -260,7 +283,12 @@ Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) { if(isDeclared(name, SYM_SORT)) { throw ParserException(name + " already declared"); } - defineType(name, t); + 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; diff --git a/src/parser/parser.h b/src/parser/parser.h index 6509b192b..6d55e195e 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -150,7 +150,7 @@ class CVC4_PUBLIC Parser { * depend on mkMutualDatatypeTypes() to check everything and clear * this out. */ - std::set<SortType> d_unresolved; + std::set<Type> d_unresolved; /** * "Preemption commands": extra commands implied by subterms that @@ -255,6 +255,11 @@ public: const std::vector<Type>& params); /** + * Returns arity of a (parameterized) sort, given a name and args. + */ + size_t getArity(const std::string& sort_name); + + /** * Checks if a symbol has been declared. * @param name the symbol name * @param type the symbol type @@ -368,6 +373,14 @@ public: SortType mkUnresolvedType(const std::string& name); /** + * Creates a new "unresolved type," used only during parsing. + */ + SortConstructorType mkUnresolvedTypeConstructor(const std::string& name, + size_t arity); + SortConstructorType mkUnresolvedTypeConstructor(const std::string& name, + const std::vector<Type>& params); + + /** * Returns true IFF name is an unresolved type. */ bool isUnresolvedType(const std::string& name); |