diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-09-28 23:58:03 -0500 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2017-09-28 21:58:03 -0700 |
commit | 821a9d90914fca4a13bc29f8ff15fb4220cbd1d4 (patch) | |
tree | 740dfcd00ef961c73029268bd2abd438a186f5f2 /src/expr/symbol_table.h | |
parent | fabc9849e7d9ab31b3622487f74235a065852caf (diff) |
Update symbol table to support operator overloading (#1154)
Diffstat (limited to 'src/expr/symbol_table.h')
-rw-r--r-- | src/expr/symbol_table.h | 77 |
1 files changed, 64 insertions, 13 deletions
diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h index e64488563..b6ca7a76f 100644 --- a/src/expr/symbol_table.h +++ b/src/expr/symbol_table.h @@ -43,33 +43,58 @@ class CVC4_PUBLIC SymbolTable { ~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 + * Bind an expression to a name in the current scope level. + * + * When doOverload is false: + * 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. + * until the current scope is popped. + * If levelZero is true the name shouldn't be already bound. + * + * When doOverload is true: + * if <code>name</code> is already bound to an expression in the current + * level, then we mark the previous bound expression and obj as overloaded + * functions. * * @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 + * @param doOverload set if the binding can overload the function name. + * + * Returns false if the binding was invalid. */ - void bind(const std::string& name, Expr obj, bool levelZero = false) throw(); + bool bind(const std::string& name, Expr obj, bool levelZero = false, + bool doOverload = 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 + * Bind a function body to a name in the current scope. + * + * When doOverload is false: + * 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). + * until the current scope is popped. + * If levelZero is true the name shouldn't be already bound. + * + * When doOverload is true: + * if <code>name</code> is already bound to an expression in the current + * level, then we mark the previous bound expression and obj as overloaded + * functions. + * + * 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 + * @param doOverload set if the binding can overload the function name. + * + * Returns false if the binding was invalid. */ - void bindDefinedFunction(const std::string& name, Expr obj, - bool levelZero = false) throw(); + bool bindDefinedFunction(const std::string& name, Expr obj, + bool levelZero = false, + bool doOverload = false) throw(); /** * Bind a type to a name in the current scope. If <code>name</code> @@ -133,7 +158,9 @@ class CVC4_PUBLIC SymbolTable { * Lookup a bound expression. * * @param name the identifier to lookup - * @returns the expression bound to <code>name</code> in the current scope. + * @returns the unique expression bound to <code>name</code> in the current scope. + * It returns the null expression if there is not a unique expression bound to + * <code>name</code> in the current scope (i.e. if there is not exactly one). */ Expr lookup(const std::string& name) const throw(); @@ -178,7 +205,31 @@ class CVC4_PUBLIC SymbolTable { /** Reset everything. */ void reset(); - + + //------------------------ operator overloading + /** is this function overloaded? */ + bool isOverloadedFunction(Expr fun) const; + + /** Get overloaded constant for type. + * If possible, it returns the defined symbol with name + * that has type t. Otherwise returns null expression. + */ + Expr getOverloadedConstantForType(const std::string& name, Type t) const; + + /** + * If possible, returns the unique defined function for a name + * that expects arguments with types "argTypes". + * For example, if argTypes = ( T1, ..., Tn ), then this may return + * an expression with type function( T1, ..., Tn ), or constructor( T1, ...., Tn ). + * + * If there is not a unique defined function for the name and argTypes, + * this returns the null expression. This can happen either if there are + * no functions with name and expected argTypes, or alternatively there is + * more than one function with name and expected argTypes. + */ + Expr getOverloadedFunctionForTypes(const std::string& name, const std::vector< Type >& argTypes) const; + //------------------------ end operator overloading + private: // Copying and assignment have not yet been implemented. SymbolTable(const SymbolTable&); |