1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
|
##########################################################################
## # 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
from antlr4.Recognizer import Recognizer
# Only print ANTLR version warning once
checked_version = False
check_version = Recognizer.checkVersion
def checkVersion_once(*args, **kwargs):
global checked_version
if not checked_version:
# Using "Recognizer.checkVersion" would cause endless recursion
check_version(*args, **kwargs)
checked_version = True
Recognizer.checkVersion = checkVersion_once
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()
|
