From b6544992abea751ec48ac0892925d7f04e5cbf10 Mon Sep 17 00:00:00 2001
From: "Christopher L. Conway" <christopherleeconway@gmail.com>
Date: Fri, 2 Apr 2010 20:04:34 +0000
Subject: [PATCH] Overriding ANTLR3 error recovery routine

---
 src/parser/antlr_input.cpp | 42 ++++++++++++++++++++++++++++++++++++++
 src/parser/antlr_input.h   |  7 +++++++
 src/parser/cvc/Cvc.g       |  1 +
 src/parser/smt/Smt.g       |  1 +
 4 files changed, 51 insertions(+)

diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index 0d6f63812..3d9006e04 100644
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -104,6 +104,47 @@ void AntlrInput::parseError(const std::string& message)
                         d_lexer->getCharPositionInLine(d_lexer));
 }
 
+void *
+AntlrInput::recoverFromMismatchedToken(pANTLR3_BASE_RECOGNIZER recognizer,
+                                       ANTLR3_UINT32 ttype,
+                                       pANTLR3_BITSET_LIST follow) {
+
+  pANTLR3_PARSER parser = (pANTLR3_PARSER) (recognizer->super);
+  pANTLR3_INT_STREAM is = parser->tstream->istream;
+  void *matchedSymbol;
+
+
+  // Create an exception if we need one
+  //
+  if(recognizer->state->exception == NULL) {
+    antlr3RecognitionExceptionNew(recognizer);
+  }
+
+  if(recognizer->mismatchIsUnwantedToken(recognizer, is, ttype) == ANTLR3_TRUE) {
+    recognizer->state->exception->type = ANTLR3_UNWANTED_TOKEN_EXCEPTION;
+    recognizer->state->exception->message
+        = (void*)ANTLR3_UNWANTED_TOKEN_EXCEPTION_NAME;
+  }
+
+  if(recognizer->mismatchIsMissingToken(recognizer, is, follow)) {
+    // We can fake the missing token and proceed
+    //
+    matchedSymbol = recognizer->getMissingSymbol(recognizer, is,
+                                                 recognizer->state->exception,
+                                                 ttype, follow);
+    recognizer->state->exception->type = ANTLR3_MISSING_TOKEN_EXCEPTION;
+    recognizer->state->exception->message = (void*)ANTLR3_MISSING_TOKEN_EXCEPTION_NAME;
+    recognizer->state->exception->token = matchedSymbol;
+    recognizer->state->exception->expecting = ttype;
+
+    // Print out the error after we insert so that ANTLRWorks sees the
+    // token in the exception.
+    //
+  }
+  reportError(recognizer);
+  Unreachable("reportError should have thrown exception in AntlrInput::recoverFromMismatchedToken");
+}
+
 void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) {
   pANTLR3_EXCEPTION ex = recognizer->state->exception;
   pANTLR3_UINT8 * tokenNames = recognizer->state->tokenNames;
@@ -310,6 +351,7 @@ void AntlrInput::setParser(pANTLR3_PARSER pParser) {
   // pass it in as an address anyway.
   d_parser->super = getParserState();
   d_parser->rec->reportError = &reportError;
+  d_parser->rec->recoverFromMismatchedToken = &recoverFromMismatchedToken;
 }
 
 
diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h
index dee7c1491..c338c528a 100644
--- a/src/parser/antlr_input.h
+++ b/src/parser/antlr_input.h
@@ -67,6 +67,13 @@ class AntlrInput : public Input {
   /** Turns an ANTLR3 exception into a message for the user and calls <code>parseError</code>. */
   static void reportError(pANTLR3_BASE_RECOGNIZER recognizer);
 
+  /** Collects information from a parse error and calls reportError. Replaces the default
+   * implementation, which tries to recover from the error.
+   */
+  static void *
+  recoverFromMismatchedToken(pANTLR3_BASE_RECOGNIZER recognizer,
+                             ANTLR3_UINT32 ttype, pANTLR3_BITSET_LIST follow);
+
 public:
 
   /** Create a file input.
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 8b8f251ae..428e2432e 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -79,6 +79,7 @@ using namespace CVC4::parser;
 #define MK_CONST EXPR_MANAGER->mkConst
 }
 
+
 /**
  * Parses an expression.
  * @return the parsed expression
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index 93b8560d0..c0b184abf 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -79,6 +79,7 @@ using namespace CVC4::parser;
 #define MK_CONST EXPR_MANAGER->mkConst
 }
 
+
 /**
  * Parses an expression.
  * @return the parsed expression
-- 
2.30.2