1 /********************* */
2 /*! \file symbol_table.h
4 ** Top contributors (to current version):
5 ** Morgan Deters, Christopher L. Conway, Francois Bobot
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
8 ** in the top-level source directory) and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
12 ** \brief Convenience class for scoping variable and type declarations.
14 ** Convenience class for scoping variable and type declarations.
17 #include "cvc4_public.h"
19 #ifndef __CVC4__SYMBOL_TABLE_H
20 #define __CVC4__SYMBOL_TABLE_H
24 #include <ext/hash_map>
26 #include "expr/expr.h"
27 #include "util/hash.h"
29 #include "context/cdhashset_forward.h"
30 #include "context/cdhashmap_forward.h"
38 }/* CVC4::context namespace */
40 class CVC4_PUBLIC ScopeException
: public Exception
{
41 };/* class ScopeException */
44 * A convenience class for handling scoped declarations. Implements the usual
45 * nested scoping rules for declarations, with separate bindings for expressions
48 class CVC4_PUBLIC SymbolTable
{
49 /** The context manager for the scope maps. */
50 context::Context
* d_context
;
52 /** A map for expressions. */
53 context::CDHashMap
<std::string
, Expr
, StringHashFunction
> *d_exprMap
;
55 /** A map for types. */
56 context::CDHashMap
<std::string
, std::pair
<std::vector
<Type
>, Type
>, StringHashFunction
> *d_typeMap
;
58 /** A set of defined functions. */
59 context::CDHashSet
<Expr
, ExprHashFunction
> *d_functions
;
62 /** Create a symbol table. */
65 /** Destroy a symbol table. */
69 * Bind an expression to a name in the current scope level. If
70 * <code>name</code> is already bound to an expression in the current
71 * level, then the binding is replaced. If <code>name</code> is bound
72 * in a previous level, then the binding is "covered" by this one
73 * until the current scope is popped. If levelZero is true the name
74 * shouldn't be already bound.
76 * @param name an identifier
77 * @param obj the expression to bind to <code>name</code>
78 * @param levelZero set if the binding must be done at level 0
80 void bind(const std::string
& name
, Expr obj
, bool levelZero
= false) throw();
83 * Bind a function body to a name in the current scope. If
84 * <code>name</code> is already bound to an expression in the current
85 * level, then the binding is replaced. If <code>name</code> is bound
86 * in a previous level, then the binding is "covered" by this one
87 * until the current scope is popped. Same as bind() but registers
88 * this as a function (so that isBoundDefinedFunction() returns true).
90 * @param name an identifier
91 * @param obj the expression to bind to <code>name</code>
92 * @param levelZero set if the binding must be done at level 0
94 void bindDefinedFunction(const std::string
& name
, Expr obj
, bool levelZero
= false) throw();
97 * Bind a type to a name in the current scope. If <code>name</code>
98 * is already bound to a type in the current level, then the binding
99 * is replaced. If <code>name</code> is bound in a previous level,
100 * then the binding is "covered" by this one until the current scope
103 * @param name an identifier
104 * @param t the type to bind to <code>name</code>
105 * @param levelZero set if the binding must be done at level 0
107 void bindType(const std::string
& name
, Type t
, bool levelZero
= false) throw();
110 * Bind a type to a name in the current scope. If <code>name</code>
111 * is already bound to a type or type constructor in the current
112 * level, then the binding is replaced. If <code>name</code> is
113 * bound in a previous level, then the binding is "covered" by this
114 * one until the current scope is popped.
116 * @param name an identifier
117 * @param params the parameters to the type
118 * @param t the type to bind to <code>name</code>
119 * @param levelZero true to bind it globally (default is to bind it
120 * locally within the current scope)
122 void bindType(const std::string
& name
,
123 const std::vector
<Type
>& params
,
124 Type t
, bool levelZero
= false) throw();
127 * Check whether a name is bound to an expression with either bind()
128 * or bindDefinedFunction().
130 * @param name the identifier to check.
131 * @returns true iff name is bound in the current scope.
133 bool isBound(const std::string
& name
) const throw();
136 * Check whether a name was bound to a function with bindDefinedFunction().
138 bool isBoundDefinedFunction(const std::string
& name
) const throw();
141 * Check whether an Expr was bound to a function (i.e., was the
142 * second arg to bindDefinedFunction()).
144 bool isBoundDefinedFunction(Expr func
) const throw();
147 * Check whether a name is bound to a type (or type constructor).
149 * @param name the identifier to check.
150 * @returns true iff name is bound to a type in the current scope.
152 bool isBoundType(const std::string
& name
) const throw();
155 * Lookup a bound expression.
157 * @param name the identifier to lookup
158 * @returns the expression bound to <code>name</code> in the current scope.
160 Expr
lookup(const std::string
& name
) const throw();
163 * Lookup a bound type.
165 * @param name the type identifier to lookup
166 * @returns the type bound to <code>name</code> in the current scope.
168 Type
lookupType(const std::string
& name
) const throw();
171 * Lookup a bound parameterized type.
173 * @param name the type-constructor identifier to lookup
174 * @param params the types to use to parameterize the type
175 * @returns the type bound to <code>name(<i>params</i>)</code> in
178 Type
lookupType(const std::string
& name
,
179 const std::vector
<Type
>& params
) const throw();
182 * Lookup the arity of a bound parameterized type.
184 size_t lookupArity(const std::string
& name
);
187 * Pop a scope level. Deletes all bindings since the last call to
188 * <code>pushScope</code>. Calls to <code>pushScope</code> and
189 * <code>popScope</code> must be "properly nested." I.e., a call to
190 * <code>popScope</code> is only legal if the number of prior calls to
191 * <code>pushScope</code> on this <code>SymbolTable</code> is strictly
192 * greater than then number of prior calls to <code>popScope</code>. */
193 void popScope() throw(ScopeException
);
195 /** Push a scope level. */
196 void pushScope() throw();
198 /** Get the current level of this symbol table. */
199 size_t getLevel() const throw();
201 /** Reset everything. */
204 };/* class SymbolTable */
206 }/* CVC4 namespace */
208 #endif /* __CVC4__SYMBOL_TABLE_H */