Adding Parser::setInput and using it in InteractiveShell (Fixes: #225)

Removing ParserBuilder::withStateFrom

3 files changed, 32 insertions, 20 deletions

diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index 3d37ade43..587c07495 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -18,6 +18,7 @@
 
 #include "interactive_shell.h"
 #include "expr/command.h"
+#include "parser/input.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
 
@@ -25,6 +26,8 @@ using namespace std;
 
 namespace CVC4 {
 
+const string InteractiveShell::INPUT_FILENAME = "<shell>";
+
 Command* InteractiveShell::readCommand() {
   /* Don't do anything if the input is closed. */
   if( d_in.eof() ) {
@@ -90,23 +93,26 @@ Command* InteractiveShell::readCommand() {
     }
   }
 
-  Parser *parser = 
-    d_parserBuilder
-        .withStringInput(input)
-        .withStateFrom(d_lastParser)
-        .build();
+  d_parser->setInput(Input::newStringInput(d_language,input,INPUT_FILENAME));
+  // Parser *parser = 
+  //   d_parserBuilder
+  //       .withStringInput(input)
+  //       .withStateFrom(d_lastParser)
+  //       .build();
 
   /* There may be more than one command in the input. Build up a
      sequence. */
   CommandSequence *cmd_seq = new CommandSequence();
   Command *cmd;
 
-  while( (cmd = parser->nextCommand()) ) {
+  while( (cmd = d_parser->nextCommand()) ) {
     cmd_seq->addCommand(cmd);
   }
 
-  delete d_lastParser;
-  d_lastParser = parser;
+  // if( d_lastParser ) {
+  //   delete d_lastParser;
+  // }
+  // d_lastParser = parser;
 
   return cmd_seq;
 }
diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h
index 8f207145e..a60278eba 100644
--- a/src/main/interactive_shell.h
+++ b/src/main/interactive_shell.h
@@ -21,6 +21,7 @@
 #include <string>
 
 #include "parser/parser_builder.h"
+#include "util/language.h"
 #include "util/options.h"
 
 namespace CVC4 {
@@ -32,16 +33,20 @@ namespace CVC4 {
 class CVC4_PUBLIC InteractiveShell {
   std::istream& d_in;
   std::ostream& d_out;
-  ParserBuilder d_parserBuilder;
-  Parser* d_lastParser;
+  Parser* d_parser;
+  const InputLanguage d_language;
+
+  static const std::string INPUT_FILENAME;
 
 public:
-  InteractiveShell(ParserBuilder& parserBuilder,
+  InteractiveShell(ExprManager& exprManager,
                   const Options& options) : 
     d_in(*options.in),
     d_out(*options.out),
-    d_parserBuilder(parserBuilder),
-    d_lastParser(NULL) {
+    d_language(options.inputLanguage) {
+    ParserBuilder parserBuilder(exprManager,INPUT_FILENAME,options);
+    /* Create parser with bogus input. */
+    d_parser = parserBuilder.withStringInput("").build();
   }
 
   /** Read a command from the interactive shell. This will read as
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 8bca6190e..7943da0e7 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -229,22 +229,23 @@ int runCvc4(int argc, char* argv[]) {
     Warning.getStream() << Expr::setlanguage(language);
   }
 
-  ParserBuilder parserBuilder =
-    ParserBuilder(exprMgr, filename, options);
-
-  if( inputFromStdin ) {
-    parserBuilder.withStreamInput(cin);
-  }
 
   // Parse and execute commands until we are done
   Command* cmd;
   if( options.interactive ) {
-    InteractiveShell shell(parserBuilder,options);
+    InteractiveShell shell(exprMgr,options);
     while((cmd = shell.readCommand())) {
       doCommand(smt,cmd);
       delete cmd;
     }
   } else {
+    ParserBuilder parserBuilder =
+      ParserBuilder(exprMgr, filename, options);
+
+    if( inputFromStdin ) {
+      parserBuilder.withStreamInput(cin);
+    }
+
     Parser *parser = parserBuilder.build();
     while((cmd = parser->nextCommand())) {
       doCommand(smt, cmd);