aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
Diffstat (limited to 'doc')
-rw-r--r--doc/sphinx/README.rst15
-rw-r--r--doc/sphinx/addendum/generalized-rewriting.rst2
-rw-r--r--doc/sphinx/addendum/ring.rst23
-rw-r--r--doc/sphinx/proof-engine/ssreflect-proof-language.rst25
-rw-r--r--doc/sphinx/proof-engine/tactics.rst13
-rw-r--r--doc/tools/coqrst/coqdoc/main.py4
-rw-r--r--doc/tools/coqrst/coqdomain.py136
7 files changed, 134 insertions, 84 deletions
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
<http://www.sphinx-doc.org/en/stable/markup/para.html#directive-productionlist>`_.
+ 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/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst
index e10e16c10..e4d24a1f7 100644
--- a/doc/sphinx/addendum/generalized-rewriting.rst
+++ b/doc/sphinx/addendum/generalized-rewriting.rst
@@ -106,7 +106,7 @@ argument.
Morphisms can also be contravariant in one or more of their arguments.
A morphism is contravariant on an argument associated to the relation
-instance :math`R` if it is covariant on the same argument when the inverse
+instance :math:`R` if it is covariant on the same argument when the inverse
relation :math:`R^{−1}` (``inverse R`` in Coq) is considered. The special arrow ``-->``
is used in signatures for contravariant morphisms.
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
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 3b2009657..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`).
@@ -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
@@ -3657,7 +3657,8 @@ selective rewriting, blocking on the fly the reduction in the term ``t``.
.. coqtop:: reset
- From Coq Require Import ssreflect ssrfun ssrbool List.
+ From Coq Require Import ssreflect ssrfun ssrbool.
+ From Coq Require Import List.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
@@ -5241,7 +5242,7 @@ Notation scope
Module name
-.. prodn:: name ::= @qualid
+.. prodn:: modname ::= @qualid
Natural number
@@ -5251,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`.
@@ -5353,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 }
@@ -5368,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 }
@@ -5381,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
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 29c2f8b81..d0a0d568e 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -3949,9 +3949,20 @@ succeeds, and results in an error otherwise.
:name: constr_eq
This tactic checks whether its arguments are equal modulo alpha
- conversion and casts.
+ conversion, casts and universe constraints. It may unify universes.
.. exn:: Not equal.
+.. exn:: Not equal (due to universes).
+
+.. tacn:: constr_eq_strict @term @term
+ :name: constr_eq_strict
+
+ This tactic checks whether its arguments are equal modulo alpha
+ conversion, casts and universe constraints. It does not add new
+ constraints.
+
+.. exn:: Not equal.
+.. exn:: Not equal (due to universes).
.. tacn:: unify @term @term
:name: unify
diff --git a/doc/tools/coqrst/coqdoc/main.py b/doc/tools/coqrst/coqdoc/main.py
index cedd60d3b..57adcb287 100644
--- a/doc/tools/coqrst/coqdoc/main.py
+++ b/doc/tools/coqrst/coqdoc/main.py
@@ -20,6 +20,7 @@ lexer.
"""
import os
+import platform
from tempfile import mkstemp
from subprocess import check_output
@@ -36,6 +37,9 @@ def coqdoc(coq_code, coqdoc_bin=None):
"""Get the output of coqdoc on coq_code."""
coqdoc_bin = coqdoc_bin or os.path.join(os.getenv("COQBIN"), "coqdoc")
fd, filename = mkstemp(prefix="coqdoc-", suffix=".v")
+ if platform.system().startswith("CYGWIN"):
+ # coqdoc currently doesn't accept cygwin style paths in the form "/cygdrive/c/..."
+ filename = check_output(["cygpath", "-w", filename]).decode("utf-8").strip()
try:
os.write(fd, COQDOC_HEADER.encode("utf-8"))
os.write(fd, coq_code.encode("utf-8"))
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
<http://www.sphinx-doc.org/en/stable/markup/para.html#directive-productionlist>`_.
+
+ 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] != "<inline":
- raise ProdnError("Expected atom on LHS")
- lhs = inline_lhs[0]
- # register link target
- subnode = addnodes.production()
- subnode['tokenname'] = lhs
- idname = 'grammar-token-%s' % subnode['tokenname']
- if idname not in self.state.document.ids:
- subnode['ids'].append(idname)
- self.state.document.note_implicit_target(subnode, subnode)
- objects['token', subnode['tokenname']] = env.docname, idname
- subnode.extend(token_xrefs(lhs))
- # patch in link target
- inline_lhs['ids'].append(idname)
- except ProdnError as err:
- getLogger(__name__).warning("Could not create link target for prodn: " + str(err) +
- "\nSphinx represents the prodn as: " + str(node) + "\n")
- return [idx, node]
+ self._warn_if_duplicate_name(objects, name)
+ objects[name] = env.docname, targetid
class ExceptionObject(NotationObject):
"""An error raised by a Coq command or tactic.
@@ -841,11 +872,6 @@ class CoqOptionIndex(CoqSubdomainsIndex):
class CoqGallinaIndex(CoqSubdomainsIndex):
name, localname, shortname, subdomains = "thmindex", "Gallina Index", "theorems", ["thm"]
-# we specify an index to make productions fit into the framework of notations
-# but not likely to include a link to this index
-class CoqProductionIndex(CoqSubdomainsIndex):
- name, localname, shortname, subdomains = "prodnindex", "Production Index", "productions", ["prodn"]
-
class CoqExceptionIndex(CoqSubdomainsIndex):
name, localname, shortname, subdomains = "exnindex", "Errors and Warnings Index", "errors", ["exn", "warn"]
@@ -952,7 +978,7 @@ class CoqDomain(Domain):
'g': CoqCodeRole
}
- indices = [CoqVernacIndex, CoqTacticIndex, CoqOptionIndex, CoqGallinaIndex, CoqProductionIndex, CoqExceptionIndex]
+ indices = [CoqVernacIndex, CoqTacticIndex, CoqOptionIndex, CoqGallinaIndex, CoqExceptionIndex]
data_version = 1
initial_data = {
@@ -1047,7 +1073,7 @@ def setup(app):
# A few sanity checks:
subdomains = set(obj.subdomain for obj in CoqDomain.directives.values())
- assert subdomains == set(chain(*(idx.subdomains for idx in CoqDomain.indices)))
+ assert subdomains.issuperset(chain(*(idx.subdomains for idx in CoqDomain.indices)))
assert subdomains.issubset(CoqDomain.roles.keys())
# Add domain, directives, and roles
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 12:11:18 +0000