From 36e38a3768251dbcf20c4de2b746e5eee33da909 Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Fri, 18 May 2018 01:12:10 -0400 Subject: [doc] Use productionlist instead of prodn in ring.rst --- doc/sphinx/addendum/ring.rst | 23 +++++++++++------------ 1 file changed, 11 insertions(+), 12 deletions(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index 47d3a7d7c..6a9b343ba 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -310,16 +310,15 @@ The :n:`@ident` is not relevant. It is just used for error messages. The axioms. The optional list of modifiers is used to tailor the behavior of the tactic. The following list describes their syntax and effects: -.. prodn:: - ring_mod ::= abstract %| decidable @term %| morphism @term - %| setoid @term @term - %| constants [@ltac] - %| preprocess [@ltac] - %| postprocess [@ltac] - %| power_tac @term [@ltac] - %| sign @term - %| div @term - +.. productionlist:: coq + ring_mod : abstract | decidable `term` | morphism `term` + : | setoid `term` `term` + : | constants [`ltac`] + : | preprocess [`ltac`] + : | postprocess [`ltac`] + : | power_tac `term` [`ltac`] + : | sign `term` + : | div `term` abstract declares the ring as abstract. This is the default. @@ -663,8 +662,8 @@ messages. :n:`@term` is a proof that the field signature satisfies the (semi-)field axioms. The optional list of modifiers is used to tailor the behavior of the tactic. -.. prodn:: - field_mod := @ring_mod %| completeness @term +.. productionlist:: coq + field_mod : `ring_mod` | completeness `term` Since field tactics are built upon ``ring`` tactics, all modifiers of the ``Add Ring`` apply. There is only one -- cgit v1.2.3 From 4687e40504024b51b63bc5681feba13ea6dffbaf Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Fri, 18 May 2018 01:09:26 -0400 Subject: [doc] Fix uncaught duplicate-label errors in the SSReflect chapter --- doc/sphinx/proof-engine/ssreflect-proof-language.rst | 20 ++++++++------------ 1 file changed, 8 insertions(+), 12 deletions(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 1c554acdb..16d0420ec 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -2402,7 +2402,7 @@ tactic: The behavior of the defective have tactic makes it possible to generalize it in the following general construction: -.. tacn:: have {* @i_item } {? @i_pattern } {? @s_item | {+ @binder } } {? : @term } {? := @term | by @tactic } +.. tacn:: have {* @i_item } {? @i_pattern } {? @s_item | {+ @ssr_binder } } {? : @term } {? := @term | by @tactic } Open syntax is supported for both :token:`term`. For the description of :token:`i_item` and :token:`s_item` see section @@ -5242,7 +5242,7 @@ Notation scope Module name -.. prodn:: name ::= @qualid +.. prodn:: modname ::= @qualid Natural number @@ -5252,14 +5252,10 @@ where :token:`ident` is an Ltac variable denoting a standard |Coq| numeral (should not be the name of a tactic which can be followed by a bracket ``[``, like ``do``, ``have``,…) -Pattern - -.. prodn:: pattern ::= @term - Items and switches ~~~~~~~~~~~~~~~~~~ -.. prodn:: binder ::= @ident %| ( @ident {? : @term } ) +.. prodn:: ssr_binder ::= @ident %| ( @ident {? : @term } ) binder see :ref:`abbreviations_ssr`. @@ -5354,8 +5350,8 @@ case analysis see :ref:`the_defective_tactics_ssr` rewrite see :ref:`rewriting_ssr` -.. tacn:: have {* @i_item } {? @i_pattern } {? @s_item %| {+ @binder } } {? : @term } := @term -.. tacv:: have {* @i_item } {? @i_pattern } {? @s_item %| {+ @binder } } : @term {? by @tactic } +.. tacn:: have {* @i_item } {? @i_pattern } {? @s_item %| {+ @ssr_binder } } {? : @term } := @term +.. tacv:: have {* @i_item } {? @i_pattern } {? @s_item %| {+ @ssr_binder } } : @term {? by @tactic } .. tacn:: have suff {? @clear_switch } {? @i_pattern } {? : @term } := @term .. tacv:: have suff {? @clear_switch } {? @i_pattern } : @term {? by @tactic } .. tacv:: gen have {? @ident , } {? @i_pattern } : {+ @gen_item } / @term {? by @tactic } @@ -5369,9 +5365,9 @@ forward chaining see :ref:`structure_ssr` specializing see :ref:`structure_ssr` -.. tacn:: suff {* @i_item } {? @i_pattern } {+ @binder } : @term {? by @tactic } +.. tacn:: suff {* @i_item } {? @i_pattern } {+ @ssr_binder } : @term {? by @tactic } :name: suff -.. tacv:: suffices {* @i_item } {? @i_pattern } {+ @binder } : @term {? by @tactic } +.. tacv:: suffices {* @i_item } {? @i_pattern } {+ @ssr_binder } : @term {? by @tactic } :name: suffices .. tacv:: suff {? have } {? @clear_switch } {? @i_pattern } : @term {? by @tactic } .. tacv:: suffices {? have } {? @clear_switch } {? @i_pattern } : @term {? by @tactic } @@ -5382,7 +5378,7 @@ backchaining see :ref:`structure_ssr` local definition :ref:`definitions_ssr` -.. tacv:: pose @ident {+ @binder } := @term +.. tacv:: pose @ident {+ @ssr_binder } := @term local function definition -- cgit v1.2.3 From 21a0af5b7743e5a1013438210492991b51d878c4 Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Fri, 18 May 2018 01:09:06 -0400 Subject: [doc] Fix a typo in the ssreflect chapter --- doc/sphinx/proof-engine/ssreflect-proof-language.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 16d0420ec..ab52c2ce7 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -1484,7 +1484,7 @@ The abstract tactic ``````````````````` .. tacn:: abstract: {+ d_item} - :name abstract (ssreflect) + :name: abstract (ssreflect) This tactic assigns an abstract constant previously introduced with the ``[: name ]`` intro pattern (see section :ref:`introduction_ssr`). -- cgit v1.2.3 From 3d8342c2c26f710583e6b9246bd1069cb8b42d7d Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Fri, 18 May 2018 01:10:15 -0400 Subject: [doc] Rewrite and document the prodn directive It was broken and undocumented. We dropped the git logs, too, so it wasn't clear who wrote it and why it was introduced in the first place. --- doc/sphinx/README.rst | 15 ++++- doc/tools/coqrst/coqdomain.py | 136 +++++++++++++++++++++++++----------------- 2 files changed, 95 insertions(+), 56 deletions(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index 35a605ddd..32de15ee3 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -123,11 +123,24 @@ Here is the list of all objects of the Coq domain (The symbol :black_nib: indica :cmd:`Variant` and :cmd:`Record` get an automatic declaration of the induction principles. -``.. prodn::`` :black_nib: Grammar productions. +``.. prodn::`` A grammar production. This is useful if you intend to document individual grammar productions. Otherwise, use Sphinx's `production lists `_. + Unlike ``.. productionlist``\ s, this directive accepts notation syntax. + + + Usage:: + + .. prodn:: token += production + .. prodn:: token ::= production + + Example:: + + .. prodn:: term += let: @pattern := @term in @term + .. prodn:: occ_switch ::= { {? + %| - } {* @num } } + ``.. tacn::`` :black_nib: A tactic, or a tactic notation. Example:: diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index ab3a485b2..c9487abf0 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -28,6 +28,7 @@ from docutils.parsers.rst.directives.admonitions import BaseAdmonition from sphinx import addnodes from sphinx.roles import XRefRole +from sphinx.errors import ExtensionError from sphinx.util.nodes import set_source_info, set_role_source_info, make_refnode from sphinx.util.logging import getLogger from sphinx.directives import ObjectDescription @@ -103,10 +104,16 @@ class CoqObject(ObjectDescription): 'undocumented': directives.flag } - def _subdomain(self): + def subdomain_data(self): if self.subdomain is None: raise ValueError() - return self.subdomain + return self.env.domaindata['coq']['objects'][self.subdomain] + + def _render_annotation(self, signode): + if self.annotation: + annot_node = nodes.inline(self.annotation, self.annotation, classes=['sigannot']) + signode += addnodes.desc_annotation(self.annotation, '', annot_node) + signode += nodes.Text(' ') def handle_signature(self, signature, signode): """Prefix signature with the proper annotation, then render it using @@ -114,29 +121,32 @@ class CoqObject(ObjectDescription): :returns: the name given to the resulting node, if any """ - if self.annotation: - annotation = self.annotation + ' ' - signode += addnodes.desc_annotation(annotation, annotation) + self._render_annotation(signode) self._render_signature(signature, signode) return self._names.get(signature) or self._name_from_signature(signature) + def _warn_if_duplicate_name(self, objects, name): + """Check that two objects in the same domain don't have the same name.""" + if name in objects: + MSG = 'Duplicate object: {}; other is at {}' + msg = MSG.format(name, self.env.doc2path(objects[name][0])) + self.state_machine.reporter.warning(msg, line=self.lineno) + def _record_name(self, name, target_id): """Record a name, mapping it to target_id Warns if another object of the same name already exists. """ - names_in_subdomain = self.env.domaindata['coq']['objects'][self._subdomain()] - # Check that two objects in the same domain don't have the same name - if name in names_in_subdomain: - self.state_machine.reporter.warning( - 'Duplicate Coq object: {}; other is at {}'.format( - name, self.env.doc2path(names_in_subdomain[name][0])), - line=self.lineno) + names_in_subdomain = self.subdomain_data() + self._warn_if_duplicate_name(names_in_subdomain, name) names_in_subdomain[name] = (self.env.docname, self.objtype, target_id) + def _target_id(self, name): + return make_target(self.objtype, nodes.make_id(name)) + def _add_target(self, signode, name): """Register a link target ‘name’, pointing to signode.""" - targetid = make_target(self.objtype, nodes.make_id(name)) + targetid = self._target_id(name) if targetid not in self.state.document.ids: signode['ids'].append(targetid) signode['names'].append(name) @@ -314,50 +324,71 @@ class OptionObject(NotationObject): def _name_from_signature(self, signature): return stringify_with_ellipses(signature) -class ProductionObject(NotationObject): - """Grammar productions. +class ProductionObject(CoqObject): + r"""A grammar production. This is useful if you intend to document individual grammar productions. Otherwise, use Sphinx's `production lists `_. + + Unlike ``.. productionlist``\ s, this directive accepts notation syntax. + + + Usage:: + + .. prodn:: token += production + .. prodn:: token ::= production + + Example:: + + .. prodn:: term += let: @pattern := @term in @term + .. prodn:: occ_switch ::= { {? + %| - } {* @num } } + """ - # FIXME (CPC): I have no idea what this does :/ Someone should add an example. subdomain = "prodn" - index_suffix = None - annotation = None + #annotation = "Grammar production" - # override to create link targets for production left-hand sides - def run(self): + def _render_signature(self, signature, signode): + raise NotImplementedError(self) + + SIG_ERROR = ("Invalid syntax in ``.. prodn::`` directive" + + "\nExpected ``name ::= ...`` or ``name += ...``" + + " (e.g. ``pattern += constr:(@ident)``)") + + def handle_signature(self, signature, signode): + nsplits = 2 + parts = signature.split(maxsplit=nsplits) + if len(parts) != 3: + raise ExtensionError(ProductionObject.SIG_ERROR) + + lhs, op, rhs = (part.strip() for part in parts) + if op not in ["::=", "+="]: + raise ExtensionError(ProductionObject.SIG_ERROR) + + self._render_annotation(signode) + + lhs_op = '{} {} '.format(lhs, op) + lhs_node = nodes.literal(lhs_op, lhs_op) + + position = self.state_machine.get_source_and_line(self.lineno) + rhs_node = parse_notation(rhs, *position) + signode += addnodes.desc_name(signature, '', lhs_node, rhs_node) + + return ('token', lhs) if op == '::=' else None + + def _add_index_entry(self, name, target): + pass + + def _target_id(self, name): + # Use `name[1]` instead of ``nodes.make_id(name[1])`` to work around + # https://github.com/sphinx-doc/sphinx/issues/4983 + return 'grammar-token-{}'.format(name[1]) + + def _record_name(self, name, targetid): env = self.state.document.settings.env objects = env.domaindata['std']['objects'] - - class ProdnError(Exception): - """Exception for ill-formed prodn""" - pass - - [idx, node] = super().run() - try: - # find LHS of production - inline_lhs = node[0][0][0][0] # may be fragile !!! - lhs_str = str(inline_lhs) - if lhs_str[0:7] != "