1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
|
/********************* */
/*! \file symbol_table.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: Christopher L. Conway
** Minor contributors (to current version): Andrew Reynolds, Dejan Jovanovic, Francois Bobot
** This file is part of the CVC4 project.
** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
** \brief Convenience class for scoping variable and type declarations.
**
** Convenience class for scoping variable and type declarations.
**/
#include "cvc4_public.h"
#ifndef __CVC4__SYMBOL_TABLE_H
#define __CVC4__SYMBOL_TABLE_H
#include <vector>
#include <utility>
#include <ext/hash_map>
#include "expr/expr.h"
#include "util/hash.h"
#include "context/cdhashset_forward.h"
#include "context/cdhashmap_forward.h"
namespace CVC4 {
class Type;
namespace context {
class Context;
}/* CVC4::context namespace */
class CVC4_PUBLIC ScopeException : public Exception {
};/* class ScopeException */
/**
* 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 SymbolTable {
/** The context manager for the scope maps. */
context::Context* d_context;
/** A map for expressions. */
context::CDHashMap<std::string, Expr, StringHashFunction> *d_exprMap;
/** A map for types. */
context::CDHashMap<std::string, std::pair<std::vector<Type>, Type>, StringHashFunction> *d_typeMap;
/** A set of defined functions. */
context::CDHashSet<Expr, ExprHashFunction> *d_functions;
public:
/** Create a symbol table. */
SymbolTable();
/** Destroy a symbol table. */
~SymbolTable();
/**
* Bind an expression to a name in the current scope level. If
* <code>name</code> is already bound to an expression 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. If levelZero is true the name
* shouldn't be already bound.
*
* @param name an identifier
* @param obj the expression to bind to <code>name</code>
* @param levelZero set if the binding must be done at level 0
*/
void bind(const std::string& name, Expr obj, bool levelZero = false) throw();
/**
* Bind a function body to a name in the current scope. If
* <code>name</code> is already bound to an expression 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. Same as bind() but registers
* this as a function (so that isBoundDefinedFunction() returns true).
*
* @param name an identifier
* @param obj the expression to bind to <code>name</code>
* @param levelZero set if the binding must be done at level 0
*/
void bindDefinedFunction(const std::string& name, Expr obj, bool levelZero = false) 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>
* @param levelZero set if the binding must be done at level 0
*/
void bindType(const std::string& name, Type t, bool levelZero = false) throw();
/**
* Bind a type to a name in the current scope. If <code>name</code>
* is already bound to a type or type constructor 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 params the parameters to the type
* @param t the type to bind to <code>name</code>
* @param levelZero true to bind it globally (default is to bind it
* locally within the current scope)
*/
void bindType(const std::string& name,
const std::vector<Type>& params,
Type t, bool levelZero = false) throw();
/**
* Check whether a name is bound to an expression with either bind()
* or bindDefinedFunction().
*
* @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 was bound to a function with bindDefinedFunction().
*/
bool isBoundDefinedFunction(const std::string& name) const throw();
/**
* Check whether an Expr was bound to a function (i.e., was the
* second arg to bindDefinedFunction()).
*/
bool isBoundDefinedFunction(Expr func) const throw();
/**
* Check whether a name is bound to a type (or type constructor).
*
* @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 type identifier to lookup
* @returns the type bound to <code>name</code> in the current scope.
*/
Type lookupType(const std::string& name) const throw();
/**
* Lookup a bound parameterized type.
*
* @param name the type-constructor identifier to lookup
* @param params the types to use to parameterize the type
* @returns the type bound to <code>name(<i>params</i>)</code> in
* the current scope.
*/
Type lookupType(const std::string& name,
const std::vector<Type>& params) const throw();
/**
* Lookup the arity of a bound parameterized type.
*/
size_t lookupArity(const std::string& name);
/**
* 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>SymbolTable</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();
/** Get the current level of this symbol table. */
size_t getLevel() const throw();
/** Reset everything. */
void reset();
};/* class SymbolTable */
}/* CVC4 namespace */
#endif /* __CVC4__SYMBOL_TABLE_H */
|
