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

Removing ParserBuilder::withStateFrom

7 files changed, 59 insertions, 102 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);
diff --git a/src/parser/input.h b/src/parser/input.h
index 7cfafe429..8a35480cd 100644
--- a/src/parser/input.h
+++ b/src/parser/input.h
@@ -99,6 +99,8 @@ class CVC4_PUBLIC Input {
   Input(const Input& input) { Unimplemented("Copy constructor for Input."); }
   Input& operator=(const Input& input) { Unimplemented("operator= for Input."); }
 
+public:
+
   /** Create an input for the given file.
     *
     * @param lang the input language
@@ -132,7 +134,6 @@ class CVC4_PUBLIC Input {
                                const std::string& name)
     throw (InputStreamException, AssertionException);
 
-public:
 
   /** Destructor. Frees the input stream and closes the input. */
   virtual ~Input();
@@ -151,8 +152,8 @@ protected:
   /** Retrieve the input stream for this parser. */
   InputStream *getInputStream();
 
-  /** Parse a command from
-   * the input by invoking the implementation-specific parsing method.  Returns
+  /** Parse a command from the input by invoking the
+   * implementation-specific parsing method.  Returns
    * <code>NULL</code> if there is no command there to parse.
    *
    * @throws ParserException if an error is encountered during parsing.
@@ -166,10 +167,9 @@ protected:
   virtual void parseError(const std::string& msg)
     throw (ParserException, AssertionException) = 0;
 
-  /** Parse an
-   * expression from the input by invoking the implementation-specific
-   * parsing method. Returns a null <code>Expr</code> if there is no
-   * expression there to parse.
+  /** Parse an expression from the input by invoking the
+   * implementation-specific parsing method. Returns a null
+   * <code>Expr</code> if there is no expression there to parse.
    *
    * @throws ParserException if an error is encountered during parsing.
    */
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 280bd3c97..ed7db63cf 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -160,6 +160,14 @@ public:
     return d_input;
   }
 
+  /** Deletes and replaces the current parser input. */
+  void setInput(Input* input)  {
+    delete d_input;
+    d_input = input;
+    d_input->setParser(*this);
+    d_done = false;
+  }
+
   /**
    * Check if we are done -- either the end of input has been reached, or some
    * error has been encountered.
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index 7291da1db..2bf0aac31 100644
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -29,67 +29,36 @@ namespace CVC4 {
 
 namespace parser {
 
-/*class FileInputBuilder : public InputBuilder {
-  bool d_useMmap;
-public:
-  FileInputBuilder(InputLanguage lang, const std::string& filename, bool useMmap) :
-    InputBuilder(lang,filename),
-    d_useMmap(useMmap) {
-  }
-  ParserBuilder& useMmap();
-
-  Input& build() {
-    return Input::newFileInput(d_lang,d_name,d_useMmap);
-  }
-};
-
-class StringInputBuilder : public InputBuilder {
-  std::string d_input;
-public:
-  StringInputBuilder(InputLanguage lang, const std::string& input, const std::string& name) :
-    InputBuilder(lang,name),
-    d_input(input) {
-  }
-
-  Input& build() {
-    return Input::newStringInput(lang,input,name);
-  }
-};*/
-
-ParserBuilder::ParserBuilder(ExprManager& exprManager, const std::string& filename)//  :
-    // d_inputType(FILE_INPUT),
-    // d_lang(language::input::LANG_AUTO),
-  : d_filename(filename),
-    // d_streamInput(NULL),
-   d_exprManager(exprManager)
-    // d_checksEnabled(true),
-    // d_strictMode(false),
-    // d_mmap(false)
-{
+ParserBuilder::ParserBuilder(ExprManager& exprManager, 
+                             const std::string& filename) : 
+  d_filename(filename),
+  d_exprManager(exprManager) {
   init(exprManager,filename);
 }
 
-  ParserBuilder::ParserBuilder(ExprManager& exprManager, const std::string& filename, const Options& options) :
+ParserBuilder::ParserBuilder(ExprManager& exprManager, 
+                             const std::string& filename, 
+                             const Options& options) :
   d_filename(filename),
-   d_exprManager(exprManager)
-{
+  d_exprManager(exprManager) {
   init(exprManager,filename);
   withOptions(options);
 }
 
-  void ParserBuilder::init(ExprManager& exprManager, const std::string& filename) {
+void ParserBuilder::init(ExprManager& exprManager, 
+                         const std::string& filename) {
   d_inputType = FILE_INPUT;
   d_lang = language::input::LANG_AUTO;
   d_filename = filename;
   d_streamInput = NULL;
   d_exprManager = exprManager;
-  d_parserToUseForState = NULL;
   d_checksEnabled = true;
   d_strictMode = false;
   d_mmap = false;
 }
 
-Parser *ParserBuilder::build() throw (InputStreamException,AssertionException) {
+Parser *ParserBuilder::build() 
+  throw (InputStreamException,AssertionException) {
   Input *input = NULL;
   switch( d_inputType ) {
   case FILE_INPUT:
@@ -125,11 +94,6 @@ 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;
 }
 
@@ -172,11 +136,6 @@ 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 44cb8285e..f1fd26ec1 100644
--- a/src/parser/parser_builder.h
+++ b/src/parser/parser_builder.h
@@ -34,20 +34,6 @@ class ExprManager;
 
 namespace parser {
 
-/*
-class InputBuilder {
-protected:
-  InputLanguage d_lang;
-  std::string d_name;
-public:
-  InputBuilder(InputLanguage lang, const std::string& name) :
-    d_lang(lang),
-    d_name(name) {
-  }
-  virtual Input& build() = 0;
-};
-*/
-
 class Parser;
 
 /**
@@ -80,9 +66,6 @@ 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;
 
@@ -131,11 +114,6 @@ 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);