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

Removing ParserBuilder::withStateFrom

4 files changed, 27 insertions, 82 deletions

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);