Some items from the CVC4 public interface review:

* rename DeclarationScope to SymbolTable
* rename all HashStrategy -> HashFunction (which we often have anyways)
* remove CDCircList (no one is currently using it)

1 files changed, 205 insertions, 0 deletions

diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h
new file mode 100644
index 000000000..ee04b17fd
--- /dev/null
+++ b/src/expr/symbol_table.h
@@ -0,0 +1,205 @@
+/*********************                                                        */
+/*! \file symbol_table.h
+ ** \verbatim
+ ** Original author: cconway
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): ajreynol, dejan, bobot
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Convenience class for scoping variable and type declarations.
+ **
+ ** Convenience class for scoping variable and type declarations.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__SYMBOL_TABLE_H
+#define __CVC4__SYMBOL_TABLE_H
+
+#include <vector>
+#include <utility>
+#include <ext/hash_map>
+
+#include "expr/expr.h"
+#include "util/hash.h"
+
+#include "context/cdhashset_forward.h"
+#include "context/cdhashmap_forward.h"
+
+namespace CVC4 {
+
+class Type;
+
+namespace context {
+  class Context;
+}/* CVC4::context namespace */
+
+class CVC4_PUBLIC ScopeException : public Exception {
+};/* class ScopeException */
+
+/**
+ * A convenience class for handling scoped declarations. Implements the usual
+ * nested scoping rules for declarations, with separate bindings for expressions
+ * and types.
+ */
+class CVC4_PUBLIC SymbolTable {
+  /** The context manager for the scope maps. */
+  context::Context* d_context;
+
+  /** A map for expressions. */
+  context::CDHashMap<std::string, Expr, StringHashFunction> *d_exprMap;
+
+  /** A map for types. */
+  context::CDHashMap<std::string, std::pair<std::vector<Type>, Type>, StringHashFunction> *d_typeMap;
+
+  /** A set of defined functions. */
+  context::CDHashSet<Expr, ExprHashFunction> *d_functions;
+
+public:
+  /** Create a declaration scope. */
+  SymbolTable();
+
+  /** Destroy a declaration scope. */
+  ~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
+   * 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.
+   *
+   * @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
+   */
+  void bind(const std::string& name, Expr obj, bool levelZero = false) throw(AssertionException);
+
+  /**
+   * Bind a function body to a name in the current scope.  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).
+   *
+   * @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
+   */
+  void bindDefinedFunction(const std::string& name, Expr obj, bool levelZero = false) throw(AssertionException);
+
+  /**
+   * Bind a type to a name in the current scope.  If <code>name</code>
+   * is already bound to a type 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.
+   *
+   * @param name an identifier
+   * @param t the type to bind to <code>name</code>
+   * @param levelZero set if the binding must be done at level 0
+   */
+  void bindType(const std::string& name, Type t, bool levelZero = false) throw();
+
+  /**
+   * Bind a type to a name in the current scope.  If <code>name</code>
+   * is already bound to a type or type constructor 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.
+   *
+   * @param name an identifier
+   * @param params the parameters to the type
+   * @param t the type to bind to <code>name</code>
+   */
+  void bindType(const std::string& name,
+                const std::vector<Type>& params,
+                Type t, bool levelZero = false) throw();
+
+  /**
+   * Check whether a name is bound to an expression with either bind()
+   * or bindDefinedFunction().
+   *
+   * @param name the identifier to check.
+   * @returns true iff name is bound in the current scope.
+   */
+  bool isBound(const std::string& name) const throw();
+
+  /**
+   * Check whether a name was bound to a function with bindDefinedFunction().
+   */
+  bool isBoundDefinedFunction(const std::string& name) const throw();
+
+  /**
+   * Check whether an Expr was bound to a function (i.e., was the
+   * second arg to bindDefinedFunction()).
+   */
+  bool isBoundDefinedFunction(Expr func) const throw();
+
+  /**
+   * Check whether a name is bound to a type (or type constructor).
+   *
+   * @param name the identifier to check.
+   * @returns true iff name is bound to a type in the current scope.
+   */
+  bool isBoundType(const std::string& name) const throw();
+
+  /**
+   * Lookup a bound expression.
+   *
+   * @param name the identifier to lookup
+   * @returns the expression bound to <code>name</code> in the current scope.
+   */
+  Expr lookup(const std::string& name) const throw(AssertionException);
+
+  /**
+   * Lookup a bound type.
+   *
+   * @param name the type identifier to lookup
+   * @returns the type bound to <code>name</code> in the current scope.
+   */
+  Type lookupType(const std::string& name) const throw(AssertionException);
+
+  /**
+   * Lookup a bound parameterized type.
+   *
+   * @param name the type-constructor identifier to lookup
+   * @param params the types to use to parameterize the type
+   * @returns the type bound to <code>name(<i>params</i>)</code> in
+   * the current scope.
+   */
+  Type lookupType(const std::string& name,
+                  const std::vector<Type>& params) const throw(AssertionException);
+
+  /**
+   * Lookup the arity of a bound parameterized type.
+   */
+  size_t lookupArity(const std::string& name);
+
+  /**
+   * Pop a scope level. Deletes all bindings since the last call to
+   * <code>pushScope</code>. Calls to <code>pushScope</code> and
+   * <code>popScope</code> must be "properly nested." I.e., a call to
+   * <code>popScope</code> is only legal if the number of prior calls to
+   * <code>pushScope</code> on this <code>SymbolTable</code> is strictly
+   * greater than then number of prior calls to <code>popScope</code>. */
+  void popScope() throw(ScopeException);
+
+  /** Push a scope level. */
+  void pushScope() throw();
+
+  /** Get the current level of this declaration scope. */
+  size_t getLevel() const throw();
+
+};/* class SymbolTable */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__SYMBOL_TABLE_H */