1 /********************* */
2 /*! \file symbol_table.h
4 ** Original author: cconway
5 ** Major contributors: mdeters
6 ** Minor contributors (to current version): ajreynol, dejan, bobot
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief Convenience class for scoping variable and type declarations.
16 ** Convenience class for scoping variable and type declarations.
19 #include "cvc4_public.h"
21 #ifndef __CVC4__SYMBOL_TABLE_H
22 #define __CVC4__SYMBOL_TABLE_H
26 #include <ext/hash_map>
28 #include "expr/expr.h"
29 #include "util/hash.h"
31 #include "context/cdhashset_forward.h"
32 #include "context/cdhashmap_forward.h"
40 }/* CVC4::context namespace */
42 class CVC4_PUBLIC ScopeException
: public Exception
{
43 };/* class ScopeException */
46 * A convenience class for handling scoped declarations. Implements the usual
47 * nested scoping rules for declarations, with separate bindings for expressions
50 class CVC4_PUBLIC SymbolTable
{
51 /** The context manager for the scope maps. */
52 context::Context
* d_context
;
54 /** A map for expressions. */
55 context::CDHashMap
<std::string
, Expr
, StringHashFunction
> *d_exprMap
;
57 /** A map for types. */
58 context::CDHashMap
<std::string
, std::pair
<std::vector
<Type
>, Type
>, StringHashFunction
> *d_typeMap
;
60 /** A set of defined functions. */
61 context::CDHashSet
<Expr
, ExprHashFunction
> *d_functions
;
64 /** Create a declaration scope. */
67 /** Destroy a declaration scope. */
71 * Bind an expression to a name in the current scope level. If
72 * <code>name</code> is already bound to an expression in the current
73 * level, then the binding is replaced. If <code>name</code> is bound
74 * in a previous level, then the binding is "covered" by this one
75 * until the current scope is popped. If levelZero is true the name
76 * shouldn't be already bound.
78 * @param name an identifier
79 * @param obj the expression to bind to <code>name</code>
80 * @param levelZero set if the binding must be done at level 0
82 void bind(const std::string
& name
, Expr obj
, bool levelZero
= false) throw(AssertionException
);
85 * Bind a function body to a name in the current scope. If
86 * <code>name</code> is already bound to an expression in the current
87 * level, then the binding is replaced. If <code>name</code> is bound
88 * in a previous level, then the binding is "covered" by this one
89 * until the current scope is popped. Same as bind() but registers
90 * this as a function (so that isBoundDefinedFunction() returns true).
92 * @param name an identifier
93 * @param obj the expression to bind to <code>name</code>
94 * @param levelZero set if the binding must be done at level 0
96 void bindDefinedFunction(const std::string
& name
, Expr obj
, bool levelZero
= false) throw(AssertionException
);
99 * Bind a type to a name in the current scope. If <code>name</code>
100 * is already bound to a type in the current level, then the binding
101 * is replaced. If <code>name</code> is bound in a previous level,
102 * then the binding is "covered" by this one until the current scope
105 * @param name an identifier
106 * @param t the type to bind to <code>name</code>
107 * @param levelZero set if the binding must be done at level 0
109 void bindType(const std::string
& name
, Type t
, bool levelZero
= false) throw();
112 * Bind a type to a name in the current scope. If <code>name</code>
113 * is already bound to a type or type constructor in the current
114 * level, then the binding is replaced. If <code>name</code> is
115 * bound in a previous level, then the binding is "covered" by this
116 * one until the current scope is popped.
118 * @param name an identifier
119 * @param params the parameters to the type
120 * @param t the type to bind to <code>name</code>
121 * @param levelZero true to bind it globally (default is to bind it
122 * locally within the current scope)
124 void bindType(const std::string
& name
,
125 const std::vector
<Type
>& params
,
126 Type t
, bool levelZero
= false) throw();
129 * Check whether a name is bound to an expression with either bind()
130 * or bindDefinedFunction().
132 * @param name the identifier to check.
133 * @returns true iff name is bound in the current scope.
135 bool isBound(const std::string
& name
) const throw();
138 * Check whether a name was bound to a function with bindDefinedFunction().
140 bool isBoundDefinedFunction(const std::string
& name
) const throw();
143 * Check whether an Expr was bound to a function (i.e., was the
144 * second arg to bindDefinedFunction()).
146 bool isBoundDefinedFunction(Expr func
) const throw();
149 * Check whether a name is bound to a type (or type constructor).
151 * @param name the identifier to check.
152 * @returns true iff name is bound to a type in the current scope.
154 bool isBoundType(const std::string
& name
) const throw();
157 * Lookup a bound expression.
159 * @param name the identifier to lookup
160 * @returns the expression bound to <code>name</code> in the current scope.
162 Expr
lookup(const std::string
& name
) const throw(AssertionException
);
165 * Lookup a bound type.
167 * @param name the type identifier to lookup
168 * @returns the type bound to <code>name</code> in the current scope.
170 Type
lookupType(const std::string
& name
) const throw(AssertionException
);
173 * Lookup a bound parameterized type.
175 * @param name the type-constructor identifier to lookup
176 * @param params the types to use to parameterize the type
177 * @returns the type bound to <code>name(<i>params</i>)</code> in
180 Type
lookupType(const std::string
& name
,
181 const std::vector
<Type
>& params
) const throw(AssertionException
);
184 * Lookup the arity of a bound parameterized type.
186 size_t lookupArity(const std::string
& name
);
189 * Pop a scope level. Deletes all bindings since the last call to
190 * <code>pushScope</code>. Calls to <code>pushScope</code> and
191 * <code>popScope</code> must be "properly nested." I.e., a call to
192 * <code>popScope</code> is only legal if the number of prior calls to
193 * <code>pushScope</code> on this <code>SymbolTable</code> is strictly
194 * greater than then number of prior calls to <code>popScope</code>. */
195 void popScope() throw(ScopeException
);
197 /** Push a scope level. */
198 void pushScope() throw();
200 /** Get the current level of this declaration scope. */
201 size_t getLevel() const throw();
203 };/* class SymbolTable */
205 }/* CVC4 namespace */
207 #endif /* __CVC4__SYMBOL_TABLE_H */