1 /********************* */
2 /*! \file symbol_table.h
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Morgan Deters, Christopher L. Conway
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2021 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
26 #include "base/exception.h"
36 class CVC4_PUBLIC ScopeException
: public Exception
{};
39 * A convenience class for handling scoped declarations. Implements the usual
40 * nested scoping rules for declarations, with separate bindings for expressions
43 class CVC4_PUBLIC SymbolTable
{
45 /** Create a symbol table. */
50 * Bind an expression to a name in the current scope level.
52 * When doOverload is false:
53 * if <code>name</code> is already bound to an expression in the current
54 * level, then the binding is replaced. If <code>name</code> is bound
55 * in a previous level, then the binding is "covered" by this one
56 * until the current scope is popped.
57 * If levelZero is true the name shouldn't be already bound.
59 * When doOverload is true:
60 * if <code>name</code> is already bound to an expression in the current
61 * level, then we mark the previous bound expression and obj as overloaded
64 * @param name an identifier
65 * @param obj the expression to bind to <code>name</code>
66 * @param levelZero set if the binding must be done at level 0
67 * @param doOverload set if the binding can overload the function name.
69 * Returns false if the binding was invalid.
71 bool bind(const std::string
& name
,
73 bool levelZero
= false,
74 bool doOverload
= false);
77 * Bind a type to a name in the current scope. If <code>name</code>
78 * is already bound to a type in the current level, then the binding
79 * is replaced. If <code>name</code> is bound in a previous level,
80 * then the binding is "covered" by this one until the current scope
83 * @param name an identifier
84 * @param t the type to bind to <code>name</code>
85 * @param levelZero set if the binding must be done at level 0
87 void bindType(const std::string
& name
, api::Sort t
, bool levelZero
= false);
90 * Bind a type to a name in the current scope. If <code>name</code>
91 * is already bound to a type or type constructor in the current
92 * level, then the binding is replaced. If <code>name</code> is
93 * bound in a previous level, then the binding is "covered" by this
94 * one until the current scope is popped.
96 * @param name an identifier
97 * @param params the parameters to the type
98 * @param t the type to bind to <code>name</code>
99 * @param levelZero true to bind it globally (default is to bind it
100 * locally within the current scope)
102 void bindType(const std::string
& name
,
103 const std::vector
<api::Sort
>& params
,
105 bool levelZero
= false);
108 * Check whether a name is bound to an expression with bind().
110 * @param name the identifier to check.
111 * @returns true iff name is bound in the current scope.
113 bool isBound(const std::string
& name
) const;
116 * Check whether a name is bound to a type (or type constructor).
118 * @param name the identifier to check.
119 * @returns true iff name is bound to a type in the current scope.
121 bool isBoundType(const std::string
& name
) const;
124 * Lookup a bound expression.
126 * @param name the identifier to lookup
127 * @returns the unique expression bound to <code>name</code> in the current
129 * It returns the null expression if there is not a unique expression bound to
130 * <code>name</code> in the current scope (i.e. if there is not exactly one).
132 api::Term
lookup(const std::string
& name
) const;
135 * Lookup a bound type.
137 * @param name the type identifier to lookup
138 * @returns the type bound to <code>name</code> in the current scope.
140 api::Sort
lookupType(const std::string
& name
) const;
143 * Lookup a bound parameterized type.
145 * @param name the type-constructor identifier to lookup
146 * @param params the types to use to parameterize the type
147 * @returns the type bound to <code>name(<i>params</i>)</code> in
150 api::Sort
lookupType(const std::string
& name
,
151 const std::vector
<api::Sort
>& params
) const;
154 * Lookup the arity of a bound parameterized type.
156 size_t lookupArity(const std::string
& name
);
159 * Pop a scope level, deletes all bindings since the last call to pushScope,
160 * and decreases the level by 1.
162 * @throws ScopeException if the scope level is 0.
166 /** Push a scope level and increase the scope level by 1. */
169 /** Get the current level of this symbol table. */
170 size_t getLevel() const;
172 /** Reset everything. */
174 /** Reset assertions. */
175 void resetAssertions();
177 //------------------------ operator overloading
178 /** is this function overloaded? */
179 bool isOverloadedFunction(api::Term fun
) const;
181 /** Get overloaded constant for type.
182 * If possible, it returns the defined symbol with name
183 * that has type t. Otherwise returns null expression.
185 api::Term
getOverloadedConstantForType(const std::string
& name
,
189 * If possible, returns the unique defined function for a name
190 * that expects arguments with types "argTypes".
191 * For example, if argTypes = (T1, ..., Tn), then this may return an
192 * expression with type function(T1, ..., Tn), or constructor(T1, ...., Tn).
194 * If there is not a unique defined function for the name and argTypes,
195 * this returns the null expression. This can happen either if there are
196 * no functions with name and expected argTypes, or alternatively there is
197 * more than one function with name and expected argTypes.
199 api::Term
getOverloadedFunctionForTypes(
200 const std::string
& name
, const std::vector
<api::Sort
>& argTypes
) const;
201 //------------------------ end operator overloading
204 /** The implementation of the symbol table */
205 class Implementation
;
206 std::unique_ptr
<Implementation
> d_implementation
;
207 }; /* class SymbolTable */
211 #endif /* CVC4__SYMBOL_TABLE_H */