diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-03-10 03:58:23 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-03-10 03:58:23 +0000 |
commit | f50d6702ad0ffc5a10308abc2a43f86a9b623a8c (patch) | |
tree | 6f1ce4e5d07b94ab1d9fbfcd5cf6603b0017078b | |
parent | 0cd57d89001a73ea1ebe0d43b2cb720d68cca82a (diff) |
Lexical scoping for let-bound variables (Bug #53)
-rw-r--r-- | src/parser/antlr_parser.cpp | 8 | ||||
-rw-r--r-- | src/parser/antlr_parser.h | 2 | ||||
-rw-r--r-- | src/parser/smt/smt_parser.g | 2 |
3 files changed, 12 insertions, 0 deletions
diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp index cadff04ac..593a89873 100644 --- a/src/parser/antlr_parser.cpp +++ b/src/parser/antlr_parser.cpp @@ -193,6 +193,14 @@ AntlrParser::defineVar(const std::string& name, const Expr& val) { Assert(isDeclared(name)); } +void +AntlrParser::undefineVar(const std::string& name) { + Assert(isDeclared(name)); + d_varSymbolTable.unbindName(name); + Assert(!isDeclared(name)); +} + + const Type* AntlrParser::newSort(const std::string& name) { Debug("parser") << "newSort(" << name << ")" << std::endl; diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h index 5a6beb132..94d919555 100644 --- a/src/parser/antlr_parser.h +++ b/src/parser/antlr_parser.h @@ -254,6 +254,8 @@ protected: /** Create a new variable definition (e.g., from a let binding). */ void defineVar(const std::string& name, const Expr& val); + /** Remove a variable definition (e.g., from a let binding). */ + void undefineVar(const std::string& name); /** Returns a function type over the given domain and range types. */ const Type* functionType(const Type* domain, const Type* range); diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g index c12aa5f7a..d1ac50651 100644 --- a/src/parser/smt/smt_parser.g +++ b/src/parser/smt/smt_parser.g @@ -154,6 +154,7 @@ annotatedFormula returns [CVC4::Expr formula] LPAREN LET LPAREN name=variable[CHECK_UNDECLARED] expr1=annotatedFormula RPAREN { defineVar(name,expr1); } formula=annotatedFormula + { undefineVar(name); } RPAREN | /* An flet binding */ @@ -161,6 +162,7 @@ annotatedFormula returns [CVC4::Expr formula] LPAREN FLET LPAREN name=function_var[CHECK_UNDECLARED] expr1=annotatedFormula RPAREN { defineVar(name,expr1); } formula=annotatedFormula + { undefineVar(name); } RPAREN | /* A non-built-in function application */ |