diff options
Diffstat (limited to 'src/expr/declaration_scope.h')
-rw-r--r-- | src/expr/declaration_scope.h | 132 |
1 files changed, 132 insertions, 0 deletions
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_ */ |