diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-04-13 22:50:07 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-04-13 22:50:07 +0000 |
commit | 12a8a7f9a90e45e8313f26af527a52e6dda943d3 (patch) | |
tree | 3ea9f198ee002e3f27af1fedcadd3fd318e8df2c /src | |
parent | e6d5046baca8b490e2ef93631216fe34e08d6aaa (diff) |
Merging from branches/decl-scopes (r401:411)
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/Makefile.am | 5 | ||||
-rw-r--r-- | src/expr/declaration_scope.cpp | 74 | ||||
-rw-r--r-- | src/expr/declaration_scope.h | 132 | ||||
-rw-r--r-- | src/parser/parser_state.cpp | 16 | ||||
-rw-r--r-- | src/parser/parser_state.h | 16 | ||||
-rw-r--r-- | src/parser/smt/Smt.g | 5 |
6 files changed, 233 insertions, 15 deletions
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index 1f5e403cc..67970d453 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -24,7 +24,10 @@ libexpr_la_SOURCES = \ @srcdir@/expr.cpp \ type.cpp \ command.h \ - command.cpp + command.cpp \ + declaration_scope.h \ + declaration_scope.cpp + EXTRA_DIST = \ @srcdir@/kind.h \ diff --git a/src/expr/declaration_scope.cpp b/src/expr/declaration_scope.cpp new file mode 100644 index 000000000..c326817ad --- /dev/null +++ b/src/expr/declaration_scope.cpp @@ -0,0 +1,74 @@ +/********************* */ +/** declaration_scope.cpp + ** Original author: cconway + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** Convenience class for scoping variable and type declarations (implementation) + **/ + +#include "declaration_scope.h" +#include "expr.h" +#include "type.h" + +#include "context/cdmap.h" +#include "context/context.h" + +#include <string> + +namespace CVC4 { + +using namespace context; + +DeclarationScope::DeclarationScope() : + d_context(new Context()), + d_exprMap(new (true) CDMap<std::string,Expr,StringHashFunction>(d_context)), + d_typeMap(new (true) CDMap<std::string,Type*,StringHashFunction>(d_context)) { +} + +DeclarationScope::~DeclarationScope() { + d_exprMap->deleteSelf(); + delete d_context; +} + +void DeclarationScope::bind(const std::string& name, const Expr& obj) throw () { + d_exprMap->insert(name,obj); +} + +bool DeclarationScope::isBound(const std::string& name) const throw () { + return d_exprMap->find(name) != d_exprMap->end(); +} + +Expr DeclarationScope::lookup(const std::string& name) const throw () { + return (*d_exprMap->find(name)).second; +} + +void DeclarationScope::bindType(const std::string& name, Type* t) throw () { + d_typeMap->insert(name,t); +} + +bool DeclarationScope::isBoundType(const std::string& name) const throw () { + return d_typeMap->find(name) != d_typeMap->end(); +} + +Type* DeclarationScope::lookupType(const std::string& name) const throw () { + return (*d_typeMap->find(name)).second; +} + + +void DeclarationScope::popScope() throw (ScopeException) { + if( d_context->getLevel() == 0 ) { + throw ScopeException(); + } + d_context->pop(); +} + +void DeclarationScope::pushScope() throw () { + d_context->push(); +} + +} // namespace CVC4 diff --git a/src/expr/declaration_scope.h b/src/expr/declaration_scope.h new file mode 100644 index 000000000..e08c25173 --- /dev/null +++ b/src/expr/declaration_scope.h @@ -0,0 +1,132 @@ +/********************* */ +/** context.h + ** Original author: cconway + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** Convenience class for scoping variable and type declarations. + **/ + +#ifndef DECLARATION_SCOPE_H_ +#define DECLARATION_SCOPE_H_ + +#include "expr.h" + +#include <ext/hash_map> + +namespace CVC4 { + +class Type; + +namespace context { + +class Context; + +template <class Key, class Data, class HashFcn> +class CDMap; + +} //namespace context + +/** A basic hash function for std::string + * TODO: Does this belong somewhere else (like util/)? + */ +struct StringHashFunction { + size_t operator()(const std::string& str) const { + return __gnu_cxx::hash<const char*>()(str.c_str()); + } +}; + +class CVC4_PUBLIC ScopeException : public Exception { +}; + +/** + * A convenience class for handling scoped declarations. Implements the usual + * nested scoping rules for declarations, with separate bindings for expressions + * and types. + */ +class CVC4_PUBLIC DeclarationScope { + /** The context manager for the scope maps. */ + context::Context *d_context; + + /** A map for expressions. */ + context::CDMap<std::string,Expr,StringHashFunction> *d_exprMap; + + /** A map for types. */ + context::CDMap<std::string,Type*,StringHashFunction> *d_typeMap; + +public: + /** Create a declaration scope. */ + DeclarationScope(); + + /** Destroy a declaration scope. */ + ~DeclarationScope(); + + /** Bind an expression to a name in the current scope level. + * If <code>name</code> is already bound in the current level, then the + * binding is replaced. If <code>name</code> is bound in a previous + * level, then the binding is "covered" by this one until the current + * scope is popped. + * + * @param name an identifier + * @param obj the expression to bind to <code>name</code> + */ + void bind(const std::string& name, const Expr& obj) throw (); + + /** Bind a type to a name in the current scope. + * If <code>name</code> is already bound to a type in the current level, + * then the binding is replaced. If <code>name</code> is bound in a + * previous level, then the binding is "covered" by this one until the + * current scope is popped. + * + * @param name an identifier + * @param t the type to bind to <code>name</code> + */ + void bindType(const std::string& name, Type* t) throw (); + + /** Check whether a name is bound to an expression. + * + * @param name the identifier to check. + * @returns true iff name is bound in the current scope. + */ + bool isBound(const std::string& name) const throw (); + + /** Check whether a name is bound to a type. + * + * @param name the identifier to check. + * @returns true iff name is bound to a type in the current scope. + */ + bool isBoundType(const std::string& name) const throw (); + + /** Lookup a bound expression. + * + * @param name the identifier to lookup + * @returns the expression bound to <code>name</code> in the current scope. + */ + Expr lookup(const std::string& name) const throw (); + + /** Lookup a bound type. + * + * @param name the identifier to lookup + * @returns the type bound to <code>name</code> in the current scope. + */ + Type* lookupType(const std::string& name) const throw (); + + /** Pop a scope level. Deletes all bindings since the last call to + * <code>pushScope</code>. Calls to <code>pushScope</code> and + * <code>popScope</code> must be "properly nested." I.e., a call to + * <code>popScope</code> is only legal if the number of prior calls to + * <code>pushScope</code> on this <code>DeclarationScope</code> is strictly + * greater than then number of prior calls to <code>popScope</code>. */ + void popScope() throw (ScopeException); + + /** Push a scope level. */ + void pushScope() throw (); +}; + +} // namespace CVC4 + +#endif /* DECLARATION_SCOPE_H_ */ diff --git a/src/parser/parser_state.cpp b/src/parser/parser_state.cpp index 6cc8f6d9c..5f07b16b7 100644 --- a/src/parser/parser_state.cpp +++ b/src/parser/parser_state.cpp @@ -50,7 +50,7 @@ Expr ParserState::getSymbol(const std::string& name, SymbolType type) { switch( type ) { case SYM_VARIABLE: // Functions share var namespace - return d_varTable.getObject(name); + return d_declScope.lookup(name); default: Unhandled(type); @@ -72,7 +72,7 @@ ParserState::getType(const std::string& var_name, Type* ParserState::getSort(const std::string& name) { Assert( isDeclared(name, SYM_SORT) ); - Type* t = d_sortTable.getObject(name); + Type *t = d_declScope.lookupType(name); return t; } @@ -112,16 +112,18 @@ ParserState::mkVars(const std::vector<std::string> names, void ParserState::defineVar(const std::string& name, const Expr& val) { Assert(!isDeclared(name)); - d_varTable.bindName(name,val); + d_declScope.bind(name,val); Assert(isDeclared(name)); } +/* void ParserState::undefineVar(const std::string& name) { Assert(isDeclared(name)); - d_varTable.unbindName(name); + d_declScope.unbind(name); Assert(!isDeclared(name)); } +*/ void ParserState::setLogic(const std::string& name) { @@ -137,7 +139,7 @@ ParserState::mkSort(const std::string& name) { Debug("parser") << "newSort(" << name << ")" << std::endl; Assert( !isDeclared(name, SYM_SORT) ) ; Type* type = d_exprManager->mkSort(name); - d_sortTable.bindName(name, type); + d_declScope.bindType(name, type); Assert( isDeclared(name, SYM_SORT) ) ; return type; } @@ -154,9 +156,9 @@ ParserState::mkSorts(const std::vector<std::string>& names) { bool ParserState::isDeclared(const std::string& name, SymbolType type) { switch(type) { case SYM_VARIABLE: - return d_varTable.isBound(name); + return d_declScope.isBound(name); case SYM_SORT: - return d_sortTable.isBound(name); + return d_declScope.isBoundType(name); default: Unhandled(type); } diff --git a/src/parser/parser_state.h b/src/parser/parser_state.h index 3e0771070..de624e3a0 100644 --- a/src/parser/parser_state.h +++ b/src/parser/parser_state.h @@ -20,6 +20,7 @@ #include <string> +#include "expr/declaration_scope.h" #include "expr/expr.h" #include "expr/kind.h" #include "parser/input.h" @@ -96,11 +97,8 @@ class ParserState { /** The input that we're parsing. */ Input *d_input; - /** The symbol table lookup */ - SymbolTable<Expr> d_varTable; - - /** The sort table */ - SymbolTable<Type*> d_sortTable; + /** The symbol table */ + DeclarationScope d_declScope; /** The name of the input file. */ std::string d_filename; @@ -128,6 +126,12 @@ public: return d_input; } + /** Set the declaration scope manager for this input. NOTE: This should <em>only</me> be + * called before parsing begins. Otherwise, previous declarations will be lost. */ + inline void setDeclarationScope(DeclarationScope declScope) { + d_declScope = declScope; + } + /** * Check if we are done -- either the end of input has been reached, or some * error has been encountered. @@ -251,6 +255,8 @@ public: d_input->parseError(msg); } + inline void pushScope() { d_declScope.pushScope(); } + inline void popScope() { d_declScope.popScope(); } }; // class ParserState } // namespace parser diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index 160bd321f..25c2fbc89 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -198,10 +198,11 @@ annotatedFormula[CVC4::Expr& expr] (LET_TOK LPAREN_TOK let_identifier[name,CHECK_UNDECLARED] | FLET_TOK LPAREN_TOK flet_identifier[name,CHECK_UNDECLARED] ) annotatedFormula[expr] RPAREN_TOK - { PARSER_STATE->defineVar(name,expr); } + { PARSER_STATE->pushScope(); + PARSER_STATE->defineVar(name,expr); } annotatedFormula[expr] RPAREN_TOK - { PARSER_STATE->undefineVar(name); } + { PARSER_STATE->popScope(); } | /* a variable */ ( identifier[name,CHECK_DECLARED,SYM_VARIABLE] |