src/expr/symbol_table.h

   1 /*********************                                                        */
   2 /*! \file symbol_table.h
   3  ** \verbatim
   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
  11  **
  12  ** \brief Convenience class for scoping variable and type declarations.
  13  **
  14  ** Convenience class for scoping variable and type declarations.
  15  **/
  16
  17 #include "cvc4_public.h"
  18
  19 #ifndef CVC4__SYMBOL_TABLE_H
  20 #define CVC4__SYMBOL_TABLE_H
  21
  22 #include <memory>
  23 #include <string>
  24 #include <vector>
  25
  26 #include "base/exception.h"
  27
  28 namespace CVC4 {
  29
  30 namespace api {
  31 class Solver;
  32 class Sort;
  33 class Term;
  34 }  // namespace api
  35
  36 class CVC4_PUBLIC ScopeException : public Exception {};
  37
  38 /**
  39  * A convenience class for handling scoped declarations. Implements the usual
  40  * nested scoping rules for declarations, with separate bindings for expressions
  41  * and types.
  42  */
  43 class CVC4_PUBLIC SymbolTable {
  44  public:
  45   /** Create a symbol table. */
  46   SymbolTable();
  47   ~SymbolTable();
  48
  49   /**
  50    * Bind an expression to a name in the current scope level.
  51    *
  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.
  58    *
  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
  62    * functions.
  63    *
  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.
  68    *
  69    * Returns false if the binding was invalid.
  70    */
  71   bool bind(const std::string& name,
  72             api::Term obj,
  73             bool levelZero = false,
  74             bool doOverload = false);
  75
  76   /**
  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
  81    * is popped.
  82    *
  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
  86    */
  87   void bindType(const std::string& name, api::Sort t, bool levelZero = false);
  88
  89   /**
  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.
  95    *
  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)
 101    */
 102   void bindType(const std::string& name,
 103                 const std::vector<api::Sort>& params,
 104                 api::Sort t,
 105                 bool levelZero = false);
 106
 107   /**
 108    * Check whether a name is bound to an expression with bind().
 109    *
 110    * @param name the identifier to check.
 111    * @returns true iff name is bound in the current scope.
 112    */
 113   bool isBound(const std::string& name) const;
 114
 115   /**
 116    * Check whether a name is bound to a type (or type constructor).
 117    *
 118    * @param name the identifier to check.
 119    * @returns true iff name is bound to a type in the current scope.
 120    */
 121   bool isBoundType(const std::string& name) const;
 122
 123   /**
 124    * Lookup a bound expression.
 125    *
 126    * @param name the identifier to lookup
 127    * @returns the unique expression bound to <code>name</code> in the current
 128    * scope.
 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).
 131    */
 132   api::Term lookup(const std::string& name) const;
 133
 134   /**
 135    * Lookup a bound type.
 136    *
 137    * @param name the type identifier to lookup
 138    * @returns the type bound to <code>name</code> in the current scope.
 139    */
 140   api::Sort lookupType(const std::string& name) const;
 141
 142   /**
 143    * Lookup a bound parameterized type.
 144    *
 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
 148    * the current scope.
 149    */
 150   api::Sort lookupType(const std::string& name,
 151                        const std::vector<api::Sort>& params) const;
 152
 153   /**
 154    * Lookup the arity of a bound parameterized type.
 155    */
 156   size_t lookupArity(const std::string& name);
 157
 158   /**
 159    * Pop a scope level, deletes all bindings since the last call to pushScope,
 160    * and decreases the level by 1.
 161    *
 162    * @throws ScopeException if the scope level is 0.
 163    */
 164   void popScope();
 165
 166   /** Push a scope level and increase the scope level by 1. */
 167   void pushScope();
 168
 169   /** Get the current level of this symbol table. */
 170   size_t getLevel() const;
 171
 172   /** Reset everything. */
 173   void reset();
 174   /** Reset assertions. */
 175   void resetAssertions();
 176
 177   //------------------------ operator overloading
 178   /** is this function overloaded? */
 179   bool isOverloadedFunction(api::Term fun) const;
 180
 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.
 184   */
 185   api::Term getOverloadedConstantForType(const std::string& name,
 186                                          api::Sort t) const;
 187
 188   /**
 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).
 193    *
 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.
 198    */
 199   api::Term getOverloadedFunctionForTypes(
 200       const std::string& name, const std::vector<api::Sort>& argTypes) const;
 201   //------------------------ end operator overloading
 202
 203  private:
 204   /** The implementation of the symbol table */
 205   class Implementation;
 206   std::unique_ptr<Implementation> d_implementation;
 207 }; /* class SymbolTable */
 208
 209 }  // namespace CVC4
 210
 211 #endif /* CVC4__SYMBOL_TABLE_H */