Refactoring Input/Parser code to support external manipulation of the parser state.

3 files changed, 30 insertions, 43 deletions

diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index 4539a6d43..cf22c5290 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -50,7 +50,7 @@ options {
 
 @parser::includes {
 #include "expr/command.h"
-#include "parser/parser_state.h"
+#include "parser/parser.h"
 
 namespace CVC4 {
   class Expr;
@@ -61,8 +61,8 @@ namespace CVC4 {
 #include "expr/expr.h"
 #include "expr/kind.h"
 #include "expr/type.h"
-#include "parser/antlr_input.h"
-#include "parser/parser_state.h"
+#include "parser/input.h"
+#include "parser/parser.h"
 #include "util/integer.h"
 #include "util/output.h"
 #include "util/rational.h"
@@ -74,7 +74,7 @@ using namespace CVC4::parser;
 /* These need to be macros so they can refer to the PARSER macro, which will be defined
  * by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */
 #undef PARSER_STATE 
-#define PARSER_STATE ((ParserState*)PARSER->super)
+#define PARSER_STATE ((Parser*)PARSER->super)
 #undef EXPR_MANAGER
 #define EXPR_MANAGER PARSER_STATE->getExprManager()
 #undef MK_EXPR
@@ -85,11 +85,11 @@ using namespace CVC4::parser;
 /**   
  * Sets the logic for the current benchmark. Declares any logic symbols.
  *
- * @param parserState pointer to the current parser state
+ * @param parser the CVC4 Parser object
  * @param name the name of the logic (e.g., QF_UF, AUFLIA)
  */
 void
-setLogic(ParserState *parserState, const std::string& name) {
+setLogic(Parser *parser, const std::string& name) {
   if( name == "QF_UF" ) {
     parserState->mkSort("U");
   } else if(name == "QF_LRA"){
@@ -174,7 +174,7 @@ benchAttribute returns [CVC4::Command* smt_command]
  */
 annotatedFormula[CVC4::Expr& expr]
 @init {
-  Debug("parser") << "annotated formula: " << AntlrInput::tokenText(LT(1)) << std::endl;
+  Debug("parser") << "annotated formula: " << Input::tokenText(LT(1)) << std::endl;
   Kind kind;
   std::string name;
   std::vector<Expr> args; /* = getExprVector(); */
@@ -236,11 +236,11 @@ annotatedFormula[CVC4::Expr& expr]
   | TRUE_TOK          { expr = MK_CONST(true); }
   | FALSE_TOK         { expr = MK_CONST(false); }
   | NUMERAL_TOK
-    { Integer num( AntlrInput::tokenText($NUMERAL_TOK) );
+    { Integer num( Input::tokenText($NUMERAL_TOK) );
       expr = MK_CONST(num); }
   | RATIONAL_TOK
     { // FIXME: This doesn't work because an SMT rational is not a valid GMP rational string
-      Rational rat( AntlrInput::tokenText($RATIONAL_TOK) );
+      Rational rat( Input::tokenText($RATIONAL_TOK) );
       expr = MK_CONST(rat); }
     // NOTE: Theory constants go here
     /* TODO: let, flet, quantifiers, arithmetic constants */
@@ -263,7 +263,7 @@ annotatedFormulas[std::vector<CVC4::Expr>& formulas, CVC4::Expr& expr]
 */
 builtinOp[CVC4::Kind& kind]
 @init {
-  Debug("parser") << "builtin: " << AntlrInput::tokenText(LT(1)) << std::endl;
+  Debug("parser") << "builtin: " << Input::tokenText(LT(1)) << std::endl;
 }
   : NOT_TOK      { $kind = CVC4::kind::NOT;     }
   | IMPLIES_TOK  { $kind = CVC4::kind::IMPLIES; }
@@ -417,7 +417,7 @@ identifier[std::string& id,
 		   CVC4::parser::DeclarationCheck check, 
            CVC4::parser::SymbolType type] 
   : IDENTIFIER
-    { id = AntlrInput::tokenText($IDENTIFIER);
+    { id = Input::tokenText($IDENTIFIER);
       Debug("parser") << "identifier: " << id
                       << " check? " << toString(check)
                       << " type? " << toString(type) << std::endl;
@@ -432,7 +432,7 @@ identifier[std::string& id,
 let_identifier[std::string& id,
     		   CVC4::parser::DeclarationCheck check] 
   : LET_IDENTIFIER
-    { id = AntlrInput::tokenText($LET_IDENTIFIER);
+    { id = Input::tokenText($LET_IDENTIFIER);
       Debug("parser") << "let_identifier: " << id
                       << " check? " << toString(check) << std::endl;
       PARSER_STATE->checkDeclaration(id, check, SYM_VARIABLE); }
@@ -446,7 +446,7 @@ let_identifier[std::string& id,
 flet_identifier[std::string& id,
     		    CVC4::parser::DeclarationCheck check] 
   : FLET_IDENTIFIER
-    { id = AntlrInput::tokenText($FLET_IDENTIFIER);
+    { id = Input::tokenText($FLET_IDENTIFIER);
       Debug("parser") << "flet_identifier: " << id
                       << " check? " << toString(check) << std::endl;
       PARSER_STATE->checkDeclaration(id, check); }
diff --git a/src/parser/smt/smt_input.cpp b/src/parser/smt/smt_input.cpp
index 1bff3d18f..451310cfd 100644
--- a/src/parser/smt/smt_input.cpp
+++ b/src/parser/smt/smt_input.cpp
@@ -15,9 +15,10 @@
 
 #include <antlr3.h>
 
+#include "smt_input.h"
 #include "expr/expr_manager.h"
+#include "parser/parser.h"
 #include "parser/parser_exception.h"
-#include "parser/smt/smt_input.h"
 #include "parser/smt/generated/SmtLexer.h"
 #include "parser/smt/generated/SmtParser.h"
 
@@ -25,20 +26,9 @@ namespace CVC4 {
 namespace parser {
 
 /* Use lookahead=2 */
-SmtInput::SmtInput(ExprManager* exprManager, const std::string& filename,
-                   bool useMmap) :
-  AntlrInput(exprManager, filename, 2, useMmap) {
-  init();
-}
-
-SmtInput::SmtInput(ExprManager* exprManager, const std::string& input,
-                   const std::string& name) :
-  AntlrInput(exprManager, input, name, 2) {
-  init();
-}
-
-void SmtInput::init() {
-  pANTLR3_INPUT_STREAM input = getInputStream();
+SmtInput::SmtInput(AntlrInputStream *inputStream) :
+  Input(inputStream, 2) {
+  pANTLR3_INPUT_STREAM input = inputStream->getAntlr3InputStream();
   AlwaysAssert( input != NULL );
 
   d_pSmtLexer = SmtLexerNew(input);
@@ -46,7 +36,7 @@ void SmtInput::init() {
     throw ParserException("Failed to create SMT lexer.");
   }
 
-  setLexer( d_pSmtLexer->pLexer );
+  setAntlr3Lexer( d_pSmtLexer->pLexer );
 
   pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream();
   AlwaysAssert( tokenStream != NULL );
@@ -56,7 +46,7 @@ void SmtInput::init() {
     throw ParserException("Failed to create SMT parser.");
   }
 
-  setParser(d_pSmtParser->pParser);
+  setAntlr3Parser(d_pSmtParser->pParser);
 }
 
 
@@ -65,11 +55,11 @@ SmtInput::~SmtInput() {
   d_pSmtParser->free(d_pSmtParser);
 }
 
-Command* SmtInput::doParseCommand() throw (ParserException) {
+Command* SmtInput::parseCommand() throw (ParserException) {
   return d_pSmtParser->parseCommand(d_pSmtParser);
 }
 
-Expr SmtInput::doParseExpr() throw (ParserException) {
+Expr SmtInput::parseExpr() throw (ParserException) {
   return d_pSmtParser->parseExpr(d_pSmtParser);
 }
 
diff --git a/src/parser/smt/smt_input.h b/src/parser/smt/smt_input.h
index f93a1bf0d..e9f4d2578 100644
--- a/src/parser/smt/smt_input.h
+++ b/src/parser/smt/smt_input.h
@@ -18,7 +18,7 @@
 #ifndef __CVC4__PARSER__SMT_INPUT_H
 #define __CVC4__PARSER__SMT_INPUT_H
 
-#include "parser/antlr_input.h"
+#include "parser/input.h"
 #include "parser/smt/generated/SmtLexer.h"
 #include "parser/smt/generated/SmtParser.h"
 
@@ -32,7 +32,7 @@ class ExprManager;
 
 namespace parser {
 
-class SmtInput : public AntlrInput {
+class SmtInput : public Input {
 
   /** The ANTLR3 SMT lexer for the input. */
   pSmtLexer d_pSmtLexer;
@@ -43,14 +43,11 @@ class SmtInput : public AntlrInput {
 public:
 
   /**
-   * Create a file input.
+   * Create an input.
    *
-   * @param exprManager the manager to use when building expressions from the input
-   * @param filename the path of the file to read
-   * @param useMmap <code>true</code> if the input should use memory-mapped
-   * I/O; otherwise, the input will use the standard ANTLR3 I/O implementation.
+   * @param inputStream the input stream to use
    */
-  SmtInput(ExprManager* exprManager, const std::string& filename, bool useMmap);
+  SmtInput(AntlrInputStream *inputStream);
 
   /**
    * Create a string input.
@@ -59,7 +56,7 @@ public:
    * @param input the string to read
    * @param name the "filename" to use when reporting errors
    */
-  SmtInput(ExprManager* exprManager, const std::string& input, const std::string& name);
+//  SmtInput(ExprManager* exprManager, const std::string& input, const std::string& name);
 
   /** Destructor. Frees the lexer and the parser. */
   ~SmtInput();
@@ -72,7 +69,7 @@ protected:
    *
    * @throws ParserException if an error is encountered during parsing.
    */
-  Command* doParseCommand() throw(ParserException);
+  Command* parseCommand() throw(ParserException);
 
   /**
    * Parse an expression from the input. Returns a null
@@ -80,7 +77,7 @@ protected:
    *
    * @throws ParserException if an error is encountered during parsing.
    */
-  Expr doParseExpr() throw(ParserException);
+  Expr parseExpr() throw(ParserException);
 
 private: