From 0a3ecb598dac9e5e7416f88403dbf73d558c8739 Mon Sep 17 00:00:00 2001 From: "Christopher L. Conway" Date: Sat, 23 Oct 2010 14:49:06 +0000 Subject: [PATCH] Adding Parser::setInput and using it in InteractiveShell (Fixes: #225) Removing ParserBuilder::withStateFrom --- src/main/interactive_shell.cpp | 22 +++++++----- src/main/interactive_shell.h | 15 +++++--- src/main/main.cpp | 15 ++++---- src/parser/input.h | 14 ++++---- src/parser/parser.h | 8 +++++ src/parser/parser_builder.cpp | 65 +++++++--------------------------- src/parser/parser_builder.h | 22 ------------ 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 = ""; + 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 #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 * NULL 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 Expr if there is no - * expression there to parse. + /** Parse an expression from the input by invoking the + * implementation-specific parsing method. Returns a null + * Expr 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 parser is NULL, - * 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); -- 2.30.2