From: François Bobot <francois@bobot.eu>
Date: Fri, 22 Jun 2012 15:11:21 +0000 (+0000)
Subject: parser: add some acces function and recover the original nextToken from antlr3
X-Git-Tag: cvc5-1.0.0~7964
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=eda7d4df5481030d4e9cb6ef4a33d52afc8f7e0a;p=cvc5.git

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 52d98435e..7336dd084 100644
--- 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 10a4b907d..2d468a7d6 100644
--- 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 870edb928..d714c4975 100644
--- 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 92b039eda..1b8c97713 100644
--- 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.