diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-10-20 20:41:03 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-10-20 20:41:03 +0000 |
commit | 93e8bc35db891c6041f9690366be933433a0ad52 (patch) | |
tree | e946c0824d6d91c44ecc97a627411e5d6c334ea9 /src/parser | |
parent | daad722774087de1cf35714868d3762b3ea7cb21 (diff) |
Adding support for interactive mode
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/antlr_input.h | 10 | ||||
-rw-r--r-- | src/parser/antlr_input_imports.cpp | 17 | ||||
-rw-r--r-- | src/parser/input.h | 9 | ||||
-rw-r--r-- | src/parser/parser.h | 9 | ||||
-rw-r--r-- | src/parser/parser_builder.cpp | 38 |
5 files changed, 33 insertions, 50 deletions
diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h index e55e07efd..d86a18004 100644 --- a/src/parser/antlr_input.h +++ b/src/parser/antlr_input.h @@ -180,6 +180,8 @@ public: /** Get a bitvector constant from the text of the number and the size token */ static BitVector tokenToBitvector(pANTLR3_COMMON_TOKEN number, pANTLR3_COMMON_TOKEN size); + std::string getUnparsedText(); + protected: /** Create an input. This input takes ownership of the given input stream, * and will delete it at destruction time. @@ -210,6 +212,14 @@ protected: virtual void setParser(Parser& parser); }; +inline std::string AntlrInput::getUnparsedText() { + const char *base = (const char *)d_antlr3InputStream->data; + const char *cur = (const char *)d_antlr3InputStream->nextChar; + + return std::string(cur, d_antlr3InputStream->sizeBuf - (cur - base)); +} + + inline std::string AntlrInput::tokenText(pANTLR3_COMMON_TOKEN token) { ANTLR3_MARKER start = token->getStartIndex(token); ANTLR3_MARKER end = token->getStopIndex(token); diff --git a/src/parser/antlr_input_imports.cpp b/src/parser/antlr_input_imports.cpp index a1ebee523..2805d518a 100644 --- a/src/parser/antlr_input_imports.cpp +++ b/src/parser/antlr_input_imports.cpp @@ -56,6 +56,7 @@ #include "antlr_input.h" #include "parser.h" +#include "parser_exception.h" #include "util/Assert.h" using namespace std; @@ -89,6 +90,14 @@ void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) { pANTLR3_UINT8 * tokenNames = recognizer->state->tokenNames; stringstream ss; + // Dig the CVC4 objects out of the ANTLR3 mess + pANTLR3_PARSER antlr3Parser = (pANTLR3_PARSER)(recognizer->super); + AlwaysAssert(antlr3Parser!=NULL); + Parser *parser = (Parser*)(antlr3Parser->super); + AlwaysAssert(parser!=NULL); + AntlrInput *input = (AntlrInput*) parser->getInput() ; + AlwaysAssert(input!=NULL); + // Signal we are in error recovery now recognizer->state->errorRecovery = ANTLR3_TRUE; @@ -252,14 +261,6 @@ void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) { break; } - // Now get ready to throw an exception - pANTLR3_PARSER antlr3Parser = (pANTLR3_PARSER)(recognizer->super); - AlwaysAssert(antlr3Parser!=NULL); - Parser *parser = (Parser*)(antlr3Parser->super); - AlwaysAssert(parser!=NULL); - AntlrInput *input = (AntlrInput*) parser->getInput() ; - AlwaysAssert(input!=NULL); - // Call the error display routine input->parseError(ss.str()); } diff --git a/src/parser/input.h b/src/parser/input.h index 1a90a4191..7cfafe429 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -47,7 +47,7 @@ public: virtual ~InputStreamException() throw() { } }; -/** Wrapper around an ANTLR3 input stream. */ +/** Wrapper around an input stream. */ class InputStream { /** The name of this input stream. */ @@ -93,7 +93,7 @@ class CVC4_PUBLIC Input { /** The input stream. */ InputStream *d_inputStream; - /* Since we own d_tokenStream and it needs to be freed, we need to prevent + /* Since we own d_inputStream and it needs to be freed, we need to prevent * copy construction and assignment. */ Input(const Input& input) { Unimplemented("Copy constructor for Input."); } @@ -134,9 +134,12 @@ class CVC4_PUBLIC Input { public: - /** Destructor. Frees the token stream and closes the input. */ + /** Destructor. Frees the input stream and closes the input. */ virtual ~Input(); + /** Retrieve the remaining text in this input. */ + virtual std::string getUnparsedText() = 0; + protected: /** Create an input. diff --git a/src/parser/parser.h b/src/parser/parser.h index 4d1e64176..280bd3c97 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -160,12 +160,6 @@ public: return d_input; } - /** Set the declaration scope manager for this input. NOTE: This should <em>only</me> be - * called before parsing begins. Otherwise, previous declarations will be lost. */ -/* inline void setDeclarationScope(DeclarationScope declScope) { - d_declScope = declScope; - }*/ - /** * Check if we are done -- either the end of input has been reached, or some * error has been encountered. @@ -189,7 +183,8 @@ public: /** Enable strict parsing, according to the language standards. */ void enableStrictMode() { d_strictMode = true; } - /** Disable strict parsing. Allows certain syntactic infelicities to pass without comment. */ + /** Disable strict parsing. Allows certain syntactic infelicities to + pass without comment. */ void disableStrictMode() { d_strictMode = false; } bool strictModeEnabled() { return d_strictMode; } diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index f53d7cc9c..dcc052c3a 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -84,46 +84,20 @@ Parser *ParserBuilder::build() throw (InputStreamException,AssertionException) { default: Unreachable(); } + + Parser *parser = NULL; switch(d_lang) { case language::input::LANG_SMTLIB: - return new Smt(&d_exprManager, input, d_strictMode); + parser = new Smt(&d_exprManager, input, d_strictMode); case language::input::LANG_SMTLIB_V2: - return new Smt2(&d_exprManager, input, d_strictMode); + parser = new Smt2(&d_exprManager, input, d_strictMode); default: - return new Parser(&d_exprManager, input, d_strictMode); + parser = new Parser(&d_exprManager, input, d_strictMode); } -} - -/*ParserBuilder& ParserBuilder::disableChecks() { - d_checksEnabled = false; - return *this; -} -ParserBuilder& ParserBuilder::disableMmap() { - d_mmap = false; - return *this; -} - -ParserBuilder& ParserBuilder::disableStrictMode() { - d_strictMode = false; - return *this; + return parser; } -ParserBuilder& ParserBuilder::enableChecks() { - d_checksEnabled = true; - return *this; -} - -ParserBuilder& ParserBuilder::enableMmap() { - d_mmap = true; - return *this; -} - -ParserBuilder& ParserBuilder::enableStrictMode() { - d_strictMode = true; - return *this; -}*/ - ParserBuilder& ParserBuilder::withChecks(bool flag) { d_checksEnabled = flag; return *this; |