Merging from branches/decl-scopes (r401:411)

3 files changed, 23 insertions, 14 deletions

diff --git a/src/parser/parser_state.cpp b/src/parser/parser_state.cpp
index 6cc8f6d9c..5f07b16b7 100644
--- a/src/parser/parser_state.cpp
+++ b/src/parser/parser_state.cpp
@@ -50,7 +50,7 @@ Expr ParserState::getSymbol(const std::string& name, SymbolType type) {
   switch( type ) {
 
   case SYM_VARIABLE: // Functions share var namespace
-    return d_varTable.getObject(name);
+    return d_declScope.lookup(name);
 
   default:
     Unhandled(type);
@@ -72,7 +72,7 @@ ParserState::getType(const std::string& var_name,
 
 Type* ParserState::getSort(const std::string& name) {
   Assert( isDeclared(name, SYM_SORT) );
-  Type* t = d_sortTable.getObject(name);
+  Type *t = d_declScope.lookupType(name);
   return t;
 }
 
@@ -112,16 +112,18 @@ ParserState::mkVars(const std::vector<std::string> names,
 void
 ParserState::defineVar(const std::string& name, const Expr& val) {
   Assert(!isDeclared(name));
-  d_varTable.bindName(name,val);
+  d_declScope.bind(name,val);
   Assert(isDeclared(name));
 }
 
+/*
 void
 ParserState::undefineVar(const std::string& name) {
   Assert(isDeclared(name));
-  d_varTable.unbindName(name);
+  d_declScope.unbind(name);
   Assert(!isDeclared(name));
 }
+*/
 
 void
 ParserState::setLogic(const std::string& name) {
@@ -137,7 +139,7 @@ ParserState::mkSort(const std::string& name) {
   Debug("parser") << "newSort(" << name << ")" << std::endl;
   Assert( !isDeclared(name, SYM_SORT) ) ;
   Type* type = d_exprManager->mkSort(name);
-  d_sortTable.bindName(name, type);
+  d_declScope.bindType(name, type);
   Assert( isDeclared(name, SYM_SORT) ) ;
   return type;
 }
@@ -154,9 +156,9 @@ ParserState::mkSorts(const std::vector<std::string>& names) {
 bool ParserState::isDeclared(const std::string& name, SymbolType type) {
   switch(type) {
   case SYM_VARIABLE:
-    return d_varTable.isBound(name);
+    return d_declScope.isBound(name);
   case SYM_SORT:
-    return d_sortTable.isBound(name);
+    return d_declScope.isBoundType(name);
   default:
     Unhandled(type);
   }
diff --git a/src/parser/parser_state.h b/src/parser/parser_state.h
index 3e0771070..de624e3a0 100644
--- a/src/parser/parser_state.h
+++ b/src/parser/parser_state.h
@@ -20,6 +20,7 @@
 
 #include <string>
 
+#include "expr/declaration_scope.h"
 #include "expr/expr.h"
 #include "expr/kind.h"
 #include "parser/input.h"
@@ -96,11 +97,8 @@ class ParserState {
   /** The input that we're parsing. */
   Input *d_input;
 
-  /** The symbol table lookup */
-  SymbolTable<Expr> d_varTable;
-
-  /** The sort table */
-  SymbolTable<Type*> d_sortTable;
+  /** The symbol table */
+  DeclarationScope d_declScope;
 
   /** The name of the input file. */
   std::string d_filename;
@@ -128,6 +126,12 @@ public:
     return d_input;
   }
 
+  /** Set the declaration scope manager for this input. NOTE: This should <em>only</me> be
+   * called before parsing begins. Otherwise, previous declarations will be lost. */
+  inline void setDeclarationScope(DeclarationScope declScope) {
+    d_declScope = declScope;
+  }
+
   /**
    * Check if we are done -- either the end of input has been reached, or some
    * error has been encountered.
@@ -251,6 +255,8 @@ public:
     d_input->parseError(msg);
   }
 
+  inline void pushScope() { d_declScope.pushScope(); }
+  inline void popScope() { d_declScope.popScope(); }
 }; // class ParserState
 
 } // namespace parser
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index 160bd321f..25c2fbc89 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -198,10 +198,11 @@ annotatedFormula[CVC4::Expr& expr]
     (LET_TOK LPAREN_TOK let_identifier[name,CHECK_UNDECLARED]
       | FLET_TOK LPAREN_TOK flet_identifier[name,CHECK_UNDECLARED] )
     annotatedFormula[expr] RPAREN_TOK
-    { PARSER_STATE->defineVar(name,expr); }
+    { PARSER_STATE->pushScope();
+      PARSER_STATE->defineVar(name,expr); }
     annotatedFormula[expr]
     RPAREN_TOK
-    { PARSER_STATE->undefineVar(name); }
+    { PARSER_STATE->popScope(); }
 
   | /* a variable */
     ( identifier[name,CHECK_DECLARED,SYM_VARIABLE]