src/expr/symbol_table.h

   1 /*********************                                                        */
   2 /*! \file symbol_table.h
   3  ** \verbatim
   4  ** Original author: Morgan Deters
   5  ** Major contributors: Christopher L. Conway
   6  ** Minor contributors (to current version): Andrew Reynolds, Dejan Jovanovic, Francois Bobot
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** 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 <vector>
  23 #include <utility>
  24 #include <ext/hash_map>
  25
  26 #include "expr/expr.h"
  27 #include "util/hash.h"
  28
  29 #include "context/cdhashset_forward.h"
  30 #include "context/cdhashmap_forward.h"
  31
  32 namespace CVC4 {
  33
  34 class Type;
  35
  36 namespace context {
  37   class Context;
  38 }/* CVC4::context namespace */
  39
  40 class CVC4_PUBLIC ScopeException : public Exception {
  41 };/* class ScopeException */
  42
  43 /**
  44  * A convenience class for handling scoped declarations. Implements the usual
  45  * nested scoping rules for declarations, with separate bindings for expressions
  46  * and types.
  47  */
  48 class CVC4_PUBLIC SymbolTable {
  49   /** The context manager for the scope maps. */
  50   context::Context* d_context;
  51
  52   /** A map for expressions. */
  53   context::CDHashMap<std::string, Expr, StringHashFunction> *d_exprMap;
  54
  55   /** A map for types. */
  56   context::CDHashMap<std::string, std::pair<std::vector<Type>, Type>, StringHashFunction> *d_typeMap;
  57
  58   /** A set of defined functions. */
  59   context::CDHashSet<Expr, ExprHashFunction> *d_functions;
  60
  61 public:
  62   /** Create a symbol table. */
  63   SymbolTable();
  64
  65   /** Destroy a symbol table. */
  66   ~SymbolTable();
  67
  68   /**
  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.
  75    *
  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
  79    */
  80   void bind(const std::string& name, Expr obj, bool levelZero = false) throw();
  81
  82   /**
  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).
  89    *
  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
  93    */
  94   void bindDefinedFunction(const std::string& name, Expr obj, bool levelZero = false) throw();
  95
  96   /**
  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
 101    * is popped.
 102    *
 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
 106    */
 107   void bindType(const std::string& name, Type t, bool levelZero = false) throw();
 108
 109   /**
 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.
 115    *
 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)
 121    */
 122   void bindType(const std::string& name,
 123                 const std::vector<Type>& params,
 124                 Type t, bool levelZero = false) throw();
 125
 126   /**
 127    * Check whether a name is bound to an expression with either bind()
 128    * or bindDefinedFunction().
 129    *
 130    * @param name the identifier to check.
 131    * @returns true iff name is bound in the current scope.
 132    */
 133   bool isBound(const std::string& name) const throw();
 134
 135   /**
 136    * Check whether a name was bound to a function with bindDefinedFunction().
 137    */
 138   bool isBoundDefinedFunction(const std::string& name) const throw();
 139
 140   /**
 141    * Check whether an Expr was bound to a function (i.e., was the
 142    * second arg to bindDefinedFunction()).
 143    */
 144   bool isBoundDefinedFunction(Expr func) const throw();
 145
 146   /**
 147    * Check whether a name is bound to a type (or type constructor).
 148    *
 149    * @param name the identifier to check.
 150    * @returns true iff name is bound to a type in the current scope.
 151    */
 152   bool isBoundType(const std::string& name) const throw();
 153
 154   /**
 155    * Lookup a bound expression.
 156    *
 157    * @param name the identifier to lookup
 158    * @returns the expression bound to <code>name</code> in the current scope.
 159    */
 160   Expr lookup(const std::string& name) const throw();
 161
 162   /**
 163    * Lookup a bound type.
 164    *
 165    * @param name the type identifier to lookup
 166    * @returns the type bound to <code>name</code> in the current scope.
 167    */
 168   Type lookupType(const std::string& name) const throw();
 169
 170   /**
 171    * Lookup a bound parameterized type.
 172    *
 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
 176    * the current scope.
 177    */
 178   Type lookupType(const std::string& name,
 179                   const std::vector<Type>& params) const throw();
 180
 181   /**
 182    * Lookup the arity of a bound parameterized type.
 183    */
 184   size_t lookupArity(const std::string& name);
 185
 186   /**
 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);
 194
 195   /** Push a scope level. */
 196   void pushScope() throw();
 197
 198   /** Get the current level of this symbol table. */
 199   size_t getLevel() const throw();
 200
 201   /** Reset everything. */
 202   void reset();
 203
 204 };/* class SymbolTable */
 205
 206 }/* CVC4 namespace */
 207
 208 #endif /* __CVC4__SYMBOL_TABLE_H */