parser: add some acces function and recover the original nextToken from antlr3

in order to be able to use the stack of streams.

diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index 52d98435eb71ef3a87a005451b6eeb43f5c24276..7336dd0844622d97e21de36dba350a2a4f59f687 100644 (file)
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -312,7 +312,7 @@ void AntlrInput::setAntlr3Lexer(pANTLR3_LEXER pLexer) {
   // Override default lexer error reporting
   d_lexer->rec->reportError = &lexerError;
   // Override default nextToken function, just to prevent exceptions escaping.
-  d_lexer->rec->state->tokSource->nextToken = &nextTokenStr;
+  d_lexer->rec->state->tokSource->nextToken = &nextToken;
 }
 
 void AntlrInput::setParser(Parser& parser) {

diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h
index 10a4b907d145e088d2423b95471718e000d8fdf0..2d468a7d675d2e51f490cb57881dd28280f6a1ff 100644 (file)
--- a/src/parser/antlr_input.h
+++ b/src/parser/antlr_input.h
@@ -130,8 +130,12 @@ class AntlrInput : public Input {
   static void lexerError(pANTLR3_BASE_RECOGNIZER recognizer);
 
   /** Returns the next available lexer token from the current input stream. */
+  /* - auxillary function */
   static pANTLR3_COMMON_TOKEN
   nextTokenStr (pANTLR3_TOKEN_SOURCE toksource);
+  /* - main function */
+  static pANTLR3_COMMON_TOKEN
+  nextToken (pANTLR3_TOKEN_SOURCE toksource);
 
   /* Since we own d_tokenStream and it needs to be freed, we need to prevent
    * copy construction and assignment.
@@ -182,6 +186,9 @@ public:
   /** Retrieve the remaining text in this input. */
   std::string getUnparsedText();
 
+  /** Get the ANTLR3 lexer for this input. */
+  pANTLR3_LEXER getAntlr3Lexer(){ return d_lexer; };
+
 protected:
   /** Create an input. This input takes ownership of the given input stream,
    * and will delete it at destruction time.

diff --git a/src/parser/antlr_input_imports.cpp b/src/parser/antlr_input_imports.cpp
index 870edb92825d1646aa2ff56cfdd14d0177321472..d714c4975a725f847bf14ca48ce141b4d4cb5289 100644 (file)
--- a/src/parser/antlr_input_imports.cpp
+++ b/src/parser/antlr_input_imports.cpp
@@ -372,5 +372,66 @@ AntlrInput::nextTokenStr (pANTLR3_TOKEN_SOURCE toksource)
   }
 }
 
+/* *** CVC4 NOTE ***
+ * This is copied, totaly unmodified, from antlr3lexer.c
+ * in order to use nextTokenStr previously defined.
+ *
+ */
+pANTLR3_COMMON_TOKEN
+AntlrInput::nextToken      (pANTLR3_TOKEN_SOURCE toksource)
+{
+       pANTLR3_COMMON_TOKEN tok;
+
+       // Find the next token in the current stream
+       //
+       tok = nextTokenStr(toksource);
+
+       // If we got to the EOF token then switch to the previous
+       // input stream if there were any and just return the
+       // EOF if there are none. We must check the next token
+       // in any outstanding input stream we pop into the active
+       // role to see if it was sitting at EOF after PUSHing the
+       // stream we just consumed, otherwise we will return EOF
+       // on the reinstalled input stream, when in actual fact
+       // there might be more input streams to POP before the
+       // real EOF of the whole logical inptu stream. Hence we
+       // use a while loop here until we find somethign in the stream
+       // that isn't EOF or we reach the actual end of the last input
+       // stream on the stack.
+       //
+       while   (tok->type == ANTLR3_TOKEN_EOF)
+       {
+               pANTLR3_LEXER   lexer;
+
+               lexer   = (pANTLR3_LEXER)(toksource->super);
+
+               if  (lexer->rec->state->streams != NULL && lexer->rec->state->streams->size(lexer->rec->state->streams) > 0)
+               {
+                       // We have another input stream in the stack so we
+                       // need to revert to it, then resume the loop to check
+                       // it wasn't sitting at EOF itself.
+                       //
+                       lexer->popCharStream(lexer);
+                       tok = nextTokenStr(toksource);
+               }
+               else
+               {
+                       // There were no more streams on the input stack
+                       // so this EOF is the 'real' logical EOF for
+                       // the input stream. So we just exit the loop and 
+                       // return the EOF we have found.
+                       //
+                       break;
+               }
+               
+       }
+
+       // return whatever token we have, which may be EOF
+       //
+       return  tok;
+}
+
+
+
 } // namespace parser
 } // namespace CVC4

diff --git a/src/parser/input.h b/src/parser/input.h
index 92b039edabfa487d51e665fcfc8c32a65f6bbee4..1b8c97713c6517a36322ac60061c5292c9f0264d 100644 (file)
--- a/src/parser/input.h
+++ b/src/parser/input.h
@@ -146,6 +146,11 @@ public:
   /** Get the language that this Input is reading. */
   virtual InputLanguage getLanguage() const throw() = 0;
 
+  /** Retrieve the name of the input stream */
+  const std::string getInputStreamName(){
+    return getInputStream()->getName();
+  }
+
 protected:
 
   /** Create an input.