aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/tools/coqrst/notations/TacticNotationsParser.py
diff options
context:
space:
mode:
Diffstat (limited to 'doc/tools/coqrst/notations/TacticNotationsParser.py')
-rw-r--r--doc/tools/coqrst/notations/TacticNotationsParser.py181
1 files changed, 115 insertions, 66 deletions
diff --git a/doc/tools/coqrst/notations/TacticNotationsParser.py b/doc/tools/coqrst/notations/TacticNotationsParser.py
index 357902ddb..c7e28af52 100644
--- a/doc/tools/coqrst/notations/TacticNotationsParser.py
+++ b/doc/tools/coqrst/notations/TacticNotationsParser.py
@@ -7,28 +7,29 @@ import sys
def serializedATN():
with StringIO() as buf:
- buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\3\b")
- buf.write("A\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7\4\b")
- buf.write("\t\b\4\t\t\t\3\2\3\2\3\2\3\3\3\3\5\3\30\n\3\3\3\7\3\33")
- buf.write("\n\3\f\3\16\3\36\13\3\3\4\3\4\3\4\3\4\5\4$\n\4\3\5\3\5")
- buf.write("\5\5(\n\5\3\5\3\5\3\5\5\5-\n\5\3\5\3\5\3\6\3\6\5\6\63")
- buf.write("\n\6\3\6\3\6\5\6\67\n\6\3\6\3\6\3\7\3\7\3\b\3\b\3\t\3")
- buf.write("\t\3\t\2\2\n\2\4\6\b\n\f\16\20\2\2\2A\2\22\3\2\2\2\4\25")
- buf.write("\3\2\2\2\6#\3\2\2\2\b%\3\2\2\2\n\60\3\2\2\2\f:\3\2\2\2")
- buf.write("\16<\3\2\2\2\20>\3\2\2\2\22\23\5\4\3\2\23\24\7\2\2\3\24")
- buf.write("\3\3\2\2\2\25\34\5\6\4\2\26\30\5\f\7\2\27\26\3\2\2\2\27")
- buf.write("\30\3\2\2\2\30\31\3\2\2\2\31\33\5\6\4\2\32\27\3\2\2\2")
- buf.write("\33\36\3\2\2\2\34\32\3\2\2\2\34\35\3\2\2\2\35\5\3\2\2")
- buf.write("\2\36\34\3\2\2\2\37$\5\16\b\2 $\5\20\t\2!$\5\b\5\2\"$")
- buf.write("\5\n\6\2#\37\3\2\2\2# \3\2\2\2#!\3\2\2\2#\"\3\2\2\2$\7")
- buf.write("\3\2\2\2%\'\7\3\2\2&(\7\6\2\2\'&\3\2\2\2\'(\3\2\2\2()")
- buf.write("\3\2\2\2)*\7\b\2\2*,\5\4\3\2+-\7\b\2\2,+\3\2\2\2,-\3\2")
- buf.write("\2\2-.\3\2\2\2./\7\5\2\2/\t\3\2\2\2\60\62\7\4\2\2\61\63")
- buf.write("\5\f\7\2\62\61\3\2\2\2\62\63\3\2\2\2\63\64\3\2\2\2\64")
- buf.write("\66\5\4\3\2\65\67\5\f\7\2\66\65\3\2\2\2\66\67\3\2\2\2")
- buf.write("\678\3\2\2\289\7\5\2\29\13\3\2\2\2:;\7\b\2\2;\r\3\2\2")
- buf.write("\2<=\7\6\2\2=\17\3\2\2\2>?\7\7\2\2?\21\3\2\2\2\t\27\34")
- buf.write("#\',\62\66")
+ buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\3\t")
+ buf.write("F\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7\4\b")
+ buf.write("\t\b\4\t\t\t\4\n\t\n\3\2\3\2\3\2\3\3\3\3\5\3\32\n\3\3")
+ buf.write("\3\7\3\35\n\3\f\3\16\3 \13\3\3\4\3\4\3\4\3\4\3\4\5\4\'")
+ buf.write("\n\4\3\5\3\5\5\5+\n\5\3\5\3\5\3\5\5\5\60\n\5\3\5\3\5\3")
+ buf.write("\6\3\6\5\6\66\n\6\3\6\3\6\5\6:\n\6\3\6\3\6\3\7\3\7\3\b")
+ buf.write("\3\b\3\t\3\t\3\n\3\n\3\n\2\2\13\2\4\6\b\n\f\16\20\22\2")
+ buf.write("\2\2F\2\24\3\2\2\2\4\27\3\2\2\2\6&\3\2\2\2\b(\3\2\2\2")
+ buf.write("\n\63\3\2\2\2\f=\3\2\2\2\16?\3\2\2\2\20A\3\2\2\2\22C\3")
+ buf.write("\2\2\2\24\25\5\4\3\2\25\26\7\2\2\3\26\3\3\2\2\2\27\36")
+ buf.write("\5\6\4\2\30\32\5\f\7\2\31\30\3\2\2\2\31\32\3\2\2\2\32")
+ buf.write("\33\3\2\2\2\33\35\5\6\4\2\34\31\3\2\2\2\35 \3\2\2\2\36")
+ buf.write("\34\3\2\2\2\36\37\3\2\2\2\37\5\3\2\2\2 \36\3\2\2\2!\'")
+ buf.write("\5\20\t\2\"\'\5\16\b\2#\'\5\22\n\2$\'\5\b\5\2%\'\5\n\6")
+ buf.write("\2&!\3\2\2\2&\"\3\2\2\2&#\3\2\2\2&$\3\2\2\2&%\3\2\2\2")
+ buf.write("\'\7\3\2\2\2(*\7\3\2\2)+\7\7\2\2*)\3\2\2\2*+\3\2\2\2+")
+ buf.write(",\3\2\2\2,-\7\t\2\2-/\5\4\3\2.\60\7\t\2\2/.\3\2\2\2/\60")
+ buf.write("\3\2\2\2\60\61\3\2\2\2\61\62\7\5\2\2\62\t\3\2\2\2\63\65")
+ buf.write("\7\4\2\2\64\66\5\f\7\2\65\64\3\2\2\2\65\66\3\2\2\2\66")
+ buf.write("\67\3\2\2\2\679\5\4\3\28:\5\f\7\298\3\2\2\29:\3\2\2\2")
+ buf.write(":;\3\2\2\2;<\7\5\2\2<\13\3\2\2\2=>\7\t\2\2>\r\3\2\2\2")
+ buf.write("?@\7\6\2\2@\17\3\2\2\2AB\7\7\2\2B\21\3\2\2\2CD\7\b\2\2")
+ buf.write("D\23\3\2\2\2\t\31\36&*/\659")
return buf.getvalue()
@@ -44,8 +45,8 @@ class TacticNotationsParser ( Parser ):
literalNames = [ "<INVALID>", "<INVALID>", "'{'", "'}'" ]
- symbolicNames = [ "<INVALID>", "LGROUP", "LBRACE", "RBRACE", "ATOM",
- "ID", "WHITESPACE" ]
+ symbolicNames = [ "<INVALID>", "LGROUP", "LBRACE", "RBRACE", "METACHAR",
+ "ATOM", "ID", "WHITESPACE" ]
RULE_top = 0
RULE_blocks = 1
@@ -53,19 +54,21 @@ class TacticNotationsParser ( Parser ):
RULE_repeat = 3
RULE_curlies = 4
RULE_whitespace = 5
- RULE_atomic = 6
- RULE_hole = 7
+ RULE_meta = 6
+ RULE_atomic = 7
+ RULE_hole = 8
ruleNames = [ "top", "blocks", "block", "repeat", "curlies", "whitespace",
- "atomic", "hole" ]
+ "meta", "atomic", "hole" ]
EOF = Token.EOF
LGROUP=1
LBRACE=2
RBRACE=3
- ATOM=4
- ID=5
- WHITESPACE=6
+ METACHAR=4
+ ATOM=5
+ ID=6
+ WHITESPACE=7
def __init__(self, input:TokenStream, output:TextIO = sys.stdout):
super().__init__(input, output)
@@ -106,9 +109,9 @@ class TacticNotationsParser ( Parser ):
self.enterRule(localctx, 0, self.RULE_top)
try:
self.enterOuterAlt(localctx, 1)
- self.state = 16
+ self.state = 18
self.blocks()
- self.state = 17
+ self.state = 19
self.match(TacticNotationsParser.EOF)
except RecognitionException as re:
localctx.exception = re
@@ -157,24 +160,24 @@ class TacticNotationsParser ( Parser ):
self._la = 0 # Token type
try:
self.enterOuterAlt(localctx, 1)
- self.state = 19
+ self.state = 21
self.block()
- self.state = 26
+ self.state = 28
self._errHandler.sync(self)
_alt = self._interp.adaptivePredict(self._input,1,self._ctx)
while _alt!=2 and _alt!=ATN.INVALID_ALT_NUMBER:
if _alt==1:
- self.state = 21
+ self.state = 23
self._errHandler.sync(self)
_la = self._input.LA(1)
if _la==TacticNotationsParser.WHITESPACE:
- self.state = 20
+ self.state = 22
self.whitespace()
- self.state = 23
+ self.state = 25
self.block()
- self.state = 28
+ self.state = 30
self._errHandler.sync(self)
_alt = self._interp.adaptivePredict(self._input,1,self._ctx)
@@ -196,6 +199,10 @@ class TacticNotationsParser ( Parser ):
return self.getTypedRuleContext(TacticNotationsParser.AtomicContext,0)
+ def meta(self):
+ return self.getTypedRuleContext(TacticNotationsParser.MetaContext,0)
+
+
def hole(self):
return self.getTypedRuleContext(TacticNotationsParser.HoleContext,0)
@@ -225,27 +232,32 @@ class TacticNotationsParser ( Parser ):
localctx = TacticNotationsParser.BlockContext(self, self._ctx, self.state)
self.enterRule(localctx, 4, self.RULE_block)
try:
- self.state = 33
+ self.state = 36
self._errHandler.sync(self)
token = self._input.LA(1)
if token in [TacticNotationsParser.ATOM]:
self.enterOuterAlt(localctx, 1)
- self.state = 29
+ self.state = 31
self.atomic()
pass
- elif token in [TacticNotationsParser.ID]:
+ elif token in [TacticNotationsParser.METACHAR]:
self.enterOuterAlt(localctx, 2)
- self.state = 30
+ self.state = 32
+ self.meta()
+ pass
+ elif token in [TacticNotationsParser.ID]:
+ self.enterOuterAlt(localctx, 3)
+ self.state = 33
self.hole()
pass
elif token in [TacticNotationsParser.LGROUP]:
- self.enterOuterAlt(localctx, 3)
- self.state = 31
+ self.enterOuterAlt(localctx, 4)
+ self.state = 34
self.repeat()
pass
elif token in [TacticNotationsParser.LBRACE]:
- self.enterOuterAlt(localctx, 4)
- self.state = 32
+ self.enterOuterAlt(localctx, 5)
+ self.state = 35
self.curlies()
pass
else:
@@ -303,29 +315,29 @@ class TacticNotationsParser ( Parser ):
self._la = 0 # Token type
try:
self.enterOuterAlt(localctx, 1)
- self.state = 35
+ self.state = 38
self.match(TacticNotationsParser.LGROUP)
- self.state = 37
+ self.state = 40
self._errHandler.sync(self)
_la = self._input.LA(1)
if _la==TacticNotationsParser.ATOM:
- self.state = 36
+ self.state = 39
self.match(TacticNotationsParser.ATOM)
- self.state = 39
+ self.state = 42
self.match(TacticNotationsParser.WHITESPACE)
- self.state = 40
+ self.state = 43
self.blocks()
- self.state = 42
+ self.state = 45
self._errHandler.sync(self)
_la = self._input.LA(1)
if _la==TacticNotationsParser.WHITESPACE:
- self.state = 41
+ self.state = 44
self.match(TacticNotationsParser.WHITESPACE)
- self.state = 44
+ self.state = 47
self.match(TacticNotationsParser.RBRACE)
except RecognitionException as re:
localctx.exception = re
@@ -377,27 +389,27 @@ class TacticNotationsParser ( Parser ):
self._la = 0 # Token type
try:
self.enterOuterAlt(localctx, 1)
- self.state = 46
+ self.state = 49
self.match(TacticNotationsParser.LBRACE)
- self.state = 48
+ self.state = 51
self._errHandler.sync(self)
_la = self._input.LA(1)
if _la==TacticNotationsParser.WHITESPACE:
- self.state = 47
+ self.state = 50
self.whitespace()
- self.state = 50
+ self.state = 53
self.blocks()
- self.state = 52
+ self.state = 55
self._errHandler.sync(self)
_la = self._input.LA(1)
if _la==TacticNotationsParser.WHITESPACE:
- self.state = 51
+ self.state = 54
self.whitespace()
- self.state = 54
+ self.state = 57
self.match(TacticNotationsParser.RBRACE)
except RecognitionException as re:
localctx.exception = re
@@ -434,7 +446,7 @@ class TacticNotationsParser ( Parser ):
self.enterRule(localctx, 10, self.RULE_whitespace)
try:
self.enterOuterAlt(localctx, 1)
- self.state = 56
+ self.state = 59
self.match(TacticNotationsParser.WHITESPACE)
except RecognitionException as re:
localctx.exception = re
@@ -444,6 +456,43 @@ class TacticNotationsParser ( Parser ):
self.exitRule()
return localctx
+ class MetaContext(ParserRuleContext):
+
+ def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1):
+ super().__init__(parent, invokingState)
+ self.parser = parser
+
+ def METACHAR(self):
+ return self.getToken(TacticNotationsParser.METACHAR, 0)
+
+ def getRuleIndex(self):
+ return TacticNotationsParser.RULE_meta
+
+ def accept(self, visitor:ParseTreeVisitor):
+ if hasattr( visitor, "visitMeta" ):
+ return visitor.visitMeta(self)
+ else:
+ return visitor.visitChildren(self)
+
+
+
+
+ def meta(self):
+
+ localctx = TacticNotationsParser.MetaContext(self, self._ctx, self.state)
+ self.enterRule(localctx, 12, self.RULE_meta)
+ try:
+ self.enterOuterAlt(localctx, 1)
+ self.state = 61
+ self.match(TacticNotationsParser.METACHAR)
+ except RecognitionException as re:
+ localctx.exception = re
+ self._errHandler.reportError(self, re)
+ self._errHandler.recover(self, re)
+ finally:
+ self.exitRule()
+ return localctx
+
class AtomicContext(ParserRuleContext):
def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1):
@@ -468,10 +517,10 @@ class TacticNotationsParser ( Parser ):
def atomic(self):
localctx = TacticNotationsParser.AtomicContext(self, self._ctx, self.state)
- self.enterRule(localctx, 12, self.RULE_atomic)
+ self.enterRule(localctx, 14, self.RULE_atomic)
try:
self.enterOuterAlt(localctx, 1)
- self.state = 58
+ self.state = 63
self.match(TacticNotationsParser.ATOM)
except RecognitionException as re:
localctx.exception = re
@@ -505,10 +554,10 @@ class TacticNotationsParser ( Parser ):
def hole(self):
localctx = TacticNotationsParser.HoleContext(self, self._ctx, self.state)
- self.enterRule(localctx, 14, self.RULE_hole)
+ self.enterRule(localctx, 16, self.RULE_hole)
try:
self.enterOuterAlt(localctx, 1)
- self.state = 60
+ self.state = 65
self.match(TacticNotationsParser.ID)
except RecognitionException as re:
localctx.exception = re
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-05 10:00:08 +0000