src/expr/symbol_table.h

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