diff options
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/cvc/Cvc.g | 10 | ||||
-rw-r--r-- | src/parser/parser.cpp | 28 | ||||
-rw-r--r-- | src/parser/parser.h | 26 |
3 files changed, 32 insertions, 32 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index bbeee4f7f..1a85f45c3 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1057,7 +1057,7 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t, std::string id; std::vector<Type> types; std::vector< std::pair<std::string, Type> > typeIds; - DeclarationScope* declScope; + //SymbolTable* symtab; Parser* parser; lhs = false; } @@ -1097,11 +1097,11 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t, * declared in the outer context. What follows isn't quite right, * though, since type aliases and function definitions should be * retained in the set of current declarations. */ - { /*declScope = PARSER_STATE->getDeclarationScope(); - PARSER_STATE->useDeclarationsFrom(new DeclarationScope());*/ } + { /*symtab = PARSER_STATE->getSymbolTable(); + PARSER_STATE->useDeclarationsFrom(new SymbolTable());*/ } formula[f] ( COMMA formula[f2] )? RPAREN - { /*DeclarationScope* old = PARSER_STATE->getDeclarationScope(); - PARSER_STATE->useDeclarationsFrom(declScope); + { /*SymbolTable* old = PARSER_STATE->getSymbolTable(); + PARSER_STATE->useDeclarationsFrom(symtab); delete old;*/ t = f2.isNull() ? EXPR_MANAGER->mkPredicateSubtype(f) : diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 44148a7f1..29db640c7 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -43,8 +43,8 @@ namespace parser { Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) : d_exprManager(exprManager), d_input(input), - d_declScopeAllocated(), - d_declScope(&d_declScopeAllocated), + d_symtabAllocated(), + d_symtab(&d_symtabAllocated), d_anonymousFunctionCount(0), d_done(false), d_checksEnabled(true), @@ -60,7 +60,7 @@ Expr Parser::getSymbol(const std::string& name, SymbolType type) { switch( type ) { case SYM_VARIABLE: // Functions share var namespace - return d_declScope->lookup(name); + return d_symtab->lookup(name); default: Unhandled(type); @@ -87,7 +87,7 @@ Type Parser::getType(const std::string& var_name, Type Parser::getSort(const std::string& name) { checkDeclaration(name, CHECK_DECLARED, SYM_SORT); Assert( isDeclared(name, SYM_SORT) ); - Type t = d_declScope->lookupType(name); + Type t = d_symtab->lookupType(name); return t; } @@ -95,14 +95,14 @@ Type Parser::getSort(const std::string& name, const std::vector<Type>& params) { checkDeclaration(name, CHECK_DECLARED, SYM_SORT); Assert( isDeclared(name, SYM_SORT) ); - Type t = d_declScope->lookupType(name, params); + Type t = d_symtab->lookupType(name, params); return t; } size_t Parser::getArity(const std::string& sort_name){ checkDeclaration(sort_name, CHECK_DECLARED, SYM_SORT); Assert( isDeclared(sort_name, SYM_SORT) ); - return d_declScope->lookupArity(sort_name); + return d_symtab->lookupArity(sort_name); } /* Returns true if name is bound to a boolean variable. */ @@ -125,14 +125,14 @@ bool Parser::isFunctionLike(const std::string& name) { bool Parser::isDefinedFunction(const std::string& name) { // more permissive in type than isFunction(), because defined // functions can be zero-ary and declared functions cannot. - return d_declScope->isBoundDefinedFunction(name); + return d_symtab->isBoundDefinedFunction(name); } /* Returns true if the Expr is a defined function. */ bool Parser::isDefinedFunction(Expr func) { // more permissive in type than isFunction(), because defined // functions can be zero-ary and declared functions cannot. - return d_declScope->isBoundDefinedFunction(func); + return d_symtab->isBoundDefinedFunction(func); } /* Returns true if name is bound to a function returning boolean. */ @@ -179,20 +179,20 @@ Parser::mkVars(const std::vector<std::string> names, void Parser::defineVar(const std::string& name, const Expr& val, bool levelZero) { - d_declScope->bind(name, val, levelZero); + d_symtab->bind(name, val, levelZero); Assert( isDeclared(name) ); } void Parser::defineFunction(const std::string& name, const Expr& val, bool levelZero) { - d_declScope->bindDefinedFunction(name, val, levelZero); + d_symtab->bindDefinedFunction(name, val, levelZero); Assert( isDeclared(name) ); } void Parser::defineType(const std::string& name, const Type& type) { - d_declScope->bindType(name, type); + d_symtab->bindType(name, type); Assert( isDeclared(name, SYM_SORT) ); } @@ -200,7 +200,7 @@ void Parser::defineType(const std::string& name, const std::vector<Type>& params, const Type& type) { - d_declScope->bindType(name, params, type); + d_symtab->bindType(name, params, type); Assert( isDeclared(name, SYM_SORT) ); } @@ -369,9 +369,9 @@ DatatypeType Parser::mkTupleType(const std::vector<Type>& types) { bool Parser::isDeclared(const std::string& name, SymbolType type) { switch(type) { case SYM_VARIABLE: - return d_declScope->isBound(name); + return d_symtab->isBound(name); case SYM_SORT: - return d_declScope->isBoundType(name); + return d_symtab->isBoundType(name); default: Unhandled(type); } diff --git a/src/parser/parser.h b/src/parser/parser.h index 635dd6b6c..f3210ae29 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -28,7 +28,7 @@ #include "parser/input.h" #include "parser/parser_exception.h" #include "expr/expr.h" -#include "expr/declaration_scope.h" +#include "expr/symbol_table.h" #include "expr/kind.h" #include "expr/expr_stream.h" @@ -117,15 +117,15 @@ class CVC4_PUBLIC Parser { * The declaration scope that is "owned" by this parser. May or * may not be the current declaration scope in use. */ - DeclarationScope d_declScopeAllocated; + SymbolTable d_symtabAllocated; /** * This current symbol table used by this parser. Initially points - * to d_declScopeAllocated, but can be changed (making this parser + * to d_symtabAllocated, but can be changed (making this parser * delegate its definitions and lookups to another parser). * See useDeclarationsFrom(). */ - DeclarationScope* d_declScope; + SymbolTable* d_symtab; /** How many anonymous functions we've created. */ size_t d_anonymousFunctionCount; @@ -493,8 +493,8 @@ public: } } - inline void pushScope() { d_declScope->pushScope(); } - inline void popScope() { d_declScope->popScope(); } + inline void pushScope() { d_symtab->pushScope(); } + inline void popScope() { d_symtab->popScope(); } /** * Set the current symbol table used by this parser. @@ -523,25 +523,25 @@ public: */ inline void useDeclarationsFrom(Parser* parser) { if(parser == NULL) { - d_declScope = &d_declScopeAllocated; + d_symtab = &d_symtabAllocated; } else { - d_declScope = parser->d_declScope; + d_symtab = parser->d_symtab; } } - inline void useDeclarationsFrom(DeclarationScope* scope) { - d_declScope = scope; + inline void useDeclarationsFrom(SymbolTable* symtab) { + d_symtab = symtab; } - inline DeclarationScope* getDeclarationScope() const { - return d_declScope; + inline SymbolTable* getSymbolTable() const { + return d_symtab; } /** * Gets the current declaration level. */ inline size_t getDeclarationLevel() const throw() { - return d_declScope->getLevel(); + return d_symtab->getLevel(); } /** |