##########################################################################
##         #   The Coq Proof Assistant / The Coq Development Team       ##
##  v      #         Copyright INRIA, CNRS and contributors             ##
## <O___,, # (see version control and CREDITS file for authors & dates) ##
##   \VV/  ###############################################################
##    //   #    This file is distributed under the terms of the         ##
##         #     GNU Lesser General Public License Version 2.1          ##
##         #     (see LICENSE file for the text of the license)         ##
##########################################################################
from .TacticNotationsLexer import TacticNotationsLexer
from .TacticNotationsParser import TacticNotationsParser

from antlr4 import CommonTokenStream, InputStream
from antlr4.error.ErrorListener import ErrorListener

SUBSTITUTIONS = [#("@bindings_list", "{+ (@id := @val) }"),
                 ("@qualid_or_string", "@id|@string")]

class ParseError(Exception):
    def __init__(self, msg):
        super().__init__()
        self.msg = msg

class ExceptionRaisingErrorListener(ErrorListener):
    def syntaxError(self, recognizer, offendingSymbol, line, column, msg, e):
        raise ParseError("{}:{}: {}".format(line, column, msg))

ERROR_LISTENER = ExceptionRaisingErrorListener()

def substitute(notation):
    """Perform common substitutions in the notation string.

    Nested notations quickly became unwieldy in the original ‘…’-based format,
    so they were avoided and replaced by pointers to grammar rules.  With the
    new format, it's usually nicer to remove the indirection.
    """
    for (src, dst) in SUBSTITUTIONS:
        notation = notation.replace(src, dst)
    return notation

def parse(notation):
    """Parse a notation string, optionally reporting errors to `error_listener`.

    :return: An ANTLR AST. Use one of the supplied visitors (or write your own)
             to turn it into useful output.
    """
    substituted = substitute(notation)
    lexer = TacticNotationsLexer(InputStream(substituted))
    parser = TacticNotationsParser(CommonTokenStream(lexer))
    parser.addErrorListener(ERROR_LISTENER)
    return parser.top()

@@ -883,16 +883,443 @@
 Listener
+%0Afrom antlr4.Recognizer import Recognizer%0A%0A# Only print ANTLR version warning once%0Achecked_version = False%0Acheck_version = Recognizer.checkVersion%0Adef checkVersion_once(*args, **kwargs):%0A    global checked_version%0A    if not checked_version:%0A        # Using %22Recognizer.checkVersion%22 would cause endless recursion%0A        check_version(*args, **kwargs)%0A        checked_version = True%0ARecognizer.checkVersion = checkVersion_once
 %0A%0ASUBSTI

Print ANTLR version warning only once.