Saving state between lines in interactive mode (Fixes: #223)

4 files changed, 27 insertions, 3 deletions

diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index 7af72ed2d..3d37ade43 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -93,6 +93,7 @@ Command* InteractiveShell::readCommand() {
   Parser *parser = 
     d_parserBuilder
         .withStringInput(input)
+        .withStateFrom(d_lastParser)
         .build();
 
   /* There may be more than one command in the input. Build up a
@@ -104,7 +105,9 @@ Command* InteractiveShell::readCommand() {
     cmd_seq->addCommand(cmd);
   }
 
-  delete parser;
+  delete d_lastParser;
+  d_lastParser = parser;
+
   return cmd_seq;
 }
 
diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h
index 66c134ecd..8f207145e 100644
--- a/src/main/interactive_shell.h
+++ b/src/main/interactive_shell.h
@@ -29,17 +29,19 @@ namespace CVC4 {
 
   using namespace parser;
 
-class InteractiveShell {
+class CVC4_PUBLIC InteractiveShell {
   std::istream& d_in;
   std::ostream& d_out;
   ParserBuilder d_parserBuilder;
+  Parser* d_lastParser;
 
 public:
   InteractiveShell(ParserBuilder& parserBuilder,
                   const Options& options) : 
     d_in(*options.in),
     d_out(*options.out),
-    d_parserBuilder(parserBuilder) {
+    d_parserBuilder(parserBuilder),
+    d_lastParser(NULL) {
   }
 
   /** Read a command from the interactive shell. This will read as
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index 348fb6e6d..35f7ee16c 100644
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -83,6 +83,7 @@ ParserBuilder::ParserBuilder(ExprManager& exprManager, const std::string& filena
   d_filename = filename;
   d_streamInput = NULL;
   d_exprManager = exprManager;
+  d_parserToUseForState = NULL;
   d_checksEnabled = true;
   d_strictMode = false;
   d_mmap = false;
@@ -122,6 +123,11 @@ Parser *ParserBuilder::build() throw (InputStreamException,AssertionException) {
     parser->disableChecks();
   }
 
+  if( d_parserToUseForState != NULL ) {
+    parser->d_declScope = d_parserToUseForState->d_declScope;
+    parser->d_logicOperators = d_parserToUseForState->d_logicOperators;
+  }
+
   return parser;
 }
 
@@ -164,6 +170,11 @@ ParserBuilder& ParserBuilder::withOptions(const Options& options) {
       .withStrictMode(options.strictParsing);
   }
 
+ParserBuilder& ParserBuilder::withStateFrom(const Parser* parser) {
+  d_parserToUseForState = parser;
+  return *this;
+}
+
 ParserBuilder& ParserBuilder::withStrictMode(bool flag) {
   d_strictMode = flag;
   return *this;
diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h
index 4e8c06f78..44cb8285e 100644
--- a/src/parser/parser_builder.h
+++ b/src/parser/parser_builder.h
@@ -80,6 +80,9 @@ class CVC4_PUBLIC ParserBuilder {
   /** The expression manager */
   ExprManager& d_exprManager;
 
+  /** Parser to derive the initial state from. */
+  const Parser* d_parserToUseForState;
+
   /** Should semantic checks be enabled during parsing? */
   bool d_checksEnabled;
 
@@ -128,6 +131,11 @@ public:
   /** Derive settings from the given options. */
   ParserBuilder& withOptions(const Options& options);
 
+  /** Copy the state (e.g., variable and type declaration) from
+   * an existing parser. If <code>parser</code> is <code>NULL</code>,
+   * the default initial state will be used. */
+  ParserBuilder& withStateFrom(const Parser* parser);
+
   /** Should the parser use strict mode? (Default: no) */
   ParserBuilder& withStrictMode(bool flag = true);