From 14f44c0e23c413314adf23ed1059acc5cd1fef2f Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Fri, 13 Apr 2018 00:04:25 +0200 Subject: [Sphinx] Add chapter 9. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Chapter ported by Théo Zimmermann and Maxime Dénès. --- doc/tools/coqrst/notations/TacticNotations.g | 9 +-- doc/tools/coqrst/notations/TacticNotations.tokens | 3 +- doc/tools/coqrst/notations/TacticNotationsLexer.py | 48 ++++++++------- .../coqrst/notations/TacticNotationsLexer.tokens | 3 +- .../coqrst/notations/TacticNotationsParser.py | 71 +++++++++++++++------- doc/tools/coqrst/notations/html.py | 3 + doc/tools/coqrst/notations/sphinx.py | 21 ++++++- 7 files changed, 107 insertions(+), 51 deletions(-) (limited to 'doc/tools') diff --git a/doc/tools/coqrst/notations/TacticNotations.g b/doc/tools/coqrst/notations/TacticNotations.g index 68658fe49..a889ebda7 100644 --- a/doc/tools/coqrst/notations/TacticNotations.g +++ b/doc/tools/coqrst/notations/TacticNotations.g @@ -20,13 +20,14 @@ repeat: LGROUP (ATOM)? WHITESPACE blocks (WHITESPACE)? RBRACE; curlies: LBRACE (whitespace)? blocks (whitespace)? RBRACE; whitespace: WHITESPACE; meta: METACHAR; -atomic: ATOM; -hole: ID; +atomic: ATOM (SUB)?; +hole: ID (SUB)?; LGROUP: '{' [+*?]; LBRACE: '{'; RBRACE: '}'; METACHAR: '%' [|(){}]; -ATOM: '@' | ~[@{} ]+; -ID: '@' [a-zA-Z0-9_]+; +ATOM: '@' | '_' | ~[@_{} ]+; +ID: '@' ('_'? [a-zA-Z0-9])+; +SUB: '_' '_' [a-zA-Z0-9]+; WHITESPACE: ' '+; diff --git a/doc/tools/coqrst/notations/TacticNotations.tokens b/doc/tools/coqrst/notations/TacticNotations.tokens index 76ed2b065..88b38f97a 100644 --- a/doc/tools/coqrst/notations/TacticNotations.tokens +++ b/doc/tools/coqrst/notations/TacticNotations.tokens @@ -4,6 +4,7 @@ RBRACE=3 METACHAR=4 ATOM=5 ID=6 -WHITESPACE=7 +SUB=7 +WHITESPACE=8 '{'=2 '}'=3 diff --git a/doc/tools/coqrst/notations/TacticNotationsLexer.py b/doc/tools/coqrst/notations/TacticNotationsLexer.py index 61d8d2f9e..27293e7e0 100644 --- a/doc/tools/coqrst/notations/TacticNotationsLexer.py +++ b/doc/tools/coqrst/notations/TacticNotationsLexer.py @@ -7,24 +7,28 @@ import sys def serializedATN(): with StringIO() as buf: - buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\2\t") - buf.write(".\b\1\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7") - buf.write("\4\b\t\b\3\2\3\2\3\2\3\3\3\3\3\4\3\4\3\5\3\5\3\5\3\6\3") - buf.write("\6\6\6\36\n\6\r\6\16\6\37\5\6\"\n\6\3\7\3\7\6\7&\n\7\r") - buf.write("\7\16\7\'\3\b\6\b+\n\b\r\b\16\b,\2\2\t\3\3\5\4\7\5\t\6") - buf.write("\13\7\r\b\17\t\3\2\6\4\2,-AA\4\2*+}\177\6\2\"\"BB}}\177") - buf.write("\177\6\2\62;C\\aac|\2\61\2\3\3\2\2\2\2\5\3\2\2\2\2\7\3") - buf.write("\2\2\2\2\t\3\2\2\2\2\13\3\2\2\2\2\r\3\2\2\2\2\17\3\2\2") - buf.write("\2\3\21\3\2\2\2\5\24\3\2\2\2\7\26\3\2\2\2\t\30\3\2\2\2") - buf.write("\13!\3\2\2\2\r#\3\2\2\2\17*\3\2\2\2\21\22\7}\2\2\22\23") - buf.write("\t\2\2\2\23\4\3\2\2\2\24\25\7}\2\2\25\6\3\2\2\2\26\27") - buf.write("\7\177\2\2\27\b\3\2\2\2\30\31\7\'\2\2\31\32\t\3\2\2\32") - buf.write("\n\3\2\2\2\33\"\7B\2\2\34\36\n\4\2\2\35\34\3\2\2\2\36") - buf.write("\37\3\2\2\2\37\35\3\2\2\2\37 \3\2\2\2 \"\3\2\2\2!\33\3") - buf.write("\2\2\2!\35\3\2\2\2\"\f\3\2\2\2#%\7B\2\2$&\t\5\2\2%$\3") - buf.write("\2\2\2&\'\3\2\2\2\'%\3\2\2\2\'(\3\2\2\2(\16\3\2\2\2)+") - buf.write("\7\"\2\2*)\3\2\2\2+,\3\2\2\2,*\3\2\2\2,-\3\2\2\2-\20\3") - buf.write("\2\2\2\7\2\37!\',\2") + buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\2\n") + buf.write(":\b\1\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7") + buf.write("\4\b\t\b\4\t\t\t\3\2\3\2\3\2\3\3\3\3\3\4\3\4\3\5\3\5\3") + buf.write("\5\3\6\3\6\6\6 \n\6\r\6\16\6!\5\6$\n\6\3\7\3\7\5\7(\n") + buf.write("\7\3\7\6\7+\n\7\r\7\16\7,\3\b\3\b\3\b\6\b\62\n\b\r\b\16") + buf.write("\b\63\3\t\6\t\67\n\t\r\t\16\t8\2\2\n\3\3\5\4\7\5\t\6\13") + buf.write("\7\r\b\17\t\21\n\3\2\7\4\2,-AA\4\2*+}\177\4\2BBaa\7\2") + buf.write("\"\"BBaa}}\177\177\5\2\62;C\\c|\2?\2\3\3\2\2\2\2\5\3\2") + buf.write("\2\2\2\7\3\2\2\2\2\t\3\2\2\2\2\13\3\2\2\2\2\r\3\2\2\2") + buf.write("\2\17\3\2\2\2\2\21\3\2\2\2\3\23\3\2\2\2\5\26\3\2\2\2\7") + buf.write("\30\3\2\2\2\t\32\3\2\2\2\13#\3\2\2\2\r%\3\2\2\2\17.\3") + buf.write("\2\2\2\21\66\3\2\2\2\23\24\7}\2\2\24\25\t\2\2\2\25\4\3") + buf.write("\2\2\2\26\27\7}\2\2\27\6\3\2\2\2\30\31\7\177\2\2\31\b") + buf.write("\3\2\2\2\32\33\7\'\2\2\33\34\t\3\2\2\34\n\3\2\2\2\35$") + buf.write("\t\4\2\2\36 \n\5\2\2\37\36\3\2\2\2 !\3\2\2\2!\37\3\2\2") + buf.write("\2!\"\3\2\2\2\"$\3\2\2\2#\35\3\2\2\2#\37\3\2\2\2$\f\3") + buf.write("\2\2\2%*\7B\2\2&(\7a\2\2\'&\3\2\2\2\'(\3\2\2\2()\3\2\2") + buf.write("\2)+\t\6\2\2*\'\3\2\2\2+,\3\2\2\2,*\3\2\2\2,-\3\2\2\2") + buf.write("-\16\3\2\2\2./\7a\2\2/\61\7a\2\2\60\62\t\6\2\2\61\60\3") + buf.write("\2\2\2\62\63\3\2\2\2\63\61\3\2\2\2\63\64\3\2\2\2\64\20") + buf.write("\3\2\2\2\65\67\7\"\2\2\66\65\3\2\2\2\678\3\2\2\28\66\3") + buf.write("\2\2\289\3\2\2\29\22\3\2\2\2\t\2!#\',\638\2") return buf.getvalue() @@ -40,7 +44,8 @@ class TacticNotationsLexer(Lexer): METACHAR = 4 ATOM = 5 ID = 6 - WHITESPACE = 7 + SUB = 7 + WHITESPACE = 8 channelNames = [ u"DEFAULT_TOKEN_CHANNEL", u"HIDDEN" ] @@ -50,10 +55,11 @@ class TacticNotationsLexer(Lexer): "'{'", "'}'" ] symbolicNames = [ "", - "LGROUP", "LBRACE", "RBRACE", "METACHAR", "ATOM", "ID", "WHITESPACE" ] + "LGROUP", "LBRACE", "RBRACE", "METACHAR", "ATOM", "ID", "SUB", + "WHITESPACE" ] ruleNames = [ "LGROUP", "LBRACE", "RBRACE", "METACHAR", "ATOM", "ID", - "WHITESPACE" ] + "SUB", "WHITESPACE" ] grammarFileName = "TacticNotations.g" diff --git a/doc/tools/coqrst/notations/TacticNotationsLexer.tokens b/doc/tools/coqrst/notations/TacticNotationsLexer.tokens index 76ed2b065..88b38f97a 100644 --- a/doc/tools/coqrst/notations/TacticNotationsLexer.tokens +++ b/doc/tools/coqrst/notations/TacticNotationsLexer.tokens @@ -4,6 +4,7 @@ RBRACE=3 METACHAR=4 ATOM=5 ID=6 -WHITESPACE=7 +SUB=7 +WHITESPACE=8 '{'=2 '}'=3 diff --git a/doc/tools/coqrst/notations/TacticNotationsParser.py b/doc/tools/coqrst/notations/TacticNotationsParser.py index c7e28af52..645f07897 100644 --- a/doc/tools/coqrst/notations/TacticNotationsParser.py +++ b/doc/tools/coqrst/notations/TacticNotationsParser.py @@ -7,29 +7,31 @@ import sys def serializedATN(): with StringIO() as buf: - 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("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\3\n") + buf.write("J\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") + buf.write("\3\b\3\t\3\t\5\tD\n\t\3\n\3\n\5\nH\n\n\3\n\2\2\13\2\4") + buf.write("\6\b\n\f\16\20\22\2\2\2L\2\24\3\2\2\2\4\27\3\2\2\2\6&") + buf.write("\3\2\2\2\b(\3\2\2\2\n\63\3\2\2\2\f=\3\2\2\2\16?\3\2\2") + buf.write("\2\20A\3\2\2\2\22E\3\2\2\2\24\25\5\4\3\2\25\26\7\2\2\3") + buf.write("\26\3\3\2\2\2\27\36\5\6\4\2\30\32\5\f\7\2\31\30\3\2\2") + buf.write("\2\31\32\3\2\2\2\32\33\3\2\2\2\33\35\5\6\4\2\34\31\3\2") + buf.write("\2\2\35 \3\2\2\2\36\34\3\2\2\2\36\37\3\2\2\2\37\5\3\2") + buf.write("\2\2 \36\3\2\2\2!\'\5\20\t\2\"\'\5\16\b\2#\'\5\22\n\2") + buf.write("$\'\5\b\5\2%\'\5\n\6\2&!\3\2\2\2&\"\3\2\2\2&#\3\2\2\2") + buf.write("&$\3\2\2\2&%\3\2\2\2\'\7\3\2\2\2(*\7\3\2\2)+\7\7\2\2*") + buf.write(")\3\2\2\2*+\3\2\2\2+,\3\2\2\2,-\7\n\2\2-/\5\4\3\2.\60") + buf.write("\7\n\2\2/.\3\2\2\2/\60\3\2\2\2\60\61\3\2\2\2\61\62\7\5") + buf.write("\2\2\62\t\3\2\2\2\63\65\7\4\2\2\64\66\5\f\7\2\65\64\3") + buf.write("\2\2\2\65\66\3\2\2\2\66\67\3\2\2\2\679\5\4\3\28:\5\f\7") + buf.write("\298\3\2\2\29:\3\2\2\2:;\3\2\2\2;<\7\5\2\2<\13\3\2\2\2") + buf.write("=>\7\n\2\2>\r\3\2\2\2?@\7\6\2\2@\17\3\2\2\2AC\7\7\2\2") + buf.write("BD\7\t\2\2CB\3\2\2\2CD\3\2\2\2D\21\3\2\2\2EG\7\b\2\2F") + buf.write("H\7\t\2\2GF\3\2\2\2GH\3\2\2\2H\23\3\2\2\2\13\31\36&*/") + buf.write("\659CG") return buf.getvalue() @@ -46,7 +48,7 @@ class TacticNotationsParser ( Parser ): literalNames = [ "", "", "'{'", "'}'" ] symbolicNames = [ "", "LGROUP", "LBRACE", "RBRACE", "METACHAR", - "ATOM", "ID", "WHITESPACE" ] + "ATOM", "ID", "SUB", "WHITESPACE" ] RULE_top = 0 RULE_blocks = 1 @@ -68,7 +70,8 @@ class TacticNotationsParser ( Parser ): METACHAR=4 ATOM=5 ID=6 - WHITESPACE=7 + SUB=7 + WHITESPACE=8 def __init__(self, input:TokenStream, output:TextIO = sys.stdout): super().__init__(input, output) @@ -502,6 +505,9 @@ class TacticNotationsParser ( Parser ): def ATOM(self): return self.getToken(TacticNotationsParser.ATOM, 0) + def SUB(self): + return self.getToken(TacticNotationsParser.SUB, 0) + def getRuleIndex(self): return TacticNotationsParser.RULE_atomic @@ -518,10 +524,19 @@ class TacticNotationsParser ( Parser ): localctx = TacticNotationsParser.AtomicContext(self, self._ctx, self.state) self.enterRule(localctx, 14, self.RULE_atomic) + self._la = 0 # Token type try: self.enterOuterAlt(localctx, 1) self.state = 63 self.match(TacticNotationsParser.ATOM) + self.state = 65 + self._errHandler.sync(self) + _la = self._input.LA(1) + if _la==TacticNotationsParser.SUB: + self.state = 64 + self.match(TacticNotationsParser.SUB) + + except RecognitionException as re: localctx.exception = re self._errHandler.reportError(self, re) @@ -539,6 +554,9 @@ class TacticNotationsParser ( Parser ): def ID(self): return self.getToken(TacticNotationsParser.ID, 0) + def SUB(self): + return self.getToken(TacticNotationsParser.SUB, 0) + def getRuleIndex(self): return TacticNotationsParser.RULE_hole @@ -555,10 +573,19 @@ class TacticNotationsParser ( Parser ): localctx = TacticNotationsParser.HoleContext(self, self._ctx, self.state) self.enterRule(localctx, 16, self.RULE_hole) + self._la = 0 # Token type try: self.enterOuterAlt(localctx, 1) - self.state = 65 + self.state = 67 self.match(TacticNotationsParser.ID) + self.state = 69 + self._errHandler.sync(self) + _la = self._input.LA(1) + if _la==TacticNotationsParser.SUB: + self.state = 68 + self.match(TacticNotationsParser.SUB) + + except RecognitionException as re: localctx.exception = re self._errHandler.reportError(self, re) diff --git a/doc/tools/coqrst/notations/html.py b/doc/tools/coqrst/notations/html.py index 9c94a4b2d..87a41cf9f 100644 --- a/doc/tools/coqrst/notations/html.py +++ b/doc/tools/coqrst/notations/html.py @@ -41,6 +41,9 @@ class TacticNotationsToHTMLVisitor(TacticNotationsVisitor): def visitHole(self, ctx:TacticNotationsParser.HoleContext): tags.span(ctx.ID().getText()[1:], _class="hole") + sub = ctx.SUB() + if sub: + tags.sub(sub.getText()[1:]) def visitMeta(self, ctx:TacticNotationsParser.MetaContext): txt = ctx.METACHAR().getText()[1:] diff --git a/doc/tools/coqrst/notations/sphinx.py b/doc/tools/coqrst/notations/sphinx.py index 26a5f6968..e05b83418 100644 --- a/doc/tools/coqrst/notations/sphinx.py +++ b/doc/tools/coqrst/notations/sphinx.py @@ -56,19 +56,36 @@ class TacticNotationsToSphinxVisitor(TacticNotationsVisitor): def visitAtomic(self, ctx:TacticNotationsParser.AtomicContext): atom = ctx.ATOM().getText() - return [nodes.inline(atom, atom)] + sub = ctx.SUB() + node = nodes.inline(atom, atom) + + if sub: + sub_index = sub.getText()[2:] + node += nodes.subscript(sub_index, sub_index) + + return [node] def visitHole(self, ctx:TacticNotationsParser.HoleContext): hole = ctx.ID().getText() token_name = hole[1:] node = nodes.inline(hole, token_name, classes=["hole"]) + + sub = ctx.SUB() + if sub: + sub_index = sub.getText()[2:] + node += nodes.subscript(sub_index, sub_index) + return [addnodes.pending_xref(token_name, node, reftype='token', refdomain='std', reftarget=token_name)] def visitMeta(self, ctx:TacticNotationsParser.MetaContext): meta = ctx.METACHAR().getText() metachar = meta[1:] # remove escape char token_name = metachar - return [nodes.inline(metachar, token_name, classes=["meta"])] + if (metachar == "{") or (metachar == "}"): + classes=[] + else: + classes=["meta"] + return [nodes.inline(metachar, token_name, classes=classes)] def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext): return [nodes.Text(" ")] -- cgit v1.2.3