diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/02-specification-language/10441-static-poly-section.rst | 11 | ||||
| -rw-r--r-- | doc/plugin_tutorial/tuto1/src/simple_print.ml | 9 | ||||
| -rw-r--r-- | doc/sphinx/README.rst | 30 | ||||
| -rw-r--r-- | doc/sphinx/README.template.rst | 28 | ||||
| -rw-r--r-- | doc/sphinx/addendum/ring.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/addendum/universe-polymorphism.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 28 | ||||
| -rw-r--r-- | doc/tools/coqrst/coqdomain.py | 21 | ||||
| -rw-r--r-- | doc/tools/docgram/README.md | 208 | ||||
| -rw-r--r-- | doc/tools/docgram/common.edit_mlg | 220 | ||||
| -rw-r--r-- | doc/tools/docgram/doc_grammar.ml | 1572 | ||||
| -rw-r--r-- | doc/tools/docgram/fullGrammar | 3174 | ||||
| -rw-r--r-- | doc/tools/docgram/orderedGrammar | 4170 | ||||
| -rw-r--r-- | doc/tools/docgram/prodn.edit_mlg | 14 | ||||
| -rw-r--r-- | doc/tools/docgram/productionlist.edit_mlg | 25 |
15 files changed, 9481 insertions, 33 deletions
diff --git a/doc/changelog/02-specification-language/10441-static-poly-section.rst b/doc/changelog/02-specification-language/10441-static-poly-section.rst new file mode 100644 index 0000000000..7f0345d946 --- /dev/null +++ b/doc/changelog/02-specification-language/10441-static-poly-section.rst @@ -0,0 +1,11 @@ +- The universe polymorphism setting now applies from the opening of a section. + In particular, it is not possible anymore to mix polymorphic and monomorphic + definitions in a section when there are no variables nor universe constraints + defined in this section. This makes the behaviour consistent with the + documentation. (`#10441 <https://github.com/coq/coq/pull/10441>`_, + by Pierre-Marie Pédrot) + +- The :cmd:`Section` vernacular command now accepts the "universes" attribute. In + addition to setting the section universe polymorphism, it also locally sets + the universe polymorphic option inside the section. + (`#10441 <https://github.com/coq/coq/pull/10441>`_, by Pierre-Marie Pédrot) diff --git a/doc/plugin_tutorial/tuto1/src/simple_print.ml b/doc/plugin_tutorial/tuto1/src/simple_print.ml index ba989b1bac..88afec14d5 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_print.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_print.ml @@ -2,14 +2,15 @@ type constr is given in the coq-dpdgraph plugin. *) let simple_body_access gref = + let open Names.GlobRef in match gref with - | Globnames.VarRef _ -> + | VarRef _ -> failwith "variables are not covered in this example" - | Globnames.IndRef _ -> + | IndRef _ -> failwith "inductive types are not covered in this example" - | Globnames.ConstructRef _ -> + | ConstructRef _ -> failwith "constructors are not covered in this example" - | Globnames.ConstRef cst -> + | ConstRef cst -> let cb = Environ.lookup_constant cst (Global.env()) in match Global.body_of_constant_body Library.indirect_accessor cb with | Some(e, _, _) -> EConstr.of_constr e diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index b20669c7f1..549598b187 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -64,7 +64,14 @@ The signatures of most objects can be written using a succinct DSL for Coq notat an alternative, indicating than one of multiple constructs can be used ``%{``, ``%}``, ``%|`` - an escaped character (rendered without the leading ``%``). In most cases, escaping is not necessary. In particular, the following expressions are all parsed as plain text, and do not need escaping: ``{ xyz }``, ``x |- y``. But the following escapes *are* needed: ``{| a b %| c | d }``, ``all: %{``. (We use ``%`` instead of the usual ``\`` because you'd have to type ``\`` twice in your reStructuredText file.) + an escaped character (rendered without the leading ``%``). In most cases, + escaping is not necessary. In particular, the following expressions are + all parsed as plain text, and do not need escaping: ``{ xyz }``, ``x |- y``. + But the following escapes *are* needed: ``{| a b %| c | d }``, ``all: %{``. + (We use ``%`` instead of the usual ``\`` because you'd have to type ``\`` + twice in your reStructuredText file.) + + For more details and corner cases, see `Advanced uses of notations`_ below. .. FIXME document the new subscript support @@ -300,7 +307,7 @@ In addition to the objects above, the ``coqrst`` Sphinx plugin defines the follo \WTEG{\forall~x:T,U}{\Prop} ``.. preamble::`` A reST directive to include a TeX file. - Mostly useful to let MathJax know about `\def`s and `\newcommand`s. The + Mostly useful to let MathJax know about `\def`\s and `\newcommand`\s. The contents of the TeX file are wrapped in a math environment, as MathJax doesn't process LaTeX definitions otherwise. @@ -536,7 +543,24 @@ Emacs The ``dev/tools/coqdev.el`` folder contains a convenient Emacs function to quickly insert Sphinx roles and quotes. It takes a single character (one of ``gntm:```), and inserts one of ``:g:``, ``:n:``, ``:t:``, or an arbitrary role, or double quotes. You can also select a region of text, and wrap it in single or double backticks using that function. -Use the following snippet to bind it to :kbd:`F12` in ``rst-mode``:: +Use the following snippet to bind it to `F12` in ``rst-mode``:: (with-eval-after-load 'rst (define-key rst-mode-map (kbd "<f12>") #'coqdev-sphinx-rst-coq-action)) + + +Advanced uses of notations +-------------------------- + + + - Use `%` to escape grammar literal strings that are the same as metasyntax, + such as ``{``, ``|``, ``}`` and ``{|``. (While this is optional for + ``|`` and ``{ ... }`` outside of ``{| ... }``, always using the escape + requires less thought.) + + - Literals such as ``|-`` and ``||`` don't need to be escaped. + + - The literal ``%`` shouldn't be escaped. + + - Don't use the escape for a ``|`` separator in ``{*`` and ``{+``. These + should appear as ``{*|`` and ``{+|``. diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst index 2093765608..51d5174567 100644 --- a/doc/sphinx/README.template.rst +++ b/doc/sphinx/README.template.rst @@ -64,7 +64,14 @@ The signatures of most objects can be written using a succinct DSL for Coq notat an alternative, indicating than one of multiple constructs can be used ``%{``, ``%}``, ``%|`` - an escaped character (rendered without the leading ``%``). In most cases, escaping is not necessary. In particular, the following expressions are all parsed as plain text, and do not need escaping: ``{ xyz }``, ``x |- y``. But the following escapes *are* needed: ``{| a b %| c | d }``, ``all: %{``. (We use ``%`` instead of the usual ``\`` because you'd have to type ``\`` twice in your reStructuredText file.) + an escaped character (rendered without the leading ``%``). In most cases, + escaping is not necessary. In particular, the following expressions are + all parsed as plain text, and do not need escaping: ``{ xyz }``, ``x |- y``. + But the following escapes *are* needed: ``{| a b %| c | d }``, ``all: %{``. + (We use ``%`` instead of the usual ``\`` because you'd have to type ``\`` + twice in your reStructuredText file.) + + For more details and corner cases, see `Advanced uses of notations`_ below. .. FIXME document the new subscript support @@ -290,7 +297,24 @@ Emacs The ``dev/tools/coqdev.el`` folder contains a convenient Emacs function to quickly insert Sphinx roles and quotes. It takes a single character (one of ``gntm:```), and inserts one of ``:g:``, ``:n:``, ``:t:``, or an arbitrary role, or double quotes. You can also select a region of text, and wrap it in single or double backticks using that function. -Use the following snippet to bind it to :kbd:`F12` in ``rst-mode``:: +Use the following snippet to bind it to `F12` in ``rst-mode``:: (with-eval-after-load 'rst (define-key rst-mode-map (kbd "<f12>") #'coqdev-sphinx-rst-coq-action)) + + +Advanced uses of notations +-------------------------- + + + - Use `%` to escape grammar literal strings that are the same as metasyntax, + such as ``{``, ``|``, ``}`` and ``{|``. (While this is optional for + ``|`` and ``{ ... }`` outside of ``{| ... }``, always using the escape + requires less thought.) + + - Literals such as ``|-`` and ``||`` don't need to be escaped. + + - The literal ``%`` shouldn't be escaped. + + - Don't use the escape for a ``|`` separator in ``{*`` and ``{+``. These + should appear as ``{*|`` and ``{+|``. diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index 3f4d5cc784..1098aa75da 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -76,7 +76,7 @@ an arbitrary order: ===== =============== ========================= Then normalize the “abstract” polynomial -:math:`((V_1 \otimes V_2 ) \oplus V_2) \oplus (V_0 \otimes 2)` +:math:`((V_1 \oplus V_2 ) \otimes V_2) \oplus (V_0 \otimes 2)` In our example the normal form is: :math:`(2 \otimes V_0 ) \oplus (V_1 \otimes V_2) \oplus (V_2 \otimes V_2 )`. Then substitute the variables by their values in the variables map to diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 395b5ce2d3..7e698bfb66 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -144,6 +144,8 @@ Many other commands support the ``Polymorphic`` flag, including: - ``Lemma``, ``Axiom``, and all the other “definition” keywords support polymorphism. +- :cmd:`Section` will locally set the polymorphism flag inside the section. + - ``Variables``, ``Context``, ``Universe`` and ``Constraint`` in a section support polymorphism. This means that the universe variables (and associated constraints) are discharged polymorphically over definitions that use diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index cc4976587d..1b9e3ce0f3 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -487,7 +487,7 @@ used as a convenient shorthand for abstractions, especially in local definitions or type expressions. Wildcards may be interpreted as abstractions (see for example sections -:ref:`definitions_ssr` and ref:`structure_ssr`), or their content can be +:ref:`definitions_ssr` and :ref:`structure_ssr`), or their content can be inferred from the whole context of the goal (see for example section :ref:`abbreviations_ssr`). @@ -983,13 +983,13 @@ During the course of a proof |Coq| always present the user with a Fk : Pk … ================= - forall (xl : Tl ) …, + forall (xl : Tl) …, let ym := bm in … in Pn -> … -> C The *goal* to be proved appears below the double line; above the line is the *context* of the sequent, a set of declarations of *constants* -``ci`` , *defined constants* d i , and *facts* ``Fk`` that can be used to +``ci`` , *defined constants* ``dj`` , and *facts* ``Fk`` that can be used to prove the goal (usually, ``Ti`` , ``Tj : Type`` and ``Pk : Prop``). The various kinds of declarations can come in any order. The top part of the @@ -1893,9 +1893,9 @@ under fresh |SSR| names. case E : a => H. Show 2. -Combining the generation of named equations mechanism with thecase +Combining the generation of named equations mechanism with the :tacn:`case` tactic strengthens the power of a case analysis. On the other hand, -when combined with the elim tactic, this feature is mostly useful for +when combined with the :tacn:`elim` tactic, this feature is mostly useful for debug purposes, to trace the values of decomposed parameters and pinpoint failing branches. @@ -2022,7 +2022,7 @@ be substituted. The equation always refers to the first :token:`d_item` in the actual tactic call, before any padding with initial ``_``. Thus, if an inductive type - has two family parameters, it is possible to have|SSR| generate an + has two family parameters, it is possible to have |SSR| generate an equation for the second one by omitting the pattern for the first; note however that this will fail if the type of the second parameter depends on the value of the first parameter. @@ -2320,7 +2320,7 @@ For instance, the tactic: tactic; do 1? rewrite mult_comm. rewrites at most one time the lemma ``mult_comm`` in all the subgoals -generated by tactic , whereas the tactic: +generated by tactic, whereas the tactic: .. coqdoc:: @@ -2511,7 +2511,7 @@ which behave like: have: term ; first by tactic. move=> clear_switch i_item. -Note that the :token:`clear_switch` *precedes* the:token:`i_item`, which +Note that the :token:`clear_switch` *precedes* the :token:`i_item`, which allows to reuse a name of the context, possibly used by the proof of the assumption, to introduce the new assumption itself. @@ -2783,7 +2783,7 @@ The + the order of the generated subgoals is inversed -+ but the optional clear item is still performed in the *second* ++ the optional clear item is still performed in the *second* branch. This means that the tactic: .. coqdoc:: @@ -2929,7 +2929,7 @@ facts. If an :token:`ident` is prefixed with the ``@`` mark, then a let-in redex is created, which keeps track if its body (if any). The syntax -``( ident := c_pattern)`` allows to generalize an arbitrary term using a +:n:`(@ident := @c_pattern)` allows to generalize an arbitrary term using a given name. Note that its simplest form ``(x := y)`` is just a renaming of ``y`` into ``x``. In particular, this can be useful in order to simulate the generalization of a section variable, otherwise not allowed. Indeed @@ -3917,7 +3917,7 @@ definitely want to avoid repeating large subterms of the goal in the proof script. We do this by “clamping down” selected function symbols in the goal, which prevents them from being considered in simplification or rewriting steps. This clamping is accomplished by -using the occurrence switches (see section:ref:`abbreviations_ssr`) +using the occurrence switches (see section :ref:`abbreviations_ssr`) together with “term tagging” operations. |SSR| provides two levels of tagging. @@ -4385,7 +4385,7 @@ Contextual patterns in rewrite Note: the simplification rule ``addSn`` is applied only under the ``f`` symbol. - Then we simplify also the first addition and expand 0 into 0+0. + Then we simplify also the first addition and expand ``0`` into ``0 + 0``. .. coqtop:: all @@ -4738,7 +4738,7 @@ Interpreting assumptions Interpreting an assumption in the context of a proof consists in applying to it a lemma before generalizing, and/or decomposing this assumption. For instance, with the extensive use of boolean reflection -(see section :ref:`views_and_reflection_ssr`.4), it is quite frequent +(see section :ref:`views_and_reflection_ssr`), it is quite frequent to need to decompose the logical interpretation of (the boolean expression of) a fact, rather than the fact itself. This can be achieved by a combination of ``move : _ => _`` switches, like in the @@ -5201,7 +5201,7 @@ There are three steps in the behavior of an assumption view tactic: For a ``case/term`` tactic, the generalisation step is replaced by a case analysis step. -*View hints* are declared by the user (see section:ref:`views_and_reflection_ssr`.8) and are +*View hints* are declared by the user (see section :ref:`views_and_reflection_ssr`) and are stored in the Hint View database. The proof engine automatically detects from the shape of the top assumption ``top`` and of the view lemma ``term`` provided to the tactic the appropriate view hint in the diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 6c32a4968c..eff70bdac5 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -15,6 +15,7 @@ could imagine extending it. # pylint: disable=too-few-public-methods +import os import re from itertools import chain from collections import defaultdict @@ -42,7 +43,7 @@ from .notations.parsing import ParseError from .notations.sphinx import sphinxify from .notations.plain import stringify_with_ellipses -PARSE_ERROR = """Parse error in notation! +PARSE_ERROR = """{}:{} Parse error in notation! Offending notation: {} Error message: {}""" @@ -53,14 +54,14 @@ def notation_to_sphinx(notation, source, line, rawtext=None): node.source, node.line = source, line return node except ParseError as e: - raise ExtensionError(PARSE_ERROR.format(notation, e.msg)) from e + raise ExtensionError(PARSE_ERROR.format(os.path.basename(source), line, notation, e.msg)) from e def notation_to_string(notation): """Parse notation and format it as a string with ellipses.""" try: return stringify_with_ellipses(notation) except ParseError as e: - raise ExtensionError(PARSE_ERROR.format(notation, e.msg)) from e + raise ExtensionError(PARSE_ERROR.format(os.path.basename(source), line, notation, e.msg)) from e def highlight_using_coqdoc(sentence): """Lex sentence using coqdoc, and yield inline nodes for each token""" @@ -426,7 +427,7 @@ class ProductionObject(CoqObject): def _render_signature(self, signature, signode): raise NotImplementedError(self) - SIG_ERROR = ("Invalid syntax in ``.. prodn::`` directive" + SIG_ERROR = ("{}: Invalid syntax in ``.. prodn::`` directive" + "\nExpected ``name ::= ...`` or ``name += ...``" + " (e.g. ``pattern += constr:(@ident)``)") @@ -434,11 +435,13 @@ class ProductionObject(CoqObject): nsplits = 2 parts = signature.split(maxsplit=nsplits) if len(parts) != 3: - raise ExtensionError(ProductionObject.SIG_ERROR) + loc = os.path.basename(get_node_location(signode)) + raise ExtensionError(ProductionObject.SIG_ERROR.format(loc)) lhs, op, rhs = (part.strip() for part in parts) if op not in ["::=", "+="]: - raise ExtensionError(ProductionObject.SIG_ERROR) + loc = os.path.basename(get_node_location(signode)) + raise ExtensionError(ProductionObject.SIG_ERROR.format(loc)) self._render_annotation(signode) @@ -681,7 +684,7 @@ class ExampleDirective(BaseAdmonition): class PreambleDirective(Directive): r"""A reST directive to include a TeX file. - Mostly useful to let MathJax know about `\def`s and `\newcommand`s. The + Mostly useful to let MathJax know about `\def`\s and `\newcommand`\s. The contents of the TeX file are wrapped in a math environment, as MathJax doesn't process LaTeX definitions otherwise. @@ -850,12 +853,12 @@ class CoqtopBlocksTransform(Transform): unexpected_options = list(options - {'all', 'none', 'in', 'out'}) if unexpected_options: - loc = get_node_location(node) + loc = os.path.basename(get_node_location(node)) raise ExtensionError("{}: Unexpected options for .. coqtop:: {}".format(loc,unexpected_options)) # Display options if len(options) != 1: - loc = get_node_location(node) + loc = os.path.basename(get_node_location(node)) raise ExtensionError("{}: Exactly one display option must be passed to .. coqtop::".format(loc)) opt_all = 'all' in options diff --git a/doc/tools/docgram/README.md b/doc/tools/docgram/README.md new file mode 100644 index 0000000000..98fdc38ca7 --- /dev/null +++ b/doc/tools/docgram/README.md @@ -0,0 +1,208 @@ +# Grammar extraction tool for documentation + +`doc_grammar` extracts Coq's grammar from `.mlg` files, edits it and inserts it in +chunks into `.rst` files. The tool currently inserts Sphinx +`productionlist` constructs. It also generates a file with `prodn` constructs +for the entire grammar, but updates to `tacn` and `cmd` constructs must be done +manually since the grammar doesn't have names for them as it does for +nonterminals. There is an option to report which `tacn` and `cmd` were not +found in the `.rst` files. `tacv` and `cmdv` constructs are not processed at all. + +The mlg grammars present several challenges to generating an accurate grammar +for documentation purposes: + +* The 30+ mlg files don't define an overall order in which nonterminals should + appear in a complete grammar. + +* Even within a single mlg file, nonterminals and productions are often given + in an order that's much different from what a reader of the documentation would + expect. In a small number of cases, changing the order in the mlg would change + how some inputs are parsed, in particular when the order determines how to distinguish + otherwise ambiguous inputs. + + Strictly speaking, that means our grammar is not a context free grammar even though + we gloss over that distinction in the documentation. + +* For a few nonterminals, some productions are only available if certain plugins + are activated (e.g. SSR). Readers should be informed about these. + +* Some limited parts of the grammar are defined in OCaml, including lookahead symbols + like `test_bracket_ident` and references to nonterminals in other files using + qualified names such as `Prim.ident`. A few symbols are defined multiple times, + such as `scope` and `orient`. + +## What the tool does + +1. The tool reads all the `mlg` files and generates `fullGrammar`, which includes +all the grammar without the actions for each production or the OCaml code. This +file is provided as a convenience to make it easier to examine the (mostly) +unprocessed grammar of the mlg files with less clutter. Nonterminals that use +levels (`"5" RIGHTA` below) are modified, for example: + +``` +tactic_expr: + [ "5" RIGHTA + [ te = binder_tactic -> { te } ] +``` + +becomes + +``` +tactic_expr5: [ +| binder_tactic +| tactic_expr4 +] +``` + +2. The tool applies grammar editing operations specified by `common.edit_mlg` to +generate `editedGrammar`. + +3. `orderedGrammar` gives the desired order for the nonterminals and productions +in the documented grammar. Developers should edit this file to change the order. +`doc_grammar` updates `orderedGrammar` so it has the same set of nonterminals and productions +as `editedGrammar`. The update process removes manually-added comments from +`orderedGrammar` while automatically-generated comments will be regenerated. + +4. The tool applies further edits to the grammar specified by `productionlist.edit_mlg`, +then it updates the productionlists in the `.rst` files as specified by comments in the form +`.. insertgram <first nt> <last nt>`. The edits are primarily to expand +`.mlg` constructs such as `LIST1` and `OPT` into separate productions. The tool +generates `productionlistGrammar`, which has the entire grammar in the form of `productionlists`. + +5. Using the grammar produced in step 3, the tool applies edits specified by +`prodn.edit_mlg` and generates `prodnGrammar`, representing each production as +a Sphinx `prodn` construct. Differently-edited grammars are used because `prodn` +can naturally represent `LIST1 x SEP ','` whereas that is awkward for `productionlists`. + +## How to use the tool + +* `make doc_gram` updates `fullGrammar`. + +* `make doc_gram_verify` verifies that `fullGrammar` is consistent with the `.mlg` files. + This is for use by CI. + +* `make doc_gram_rsts` updates the `*Grammar` and `.rst` files. + +Changes to `fullGrammar`, `orderedGrammar` and the `.rsts` should be checked in to git. +The other `*Grammar` files should not. + +### Command line arguments + +The executable takes a list of `.mlg` and `.rst` files as arguments. The tool +inserts the grammar into the `.rsts` as specified by comments in those files. +The order of the `.mlg` files affects the order of nonterminals and productions in +`fullGrammar`. The order doesn't matter for the `.rst` files. + +Specifying the `-verify` command line argument avoids updating any of the files, +but verifies that the current files are consistent. This setting is meant for +use in CI; it will be up to each developer to include the changes to `*Grammar` and +the `.rst` files in their PRs when they've changed the grammar. + +Other command line arguments: + +* `-check-tacs` reports on differences in tactics between the `rsts` and the grammar + +* `-check-cmds` reports on differences in commands between the `rsts` and the grammar + +* `-no-warn` suppresses printing of some warning messages + +* `-short` limits processing to updating/verifying only the `fullGrammar` file + +* `-verbose` prints more messages about the grammar + +* `-verify` described above + +### Grammar editing scripts + +The grammar editing scripts `*.edit_mlg` are similar in format to `.mlg` files stripped +of all OCaml features. This is an easy way to include productions to match or add without +writing another parser. The `DOC_GRAMMAR` token at the beginning of each file +signals the use of streamlined syntax. + +Each edit file has a series of items in the form of productions. Items are applied +in the order they appear. There are two types of editing operations: + +* Global edits - edit rules that apply to the entire grammar in a single operation. + These are identified by using specific reserved names as the non-terminal name. + +* Local edits - edit rules that apply to the productions of a single non-terminal. + The rule is a local edit if the non-terminal name isn't reserved. Individual + productions within a local edit that begin with a different set of reserved names + edit existing productions. For example `binders: [ | DELETE Pcoq.Constr.binders ]` + deletes the production `binders: [ | Pcoq.Constr.binders]` + +Productions that don't begin with a reserved name are added to the grammar, +such as `empty: [ | ]`, which adds a new non-terminal `empty` with an +empty production on the right-hand side. + +Another example: `LEFTQMARK: [ | "?" ]` is a local edit that treats `LEFTQMARK` as +the name of a non-terminal and adds one production for it. (We know that LEFTQMARK +is a token but doc_grammar does not.) `SPLICE: [ | LEFTQMARK ]` requests replacing all +uses of `LEFTQMARK` anywhere in the grammar with its productions and removing the +non-terminal. The combined effect of these two is to replace all uses of +`LEFTQMARK` with `"?"`. + +Here are the current operations. They are likely to be refined as we learn +what operations are most useful while we update the mlg files and documentation: + +### Global edits + +`DELETE` - deletes the specified non-terminals anywhere in the grammar. Each +should appear as a separate production. Useful for removing non-terminals that +only do lookahead that shouldn't be in the documentation. + +`RENAME` - each production specifies an (old name, new name) pair of +non-terminals to rename. + +`SPLICE` - requests replacing all uses of the nonterminals anywhere in the +grammar with its productions and removing the non-terminal. Each should appear +as a separate production. (Doesn't work recursively; splicing for both +`A: [ | B ]` and `B: [ | C ]` must be done in separate SPLICE operations.) + +`EXPAND` - expands LIST0, LIST1, LIST* ... SEP and OPT constructs into +new non-terminals + +### Local edits + +`DELETE <production>` - removes the specified production from the grammar + +`EDIT <production>` - modifies the specified production using the following tags +that appear in the specified production: + +* `USE_NT <name>` LIST* - extracts LIST* as new nonterminal with the specified + new non-terminal name + +* `ADD_OPT <grammar symbol>` - looks for a production that matches the specified + production **without** `<grammar_symbol>`. If found, both productions are + replaced with single production with `OPT <grammar_symbol>` + + The current version handles a single USE_NT or ADD_OPT per EDIT. + +* `REPLACE` - (2 sequential productions) - removes `<oldprod>` and + inserts `<newprod>` in its place. + +``` +| REPLACE <oldprod> +| WITH <newprod> +``` + +* (any other nonterminal name) - adds a new production (and possibly a new nonterminal) +to the grammar. + +### `.rst` file updates + +`doc_grammar` updates `.rst` files when it sees the following 3 lines + +``` +.. insertgram <start> <end> +.. productionlist:: XXX +``` + +The end of the existing `productionlist` is recognized by a blank line. + +### Other details + +The output identifies productions from plugins that aren't automatically loaded with +`(* XXX plugin *)` in grammar files and with `(XXX plugin)` in productionlists. +If desired, this mechanism could be extended to tag certain productions as deprecated, +perhaps in conjunction with a coqpp change. diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg new file mode 100644 index 0000000000..ea94e21ff3 --- /dev/null +++ b/doc/tools/docgram/common.edit_mlg @@ -0,0 +1,220 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \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) *) +(************************************************************************) + +(* Defines additional productions and edits for use in documentation. Not compiled into Coq *) + +DOC_GRAMMAR + +(* additional nts to be spliced *) + +LEFTQMARK: [ +| "?" +] + +SPLICE: [ +| LEFTQMARK +] + +hyp: [ +| var +] + +tactic_then_gen: [ +| EDIT ADD_OPT tactic_expr5 "|" tactic_then_gen +| EDIT ADD_OPT tactic_expr5 ".." tactic_then_last +] + +SPLICE: [ +| hyp +| identref +| pattern_ident (* depends on previous LEFTQMARK splice todo: improve *) +| constr_eval (* splices as multiple prods *) +| tactic_then_last (* todo: dependency on c.edit_mlg edit?? really useful? *) +| Prim.name +| ltac_selector +| Constr.ident +| tactic_then_locality (* todo: cleanup *) +| attribute_list +] + +RENAME: [ + (* map missing names for rhs *) +| _binders binders +| Constr.constr term +| Constr.constr_pattern constr_pattern +| Constr.global global +| Constr.lconstr lconstr +| Constr.lconstr_pattern lconstr_pattern +| G_vernac.query_command query_command +| G_vernac.section_subset_expr section_subset_expr +| nonsimple_intropattern intropattern +| Pltac.tactic tactic +| Pltac.tactic_expr ltac_expr +| Prim.ident ident +| Prim.reference reference +| Pvernac.Vernac_.main_entry vernac_control +| Tactic.tactic tactic +| tactic3 ltac_expr3 (* todo: can't figure out how this gets mapped by coqpp *) +| tactic1 ltac_expr1 (* todo: can't figure out how this gets mapped by coqpp *) +| tactic0 ltac_expr0 (* todo: can't figure out how this gets mapped by coqpp *) +| tactic_expr5 ltac_expr +| tactic_expr4 ltac_expr4 +| tactic_expr3 ltac_expr3 +| tactic_expr2 ltac_expr2 +| tactic_expr1 ltac_expr1 +| tactic_expr0 ltac_expr0 + + (* elementary renaming/OCaml-defined productions *) +| clause clause_dft_concl +| in_clause' in_clause +| l_constr lconstr (* todo: should delete the production *) + + (* SSR *) +| G_vernac.def_body def_body +| Pcoq.Constr.constr term +| Prim.by_notation by_notation +| Prim.identref ident +| Prim.natural natural +| Vernac.rec_definition rec_definition + + (* rename on lhs *) +| intropatterns intropattern_list_opt +| Constr.closed_binder closed_binder + + (* historical name *) +| constr term +] + +DELETE: [ +| check_for_coloneq +| impl_ident_head +| local_test_lpar_id_colon +| lookup_at_as_comma +| only_starredidentrefs +| test_bracket_ident +| test_lpar_id_coloneq +| test_lpar_id_rpar +| test_lpar_idnum_coloneq +| test_show_goal + + (* SSR *) +(* | ssr_null_entry *) +| ssrtermkind (* todo: rename as "test..." *) +| term_annotation (* todo: rename as "test..." *) +| test_idcomma +| test_nohidden +| test_not_ssrslashnum +| test_ssr_rw_syntax +| test_ssreqid +| test_ssrfwdid +| test_ssrseqvar +| test_ssrslashnum00 +| test_ssrslashnum01 +| test_ssrslashnum10 +| test_ssrslashnum11 +| test_ident_no_do +| ssrdoarg (* todo: this and the next one should be removed from the grammar? *) +| ssrseqdir +] + +ident: [ +| DELETE IDENT ssr_null_entry +] + +natural: [ +| DELETE _natural +] + + + (* added productions *) + +empty: [ (* todo: (bug) this is getting converted to empty -> empty *) +| +] + +lpar_id_coloneq: [ +| "(" IDENT; ":=" +] + +name_colon: [ +| IDENT; ":" +| "_" ":" (* todo: should "_" be a keyword or an identifier? *) +] + +int: [ (* todo: probably should be NUMERAL *) +| integer +] + +command_entry: [ +| noedit_mode +] + +binders: [ +| DELETE Pcoq.Constr.binders (* todo: not sure why there are 2 "binders:" *) +] + +(* edits to simplify *) + +ltac_expr1: [ +| EDIT match_key ADD_OPT "reverse" "goal" "with" match_context_list "end" +] + +match_context_list: [ +| EDIT ADD_OPT "|" LIST1 match_context_rule SEP "|" +] + +match_hyps: [ +| REPLACE name ":=" "[" match_pattern "]" ":" match_pattern +| WITH name ":=" OPT ("[" match_pattern "]" ":") match_pattern +| DELETE name ":=" match_pattern +] + +match_list: [ +| EDIT ADD_OPT "|" LIST1 match_rule SEP "|" +] + + +selector_body: [ +| REPLACE range_selector_or_nth (* depends on whether range_selector_or_nth is deleted first *) +| WITH LIST1 range_selector SEP "," +] + +range_selector_or_nth: [ +| DELETENT +] + +simple_tactic: [ +| DELETE "intros" +| REPLACE "intros" ne_intropatterns +| WITH "intros" intropattern_list_opt +| DELETE "eintros" +| REPLACE "eintros" ne_intropatterns +| WITH "eintros" intropattern_list_opt +] + +intropattern_list_opt: [ +| DELETE LIST0 intropattern +| intropattern_list_opt intropattern +| empty +] + + +ne_intropatterns: [ +| DELETENT (* todo: don't use DELETENT for this *) +] + + +or_and_intropattern: [ +| DELETE "()" +| DELETE "(" simple_intropattern ")" +| REPLACE "(" simple_intropattern "," LIST1 simple_intropattern SEP "," ")" +| WITH "(" LIST0 simple_intropattern SEP "," ")" +| EDIT "[" USE_NT intropattern_or LIST1 intropattern_list_opt SEP "|" "]" +] diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml new file mode 100644 index 0000000000..9f0a1942f9 --- /dev/null +++ b/doc/tools/docgram/doc_grammar.ml @@ -0,0 +1,1572 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \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) *) +(************************************************************************) + +open Coqpp_parser +open Coqpp_ast + +let exit_code = ref 0 +let show_warn = ref true + +let fprintf = Printf.fprintf + +let error s = + exit_code := 1; + Printf.eprintf "Error: "; + Printf.eprintf s + +(* todo: checking if !show_warn is true here gives a compilation error *) +let warn s = + Printf.eprintf "Warning: "; + Printf.eprintf s + +type args = { + mlg_files : string list; + rst_files : string list; + fullGrammar : bool; + check_tacs : bool; + check_cmds : bool; + show_warn : bool; + verbose : bool; + verify : bool; +} + +let default_args = { + mlg_files = []; + rst_files = []; + fullGrammar = false; + check_tacs = false; + check_cmds = false; + show_warn = true; + verbose = false; + verify = false; +} + +(* translated symbols *) + +type doc_symbol = +| Sterm of string +| Snterm of string +| Slist1 of doc_symbol +| Slist1sep of doc_symbol * doc_symbol +| Slist0 of doc_symbol +| Slist0sep of doc_symbol * doc_symbol +| Sopt of doc_symbol +| Sparen of doc_symbol list (* for GRAMMAR EXTEND *) +| Sprod of doc_symbol list list (* for GRAMMAR EXTEND *) + (* editing operations *) +| Sedit of string +| Sedit2 of string * string + +(* nonterminals to rename or delete *) +module StringMap = Map.Make(String) +module NTMap = StringMap +module StringSet = Set.Make(String) + +type gram = { + (* map from nonterminal name to a list of prods *) + (* each production is a list of doc_symbol *) + map: doc_symbol list list NTMap.t; + (* specifies the order for nt's *) + order: string list; +} + +module DocGram = struct + (* these guarantee that order and map have a 1-1 relationship + on the nt name. They don't guarantee that nts on rhs of a production + are defined, nor do they prohibit duplicate productions *) + + exception Duplicate + exception Invalid + + (* add an nt at the end (if not already present) then set its prods *) + let g_maybe_add g nt prods = + if not (NTMap.mem nt !g.map) then + g := { !g with order = !g.order @ [nt] }; + g := { !g with map = NTMap.add nt prods !g.map } + + (* add an nt at the beginning (if not already present) then set its prods *) + let g_maybe_add_begin g nt prods = + if not (NTMap.mem nt !g.map) then + g := { !g with order = nt :: !g.order }; + g := { !g with map = NTMap.add nt prods !g.map } + + (* reverse the order of the grammar *) + let g_reverse g = + g := { !g with order = List.rev !g.order } + + (* update the productions of an existing nt *) + let g_update_prods g nt prods = + ignore (NTMap.find nt !g.map); (* don't add the nt if it's not present *) + g := { !g with map = NTMap.add nt prods !g.map } + + (* remove a non-terminal *) + let g_remove g nt = + g := { map = NTMap.remove nt !g.map; + order = List.filter (fun elt -> elt <> nt) !g.order } + + (* rename an nt and update its prods, keeping its original position. + If the new name already exists, include its prods *) + let g_rename_merge g nt nt' nprods = + let oprods = + try + let oprods = NTMap.find nt' !g.map in + g := { !g with order = List.filter (fun elt -> elt <> nt') !g.order }; + oprods + with Not_found -> + g := { !g with map = NTMap.add nt' [] !g.map }; + [] + in + g := { map = NTMap.remove nt !g.map; + order = List.map (fun n -> if n = nt then nt' else n) !g.order }; + g_update_prods g nt' (oprods @ nprods) + + (* add a new nonterminal after "ins_after" None means insert at the beginning *) + let g_add_after g ins_after nt prods = + if NTMap.mem nt !g.map then raise Duplicate; (* don't update the nt if it's already present *) + let rec insert_nt order res = + match ins_after, order with + | None, _ -> nt :: order + | Some _, [] -> raise Not_found + | Some ins_after_nt, hd :: tl -> + if hd = ins_after_nt then + (List.rev res) @ (hd :: nt :: tl) + else + insert_nt tl (hd :: res) + in + g := { order = insert_nt !g.order []; + map = NTMap.add nt prods !g.map } + + (* replace the map and order *) + let g_reorder g map order = + let order_nts = StringSet.of_list order in + let map_nts = List.fold_left (fun res b -> let (nt, _) = b in StringSet.add nt res) + StringSet.empty (NTMap.bindings map) in + if List.length order <> NTMap.cardinal map || + not (StringSet.equal order_nts map_nts) then raise Invalid; + g := { order = order; map = map } + +end +open DocGram + +(*** Print routines ***) + +let sprintf = Printf.sprintf + +let map_and_concat f ?(delim="") l = + String.concat delim (List.map f l) + +let rec db_output_prodn = function + | Sterm s -> sprintf "(Sterm %s) " s + | Snterm s -> sprintf "(Snterm %s) " s + | Slist1 sym -> sprintf "(Slist1 %s) " (db_output_prodn sym) + | Slist1sep (sym, sep) -> sprintf "(Slist1sep %s %s) " (db_output_prodn sep) (db_output_prodn sym) + | Slist0 sym -> sprintf "(Slist0 %s) " (db_output_prodn sym) + | Slist0sep (sym, sep) -> sprintf "(Slist0sep %s %s) " (db_output_prodn sep) (db_output_prodn sym) + | Sopt sym -> sprintf "(Sopt %s) " (db_output_prodn sym) + | Sparen prod -> sprintf "(Sparen %s) " (db_out_list prod) + | Sprod prods -> sprintf "(Sprod %s) " (db_out_prods prods) + | Sedit s -> sprintf "(Sedit %s) " s + | Sedit2 (s, s2) -> sprintf "(Sedit2 %s %s) " s s2 +and db_out_list prod = sprintf "(%s)" (map_and_concat db_output_prodn prod) +and db_out_prods prods = sprintf "( %s )" (map_and_concat ~delim:" | " db_out_list prods) + +let rec output_prod plist need_semi = function + | Sterm s -> if plist then sprintf "%s" s else sprintf "\"%s\"" s + | Snterm s -> + if plist then sprintf "`%s`" s else + sprintf "%s%s" s (if s = "IDENT" && need_semi then ";" else "") + | Slist1 sym -> sprintf "LIST1 %s" (prod_to_str ~plist [sym]) + | Slist1sep (sym, sep) -> sprintf "LIST1 %s SEP %s" (prod_to_str ~plist [sym]) (prod_to_str ~plist [sep]) + | Slist0 sym -> sprintf "LIST0 %s" (prod_to_str ~plist [sym]) + | Slist0sep (sym, sep) -> sprintf "LIST0 %s SEP %s" (prod_to_str ~plist [sym]) (prod_to_str ~plist [sep]) + | Sopt sym -> sprintf "OPT %s" (prod_to_str ~plist [sym]) + | Sparen sym_list -> sprintf "( %s )" (prod_to_str sym_list) + | Sprod sym_list -> + sprintf "[ %s ]" (String.concat " " (List.mapi (fun i r -> + let prod = (prod_to_str r) in + let sep = if i = 0 then "" else + if prod <> "" then "| " else "|" in + sprintf "%s%s" sep prod) + sym_list)) + | Sedit s -> sprintf "%s" s + (* todo: make PLUGIN info output conditional on the set of prods? *) + | Sedit2 ("PLUGIN", plugin) -> + if plist then + sprintf " (%s plugin)" plugin + else + sprintf " (* %s plugin *)" plugin + | Sedit2 ("FILE", file) -> + let file_suffix_regex = Str.regexp ".*/\\([a-zA-Z0-9_\\.]+\\)" in + let suffix = if Str.string_match file_suffix_regex file 0 then Str.matched_group 1 file else file in + if plist then + sprintf " (%s)" suffix + else + sprintf " (* %s *)" suffix + | Sedit2 (s, s2) -> sprintf "%s \"%s\"" s s2 + +and prod_to_str_r plist prod = + match prod with + | p :: tl -> + let need_semi = + match prod with + | Snterm "IDENT" :: Sterm _ :: _ + | Snterm "IDENT" :: Sprod _ :: _ -> true + | _ -> false in + (output_prod plist need_semi p) :: (prod_to_str_r plist tl) + | [] -> [] + +and prod_to_str ?(plist=false) prod = + String.concat " " (prod_to_str_r plist prod) + + +let rec output_prodn = function + | Sterm s -> let s = if List.mem s ["{"; "{|"; "|"; "}"] then "%" ^ s else s in + sprintf "%s" s + | Snterm s -> sprintf "@%s" s + | Slist1 sym -> sprintf "{+ %s }" (output_prodn sym) + | Slist1sep (sym, sep) -> sprintf "{+%s %s }" (output_sep sep) (output_prodn sym) + | Slist0 sym -> sprintf "{* %s }" (output_prodn sym) + | Slist0sep (sym, sep) -> sprintf "{*%s %s }" (output_sep sep) (output_prodn sym) + | Sopt sym -> sprintf "{? %s }" (output_prodn sym) + | Sparen sym_list -> sprintf "%s" (prod_to_prodn sym_list) + | Sprod sym_list -> + let lcurly, rcurly = if List.length sym_list = 1 then "", "" else "{| ", " }" in + sprintf "%s%s%s" + lcurly + (String.concat " " (List.mapi (fun i r -> + let prod = (prod_to_prodn r) in + let sep = if i = 0 then "" else + if prod <> "" then "| " else "|" in + sprintf "%s%s" sep prod) + sym_list)) + rcurly + | Sedit s -> sprintf "%s" s + | Sedit2 ("PLUGIN", s2) -> "" + | Sedit2 (s, s2) -> sprintf "%s \"%s\"" s s2 + +and output_sep sep = + match sep with + | Sterm s -> sprintf "%s" s (* avoid escaping separator *) + | _ -> output_prodn sep + +and prod_to_prodn prod = String.concat " " (List.map output_prodn prod) + +type fmt = [`MLG | `PRODLIST | `PRODN ] + +(* print a subset of the grammar with nts in the specified order *) +let print_in_order out g fmt nt_order hide = + List.iter (fun nt -> + if not (StringSet.mem nt hide) then + try + let prods = NTMap.find nt !g.map in + match fmt with + | `MLG -> + fprintf out "%s: [\n" nt; + List.iter (fun prod -> + let str = prod_to_str ~plist:false prod in + let pfx = if str = "" then "|" else "| " in + fprintf out "%s%s\n" pfx str) + prods; + fprintf out "]\n\n" + | `PRODLIST -> + fprintf out "%s :" nt; + List.iteri (fun i prod -> + if i > 0 then + fprintf out "%s :" (String.make (String.length nt) ' '); + let str = prod_to_str ~plist:true prod in + let pfx = if str = "" then "" else " " in + fprintf out "%s%s\n" pfx str) + prods; + | `PRODN -> + fprintf out "\n%s:\n" nt; + List.iter (fun prod -> + let str = prod_to_prodn prod in + let pfx = if str = "" then "" else " " in + fprintf out "%s%s\n" pfx str) + prods; + with Not_found -> error "Missing nt '%s' in print_in_order\n" nt) + nt_order + + +(*** Read grammar routines ***) + +let cvt_ext prod = + let rec to_doc_sym = function + | Ulist1 sym -> Slist1 (to_doc_sym sym) + | Ulist1sep (sym, s) -> Slist1sep ((to_doc_sym sym), Sterm s) + | Ulist0 sym -> Slist0 (to_doc_sym sym) + | Ulist0sep (sym, s) -> Slist0sep ((to_doc_sym sym), Sterm s) + | Uopt sym -> Sopt (to_doc_sym sym) + | Uentry s -> Snterm s + | Uentryl (s, i) -> Snterm (s ^ (string_of_int i)) + in + let from_ext = function + | ExtTerminal s -> Sterm s + | ExtNonTerminal (s, _) -> to_doc_sym s + in + List.map from_ext prod + +let rec cvt_gram_sym = function + | GSymbString s -> Sterm s + | GSymbQualid (s, level) -> + Snterm (match level with + | Some str -> s ^ str + | None -> s) + | GSymbParen l -> Sparen (cvt_gram_sym_list l) + | GSymbProd ll -> + let cvt = List.map cvt_gram_prod ll in + (match cvt with + | (Snterm x :: []) :: [] -> Snterm x + | (Sterm x :: []) :: [] -> Sterm x + | _ -> Sprod cvt) + +and cvt_gram_sym_list l = + let get_sym = function + | GSymbQualid (s, level) -> s + | _ -> "" + in + + match l with + | GSymbQualid ("LIST0", _) :: s :: GSymbQualid ("SEP", _) :: sep :: tl -> + Slist0sep (cvt_gram_sym s, cvt_gram_sym sep) :: cvt_gram_sym_list tl + | GSymbQualid ("LIST1", _) :: s :: GSymbQualid ("SEP", _) :: sep :: tl -> + Slist1sep (cvt_gram_sym s, cvt_gram_sym sep) :: cvt_gram_sym_list tl + | GSymbQualid ("LIST0", _) :: s :: tl -> + Slist0 (cvt_gram_sym s) :: cvt_gram_sym_list tl + | GSymbQualid ("LIST1", _) :: s :: tl -> + Slist1 (cvt_gram_sym s) :: cvt_gram_sym_list tl + | GSymbQualid ("OPT", _) :: s :: tl -> + Sopt (cvt_gram_sym s) :: cvt_gram_sym_list tl + | GSymbQualid ("IDENT", _) :: s2 :: tl when get_sym s2 = "" -> + cvt_gram_sym s2 :: cvt_gram_sym_list tl + | GSymbQualid ("ADD_OPT", _) :: tl -> + (Sedit "ADD_OPT") :: cvt_gram_sym_list tl + | GSymbQualid ("NOTE", _) :: GSymbQualid (s2, l) :: tl -> + (Sedit2 ("NOTE", s2)) :: cvt_gram_sym_list tl + | GSymbQualid ("USE_NT", _) :: GSymbQualid (s2, l) :: tl -> + (Sedit2 ("USE_NT", s2)) :: cvt_gram_sym_list tl + | hd :: tl -> + cvt_gram_sym hd :: cvt_gram_sym_list tl + | [] -> [] + +and cvt_gram_prod p = + List.concat (List.map (fun x -> let _, gs = x in cvt_gram_sym_list gs) p.gprod_symbs) + + +let add_symdef nt file symdef_map = + let ent = + try + StringMap.find nt !symdef_map + with Not_found -> [] + in + symdef_map := StringMap.add nt (Filename.basename file::ent) !symdef_map + +let rec edit_SELF nt cur_level next_level right_assoc prod = + let len = List.length prod in + List.mapi (fun i sym -> + match sym with + | Snterm s -> begin match s with + | s when s = nt || s = "SELF" -> + if i = 0 then Snterm next_level + else if i+1 < len then sym + else if right_assoc then Snterm cur_level else Snterm next_level + | "NEXT" -> Snterm next_level + | _ -> sym + end + | Slist1 sym -> Slist1 (List.hd (edit_SELF nt cur_level next_level right_assoc [sym])) + | Slist0 sym -> Slist0 (List.hd (edit_SELF nt cur_level next_level right_assoc [sym])) + | x -> x) + prod + + +let autoloaded_mlgs = [ (* in the order they are loaded by Coq *) + "parsing/g_constr.mlg"; + "parsing/g_prim.mlg"; + "vernac/g_vernac.mlg"; + "vernac/g_proofs.mlg"; + "toplevel/g_toplevel.mlg"; + "plugins/ltac/extraargs.mlg"; + "plugins/ltac/g_obligations.mlg"; + "plugins/ltac/coretactics.mlg"; + "plugins/ltac/extratactics.mlg"; + "plugins/ltac/profile_ltac_tactics.mlg"; + "plugins/ltac/g_auto.mlg"; + "plugins/ltac/g_class.mlg"; + "plugins/ltac/g_rewrite.mlg"; + "plugins/ltac/g_eqdecide.mlg"; + "plugins/ltac/g_tactic.mlg"; + "plugins/ltac/g_ltac.mlg"; + "plugins/syntax/g_string.mlg"; + "plugins/btauto/g_btauto.mlg"; + "plugins/rtauto/g_rtauto.mlg"; + "plugins/cc/g_congruence.mlg"; + "plugins/firstorder/g_ground.mlg"; + "plugins/syntax/g_numeral.mlg"; +] + + +let ematch prod edit = + let rec ematchr prod edit = + (*Printf.printf "%s and\n %s\n\n" (prod_to_str prod) (prod_to_str edit);*) + match (prod, edit) with + | (_, Sedit _ :: tl) + | (_, Sedit2 _ :: tl) + -> ematchr prod tl + | (Sedit _ :: tl, _) + | (Sedit2 _ :: tl, _) + -> ematchr tl edit + | (phd :: ptl, hd :: tl) -> + let m = match (phd, hd) with + | (Slist1 psym, Slist1 sym) + | (Slist0 psym, Slist0 sym) + | (Sopt psym, Sopt sym) + -> ematchr [psym] [sym] + | (Slist1sep (psym, psep), Slist1sep (sym, sep)) + | (Slist0sep (psym, psep), Slist0sep (sym, sep)) + -> ematchr [psym] [sym] && ematchr [psep] [sep] + | (Sparen psyml, Sparen syml) + -> ematchr psyml syml + | (Sprod psymll, Sprod symll) + -> List.fold_left (&&) true (List.map2 ematchr psymll symll) + | _, _ -> phd = hd + in + m && ematchr ptl tl + | ([], hd :: tl) -> false + | (phd :: ptl, []) -> false + | ([], []) -> true +in + (*Printf.printf "\n";*) + let rv = ematchr prod edit in + (*Printf.printf "%b\n" rv;*) + rv + +let has_match p prods = List.exists (fun p2 -> ematch p p2) prods + +let plugin_regex = Str.regexp "^plugins/\\([a-zA-Z0-9_]+\\)/" + +let read_mlg is_edit ast file level_renames symdef_map = + let res = ref [] in + let add_prods nt prods = + if not is_edit then + add_symdef nt file symdef_map; + let prods = if not is_edit && + not (List.mem file autoloaded_mlgs) && + Str.string_match plugin_regex file 0 then + let plugin = Str.matched_group 1 file in + List.map (fun p -> p @ [Sedit2 ("PLUGIN", plugin)]) prods + else + prods + in + (* todo: doesn't yet work perfectly with SPLICE *) +(* let prods = if not is_edit then List.map (fun p -> p @ [Sedit2 ("FILE", file)]) prods else prods in*) + res := (nt, prods) :: !res + in + let prod_loop = function + | GramExt grammar_ext -> + let get_label = function + | Some s -> s + | None -> "" + in + List.iter (fun ent -> + let len = List.length ent.gentry_rules in + List.iteri (fun i rule -> + let nt = ent.gentry_name in + let level = (get_label rule.grule_label) in + let level = if level <> "" then level else + match ent.gentry_pos with + | Some Level lev + | Some Before lev + | Some After lev + -> lev + (* Looks like FIRST/LAST can be ignored for documenting the current grammar *) + | _ -> "" in + let cur_level = nt ^ level in + let next_level = nt ^ + if i+1 < len then (get_label (List.nth ent.gentry_rules (i+1)).grule_label) else "" in + let right_assoc = (rule.grule_assoc = Some RightA) in + + if i = 0 && cur_level <> nt && not (StringMap.mem nt !level_renames) then begin + level_renames := StringMap.add nt cur_level !level_renames; + end; + let cvted = List.map cvt_gram_prod rule.grule_prods in + (* edit names for levels *) + (* See https://camlp5.github.io/doc/html/grammars.html#b:Associativity *) + let edited = List.map (edit_SELF nt cur_level next_level right_assoc) cvted in + let prods_to_add = + if cur_level <> nt && i+1 < len then + edited @ [[Snterm next_level]] + else + edited in + add_prods cur_level prods_to_add) + ent.gentry_rules + ) grammar_ext.gramext_entries + + | VernacExt vernac_ext -> + let node = match vernac_ext.vernacext_entry with + | None -> "command" + | Some c -> String.trim c.code + in + add_prods node + (List.map (fun r -> cvt_ext r.vernac_toks) vernac_ext.vernacext_rules) + | VernacArgumentExt vernac_argument_ext -> + add_prods vernac_argument_ext.vernacargext_name + (List.map (fun r -> cvt_ext r.tac_toks) vernac_argument_ext.vernacargext_rules) + | TacticExt tactic_ext -> + add_prods "simple_tactic" + (List.map (fun r -> cvt_ext r.tac_toks) tactic_ext.tacext_rules) + | ArgumentExt argument_ext -> + add_prods argument_ext.argext_name + (List.map (fun r -> cvt_ext r.tac_toks) argument_ext.argext_rules) + | _ -> () + in + + List.iter prod_loop ast; + List.rev !res + +let dir s = "doc/tools/docgram/" ^ s + +let read_mlg_edit file = + let fdir = dir file in + let level_renames = ref StringMap.empty in (* ignored *) + let symdef_map = ref StringMap.empty in (* ignored *) + read_mlg true (parse_file fdir) fdir level_renames symdef_map + +let add_rule g nt prods file = + let ent = try NTMap.find nt !g.map with Not_found -> [] in + let nodups = List.concat (List.map (fun prod -> + if has_match prod ent then begin + if !show_warn then + warn "%s: Duplicate production '%s: %s'\n" file nt (prod_to_str prod); + [] + end else + [prod]) + prods) in + g_maybe_add_begin g nt (ent @ nodups) + +let read_mlg_files g args symdef_map = + let level_renames = ref StringMap.empty in + let last_autoloaded = List.hd (List.rev autoloaded_mlgs) in + List.iter (fun file -> + (* does nt renaming, deletion and splicing *) + let rules = read_mlg false (parse_file file) file level_renames symdef_map in + let numprods = List.fold_left (fun num rule -> + let nt, prods = rule in + add_rule g nt prods file; + num + List.length prods) + 0 rules + in + if args.verbose then begin + Printf.eprintf "%s: %d nts, %d prods\n" file (List.length rules) numprods; + if file = last_autoloaded then + Printf.eprintf " Optionally loaded plugins:\n" + end + ) args.mlg_files; + g_reverse g; + !level_renames + + +(*** global editing ops ***) + +let create_edit_map edits = + let rec aux edits map = + match edits with + | [] -> map + | edit :: tl -> + let (key, binding) = edit in + aux tl (StringMap.add key binding map) + in + aux edits StringMap.empty + +(* edit a production: rename nonterminals, drop nonterminals, substitute nonterminals *) +let rec edit_prod g top edit_map prod = + let edit_nt edit_map sym0 nt = + try + let binding = StringMap.find nt edit_map in + match binding with + | "DELETE" -> [] + | "SPLICE" -> + begin + try let splice_prods = NTMap.find nt !g.map in + match splice_prods with + | [] -> assert false + | [p] -> List.rev p + | _ -> [Sprod splice_prods] + with Not_found -> error "Missing nt '%s' for splice\n" nt; [Snterm nt] + end + | _ -> [Snterm binding] + with Not_found -> [sym0] + in + + let rec edit_symbol sym0 = + match sym0 with + | Sterm s -> [sym0] + | Snterm s -> edit_nt edit_map sym0 s + | Slist1 sym -> [Slist1 (List.hd (edit_symbol sym))] + (* you'll get a run-time failure deleting a SEP symbol *) + | Slist1sep (sym, sep) -> [Slist1sep (List.hd (edit_symbol sym), (List.hd (edit_symbol sep)))] + | Slist0 sym -> [Slist0 (List.hd (edit_symbol sym))] + | Slist0sep (sym, sep) -> [Slist0sep (List.hd (edit_symbol sym), (List.hd (edit_symbol sep)))] + | Sopt sym -> [Sopt (List.hd (edit_symbol sym))] + | Sparen slist -> [Sparen (List.hd (edit_prod g false edit_map slist))] + | Sprod slistlist -> let (_, prods) = edit_rule g edit_map "" slistlist in + [Sprod prods] + | Sedit _ + | Sedit2 _ -> [sym0] (* these constructors not used here *) + in + let is_splice nt = + try + StringMap.find nt edit_map = "SPLICE" + with Not_found -> false + in + let get_splice_prods nt = + try NTMap.find nt !g.map + with Not_found -> (error "Missing nt '%s' for splice\n" nt; []) + in + + (* special case splice creating multiple new productions *) + let splice_prods = match prod with + | Snterm nt :: [] when is_splice nt -> + get_splice_prods nt + | _ -> [] + in + if top && splice_prods <> [] then + splice_prods + else + [List.rev (List.concat (List.rev (List.map (fun sym -> edit_symbol sym) prod)))] + +and edit_rule g edit_map nt rule = + let nt = + try let new_name = StringMap.find nt edit_map in + match new_name with + | "SPLICE" -> nt + | "DELETE" -> "" + | _ -> new_name + with Not_found -> nt + in + (nt, (List.concat (List.map (edit_prod g true edit_map) rule))) + +(*** splice: replace a reference to a nonterminal with its definition ***) + +(* todo: create a better splice routine, handle recursive case *) +let apply_splice g splice_map = + StringMap.iter (fun nt b -> + if not (NTMap.mem nt !g.map) then + error "Unknown nt '%s' for apply_splice\n" nt) + splice_map; + List.iter (fun b -> + let (nt, prods) = b in + let (nt', prods) = edit_rule g splice_map nt prods in + g_update_prods g nt' prods) + (NTMap.bindings !g.map); + List.iter (fun b -> + let (nt, op) = b in + match op with + | "DELETE" + | "SPLICE" -> + g_remove g nt; + | _ -> ()) + (StringMap.bindings splice_map) + +let find_first edit prods nt = + let rec find_first_r edit prods nt i = + match prods with + | [] -> + error "Can't find '%s' in REPLACE for '%s'\n" (prod_to_str edit) nt; + raise Not_found + | prod :: tl -> + if ematch prod edit then i + else find_first_r edit tl nt (i+1) + in + find_first_r edit prods nt 0 + +let remove_prod edit prods nt = + let res, got_first = List.fold_left (fun args prod -> + let res, got_first = args in + if not got_first && ematch prod edit then + res, true + else + prod :: res, got_first) + ([], false) prods in + if not got_first then + error "Can't find '%s' to DELETE for '%s'\n" (prod_to_str edit) nt; + List.rev res + +let insert_after posn insert prods = + List.concat (List.mapi (fun i prod -> + if i = posn then prod :: insert else [prod]) + prods) + +(*** replace LIST*, OPT with new nonterminals ***) + +(* generate a non-terminal name for a replacement *) +let nt_regex = Str.regexp "^[a-zA-Z_][a-zA-Z0-9_\\.]*$" +let good_name name = if Str.string_match nt_regex name 0 then name else "" +let map_name s = + let s = match s with + | "|" -> "or" + | "!" -> "exclam" + | ">" -> "gt" + | "<" -> "lt" + | "+" -> "plus" + | "?" -> "qmark" + | "}" -> "rbrace" + | "," -> "comma" + | ";" -> "semi" + | _ -> s + in + good_name s + +let rec gen_nt_name sym = + let name_from_prod prod = + let rec aux name sterm_name prod = + if name <> "" then name else + match prod with + | [] -> sterm_name + | Sterm s :: tl + | Snterm s :: tl -> + if good_name s <> "" then + aux (map_name s) sterm_name tl + else + aux name (map_name s) tl; + | sym :: tl-> + aux (gen_nt_name sym) sterm_name tl + in + aux "" "" prod + in + + let name = match sym with + | Sterm s -> map_name s + | Snterm s -> s + | Slist1 sym + | Slist1sep (sym, _) + | Slist0 sym + | Slist0sep (sym, _) + | Sopt sym -> + gen_nt_name sym + | Sparen slist -> + name_from_prod slist + | Sprod slistlist -> + name_from_prod (List.hd slistlist) + | _ -> "" + in + good_name name + +(* create a new nt for LIST* or OPT with the specified name *) +let rec maybe_add_nt g insert_after name sym queue = + let empty = [Snterm "empty"] in + let maybe_unwrap ?(multi=false) sym = + match sym with + | Sprod slist when List.length slist = 1 || multi + -> slist + | Sparen slist -> [ slist ] + | _ -> [ [sym] ] + in + let unw sym = List.hd (maybe_unwrap sym) in + let get_prods nt = + match sym with + | Slist1 sym -> let sym' = unw sym in + [ [Snterm nt] @ sym'; sym' ] + | Slist1sep (sym, sep) + | Slist0sep (sym, sep) -> let sym' = unw sym in + [ [Snterm nt; sep] @ sym'; sym' ] + | Slist0 sym -> [ [Snterm nt] @ (unw sym); empty ] + | Sopt sym -> (maybe_unwrap ~multi:true sym) @ [ empty ] + | Sprod slistlist -> slistlist + | _ -> [] + in + + let is_slist0sep sym = + match sym with + | Slist0sep _ -> true + | _ -> false + in + + (* find an existing nt with an identical definition, or generate an unused nt name *) + let rec find_name nt i = + let trial_name = sprintf "%s%s" nt (if i = 1 then "" else string_of_int i) in + try + if NTMap.find trial_name !g.map = get_prods trial_name then + trial_name + else + find_name nt (succ i) + with Not_found -> trial_name + in + let list_name sep = + match sep with + | Sterm s -> + let name = map_name s in + if name = s then "_list" else "_list_" ^ name + | _ -> "_list" + in + let nt = name ^ match sym with + | Slist1 sym -> "_list" + | Slist1sep (sym, sep) -> list_name sep + | Slist0 sym -> "_list_opt" + | Slist0sep (sym, sep) -> list_name sep (* special handling *) + | Sopt sym -> "_opt" + | Sprod slistlist -> "_alt" + | _ -> (error "Invalid symbol for USE_NT for nt '%s'\n" name; "ERROR") + in + let base_nt = find_name nt 1 in + let new_nt = if is_slist0sep sym then base_nt ^ "_opt" else base_nt in + if not (NTMap.mem new_nt !g.map) then begin + let prods = if is_slist0sep sym then [ [Snterm base_nt]; empty ] else get_prods base_nt in + g_add_after g (Some !insert_after) new_nt prods; + insert_after := new_nt; + Queue.add new_nt queue + end; + if is_slist0sep sym && not (NTMap.mem base_nt !g.map) then begin + match sym with + | Slist0sep (sym, sep) -> + let prods = get_prods base_nt in + g_add_after g (Some !insert_after) base_nt prods; + insert_after := base_nt; + Queue.add base_nt queue + | _ -> () + end; + new_nt + +(* expand LIST*, OPT and add "empty" *) +(* todo: doesn't handle recursive expansions well, such as syntax_modifier_opt *) +and expand_rule g edited_nt queue = + let rule = NTMap.find edited_nt !g.map in + let insert_after = ref edited_nt in + let rec expand rule = + let rec aux syms res = + match syms with + | [] -> res + | sym0 :: tl -> + let new_sym = match sym0 with + | Sterm _ + | Snterm _ -> + sym0 + | Slist1 sym + | Slist1sep (sym, _) + | Slist0 sym + | Slist0sep (sym, _) + | Sopt sym -> + let name = gen_nt_name sym in + if name <> "" then begin + let new_nt = maybe_add_nt g insert_after name sym0 queue in + Snterm new_nt + end else sym0 + | Sparen slist -> Sparen (expand slist) + | Sprod slistlist -> + let has_empty = List.length (List.hd (List.rev slistlist)) = 0 in + let name = gen_nt_name sym0 in + if name <> "" then begin + let new_nt = maybe_add_nt g insert_after name + (if has_empty then (Sopt (Sprod (List.rev (List.tl (List.rev slistlist))) )) + else sym0) queue + in + Snterm new_nt + end else + Sprod (List.map expand slistlist) + | Sedit _ + | Sedit2 _ -> + sym0 (* these constructors not used here *) + in + aux tl (new_sym :: res) + in + List.rev (aux rule (if edited_nt <> "empty" && ematch rule [] then [Snterm "empty"] else [])) + in + let rule' = List.map expand rule in + g_update_prods g edited_nt rule' + +let expand_lists g = + (* todo: use Queue.of_seq w OCaml 4.07+ *) + let queue = Queue.create () in + List.iter (fun nt -> Queue.add nt queue) !g.order; + try + while true do + let nt = Queue.pop queue in + expand_rule g nt queue + done + with + | Queue.Empty -> () + +let edit_all_prods g op eprods = + let do_it op eprods num = + let rec aux eprods res = + match eprods with + | [] -> res + | [Snterm old_nt; Snterm new_nt] :: tl when num = 2 -> + aux tl ((old_nt, new_nt) :: res) + | [Snterm old_nt] :: tl when num = 1 -> + aux tl ((old_nt, op) :: res) + | eprod :: tl -> + error "Production '%s: %s' must have only %d nonterminal(s)\n" + op (prod_to_str eprod) num; + aux tl res + in + let map = create_edit_map (aux eprods []) in + if op = "SPLICE" then + apply_splice g map + else (* RENAME/DELETE *) + List.iter (fun b -> let (nt, _) = b in + let prods = try NTMap.find nt !g.map with Not_found -> [] in + let (nt', prods') = edit_rule g map nt prods in + if nt' = "" then + g_remove g nt + else if nt <> nt' then + g_rename_merge g nt nt' prods' + else + g_update_prods g nt prods') + (NTMap.bindings !g.map); + in + match op with + | "RENAME" -> do_it op eprods 2; true + | "DELETE" -> do_it op eprods 1; true + | "SPLICE" -> do_it op eprods 1; true + | "EXPAND" -> + if List.length eprods > 1 || List.length (List.hd eprods) <> 0 then + error "'EXPAND:' expects a single empty production\n"; + expand_lists g; true + | _ -> false + +let edit_single_prod g edit0 prods nt = + let rec edit_single_prod_r edit prods nt seen = + match edit with + | [] -> prods + | Sedit "ADD_OPT" :: sym :: tl -> + let prods' = (try + let pfx = List.rev seen in + let posn = find_first edit0 prods nt in + let prods = insert_after posn [pfx @ (Sopt sym :: tl)] prods in + let prods = remove_prod (pfx @ (sym :: tl)) prods nt in + remove_prod (pfx @ tl) prods nt + with Not_found -> prods) in + edit_single_prod_r tl prods' nt seen + | Sedit "ADD_OPT" :: [] -> error "Bad position for ADD_OPT\n"; prods + | Sedit2 ("USE_NT", name) :: sym :: tl -> + let prods' = (try + let nt = maybe_add_nt g (ref nt) name sym (Queue.create ()) in + let pfx = List.rev seen in + let posn = find_first edit0 prods nt in + let prods = insert_after posn [pfx @ (Snterm nt :: tl)] prods in + remove_prod (pfx @ (sym :: tl)) prods nt + with Not_found -> prods) in + edit_single_prod_r tl prods' nt seen + | Sedit2 ("USE_NT", _) :: [] -> error "Bad position for USE_NT\n"; prods + | sym :: tl -> + edit_single_prod_r tl prods nt (sym :: seen) + in + edit_single_prod_r edit0 prods nt [] + +let apply_edit_file g edits = + List.iter (fun b -> + let (nt, eprod) = b in + if not (edit_all_prods g nt eprod) then begin + let rec aux eprod prods add_nt = + match eprod with + | [] -> prods, add_nt + | (Snterm "DELETE" :: oprod) :: tl -> + aux tl (remove_prod oprod prods nt) add_nt + | (Snterm "DELETENT" :: _) :: tl -> (* note this doesn't remove references *) + g_remove g nt; + aux tl prods false + | (Snterm "EDIT" :: oprod) :: tl -> + aux tl (edit_single_prod g oprod prods nt) add_nt + | (Snterm "REPLACE" :: oprod) :: (Snterm "WITH" :: rprod) :: tl -> + let prods' = (try + let posn = find_first oprod prods nt in + let prods = insert_after posn [rprod] prods in (* insert new prod *) + remove_prod oprod prods nt (* remove orig prod *) + with Not_found -> prods) + in + aux tl prods' add_nt + | (Snterm "REPLACE" :: _ as eprod) :: tl -> + error "Missing WITH after '%s' in '%s'\n" (prod_to_str eprod) nt; + aux tl prods add_nt + | prod :: tl -> + (* add a production *) + if has_match prod prods then + error "Duplicate production '%s' for %s\n" (prod_to_str prod) nt; + aux tl (prods @ [prod]) add_nt + in + let prods, add_nt = + aux eprod (try NTMap.find nt !g.map with Not_found -> []) true in + if add_nt then + g_maybe_add g nt prods + end) + edits + + +(*** main routines ***) + + (* get the nt's in the production, preserving order, don't worry about dups *) + let nts_in_prod prod = + let rec traverse = function + | Sterm s -> [] + | Snterm s -> [s] + | Slist1 sym + | Slist0 sym + | Sopt sym + -> traverse sym + | Slist1sep (sym, sep) + | Slist0sep (sym, sep) + -> traverse sym @ (traverse sep) + | Sparen sym_list -> List.concat (List.map traverse sym_list) + | Sprod sym_list_list -> List.concat (List.map (fun l -> List.concat (List.map traverse l)) sym_list_list) + | Sedit _ + | Sedit2 _ -> [] + in + List.rev (List.concat (List.map traverse prod)) + +(* get the transitive closure of a non-terminal excluding "stops" symbols. + Preserve ordering to the extent possible *) +(* todo: at the moment, the code doesn't use the ordering; consider switching to using +sets instead of lists *) +let nt_closure g start stops = + let stop_set = StringSet.of_list stops in + let rec nt_closure_r res todo = + match todo with + | [] -> res + | nt :: tl -> + if List.mem nt res || StringSet.mem nt stop_set then + nt_closure_r res tl + else begin + let more_to_do = + try + let prods = NTMap.find nt !g.map in + tl @ (List.concat (List.map nts_in_prod prods)) + with Not_found -> tl in + nt_closure_r (nt :: res) more_to_do + end + in + List.rev (nt_closure_r [] [start]) + +let header = "--------------------------------------------" +let nt_subset_in_orig_order g nts = + let subset = StringSet.of_list nts in + List.filter (fun nt -> StringSet.mem nt subset) !g.order + +let print_chunk out g seen fmt title starts ends = + fprintf out "\n\n%s:\n%s\n" title header; + List.iter (fun start -> + let nts = (nt_closure g start ends) in + print_in_order out g fmt (nt_subset_in_orig_order g nts) !seen; + seen := StringSet.union !seen (StringSet.of_list nts)) + starts + +let print_chunks g out fmt () = + let seen = ref StringSet.empty in + print_chunk out g seen fmt "lconstr" ["lconstr"] ["binder_constr"; "tactic_expr5"]; + print_chunk out g seen fmt "Gallina syntax of terms" ["binder_constr"] ["tactic_expr5"]; + print_chunk out g seen fmt "Gallina The Vernacular" ["gallina"] ["tactic_expr5"]; + print_chunk out g seen fmt "intropattern_list_opt" ["intropattern_list"; "or_and_intropattern_loc"] ["operconstr"; "tactic_expr5"]; + print_chunk out g seen fmt "simple_tactic" ["simple_tactic"] + ["tactic_expr5"; "tactic_expr3"; "tactic_expr2"; "tactic_expr1"; "tactic_expr0"]; + + (*print_chunk out g seen fmt "Ltac" ["tactic_expr5"] [];*) + print_chunk out g seen fmt "Ltac" ["tactic_expr5"] ["tactic_expr4"]; + print_chunk out g seen fmt "Ltac 4" ["tactic_expr4"] ["tactic_expr3"; "tactic_expr2"]; + print_chunk out g seen fmt "Ltac 3" ["tactic_expr3"] ["tactic_expr2"]; + print_chunk out g seen fmt "Ltac 2" ["tactic_expr2"] ["tactic_expr1"]; + print_chunk out g seen fmt "Ltac 1" ["tactic_expr1"] ["tactic_expr0"]; + print_chunk out g seen fmt "Ltac 0" ["tactic_expr0"] []; + + + print_chunk out g seen fmt "command" ["command"] []; + print_chunk out g seen fmt "vernac_toplevel" ["vernac_toplevel"] []; + print_chunk out g seen fmt "vernac_control" ["vernac_control"] [] + + (* + let ssr_tops = ["ssr_dthen"; "ssr_else"; "ssr_mpat"; "ssr_rtype"] in + seen := StringSet.union !seen (StringSet.of_list ssr_tops); + + print_chunk out g seen fmt "ssrindex" ["ssrindex"] []; + print_chunk out g seen fmt "command" ["command"] []; + print_chunk out g seen fmt "binder_constr" ["binder_constr"] []; + (*print_chunk out g seen fmt "closed_binder" ["closed_binder"] [];*) + print_chunk out g seen fmt "gallina_ext" ["gallina_ext"] []; + (*print_chunk out g seen fmt "hloc" ["hloc"] [];*) + (*print_chunk out g seen fmt "hypident" ["hypident"] [];*) + print_chunk out g seen fmt "simple_tactic" ["simple_tactic"] []; + print_chunk out g seen fmt "tactic_expr" ["tactic_expr4"; "tactic_expr1"; "tactic_expr0"] []; + fprintf out "\n\nRemainder:\n"; + print_in_order g (List.filter (fun x -> not (StringSet.mem x !seen)) !g.order) StringSet.empty; + *) + + + (*seen := StringSet.diff !seen (StringSet.of_list ssr_tops);*) + (*print_chunk out g seen fmt "vernac_toplevel" ["vernac_toplevel"] [];*) + +let start_symbols = ["vernac_toplevel"; "tactic_mode"] +let tokens = [ "BULLET"; "FIELD"; "IDENT"; "NUMERAL"; "STRING" ] (* don't report as undefined *) + +let report_bad_nts g file = + let rec get_nts refd defd bindings = + match bindings with + | [] -> refd, defd + | (nt, prods) :: tl -> + get_nts (List.fold_left (fun res prod -> + StringSet.union res (StringSet.of_list (nts_in_prod prod))) + refd prods) + (StringSet.add nt defd) tl + in + let all_nts_ref, all_nts_def = + get_nts (StringSet.of_list tokens) (StringSet.of_list tokens) (NTMap.bindings !g.map) in + + let undef = StringSet.diff all_nts_ref all_nts_def in + List.iter (fun nt -> warn "%s: Undefined symbol '%s'\n" file nt) (StringSet.elements undef); + + let reachable = + List.fold_left (fun res sym -> + StringSet.union res (StringSet.of_list (nt_closure g sym []))) + StringSet.empty start_symbols + in + let unreachable = List.filter (fun nt -> not (StringSet.mem nt reachable)) !g.order in + List.iter (fun nt -> warn "%s: Unreachable symbol '%s'\n" file nt) unreachable + + +let report_info g symdef_map = + let num_prods = List.fold_left (fun sum nt -> let prods = NTMap.find nt !g.map in sum + (List.length prods)) + 0 !g.order + in + + Printf.eprintf "\nstart symbols: %s\n" (String.concat " " start_symbols); + Printf.eprintf "%d nonterminals defined, %d productions\n" (NTMap.cardinal !g.map) num_prods; + Printf.eprintf "%d terminals\n" (List.length tokens); + + Printf.eprintf "\nSymbols with multiple definition points in *.mlg:\n"; + let bindings = List.sort (fun a b -> let (ak, _) = a and (bk, _) = b in + String.compare ak bk) (StringMap.bindings symdef_map) in + List.iter (fun b -> + let (k, v) = b in + if List.length v > 1 then begin + Printf.eprintf " %s: " k; + List.iter (fun f -> Printf.eprintf "%s " f) v; + Printf.eprintf "\n" + end) + bindings; + Printf.eprintf "\n" + + + +[@@@ocaml.warning "-32"] +let rec dump prod = + match prod with + | hd :: tl -> let s = (match hd with + | Sterm s -> sprintf "Sterm %s" s + | Snterm s -> sprintf "Snterm \"%s\"" s + | Slist1 sym -> "Slist1" + | Slist0 sym -> "Slist0" + | Sopt sym -> "Sopt" + | Slist1sep _ -> "Slist1sep" + | Slist0sep _ -> "Slist0sep" + | Sparen sym_list -> "Sparen" + | Sprod sym_list_list -> "Sprod" + | Sedit _ -> "Sedit" + | Sedit2 _ -> "Sedit2") in + Printf.printf "%s " s; + dump tl + | [] -> Printf.printf "\n" +[@@@ocaml.warning "+32"] + +let reorder_grammar eg reordered_rules file = + let og = ref { map = NTMap.empty; order = [] } in + List.iter (fun rule -> + let nt, prods = rule in + try + (* only keep nts and prods in common with editedGrammar *) + let eg_prods = NTMap.find nt !eg.map in + let prods = List.filter (fun prod -> (has_match prod eg_prods)) prods in + if NTMap.mem nt !og.map then + warn "%s: Duplicate nonterminal '%s'\n" file nt; + add_rule og nt prods file + with Not_found -> ()) + reordered_rules; + g_reverse og; + + (* insert a prod in a list after prev_prod (None=at the beginning) *) + let rec insert_prod prev_prod prod prods res = + match prev_prod, prods with + | None, _ -> prod :: prods + | Some _, [] -> raise Not_found + | Some ins_after_prod, hd :: tl -> + if ematch hd ins_after_prod then + (List.rev res) @ (hd :: prod :: tl) + else + insert_prod prev_prod prod tl (hd :: res) + in + + (* insert prods that are not already in og_prods *) + let rec upd_prods prev_prod eg_prods og_prods = + match eg_prods with + | [] -> og_prods + | prod :: tl -> + let og_prods = + if has_match prod og_prods then + List.map (fun p -> if ematch p prod then prod else p) og_prods + else + insert_prod prev_prod prod og_prods [] in + upd_prods (Some prod) tl og_prods + in + + (* add nts and prods not present in orderedGrammar *) + let _ = List.fold_left (fun prev_nt nt -> + let e_prods = NTMap.find nt !eg.map in + if not (NTMap.mem nt !og.map) then + g_add_after og prev_nt nt e_prods + else + g_update_prods og nt (upd_prods None e_prods (NTMap.find nt !og.map)); + Some nt) + None !eg.order in + g_reorder eg !og.map !og.order + + +let finish_with_file old_file verify = + let files_eq f1 f2 = + let chunksize = 8192 in + (try + let ofile = open_in_bin f1 in + let nfile = open_in_bin f2 in + let rv = if (in_channel_length ofile) <> (in_channel_length nfile) then false + else begin + let obuf = Bytes.create chunksize in + Bytes.fill obuf 0 chunksize '\x00'; + let nbuf = Bytes.create chunksize in + Bytes.fill nbuf 0 chunksize '\x00'; + let rec read () = + let olen = input ofile obuf 0 chunksize in + let _ = input nfile nbuf 0 chunksize in + if obuf <> nbuf then + false + else if olen = 0 then + true + else + read () + in + read () + end + in + close_in ofile; + close_in nfile; + rv + with Sys_error _ -> false) + in + + let temp_file = (old_file ^ "_temp") in + if verify then + if (files_eq old_file temp_file || !exit_code <> 0) then + Sys.remove temp_file + else + error "%s is not current\n" old_file + else + Sys.rename temp_file old_file + +let open_temp_bin file = + open_out_bin (sprintf "%s_temp" file) + +let find_longest_match prods str = + (* todo: require a minimum length? *) + let common_prefix_len s1 s2 = + let limit = min (String.length s1) (String.length s2) in + let rec aux off = + if off = limit then off + else if s1.[off] = s2.[off] then aux (succ off) + else off + in + aux 0 + in + + let slen = String.length str in + let rec longest best multi best_len prods = + match prods with + | [] -> best, multi, best_len + | prod :: tl -> + let pstr = String.trim (prod_to_prodn prod) in + let clen = common_prefix_len str pstr in + if clen = slen && slen = String.length pstr then + pstr, false, clen (* exact match *) + else if clen > best_len then + longest pstr false clen tl (* better match *) + else if clen = best_len then + longest best true best_len tl (* 2nd match with same length *) + else + longest best multi best_len tl (* worse match *) + in + longest "" false 0 prods + +type seen = { + nts: (string * int) NTMap.t; + tacs: (string * int) NTMap.t; + cmds: (string * int) NTMap.t; +} + +let process_rst g file args seen tac_prods cmd_prods = + let old_rst = open_in file in + let new_rst = open_temp_bin file in + let linenum = ref 0 in + let dir_regex = Str.regexp "^\\([ \t]*\\)\\.\\.[ \t]*\\([a-zA-Z0-9:]*\\)\\(.*\\)" in + let ig_args_regex = Str.regexp "^[ \t]*\\([a-zA-Z0-9_\\.]*\\)[ \t]*\\([a-zA-Z0-9_\\.]*\\)" in + let blank_regex = Str.regexp "^[ \t]*$" in + let end_prodlist_regex = Str.regexp "^[ \t]*$" in + let rec index_of_r str list index = + match list with + | [] -> None + | hd :: list -> + if hd = str then Some index + else index_of_r str list (index+1) + in + let index_of str list = index_of_r str list 0 in + let getline () = + let line = input_line old_rst in + incr linenum; + line + in + let output_insertgram start_index end_ indent is_coq_group = + let rec nthcdr n list = if n = 0 then list else nthcdr (n-1) (List.tl list) in + let rec copy_prods list = + match list with + | [] -> () + | nt :: tl -> + (try + let (prev_file, prev_linenum) = NTMap.find nt !seen.nts in + warn "%s line %d: '%s' already included at %s line %d\n" + file !linenum nt prev_file prev_linenum; + with Not_found -> + if is_coq_group then + seen := { !seen with nts = (NTMap.add nt (file, !linenum) !seen.nts)} ); + let prods = NTMap.find nt !g.map in + List.iteri (fun i prod -> + let rhs = String.trim (sprintf ": %s" (prod_to_str ~plist:true prod)) in + fprintf new_rst "%s %s %s\n" indent (if i = 0 then nt else String.make (String.length nt) ' ') rhs) + prods; + if nt <> end_ then copy_prods tl + in + copy_prods (nthcdr start_index !g.order) + in + + let process_insertgram line rhs = + if not (Str.string_match ig_args_regex rhs 0) then + error "%s line %d: bad arguments '%s' for 'insertgram'\n" file !linenum rhs + else begin + let start = Str.matched_group 1 rhs in + let end_ = Str.matched_group 2 rhs in + let start_index = index_of start !g.order in + let end_index = index_of end_ !g.order in + if start_index = None then + error "%s line %d: '%s' is undefined\n" file !linenum start; + if end_index = None then + error "%s line %d: '%s' is undefined\n" file !linenum end_; + match start_index, end_index with + | Some start_index, Some end_index -> + if start_index > end_index then + error "%s line %d: '%s' must appear before '%s' in .../orderedGrammar\n" file !linenum start end_ + else begin + try + let line2 = getline() in + if not (Str.string_match blank_regex line2 0) then + error "%s line %d: expecting a blank line after 'insertgram'\n" file !linenum + else begin + let line3 = getline() in + if not (Str.string_match dir_regex line3 0) || (Str.matched_group 2 line3) <> "productionlist::" then + error "%s line %d: expecting 'productionlist' after 'insertgram'\n" file !linenum + else begin + let indent = Str.matched_group 1 line3 in + let is_coq_group = ("coq" = String.trim (Str.matched_group 3 line3)) in + let rec skip_to_end () = + let endline = getline() in + if Str.string_match end_prodlist_regex endline 0 then begin + fprintf new_rst "%s\n\n%s\n" line line3; + output_insertgram start_index end_ indent is_coq_group; + fprintf new_rst "%s\n" endline + end else + skip_to_end () + in + skip_to_end () + end + end + with End_of_file -> error "%s line %d: unexpected end of file\n" file !linenum; + end + | _ -> () + end + + in + try + while true do + let line = getline() in + if Str.string_match dir_regex line 0 then begin + let dir = Str.matched_group 2 line in + let rhs = String.trim (Str.matched_group 3 line) in + match dir with + | "productionlist::" -> + if rhs = "coq" then + warn "%s line %d: Missing 'insertgram' before 'productionlist:: coq'\n" file !linenum; + fprintf new_rst "%s\n" line; + | "tacn::" when args.check_tacs -> + if not (StringSet.mem rhs tac_prods) then + warn "%s line %d: Unknown tactic: '%s'\n" file !linenum rhs; + if NTMap.mem rhs !seen.tacs then + warn "%s line %d: Repeated tactic: '%s'\n" file !linenum rhs; + seen := { !seen with tacs = (NTMap.add rhs (file, !linenum) !seen.tacs)}; + fprintf new_rst "%s\n" line + | "cmd::" when args.check_cmds -> + if not (StringSet.mem rhs cmd_prods) then + warn "%s line %d: Unknown command: '%s'\n" file !linenum rhs; + if NTMap.mem rhs !seen.cmds then + warn "%s line %d: Repeated command: '%s'\n" file !linenum rhs; + seen := { !seen with cmds = (NTMap.add rhs (file, !linenum) !seen.cmds)}; + fprintf new_rst "%s\n" line + | "insertgram" -> + process_insertgram line rhs + | _ -> fprintf new_rst "%s\n" line + end else + fprintf new_rst "%s\n" line; + done + with End_of_file -> (); + close_in old_rst; + close_out new_rst; + finish_with_file file args.verify + +let report_omitted_prods entries seen label split = + let maybe_warn first last n = + if first <> "" then begin + if first <> last then + warn "%ss '%s' to %s'%s' not included in .rst files (%d)\n" label first split last n + else + warn "%s %s not included in .rst files\n" label first; + end + in + + let first, last, n = List.fold_left (fun missing nt -> + let first, last, n = missing in + if NTMap.mem nt seen then begin + maybe_warn first last n; + "", "", 0 + end else + (if first = "" then nt else first), nt, n + 1) + ("", "", 0) entries in + maybe_warn first last n + +let process_grammar args = + let symdef_map = ref StringMap.empty in + let g = ref { map = NTMap.empty; order = [] } in + + let level_renames = read_mlg_files g args symdef_map in + + (* rename nts with levels *) + List.iter (fun b -> let (nt, prod) = b in + let (_, prod) = edit_rule g level_renames nt prod in + g_update_prods g nt prod) + (NTMap.bindings !g.map); + + (* print the full grammar with minimal editing *) + let out = open_temp_bin (dir "fullGrammar") in + fprintf out "%s\n%s\n\n" + "(* Coq grammar generated from .mlg files. Do not edit by hand. Not compiled into Coq *)" + "DOC_GRAMMAR"; + print_in_order out g `MLG !g.order StringSet.empty; + close_out out; + finish_with_file (dir "fullGrammar") args.verify; + + if not args.fullGrammar then begin + (* do shared edits *) + if !exit_code = 0 then begin + let common_edits = read_mlg_edit "common.edit_mlg" in + apply_edit_file g common_edits + end; + let prodn_gram = ref { map = !g.map; order = !g.order } in + + if !exit_code = 0 && not args.verify then begin + let prodlist_edits = read_mlg_edit "productionlist.edit_mlg" in + apply_edit_file g prodlist_edits; + let out = open_temp_bin (dir "productionlistGrammar") in + if args.verbose then + report_info g !symdef_map; + print_in_order out g `PRODLIST !g.order StringSet.empty; + (*print_chunks g out `PRODLIST ();*) + close_out out; + finish_with_file (dir "productionlistGrammar") args.verify; + end; + + if !exit_code = 0 && not args.verify then begin + let out = open_temp_bin (dir "editedGrammar") in + fprintf out "%s\n%s\n\n" + "(* Edited Coq grammar generated from .mlg files. Do not edit by hand. Not compiled into Coq *)" + "DOC_GRAMMAR"; + print_in_order out g `MLG !g.order StringSet.empty; + close_out out; + finish_with_file (dir "editedGrammar") args.verify; + report_bad_nts g "editedGrammar" + end; + + if !exit_code = 0 then begin + let ordered_grammar = read_mlg_edit "orderedGrammar" in + let out = open_temp_bin (dir "orderedGrammar") in + fprintf out "%s\n%s\n\n" + ("(* Defines the order to apply to editedGrammar to get productionlistGrammar.\n" ^ + "doc_grammar will modify this file to add/remove nonterminals and productions\n" ^ + "to match editedGrammar, which will remove comments. Not compiled into Coq *)") + "DOC_GRAMMAR"; + reorder_grammar g ordered_grammar "orderedGrammar"; + print_in_order out g `MLG !g.order StringSet.empty; + close_out out; + finish_with_file (dir "orderedGrammar") args.verify; + end; + + if !exit_code = 0 then begin + let plist nt = + let list = (List.map (fun t -> String.trim (prod_to_prodn t)) + (NTMap.find nt !g.map)) in + list, StringSet.of_list list in + let tac_list, tac_prods = plist "simple_tactic" in + let cmd_list, cmd_prods = plist "command" in + let seen = ref { nts=NTMap.empty; tacs=NTMap.empty; cmds=NTMap.empty } in + List.iter (fun file -> process_rst g file args seen tac_prods cmd_prods) args.rst_files; + report_omitted_prods !g.order !seen.nts "Nonterminal" ""; + if args.check_tacs then + report_omitted_prods tac_list !seen.tacs "Tactic" "\n "; + if args.check_cmds then + report_omitted_prods cmd_list !seen.cmds "Command" "\n " + end; + + (* generate output for prodn: simple_tactic, command, also for Ltac?? *) + if !exit_code = 0 && not args.verify then begin + let prodn_edits = read_mlg_edit "prodn.edit_mlg" in + apply_edit_file prodn_gram prodn_edits; + let out = open_temp_bin (dir "prodnGrammar") in + print_in_order out prodn_gram `PRODN !prodn_gram.order StringSet.empty; + close_out out; + finish_with_file (dir "prodnGrammar") args.verify + end + end + +let parse_args () = + let suffix_regex = Str.regexp ".*\\.\\([a-z]+\\)$" in + let args = + List.fold_left (fun args arg -> + match arg with + | "-check-cmds" -> { args with check_cmds = true } + | "-check-tacs" -> { args with check_tacs = true } + | "-no-warn" -> show_warn := false; { args with show_warn = true } + | "-short" -> { args with fullGrammar = true } + | "-verbose" -> { args with verbose = true } + | "-verify" -> { args with verify = true } + | arg when Str.string_match suffix_regex arg 0 -> + (match Str.matched_group 1 arg with + | "mlg" -> { args with mlg_files = (arg :: args.mlg_files) } + | "rst" -> { args with rst_files = (arg :: args.rst_files) } + | _ -> error "Unknown command line argument '%s'\n" arg; args) + | arg -> error "Unknown command line argument '%s'\n" arg; args) + default_args (List.tl (Array.to_list Sys.argv)) in + { args with mlg_files = (List.rev args.mlg_files); rst_files = (List.rev args.rst_files)} + +let () = + (*try*) + Printexc.record_backtrace true; + let args = parse_args () in + if !exit_code = 0 then begin + process_grammar args + end; + exit !exit_code + (*with _ -> Printexc.print_backtrace stdout; exit 1*) diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar new file mode 100644 index 0000000000..a83638dd73 --- /dev/null +++ b/doc/tools/docgram/fullGrammar @@ -0,0 +1,3174 @@ +(* Coq grammar generated from .mlg files. Do not edit by hand. Not compiled into Coq *) +DOC_GRAMMAR + +Constr.ident: [ +| Prim.ident +] + +Prim.name: [ +| "_" +] + +global: [ +| Prim.reference +] + +constr_pattern: [ +| constr +] + +lconstr_pattern: [ +| lconstr +] + +sort: [ +| "Set" +| "Prop" +| "SProp" +| "Type" +| "Type" "@{" "_" "}" +| "Type" "@{" universe "}" +] + +sort_family: [ +| "Set" +| "Prop" +| "SProp" +| "Type" +] + +universe_increment: [ +| "+" natural +| +] + +universe_name: [ +| global +| "Set" +| "Prop" +] + +universe_expr: [ +| universe_name universe_increment +] + +universe: [ +| "max" "(" LIST1 universe_expr SEP "," ")" +| universe_expr +] + +lconstr: [ +| operconstr200 +| l_constr +] + +constr: [ +| operconstr8 +| "@" global instance +] + +operconstr200: [ +| binder_constr +| operconstr100 +] + +operconstr100: [ +| operconstr99 "<:" binder_constr +| operconstr99 "<:" operconstr100 +| operconstr99 "<<:" binder_constr +| operconstr99 "<<:" operconstr100 +| operconstr99 ":" binder_constr +| operconstr99 ":" operconstr100 +| operconstr99 ":>" +| operconstr99 +] + +operconstr99: [ +| operconstr90 +] + +operconstr90: [ +| operconstr10 +] + +operconstr10: [ +| operconstr9 LIST1 appl_arg +| "@" global instance LIST0 operconstr9 +| "@" pattern_identref LIST1 identref +| operconstr9 +] + +operconstr9: [ +| ".." operconstr0 ".." +| operconstr8 +] + +operconstr8: [ +| operconstr1 +] + +operconstr1: [ +| operconstr0 ".(" global LIST0 appl_arg ")" +| operconstr0 ".(" "@" global LIST0 ( operconstr9 ) ")" +| operconstr0 "%" IDENT +| operconstr0 +] + +operconstr0: [ +| atomic_constr +| match_constr +| "(" operconstr200 ")" +| "{|" record_declaration bar_cbrace +| "{" binder_constr "}" +| "`{" operconstr200 "}" +| "`(" operconstr200 ")" +| "ltac" ":" "(" Pltac.tactic_expr ")" +] + +record_declaration: [ +| record_fields +] + +record_fields: [ +| record_field_declaration ";" record_fields +| record_field_declaration +| +| record_field ";" record_fields +| record_field ";" +| record_field +] + +record_field_declaration: [ +| global binders ":=" lconstr +] + +binder_constr: [ +| "forall" open_binders "," operconstr200 +| "fun" open_binders "=>" operconstr200 +| "let" name binders type_cstr ":=" operconstr200 "in" operconstr200 +| "let" single_fix "in" operconstr200 +| "let" [ "(" LIST0 name SEP "," ")" | "()" ] return_type ":=" operconstr200 "in" operconstr200 +| "let" "'" pattern200 ":=" operconstr200 "in" operconstr200 +| "let" "'" pattern200 ":=" operconstr200 case_type "in" operconstr200 +| "let" "'" pattern200 "in" pattern200 ":=" operconstr200 case_type "in" operconstr200 +| "if" operconstr200 return_type "then" operconstr200 "else" operconstr200 +| fix_constr +| "if" operconstr200 "is" ssr_dthen ssr_else (* ssr plugin *) +| "if" operconstr200 "isn't" ssr_dthen ssr_else (* ssr plugin *) +| "let" ":" ssr_mpat ":=" lconstr "in" lconstr (* ssr plugin *) +| "let" ":" ssr_mpat ":=" lconstr ssr_rtype "in" lconstr (* ssr plugin *) +| "let" ":" ssr_mpat "in" pattern200 ":=" lconstr ssr_rtype "in" lconstr (* ssr plugin *) +] + +appl_arg: [ +| lpar_id_coloneq lconstr ")" +| operconstr9 +] + +atomic_constr: [ +| global instance +| sort +| NUMERAL +| string +| "_" +| "?" "[" ident "]" +| "?" "[" pattern_ident "]" +| pattern_ident evar_instance +] + +inst: [ +| ident ":=" lconstr +] + +evar_instance: [ +| "@{" LIST1 inst SEP ";" "}" +| +] + +instance: [ +| "@{" LIST0 universe_level "}" +| +] + +universe_level: [ +| "Set" +| "Prop" +| "Type" +| "_" +| global +] + +fix_constr: [ +| single_fix +| single_fix "with" LIST1 fix_decl SEP "with" "for" identref +] + +single_fix: [ +| fix_kw fix_decl +] + +fix_kw: [ +| "fix" +| "cofix" +] + +fix_decl: [ +| identref binders_fixannot type_cstr ":=" operconstr200 +] + +match_constr: [ +| "match" LIST1 case_item SEP "," OPT case_type "with" branches "end" +] + +case_item: [ +| operconstr100 OPT [ "as" name ] OPT [ "in" pattern200 ] +] + +case_type: [ +| "return" operconstr100 +] + +return_type: [ +| OPT [ OPT [ "as" name ] case_type ] +] + +branches: [ +| OPT "|" LIST0 eqn SEP "|" +] + +mult_pattern: [ +| LIST1 pattern200 SEP "," +] + +eqn: [ +| LIST1 mult_pattern SEP "|" "=>" lconstr +] + +record_pattern: [ +| global ":=" pattern200 +] + +record_patterns: [ +| record_pattern ";" record_patterns +| record_pattern ";" +| record_pattern +| +] + +pattern200: [ +| pattern100 +] + +pattern100: [ +| pattern99 ":" binder_constr +| pattern99 ":" operconstr100 +| pattern99 +] + +pattern99: [ +| pattern90 +] + +pattern90: [ +| pattern10 +] + +pattern10: [ +| pattern1 "as" name +| pattern1 LIST1 pattern1 +| "@" Prim.reference LIST0 pattern1 +| pattern1 +] + +pattern1: [ +| pattern0 "%" IDENT +| pattern0 +] + +pattern0: [ +| Prim.reference +| "{|" record_patterns bar_cbrace +| "_" +| "(" pattern200 ")" +| "(" pattern200 "|" LIST1 pattern200 SEP "|" ")" +| NUMERAL +| string +] + +impl_ident_tail: [ +| "}" +| LIST1 name ":" lconstr "}" +| LIST1 name "}" +| ":" lconstr "}" +] + +fixannot: [ +| "{" "struct" identref "}" +| "{" "wf" constr identref "}" +| "{" "measure" constr OPT identref OPT constr "}" +| "{" "struct" name "}" +| +] + +impl_name_head: [ +| impl_ident_head +] + +binders_fixannot: [ +| impl_name_head impl_ident_tail binders_fixannot +| fixannot +| binder binders_fixannot +| +] + +open_binders: [ +| name LIST0 name ":" lconstr +| name LIST0 name binders +| name ".." name +| closed_binder binders +] + +binders: [ +| LIST0 binder +| Pcoq.Constr.binders +] + +binder: [ +| name +| closed_binder +] + +closed_binder: [ +| "(" name LIST1 name ":" lconstr ")" +| "(" name ":" lconstr ")" +| "(" name ":=" lconstr ")" +| "(" name ":" lconstr ":=" lconstr ")" +| "{" name "}" +| "{" name LIST1 name ":" lconstr "}" +| "{" name ":" lconstr "}" +| "{" name LIST1 name "}" +| "`(" LIST1 typeclass_constraint SEP "," ")" +| "`{" LIST1 typeclass_constraint SEP "," "}" +| "'" pattern0 +| [ "of" | "&" ] operconstr99 (* ssr plugin *) +] + +typeclass_constraint: [ +| "!" operconstr200 +| "{" name "}" ":" [ "!" | ] operconstr200 +| name_colon [ "!" | ] operconstr200 +| operconstr200 +] + +type_cstr: [ +| OPT [ ":" lconstr ] +| ":" lconstr +| +] + +preident: [ +| IDENT +] + +ident: [ +| IDENT +] + +pattern_ident: [ +| LEFTQMARK ident +] + +pattern_identref: [ +| pattern_ident +] + +var: [ +| ident +] + +identref: [ +| ident +] + +field: [ +| FIELD +] + +fields: [ +| field fields +| field +] + +fullyqualid: [ +| ident fields +| ident +] + +basequalid: [ +| ident fields +| ident +] + +name: [ +| "_" +| ident +] + +reference: [ +| ident fields +| ident +] + +by_notation: [ +| ne_string OPT [ "%" IDENT ] +] + +smart_global: [ +| reference +| by_notation +] + +qualid: [ +| basequalid +] + +ne_string: [ +| STRING +] + +ne_lstring: [ +| ne_string +] + +dirpath: [ +| ident LIST0 field +] + +string: [ +| STRING +] + +lstring: [ +| string +] + +integer: [ +| NUMERAL +| "-" NUMERAL +] + +natural: [ +| NUMERAL +| _natural +] + +bigint: [ +| NUMERAL +] + +bar_cbrace: [ +| "|" "}" +] + +vernac_toplevel: [ +| "Drop" "." +| "Quit" "." +| "Backtrack" natural natural natural "." +| test_show_goal "Show" "Goal" natural "at" natural "." +| Pvernac.Vernac_.main_entry +] + +opt_hintbases: [ +| +| ":" LIST1 IDENT +] + +command: [ +| "Goal" lconstr +| "Proof" +| "Proof" "Mode" string +| "Proof" lconstr +| "Abort" +| "Abort" "All" +| "Abort" identref +| "Existential" natural constr_body +| "Admitted" +| "Qed" +| "Save" identref +| "Defined" +| "Defined" identref +| "Restart" +| "Undo" +| "Undo" natural +| "Undo" "To" natural +| "Focus" +| "Focus" natural +| "Unfocus" +| "Unfocused" +| "Show" +| "Show" natural +| "Show" ident +| "Show" "Existentials" +| "Show" "Universes" +| "Show" "Conjectures" +| "Show" "Proof" +| "Show" "Intro" +| "Show" "Intros" +| "Show" "Match" reference +| "Guarded" +| "Create" "HintDb" IDENT; [ "discriminated" | ] +| "Remove" "Hints" LIST1 global opt_hintbases +| "Hint" hint opt_hintbases +| "Comments" LIST0 comment +| "Declare" "Instance" ident_decl binders ":" operconstr200 hint_info +| "Declare" "Scope" IDENT +| "Pwd" +| "Cd" +| "Cd" ne_string +| "Load" [ "Verbose" | ] [ ne_string | IDENT ] +| "Declare" "ML" "Module" LIST1 ne_string +| "Locate" locatable +| "Add" "LoadPath" ne_string as_dirpath +| "Add" "Rec" "LoadPath" ne_string as_dirpath +| "Remove" "LoadPath" ne_string +| "AddPath" ne_string "as" as_dirpath +| "AddRecPath" ne_string "as" as_dirpath +| "DelPath" ne_string +| "Type" lconstr +| "Print" printable +| "Print" smart_global OPT univ_name_list +| "Print" "Module" "Type" global +| "Print" "Module" global +| "Print" "Namespace" dirpath +| "Inspect" natural +| "Add" "ML" "Path" ne_string +| "Add" "Rec" "ML" "Path" ne_string +| "Set" option_table option_setting +| "Unset" option_table +| "Print" "Table" option_table +| "Add" IDENT IDENT LIST1 option_ref_value +| "Add" IDENT LIST1 option_ref_value +| "Test" option_table "for" LIST1 option_ref_value +| "Test" option_table +| "Remove" IDENT IDENT LIST1 option_ref_value +| "Remove" IDENT LIST1 option_ref_value +| "Write" "State" IDENT +| "Write" "State" ne_string +| "Restore" "State" IDENT +| "Restore" "State" ne_string +| "Reset" "Initial" +| "Reset" identref +| "Back" +| "Back" natural +| "BackTo" natural +| "Debug" "On" +| "Debug" "Off" +| "Declare" "Reduction" IDENT; ":=" red_expr +| "Declare" "Custom" "Entry" IDENT +| "Derive" ident "SuchThat" constr "As" ident (* derive plugin *) +| "Extraction" global (* extraction plugin *) +| "Recursive" "Extraction" LIST1 global (* extraction plugin *) +| "Extraction" string LIST1 global (* extraction plugin *) +| "Extraction" "TestCompile" LIST1 global (* extraction plugin *) +| "Separate" "Extraction" LIST1 global (* extraction plugin *) +| "Extraction" "Library" ident (* extraction plugin *) +| "Recursive" "Extraction" "Library" ident (* extraction plugin *) +| "Extraction" "Language" language (* extraction plugin *) +| "Extraction" "Inline" LIST1 global (* extraction plugin *) +| "Extraction" "NoInline" LIST1 global (* extraction plugin *) +| "Print" "Extraction" "Inline" (* extraction plugin *) +| "Reset" "Extraction" "Inline" (* extraction plugin *) +| "Extraction" "Implicit" global "[" LIST0 int_or_id "]" (* extraction plugin *) +| "Extraction" "Blacklist" LIST1 ident (* extraction plugin *) +| "Print" "Extraction" "Blacklist" (* extraction plugin *) +| "Reset" "Extraction" "Blacklist" (* extraction plugin *) +| "Extract" "Constant" global LIST0 string "=>" mlname (* extraction plugin *) +| "Extract" "Inlined" "Constant" global "=>" mlname (* extraction plugin *) +| "Extract" "Inductive" global "=>" mlname "[" LIST0 mlname "]" OPT string (* extraction plugin *) +| "Show" "Extraction" (* extraction plugin *) +| "Set" "Firstorder" "Solver" tactic +| "Print" "Firstorder" "Solver" +| "Function" LIST1 function_rec_definition_loc SEP "with" (* funind plugin *) +| "Functional" "Scheme" LIST1 fun_scheme_arg SEP "with" (* funind plugin *) +| "Functional" "Case" fun_scheme_arg (* funind plugin *) +| "Generate" "graph" "for" reference (* funind plugin *) +| "Hint" "Rewrite" orient LIST1 constr ":" LIST0 preident +| "Hint" "Rewrite" orient LIST1 constr "using" tactic ":" LIST0 preident +| "Hint" "Rewrite" orient LIST1 constr +| "Hint" "Rewrite" orient LIST1 constr "using" tactic +| "Derive" "Inversion_clear" ident "with" constr "Sort" sort_family +| "Derive" "Inversion_clear" ident "with" constr +| "Derive" "Inversion" ident "with" constr "Sort" sort_family +| "Derive" "Inversion" ident "with" constr +| "Derive" "Dependent" "Inversion" ident "with" constr "Sort" sort_family +| "Derive" "Dependent" "Inversion_clear" ident "with" constr "Sort" sort_family +| "Declare" "Left" "Step" constr +| "Declare" "Right" "Step" constr +| "Grab" "Existential" "Variables" +| "Unshelve" +| "Declare" "Equivalent" "Keys" constr constr +| "Print" "Equivalent" "Keys" +| "Optimize" "Proof" +| "Optimize" "Heap" +| "Hint" "Cut" "[" hints_path "]" opthints +| "Typeclasses" "Transparent" LIST0 reference +| "Typeclasses" "Opaque" LIST0 reference +| "Typeclasses" "eauto" ":=" debug eauto_search_strategy OPT int +| "Proof" "with" Pltac.tactic OPT [ "using" G_vernac.section_subset_expr ] +| "Proof" "using" G_vernac.section_subset_expr OPT [ "with" Pltac.tactic ] +| "Tactic" "Notation" OPT ltac_tactic_level LIST1 ltac_production_item ":=" tactic +| "Print" "Ltac" reference +| "Locate" "Ltac" reference +| "Ltac" LIST1 ltac_tacdef_body SEP "with" +| "Print" "Ltac" "Signatures" +| "Obligation" integer "of" ident ":" lglob withtac +| "Obligation" integer "of" ident withtac +| "Obligation" integer ":" lglob withtac +| "Obligation" integer withtac +| "Next" "Obligation" "of" ident withtac +| "Next" "Obligation" withtac +| "Solve" "Obligation" integer "of" ident "with" tactic +| "Solve" "Obligation" integer "with" tactic +| "Solve" "Obligations" "of" ident "with" tactic +| "Solve" "Obligations" "with" tactic +| "Solve" "Obligations" +| "Solve" "All" "Obligations" "with" tactic +| "Solve" "All" "Obligations" +| "Admit" "Obligations" "of" ident +| "Admit" "Obligations" +| "Obligation" "Tactic" ":=" tactic +| "Show" "Obligation" "Tactic" +| "Obligations" "of" ident +| "Obligations" +| "Preterm" "of" ident +| "Preterm" +| "Add" "Relation" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "as" ident +| "Add" "Relation" constr constr "reflexivity" "proved" "by" constr "as" ident +| "Add" "Relation" constr constr "as" ident +| "Add" "Relation" constr constr "symmetry" "proved" "by" constr "as" ident +| "Add" "Relation" constr constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident +| "Add" "Relation" constr constr "reflexivity" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident +| "Add" "Relation" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident +| "Add" "Relation" constr constr "transitivity" "proved" "by" constr "as" ident +| "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "as" ident +| "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "as" ident +| "Add" "Parametric" "Relation" binders ":" constr constr "as" ident +| "Add" "Parametric" "Relation" binders ":" constr constr "symmetry" "proved" "by" constr "as" ident +| "Add" "Parametric" "Relation" binders ":" constr constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident +| "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident +| "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident +| "Add" "Parametric" "Relation" binders ":" constr constr "transitivity" "proved" "by" constr "as" ident +| "Add" "Setoid" constr constr constr "as" ident +| "Add" "Parametric" "Setoid" binders ":" constr constr constr "as" ident +| "Add" "Morphism" constr ":" ident +| "Declare" "Morphism" constr ":" ident +| "Add" "Morphism" constr "with" "signature" lconstr "as" ident +| "Add" "Parametric" "Morphism" binders ":" constr "with" "signature" lconstr "as" ident +| "Print" "Rewrite" "HintDb" preident +| "Reset" "Ltac" "Profile" +| "Show" "Ltac" "Profile" +| "Show" "Ltac" "Profile" "CutOff" int +| "Show" "Ltac" "Profile" string +| "Add" "Ring" ident ":" constr OPT ring_mods (* setoid_ring plugin *) +| "Print" "Rings" (* setoid_ring plugin *) +| "Add" "Field" ident ":" constr OPT field_mods (* setoid_ring plugin *) +| "Print" "Fields" (* setoid_ring plugin *) +| "Prenex" "Implicits" LIST1 global (* ssr plugin *) +| "Search" ssr_search_arg ssr_modlocs (* ssr plugin *) +| "Print" "Hint" "View" ssrviewpos (* ssr plugin *) +| "Hint" "View" ssrviewposspc LIST1 ssrhintref (* ssr plugin *) +| "Numeral" "Notation" reference reference reference ":" ident numnotoption +| "String" "Notation" reference reference reference ":" ident +] + +reference_or_constr: [ +| global +| constr +] + +hint: [ +| "Resolve" LIST1 reference_or_constr hint_info +| "Resolve" "->" LIST1 global OPT natural +| "Resolve" "<-" LIST1 global OPT natural +| "Immediate" LIST1 reference_or_constr +| "Variables" "Transparent" +| "Variables" "Opaque" +| "Constants" "Transparent" +| "Constants" "Opaque" +| "Transparent" LIST1 global +| "Opaque" LIST1 global +| "Mode" global mode +| "Unfold" LIST1 global +| "Constructors" LIST1 global +| "Extern" natural OPT Constr.constr_pattern "=>" Pltac.tactic +] + +constr_body: [ +| ":=" lconstr +| ":" lconstr ":=" lconstr +] + +mode: [ +| LIST1 [ "+" | "!" | "-" ] +] + +vernac_control: [ +| "Time" vernac_control +| "Redirect" ne_string vernac_control +| "Timeout" natural vernac_control +| "Fail" vernac_control +| decorated_vernac +] + +decorated_vernac: [ +| LIST0 quoted_attributes vernac +] + +quoted_attributes: [ +| "#[" attribute_list "]" +] + +attribute_list: [ +| LIST0 attribute SEP "," +] + +attribute: [ +| ident attribute_value +] + +attribute_value: [ +| "=" string +| "(" attribute_list ")" +| +] + +vernac: [ +| "Local" vernac_poly +| "Global" vernac_poly +| vernac_poly +] + +vernac_poly: [ +| "Polymorphic" vernac_aux +| "Monomorphic" vernac_aux +| vernac_aux +] + +vernac_aux: [ +| "Program" gallina "." +| "Program" gallina_ext "." +| gallina "." +| gallina_ext "." +| command "." +| syntax "." +| subprf +| command_entry +] + +noedit_mode: [ +| query_command +] + +subprf: [ +| BULLET +| "{" +| "}" +] + +gallina: [ +| thm_token ident_decl binders ":" lconstr LIST0 [ "with" ident_decl binders ":" lconstr ] +| assumption_token inline assum_list +| assumptions_token inline assum_list +| def_token ident_decl def_body +| "Let" identref def_body +| OPT cumulativity_token private_token finite_token LIST1 inductive_definition SEP "with" +| "Fixpoint" LIST1 rec_definition SEP "with" +| "Let" "Fixpoint" LIST1 rec_definition SEP "with" +| "CoFixpoint" LIST1 corec_definition SEP "with" +| "Let" "CoFixpoint" LIST1 corec_definition SEP "with" +| "Scheme" LIST1 scheme SEP "with" +| "Combined" "Scheme" identref "from" LIST1 identref SEP "," +| "Register" global "as" qualid +| "Register" "Inline" global +| "Primitive" identref OPT [ ":" lconstr ] ":=" register_token +| "Universe" LIST1 identref +| "Universes" LIST1 identref +| "Constraint" LIST1 univ_constraint SEP "," +] + +register_token: [ +| register_prim_token +| register_type_token +] + +register_type_token: [ +| "#int63_type" +] + +register_prim_token: [ +| "#int63_head0" +| "#int63_tail0" +| "#int63_add" +| "#int63_sub" +| "#int63_mul" +| "#int63_div" +| "#int63_mod" +| "#int63_lsr" +| "#int63_lsl" +| "#int63_land" +| "#int63_lor" +| "#int63_lxor" +| "#int63_addc" +| "#int63_subc" +| "#int63_addcarryc" +| "#int63_subcarryc" +| "#int63_mulc" +| "#int63_diveucl" +| "#int63_div21" +| "#int63_addmuldiv" +| "#int63_eq" +| "#int63_lt" +| "#int63_le" +| "#int63_compare" +] + +thm_token: [ +| "Theorem" +| "Lemma" +| "Fact" +| "Remark" +| "Corollary" +| "Proposition" +| "Property" +] + +def_token: [ +| "Definition" +| "Example" +| "SubClass" +] + +assumption_token: [ +| "Hypothesis" +| "Variable" +| "Axiom" +| "Parameter" +| "Conjecture" +] + +assumptions_token: [ +| "Hypotheses" +| "Variables" +| "Axioms" +| "Parameters" +| "Conjectures" +] + +inline: [ +| "Inline" "(" natural ")" +| "Inline" +| +] + +univ_constraint: [ +| universe_name [ "<" | "=" | "<=" ] universe_name +] + +univ_decl: [ +| "@{" LIST0 identref [ "+" | ] [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | bar_cbrace ] ] +] + +ident_decl: [ +| identref OPT univ_decl +] + +finite_token: [ +| "Inductive" +| "CoInductive" +| "Variant" +| "Record" +| "Structure" +| "Class" +] + +cumulativity_token: [ +| "Cumulative" +| "NonCumulative" +] + +private_token: [ +| "Private" +| +] + +def_body: [ +| binders ":=" reduce lconstr +| binders ":" lconstr ":=" reduce lconstr +| binders ":" lconstr +] + +reduce: [ +| "Eval" red_expr "in" +| +] + +one_decl_notation: [ +| ne_lstring ":=" constr OPT [ ":" IDENT ] +] + +decl_sep: [ +| "and" +] + +decl_notation: [ +| "where" LIST1 one_decl_notation SEP decl_sep +| +] + +opt_constructors_or_fields: [ +| ":=" constructor_list_or_record_decl +| +] + +inductive_definition: [ +| opt_coercion ident_decl binders OPT [ ":" lconstr ] opt_constructors_or_fields decl_notation +] + +constructor_list_or_record_decl: [ +| "|" LIST1 constructor SEP "|" +| identref constructor_type "|" LIST0 constructor SEP "|" +| identref constructor_type +| identref "{" record_fields "}" +| "{" record_fields "}" +| +] + +opt_coercion: [ +| ">" +| +] + +rec_definition: [ +| ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notation +] + +corec_definition: [ +| ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notation +] + +scheme: [ +| scheme_kind +| identref ":=" scheme_kind +] + +scheme_kind: [ +| "Induction" "for" smart_global "Sort" sort_family +| "Minimality" "for" smart_global "Sort" sort_family +| "Elimination" "for" smart_global "Sort" sort_family +| "Case" "for" smart_global "Sort" sort_family +| "Equality" "for" smart_global +] + +record_field: [ +| LIST0 quoted_attributes record_binder OPT [ "|" natural ] decl_notation +] + +record_binder_body: [ +| binders of_type_with_opt_coercion lconstr +| binders of_type_with_opt_coercion lconstr ":=" lconstr +| binders ":=" lconstr +] + +record_binder: [ +| name +| name record_binder_body +] + +assum_list: [ +| LIST1 assum_coe +| simple_assum_coe +] + +assum_coe: [ +| "(" simple_assum_coe ")" +] + +simple_assum_coe: [ +| LIST1 ident_decl of_type_with_opt_coercion lconstr +] + +constructor_type: [ +| binders [ of_type_with_opt_coercion lconstr | ] +] + +constructor: [ +| identref constructor_type +] + +of_type_with_opt_coercion: [ +| ":>>" +| ":>" ">" +| ":>" +| ":" ">" ">" +| ":" ">" +| ":" +] + +gallina_ext: [ +| "Module" export_token identref LIST0 module_binder of_module_type is_module_expr +| "Module" "Type" identref LIST0 module_binder check_module_types is_module_type +| "Declare" "Module" export_token identref LIST0 module_binder ":" module_type_inl +| "Section" identref +| "Chapter" identref +| "End" identref +| "Collection" identref ":=" section_subset_expr +| "Require" export_token LIST1 global +| "From" global "Require" export_token LIST1 global +| "Import" LIST1 global +| "Export" LIST1 global +| "Include" module_type_inl LIST0 ext_module_expr +| "Include" "Type" module_type_inl LIST0 ext_module_type +| "Transparent" LIST1 smart_global +| "Opaque" LIST1 smart_global +| "Strategy" LIST1 [ strategy_level "[" LIST1 smart_global "]" ] +| "Canonical" OPT "Structure" global OPT [ OPT univ_decl def_body ] +| "Canonical" OPT "Structure" by_notation +| "Coercion" global OPT univ_decl def_body +| "Identity" "Coercion" identref ":" class_rawexpr ">->" class_rawexpr +| "Coercion" global ":" class_rawexpr ">->" class_rawexpr +| "Coercion" by_notation ":" class_rawexpr ">->" class_rawexpr +| "Context" LIST1 binder +| "Instance" instance_name ":" operconstr200 hint_info [ ":=" "{" record_declaration "}" | ":=" lconstr | ] +| "Existing" "Instance" global hint_info +| "Existing" "Instances" LIST1 global OPT [ "|" natural ] +| "Existing" "Class" global +| "Arguments" smart_global LIST0 argument_spec_block OPT [ "," LIST1 [ LIST0 more_implicits_block ] SEP "," ] OPT [ ":" LIST1 arguments_modifier SEP "," ] +| "Implicit" "Type" reserv_list +| "Implicit" "Types" reserv_list +| "Generalizable" [ "All" "Variables" | "No" "Variables" | [ "Variable" | "Variables" ] LIST1 identref ] +| "Export" "Set" option_table option_setting +| "Export" "Unset" option_table +| "Import" "Prenex" "Implicits" (* ssr plugin *) +] + +export_token: [ +| "Import" +| "Export" +| +] + +ext_module_type: [ +| "<+" module_type_inl +] + +ext_module_expr: [ +| "<+" module_expr_inl +] + +check_module_type: [ +| "<:" module_type_inl +] + +check_module_types: [ +| LIST0 check_module_type +] + +of_module_type: [ +| ":" module_type_inl +| check_module_types +] + +is_module_type: [ +| ":=" module_type_inl LIST0 ext_module_type +| +] + +is_module_expr: [ +| ":=" module_expr_inl LIST0 ext_module_expr +| +] + +functor_app_annot: [ +| "[" "inline" "at" "level" natural "]" +| "[" "no" "inline" "]" +| +] + +module_expr_inl: [ +| "!" module_expr +| module_expr functor_app_annot +] + +module_type_inl: [ +| "!" module_type +| module_type functor_app_annot +] + +module_binder: [ +| "(" export_token LIST1 identref ":" module_type_inl ")" +] + +module_expr: [ +| module_expr_atom +| module_expr module_expr_atom +] + +module_expr_atom: [ +| qualid +| "(" module_expr ")" +] + +with_declaration: [ +| "Definition" fullyqualid OPT univ_decl ":=" Constr.lconstr +| "Module" fullyqualid ":=" qualid +] + +module_type: [ +| qualid +| "(" module_type ")" +| module_type module_expr_atom +| module_type "with" with_declaration +] + +section_subset_expr: [ +| only_starredidentrefs LIST0 starredidentref +| ssexpr35 +] + +starredidentref: [ +| identref +| identref "*" +| "Type" +| "Type" "*" +] + +ssexpr35: [ +| "-" ssexpr50 +| ssexpr50 +] + +ssexpr50: [ +| ssexpr0 "-" ssexpr0 +| ssexpr0 "+" ssexpr0 +| ssexpr0 +] + +ssexpr0: [ +| starredidentref +| "(" only_starredidentrefs LIST0 starredidentref ")" +| "(" only_starredidentrefs LIST0 starredidentref ")" "*" +| "(" ssexpr35 ")" +| "(" ssexpr35 ")" "*" +] + +arguments_modifier: [ +| "simpl" "nomatch" +| "simpl" "never" +| "default" "implicits" +| "clear" "implicits" +| "clear" "scopes" +| "clear" "bidirectionality" "hint" +| "rename" +| "assert" +| "extra" "scopes" +| "clear" "scopes" "and" "implicits" +| "clear" "implicits" "and" "scopes" +] + +scope: [ +| "%" IDENT +] + +argument_spec: [ +| OPT "!" name OPT scope +] + +argument_spec_block: [ +| argument_spec +| "/" +| "&" +| "(" LIST1 argument_spec ")" OPT scope +| "[" LIST1 argument_spec "]" OPT scope +| "{" LIST1 argument_spec "}" OPT scope +] + +more_implicits_block: [ +| name +| "[" LIST1 name "]" +| "{" LIST1 name "}" +] + +strategy_level: [ +| "expand" +| "opaque" +| integer +| "transparent" +] + +instance_name: [ +| ident_decl binders +| +] + +hint_info: [ +| "|" OPT natural OPT constr_pattern +| +] + +reserv_list: [ +| LIST1 reserv_tuple +| simple_reserv +] + +reserv_tuple: [ +| "(" simple_reserv ")" +] + +simple_reserv: [ +| LIST1 identref ":" lconstr +] + +query_command: [ +| "Eval" red_expr "in" lconstr "." +| "Compute" lconstr "." +| "Check" lconstr "." +| "About" smart_global OPT univ_name_list "." +| "SearchHead" constr_pattern in_or_out_modules "." +| "SearchPattern" constr_pattern in_or_out_modules "." +| "SearchRewrite" constr_pattern in_or_out_modules "." +| "Search" searchabout_query searchabout_queries "." +| "SearchAbout" searchabout_query searchabout_queries "." +| "SearchAbout" "[" LIST1 searchabout_query "]" in_or_out_modules "." +] + +printable: [ +| "Term" smart_global OPT univ_name_list +| "All" +| "Section" global +| "Grammar" IDENT +| "Custom" "Grammar" IDENT +| "LoadPath" OPT dirpath +| "Modules" +| "Libraries" +| "ML" "Path" +| "ML" "Modules" +| "Debug" "GC" +| "Graph" +| "Classes" +| "TypeClasses" +| "Instances" smart_global +| "Coercions" +| "Coercion" "Paths" class_rawexpr class_rawexpr +| "Canonical" "Projections" +| "Tables" +| "Options" +| "Hint" +| "Hint" smart_global +| "Hint" "*" +| "HintDb" IDENT +| "Scopes" +| "Scope" IDENT +| "Visibility" OPT IDENT +| "Implicit" smart_global +| [ "Sorted" | ] "Universes" OPT printunivs_subgraph OPT ne_string +| "Assumptions" smart_global +| "Opaque" "Dependencies" smart_global +| "Transparent" "Dependencies" smart_global +| "All" "Dependencies" smart_global +| "Strategy" smart_global +| "Strategies" +| "Registered" +] + +printunivs_subgraph: [ +| "Subgraph" "(" LIST0 reference ")" +] + +class_rawexpr: [ +| "Funclass" +| "Sortclass" +| smart_global +] + +locatable: [ +| smart_global +| "Term" smart_global +| "File" ne_string +| "Library" global +| "Module" global +] + +option_setting: [ +| +| integer +| STRING +] + +option_ref_value: [ +| global +| STRING +] + +option_table: [ +| LIST1 IDENT +] + +as_dirpath: [ +| OPT [ "as" dirpath ] +] + +ne_in_or_out_modules: [ +| "inside" LIST1 global +| "outside" LIST1 global +] + +in_or_out_modules: [ +| ne_in_or_out_modules +| +] + +comment: [ +| constr +| STRING +| natural +] + +positive_search_mark: [ +| "-" +| +] + +searchabout_query: [ +| positive_search_mark ne_string OPT scope +| positive_search_mark constr_pattern +] + +searchabout_queries: [ +| ne_in_or_out_modules +| searchabout_query searchabout_queries +| +] + +univ_name_list: [ +| "@{" LIST0 name "}" +] + +syntax: [ +| "Open" "Scope" IDENT +| "Close" "Scope" IDENT +| "Delimit" "Scope" IDENT; "with" IDENT +| "Undelimit" "Scope" IDENT +| "Bind" "Scope" IDENT; "with" LIST1 class_rawexpr +| "Infix" ne_lstring ":=" constr [ "(" LIST1 syntax_modifier SEP "," ")" | ] OPT [ ":" IDENT ] +| "Notation" identref LIST0 ident ":=" constr only_parsing +| "Notation" lstring ":=" constr [ "(" LIST1 syntax_modifier SEP "," ")" | ] OPT [ ":" IDENT ] +| "Format" "Notation" STRING STRING STRING +| "Reserved" "Infix" ne_lstring [ "(" LIST1 syntax_modifier SEP "," ")" | ] +| "Reserved" "Notation" ne_lstring [ "(" LIST1 syntax_modifier SEP "," ")" | ] +] + +only_parsing: [ +| "(" "only" "parsing" ")" +| "(" "compat" STRING ")" +| +] + +level: [ +| "level" natural +| "next" "level" +] + +syntax_modifier: [ +| "at" "level" natural +| "in" "custom" IDENT +| "in" "custom" IDENT; "at" "level" natural +| "left" "associativity" +| "right" "associativity" +| "no" "associativity" +| "only" "printing" +| "only" "parsing" +| "compat" STRING +| "format" STRING OPT STRING +| IDENT; "," LIST1 IDENT SEP "," "at" level +| IDENT; "at" level +| IDENT; "at" level constr_as_binder_kind +| IDENT constr_as_binder_kind +| IDENT syntax_extension_type +] + +syntax_extension_type: [ +| "ident" +| "global" +| "bigint" +| "binder" +| "constr" +| "constr" OPT at_level OPT constr_as_binder_kind +| "pattern" +| "pattern" "at" "level" natural +| "strict" "pattern" +| "strict" "pattern" "at" "level" natural +| "closed" "binder" +| "custom" IDENT OPT at_level OPT constr_as_binder_kind +] + +at_level: [ +| "at" level +] + +constr_as_binder_kind: [ +| "as" "ident" +| "as" "pattern" +| "as" "strict" "pattern" +] + +simple_tactic: [ +| "btauto" +| "congruence" +| "congruence" integer +| "congruence" "with" LIST1 constr +| "congruence" integer "with" LIST1 constr +| "f_equal" +| "firstorder" OPT tactic firstorder_using +| "firstorder" OPT tactic "with" LIST1 preident +| "firstorder" OPT tactic firstorder_using "with" LIST1 preident +| "gintuition" OPT tactic +| "functional" "inversion" quantified_hypothesis OPT reference (* funind plugin *) +| "functional" "induction" LIST1 constr fun_ind_using with_names (* funind plugin *) +| "soft" "functional" "induction" LIST1 constr fun_ind_using with_names (* funind plugin *) +| "reflexivity" +| "exact" casted_constr +| "assumption" +| "etransitivity" +| "cut" constr +| "exact_no_check" constr +| "vm_cast_no_check" constr +| "native_cast_no_check" constr +| "casetype" constr +| "elimtype" constr +| "lapply" constr +| "transitivity" constr +| "left" +| "eleft" +| "left" "with" bindings +| "eleft" "with" bindings +| "right" +| "eright" +| "right" "with" bindings +| "eright" "with" bindings +| "constructor" +| "constructor" int_or_var +| "constructor" int_or_var "with" bindings +| "econstructor" +| "econstructor" int_or_var +| "econstructor" int_or_var "with" bindings +| "specialize" constr_with_bindings +| "specialize" constr_with_bindings "as" simple_intropattern +| "symmetry" +| "symmetry" "in" in_clause +| "split" +| "esplit" +| "split" "with" bindings +| "esplit" "with" bindings +| "exists" +| "exists" LIST1 bindings SEP "," +| "eexists" +| "eexists" LIST1 bindings SEP "," +| "intros" "until" quantified_hypothesis +| "intro" +| "intro" ident +| "intro" ident "at" "top" +| "intro" ident "at" "bottom" +| "intro" ident "after" hyp +| "intro" ident "before" hyp +| "intro" "at" "top" +| "intro" "at" "bottom" +| "intro" "after" hyp +| "intro" "before" hyp +| "move" hyp "at" "top" +| "move" hyp "at" "bottom" +| "move" hyp "after" hyp +| "move" hyp "before" hyp +| "rename" LIST1 rename SEP "," +| "revert" LIST1 hyp +| "simple" "induction" quantified_hypothesis +| "simple" "destruct" quantified_hypothesis +| "double" "induction" quantified_hypothesis quantified_hypothesis +| "admit" +| "fix" ident natural +| "cofix" ident +| "clear" LIST0 hyp +| "clear" "-" LIST1 hyp +| "clearbody" LIST1 hyp +| "generalize" "dependent" constr +| "replace" uconstr "with" constr clause by_arg_tac +| "replace" "->" uconstr clause +| "replace" "<-" uconstr clause +| "replace" uconstr clause +| "simplify_eq" +| "simplify_eq" destruction_arg +| "esimplify_eq" +| "esimplify_eq" destruction_arg +| "discriminate" +| "discriminate" destruction_arg +| "ediscriminate" +| "ediscriminate" destruction_arg +| "injection" +| "injection" destruction_arg +| "einjection" +| "einjection" destruction_arg +| "injection" "as" LIST0 simple_intropattern +| "injection" destruction_arg "as" LIST0 simple_intropattern +| "einjection" "as" LIST0 simple_intropattern +| "einjection" destruction_arg "as" LIST0 simple_intropattern +| "simple" "injection" +| "simple" "injection" destruction_arg +| "dependent" "rewrite" orient constr +| "dependent" "rewrite" orient constr "in" hyp +| "cutrewrite" orient constr +| "cutrewrite" orient constr "in" hyp +| "decompose" "sum" constr +| "decompose" "record" constr +| "absurd" constr +| "contradiction" OPT constr_with_bindings +| "autorewrite" "with" LIST1 preident clause +| "autorewrite" "with" LIST1 preident clause "using" tactic +| "autorewrite" "*" "with" LIST1 preident clause +| "autorewrite" "*" "with" LIST1 preident clause "using" tactic +| "rewrite" "*" orient uconstr "in" hyp "at" occurrences by_arg_tac +| "rewrite" "*" orient uconstr "at" occurrences "in" hyp by_arg_tac +| "rewrite" "*" orient uconstr "in" hyp by_arg_tac +| "rewrite" "*" orient uconstr "at" occurrences by_arg_tac +| "rewrite" "*" orient uconstr by_arg_tac +| "refine" uconstr +| "simple" "refine" uconstr +| "notypeclasses" "refine" uconstr +| "simple" "notypeclasses" "refine" uconstr +| "solve_constraints" +| "subst" LIST1 var +| "subst" +| "simple" "subst" +| "evar" test_lpar_id_colon "(" ident ":" lconstr ")" +| "evar" constr +| "instantiate" "(" ident ":=" lglob ")" +| "instantiate" "(" integer ":=" lglob ")" hloc +| "instantiate" +| "stepl" constr "by" tactic +| "stepl" constr +| "stepr" constr "by" tactic +| "stepr" constr +| "generalize_eqs" hyp +| "dependent" "generalize_eqs" hyp +| "generalize_eqs_vars" hyp +| "dependent" "generalize_eqs_vars" hyp +| "specialize_eqs" hyp +| "hresolve_core" "(" ident ":=" constr ")" "at" int_or_var "in" constr +| "hresolve_core" "(" ident ":=" constr ")" "in" constr +| "hget_evar" int_or_var +| "destauto" +| "destauto" "in" hyp +| "transparent_abstract" tactic3 +| "transparent_abstract" tactic3 "using" ident +| "constr_eq" constr constr +| "constr_eq_strict" constr constr +| "constr_eq_nounivs" constr constr +| "is_evar" constr +| "has_evar" constr +| "is_var" constr +| "is_fix" constr +| "is_cofix" constr +| "is_ind" constr +| "is_constructor" constr +| "is_proj" constr +| "is_const" constr +| "shelve" +| "shelve_unifiable" +| "unshelve" tactic1 +| "give_up" +| "cycle" int_or_var +| "swap" int_or_var int_or_var +| "revgoals" +| "guard" test +| "decompose" "[" LIST1 constr "]" constr +| "optimize_heap" +| "eassumption" +| "eexact" constr +| "trivial" auto_using hintbases +| "info_trivial" auto_using hintbases +| "debug" "trivial" auto_using hintbases +| "auto" OPT int_or_var auto_using hintbases +| "info_auto" OPT int_or_var auto_using hintbases +| "debug" "auto" OPT int_or_var auto_using hintbases +| "prolog" "[" LIST0 uconstr "]" int_or_var +| "eauto" OPT int_or_var OPT int_or_var auto_using hintbases +| "new" "auto" OPT int_or_var auto_using hintbases +| "debug" "eauto" OPT int_or_var OPT int_or_var auto_using hintbases +| "info_eauto" OPT int_or_var OPT int_or_var auto_using hintbases +| "dfs" "eauto" OPT int_or_var auto_using hintbases +| "autounfold" hintbases clause_dft_concl +| "autounfold_one" hintbases "in" hyp +| "autounfold_one" hintbases +| "unify" constr constr +| "unify" constr constr "with" preident +| "convert_concl_no_check" constr +| "typeclasses" "eauto" "bfs" OPT int_or_var "with" LIST1 preident +| "typeclasses" "eauto" OPT int_or_var "with" LIST1 preident +| "typeclasses" "eauto" OPT int_or_var +| "head_of_constr" ident constr +| "not_evar" constr +| "is_ground" constr +| "autoapply" constr "using" preident +| "autoapply" constr "with" preident +| "progress_evars" tactic +| "decide" "equality" +| "compare" constr constr +| "rewrite_strat" rewstrategy "in" hyp +| "rewrite_strat" rewstrategy +| "rewrite_db" preident "in" hyp +| "rewrite_db" preident +| "substitute" orient glob_constr_with_bindings +| "setoid_rewrite" orient glob_constr_with_bindings +| "setoid_rewrite" orient glob_constr_with_bindings "in" hyp +| "setoid_rewrite" orient glob_constr_with_bindings "at" occurrences +| "setoid_rewrite" orient glob_constr_with_bindings "at" occurrences "in" hyp +| "setoid_rewrite" orient glob_constr_with_bindings "in" hyp "at" occurrences +| "setoid_symmetry" +| "setoid_symmetry" "in" hyp +| "setoid_reflexivity" +| "setoid_transitivity" constr +| "setoid_etransitivity" +| "intros" ne_intropatterns +| "intros" +| "eintros" ne_intropatterns +| "eintros" +| "apply" LIST1 constr_with_bindings_arg SEP "," in_hyp_as +| "eapply" LIST1 constr_with_bindings_arg SEP "," in_hyp_as +| "simple" "apply" LIST1 constr_with_bindings_arg SEP "," in_hyp_as +| "simple" "eapply" LIST1 constr_with_bindings_arg SEP "," in_hyp_as +| "elim" constr_with_bindings_arg OPT eliminator +| "eelim" constr_with_bindings_arg OPT eliminator +| "case" induction_clause_list +| "ecase" induction_clause_list +| "fix" ident natural "with" LIST1 fixdecl +| "cofix" ident "with" LIST1 cofixdecl +| "pose" bindings_with_parameters +| "pose" constr as_name +| "epose" bindings_with_parameters +| "epose" constr as_name +| "set" bindings_with_parameters clause_dft_concl +| "set" constr as_name clause_dft_concl +| "eset" bindings_with_parameters clause_dft_concl +| "eset" constr as_name clause_dft_concl +| "remember" constr as_name eqn_ipat clause_dft_all +| "eremember" constr as_name eqn_ipat clause_dft_all +| "assert" test_lpar_id_coloneq "(" identref ":=" lconstr ")" +| "eassert" test_lpar_id_coloneq "(" identref ":=" lconstr ")" +| "assert" test_lpar_id_colon "(" identref ":" lconstr ")" by_tactic +| "eassert" test_lpar_id_colon "(" identref ":" lconstr ")" by_tactic +| "enough" test_lpar_id_colon "(" identref ":" lconstr ")" by_tactic +| "eenough" test_lpar_id_colon "(" identref ":" lconstr ")" by_tactic +| "assert" constr as_ipat by_tactic +| "eassert" constr as_ipat by_tactic +| "pose" "proof" lconstr as_ipat +| "epose" "proof" lconstr as_ipat +| "enough" constr as_ipat by_tactic +| "eenough" constr as_ipat by_tactic +| "generalize" constr +| "generalize" constr LIST1 constr +| "generalize" constr lookup_at_as_comma occs as_name LIST0 [ "," pattern_occ as_name ] +| "induction" induction_clause_list +| "einduction" induction_clause_list +| "destruct" induction_clause_list +| "edestruct" induction_clause_list +| "rewrite" LIST1 oriented_rewriter SEP "," clause_dft_concl by_tactic +| "erewrite" LIST1 oriented_rewriter SEP "," clause_dft_concl by_tactic +| "dependent" [ "simple" "inversion" | "inversion" | "inversion_clear" ] quantified_hypothesis as_or_and_ipat OPT [ "with" constr ] +| "simple" "inversion" quantified_hypothesis as_or_and_ipat in_hyp_list +| "inversion" quantified_hypothesis as_or_and_ipat in_hyp_list +| "inversion_clear" quantified_hypothesis as_or_and_ipat in_hyp_list +| "inversion" quantified_hypothesis "using" constr in_hyp_list +| "red" clause_dft_concl +| "hnf" clause_dft_concl +| "simpl" delta_flag OPT ref_or_pattern_occ clause_dft_concl +| "cbv" strategy_flag clause_dft_concl +| "cbn" strategy_flag clause_dft_concl +| "lazy" strategy_flag clause_dft_concl +| "compute" delta_flag clause_dft_concl +| "vm_compute" OPT ref_or_pattern_occ clause_dft_concl +| "native_compute" OPT ref_or_pattern_occ clause_dft_concl +| "unfold" LIST1 unfold_occ SEP "," clause_dft_concl +| "fold" LIST1 constr clause_dft_concl +| "pattern" LIST1 pattern_occ SEP "," clause_dft_concl +| "change" conversion clause_dft_concl +| "change_no_check" conversion clause_dft_concl +| "start" "ltac" "profiling" +| "stop" "ltac" "profiling" +| "reset" "ltac" "profile" +| "show" "ltac" "profile" +| "show" "ltac" "profile" "cutoff" int +| "show" "ltac" "profile" string +| "restart_timer" OPT string +| "finish_timing" OPT string +| "finish_timing" "(" string ")" OPT string +| "myred" (* micromega plugin *) +| "psatz_Z" int_or_var tactic (* micromega plugin *) +| "psatz_Z" tactic (* micromega plugin *) +| "xlia" tactic (* micromega plugin *) +| "xnlia" tactic (* micromega plugin *) +| "xnra" tactic (* micromega plugin *) +| "xnqa" tactic (* micromega plugin *) +| "sos_Z" tactic (* micromega plugin *) +| "sos_Q" tactic (* micromega plugin *) +| "sos_R" tactic (* micromega plugin *) +| "lra_Q" tactic (* micromega plugin *) +| "lra_R" tactic (* micromega plugin *) +| "psatz_R" int_or_var tactic (* micromega plugin *) +| "psatz_R" tactic (* micromega plugin *) +| "psatz_Q" int_or_var tactic (* micromega plugin *) +| "psatz_Q" tactic (* micromega plugin *) +| "nsatz_compute" constr (* nsatz plugin *) +| "omega" (* omega plugin *) +| "omega" "with" LIST1 ident (* omega plugin *) +| "omega" "with" "*" (* omega plugin *) +| "rtauto" +| "protect_fv" string "in" ident (* setoid_ring plugin *) +| "protect_fv" string (* setoid_ring plugin *) +| "ring_lookup" tactic0 "[" LIST0 constr "]" LIST1 constr (* setoid_ring plugin *) +| "field_lookup" tactic "[" LIST0 constr "]" LIST1 constr (* setoid_ring plugin *) +| "YouShouldNotTypeThis" ssrintrosarg (* ssr plugin *) +| "by" ssrhintarg (* ssr plugin *) +| "YouShouldNotTypeThis" "do" ssrdoarg (* ssr plugin *) +| "YouShouldNotTypeThis" ssrtclarg ssrseqdir ssrseqarg (* ssr plugin *) +| "clear" natural (* ssr plugin *) +| "move" ssrmovearg ssrrpat (* ssr plugin *) +| "move" ssrmovearg ssrclauses (* ssr plugin *) +| "move" ssrrpat (* ssr plugin *) +| "move" (* ssr plugin *) +| "case" ssrcasearg ssrclauses (* ssr plugin *) +| "case" (* ssr plugin *) +| "elim" ssrarg ssrclauses (* ssr plugin *) +| "elim" (* ssr plugin *) +| "apply" ssrapplyarg (* ssr plugin *) +| "apply" (* ssr plugin *) +| "exact" ssrexactarg (* ssr plugin *) +| "exact" (* ssr plugin *) +| "exact" "<:" lconstr (* ssr plugin *) +| "congr" ssrcongrarg (* ssr plugin *) +| "ssrinstancesofruleL2R" ssrterm (* ssr plugin *) +| "ssrinstancesofruleR2L" ssrterm (* ssr plugin *) +| "rewrite" ssrrwargs ssrclauses (* ssr plugin *) +| "unlock" ssrunlockargs ssrclauses (* ssr plugin *) +| "pose" ssrfixfwd (* ssr plugin *) +| "pose" ssrcofixfwd (* ssr plugin *) +| "pose" ssrfwdid ssrposefwd (* ssr plugin *) +| "set" ssrfwdid ssrsetfwd ssrclauses (* ssr plugin *) +| "abstract" ssrdgens (* ssr plugin *) +| "have" ssrhavefwdwbinders (* ssr plugin *) +| "have" "suff" ssrhpats_nobs ssrhavefwd (* ssr plugin *) +| "have" "suffices" ssrhpats_nobs ssrhavefwd (* ssr plugin *) +| "suff" "have" ssrhpats_nobs ssrhavefwd (* ssr plugin *) +| "suffices" "have" ssrhpats_nobs ssrhavefwd (* ssr plugin *) +| "suff" ssrsufffwd (* ssr plugin *) +| "suffices" ssrsufffwd (* ssr plugin *) +| "wlog" ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "wlog" "suff" ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "wlog" "suffices" ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "without" "loss" ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "without" "loss" "suff" ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "without" "loss" "suffices" ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "gen" "have" ssrclear ssr_idcomma ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "generally" "have" ssrclear ssr_idcomma ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "under" ssrrwarg (* ssr plugin *) +| "under" ssrrwarg ssrintros_ne (* ssr plugin *) +| "under" ssrrwarg ssrintros_ne "do" ssrhint3arg (* ssr plugin *) +| "under" ssrrwarg "do" ssrhint3arg (* ssr plugin *) +| "ssrinstancesoftpat" cpattern (* ssrmatching plugin *) +] + +mlname: [ +| preident (* extraction plugin *) +| string (* extraction plugin *) +] + +int_or_id: [ +| preident (* extraction plugin *) +| integer (* extraction plugin *) +] + +language: [ +| "Ocaml" (* extraction plugin *) +| "OCaml" (* extraction plugin *) +| "Haskell" (* extraction plugin *) +| "Scheme" (* extraction plugin *) +| "JSON" (* extraction plugin *) +] + +firstorder_using: [ +| "using" reference +| "using" reference "," LIST1 reference SEP "," +| "using" reference reference LIST0 reference +| +] + +fun_ind_using: [ +| "using" constr_with_bindings (* funind plugin *) +| (* funind plugin *) +] + +with_names: [ +| "as" simple_intropattern (* funind plugin *) +| (* funind plugin *) +] + +constr_comma_sequence': [ +| constr "," constr_comma_sequence' (* funind plugin *) +| constr (* funind plugin *) +] + +auto_using': [ +| "using" constr_comma_sequence' (* funind plugin *) +| (* funind plugin *) +] + +function_rec_definition_loc: [ +| Vernac.rec_definition (* funind plugin *) +] + +fun_scheme_arg: [ +| ident ":=" "Induction" "for" reference "Sort" sort_family (* funind plugin *) +] + +orient: [ +| "->" +| "<-" +| +] + +occurrences: [ +| LIST1 integer +| var +] + +glob: [ +| constr +] + +lglob: [ +| lconstr +] + +casted_constr: [ +| constr +] + +hloc: [ +| +| "in" "|-" "*" +| "in" ident +| "in" "(" "Type" "of" ident ")" +| "in" "(" "Value" "of" ident ")" +| "in" "(" "type" "of" ident ")" +| "in" "(" "value" "of" ident ")" +] + +rename: [ +| ident "into" ident +] + +by_arg_tac: [ +| "by" tactic3 +| +] + +in_clause: [ +| in_clause' +| "*" occs +| "*" "|-" concl_occ +| LIST0 hypident_occ SEP "," "|-" concl_occ +| LIST0 hypident_occ SEP "," +] + +test_lpar_id_colon: [ +| local_test_lpar_id_colon +] + +orient_string: [ +| orient preident +] + +comparison: [ +| "=" +| "<" +| "<=" +| ">" +| ">=" +] + +test: [ +| int_or_var comparison int_or_var +] + +hintbases: [ +| "with" "*" +| "with" LIST1 preident +| +] + +auto_using: [ +| "using" LIST1 uconstr SEP "," +| +] + +hints_path_atom: [ +| LIST1 global +| "_" +] + +hints_path: [ +| "(" hints_path ")" +| hints_path "*" +| "emp" +| "eps" +| hints_path "|" hints_path +| hints_path_atom +| hints_path hints_path +] + +opthints: [ +| ":" LIST1 preident +| +] + +debug: [ +| "debug" +| +] + +eauto_search_strategy: [ +| "(bfs)" +| "(dfs)" +| +] + +tactic_then_last: [ +| "|" LIST0 ( OPT tactic_expr5 ) SEP "|" +| +] + +tactic_then_gen: [ +| tactic_expr5 "|" tactic_then_gen +| tactic_expr5 ".." tactic_then_last +| ".." tactic_then_last +| tactic_expr5 +| "|" tactic_then_gen +| +] + +tactic_then_locality: [ +| "[" OPT ">" +] + +tactic_expr5: [ +| binder_tactic +| tactic_expr4 +] + +tactic_expr4: [ +| tactic_expr3 ";" binder_tactic +| tactic_expr3 ";" tactic_expr3 +| tactic_expr3 ";" tactic_then_locality tactic_then_gen "]" +| tactic_expr3 +| tactic_expr5 ";" "first" ssr_first_else (* ssr plugin *) +| tactic_expr5 ";" "first" ssrseqarg (* ssr plugin *) +| tactic_expr5 ";" "last" ssrseqarg (* ssr plugin *) +] + +tactic_expr3: [ +| "try" tactic_expr3 +| "do" int_or_var tactic_expr3 +| "timeout" int_or_var tactic_expr3 +| "time" OPT string tactic_expr3 +| "repeat" tactic_expr3 +| "progress" tactic_expr3 +| "once" tactic_expr3 +| "exactly_once" tactic_expr3 +| "infoH" tactic_expr3 +| "abstract" tactic_expr2 +| "abstract" tactic_expr2 "using" ident +| selector tactic_expr3 +| tactic_expr2 +| "do" ssrmmod ssrdotac ssrclauses (* ssr plugin *) +| "do" ssrortacarg ssrclauses (* ssr plugin *) +| "do" int_or_var ssrmmod ssrdotac ssrclauses (* ssr plugin *) +| "abstract" ssrdgens (* ssr plugin *) +] + +tactic_expr2: [ +| tactic_expr1 "+" binder_tactic +| tactic_expr1 "+" tactic_expr2 +| "tryif" tactic_expr5 "then" tactic_expr5 "else" tactic_expr2 +| tactic_expr1 "||" binder_tactic +| tactic_expr1 "||" tactic_expr2 +| tactic_expr1 +] + +tactic_expr1: [ +| match_key "goal" "with" match_context_list "end" +| match_key "reverse" "goal" "with" match_context_list "end" +| match_key tactic_expr5 "with" match_list "end" +| "first" "[" LIST0 tactic_expr5 SEP "|" "]" +| "solve" "[" LIST0 tactic_expr5 SEP "|" "]" +| "idtac" LIST0 message_token +| failkw [ int_or_var | ] LIST0 message_token +| simple_tactic +| tactic_arg +| reference LIST0 tactic_arg_compat +| tactic_expr0 +| tactic_expr5 ssrintros_ne (* ssr plugin *) +] + +tactic_expr0: [ +| "(" tactic_expr5 ")" +| "[" ">" tactic_then_gen "]" +| tactic_atom +| ssrparentacarg (* ssr plugin *) +] + +failkw: [ +| "fail" +| "gfail" +] + +binder_tactic: [ +| "fun" LIST1 input_fun "=>" tactic_expr5 +| "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" tactic_expr5 +| "info" tactic_expr5 +] + +tactic_arg_compat: [ +| tactic_arg +| Constr.constr +| "()" +] + +tactic_arg: [ +| constr_eval +| "fresh" LIST0 fresh_id +| "type_term" uconstr +| "numgoals" +] + +fresh_id: [ +| STRING +| qualid +] + +constr_eval: [ +| "eval" red_expr "in" Constr.constr +| "context" identref "[" Constr.lconstr "]" +| "type" "of" Constr.constr +] + +constr_may_eval: [ +| constr_eval +| Constr.constr +] + +tactic_atom: [ +| integer +| reference +| "()" +] + +match_key: [ +| "match" +| "lazymatch" +| "multimatch" +] + +input_fun: [ +| "_" +| ident +] + +let_clause: [ +| identref ":=" tactic_expr5 +| "_" ":=" tactic_expr5 +| identref LIST1 input_fun ":=" tactic_expr5 +] + +match_pattern: [ +| "context" OPT Constr.ident "[" Constr.lconstr_pattern "]" +| Constr.lconstr_pattern +] + +match_hyps: [ +| name ":" match_pattern +| name ":=" "[" match_pattern "]" ":" match_pattern +| name ":=" match_pattern +] + +match_context_rule: [ +| LIST0 match_hyps SEP "," "|-" match_pattern "=>" tactic_expr5 +| "[" LIST0 match_hyps SEP "," "|-" match_pattern "]" "=>" tactic_expr5 +| "_" "=>" tactic_expr5 +] + +match_context_list: [ +| LIST1 match_context_rule SEP "|" +| "|" LIST1 match_context_rule SEP "|" +] + +match_rule: [ +| match_pattern "=>" tactic_expr5 +| "_" "=>" tactic_expr5 +] + +match_list: [ +| LIST1 match_rule SEP "|" +| "|" LIST1 match_rule SEP "|" +] + +message_token: [ +| identref +| STRING +| integer +] + +ltac_def_kind: [ +| ":=" +| "::=" +] + +tacdef_body: [ +| Constr.global LIST1 input_fun ltac_def_kind tactic_expr5 +| Constr.global ltac_def_kind tactic_expr5 +] + +tactic: [ +| tactic_expr5 +] + +range_selector: [ +| natural "-" natural +| natural +] + +range_selector_or_nth: [ +| natural "-" natural OPT [ "," LIST1 range_selector SEP "," ] +| natural OPT [ "," LIST1 range_selector SEP "," ] +] + +selector_body: [ +| range_selector_or_nth +| test_bracket_ident "[" ident "]" +] + +selector: [ +| "only" selector_body ":" +] + +toplevel_selector: [ +| selector_body ":" +| "!" ":" +| "all" ":" +] + +tactic_mode: [ +| OPT toplevel_selector G_vernac.query_command +| OPT toplevel_selector "{" +| OPT ltac_selector OPT ltac_info tactic ltac_use_default +| "par" ":" OPT ltac_info tactic ltac_use_default +] + +ltac_selector: [ +| toplevel_selector +] + +ltac_info: [ +| "Info" natural +] + +ltac_use_default: [ +| "." +| "..." +] + +ltac_tactic_level: [ +| "(" "at" "level" natural ")" +] + +ltac_production_sep: [ +| "," string +] + +ltac_production_item: [ +| string +| ident "(" ident OPT ltac_production_sep ")" +| ident +] + +ltac_tacdef_body: [ +| tacdef_body +] + +withtac: [ +| "with" Tactic.tactic +| +] + +Constr.closed_binder: [ +| "(" Prim.name ":" Constr.lconstr "|" Constr.lconstr ")" +] + +glob_constr_with_bindings: [ +| constr_with_bindings +] + +rewstrategy: [ +| glob +| "<-" constr +| "subterms" rewstrategy +| "subterm" rewstrategy +| "innermost" rewstrategy +| "outermost" rewstrategy +| "bottomup" rewstrategy +| "topdown" rewstrategy +| "id" +| "fail" +| "refl" +| "progress" rewstrategy +| "try" rewstrategy +| "any" rewstrategy +| "repeat" rewstrategy +| rewstrategy ";" rewstrategy +| "(" rewstrategy ")" +| "choice" rewstrategy rewstrategy +| "old_hints" preident +| "hints" preident +| "terms" LIST0 constr +| "eval" red_expr +| "fold" constr +] + +int_or_var: [ +| integer +| identref +] + +nat_or_var: [ +| natural +| identref +] + +id_or_meta: [ +| identref +] + +open_constr: [ +| constr +] + +uconstr: [ +| constr +] + +destruction_arg: [ +| natural +| test_lpar_id_rpar constr_with_bindings +| constr_with_bindings_arg +] + +constr_with_bindings_arg: [ +| ">" constr_with_bindings +| constr_with_bindings +] + +quantified_hypothesis: [ +| ident +| natural +] + +conversion: [ +| constr +| constr "with" constr +| constr "at" occs_nums "with" constr +] + +occs_nums: [ +| LIST1 nat_or_var +| "-" nat_or_var LIST0 int_or_var +] + +occs: [ +| "at" occs_nums +| +] + +pattern_occ: [ +| constr occs +] + +ref_or_pattern_occ: [ +| smart_global occs +| constr occs +] + +unfold_occ: [ +| smart_global occs +] + +intropatterns: [ +| LIST0 intropattern +] + +ne_intropatterns: [ +| LIST1 intropattern +] + +or_and_intropattern: [ +| "[" LIST1 intropatterns SEP "|" "]" +| "()" +| "(" simple_intropattern ")" +| "(" simple_intropattern "," LIST1 simple_intropattern SEP "," ")" +| "(" simple_intropattern "&" LIST1 simple_intropattern SEP "&" ")" +] + +equality_intropattern: [ +| "->" +| "<-" +| "[=" intropatterns "]" +] + +naming_intropattern: [ +| pattern_ident +| "?" +| ident +] + +intropattern: [ +| simple_intropattern +| "*" +| "**" +] + +simple_intropattern: [ +| simple_intropattern_closed LIST0 [ "%" operconstr0 ] +] + +simple_intropattern_closed: [ +| or_and_intropattern +| equality_intropattern +| "_" +| naming_intropattern +] + +simple_binding: [ +| "(" ident ":=" lconstr ")" +| "(" natural ":=" lconstr ")" +] + +bindings: [ +| test_lpar_idnum_coloneq LIST1 simple_binding +| LIST1 constr +] + +constr_with_bindings: [ +| constr with_bindings +] + +with_bindings: [ +| "with" bindings +| +] + +red_flags: [ +| "beta" +| "iota" +| "match" +| "fix" +| "cofix" +| "zeta" +| "delta" delta_flag +] + +delta_flag: [ +| "-" "[" LIST1 smart_global "]" +| "[" LIST1 smart_global "]" +| +] + +strategy_flag: [ +| LIST1 red_flags +| delta_flag +] + +red_expr: [ +| "red" +| "hnf" +| "simpl" delta_flag OPT ref_or_pattern_occ +| "cbv" strategy_flag +| "cbn" strategy_flag +| "lazy" strategy_flag +| "compute" delta_flag +| "vm_compute" OPT ref_or_pattern_occ +| "native_compute" OPT ref_or_pattern_occ +| "unfold" LIST1 unfold_occ SEP "," +| "fold" LIST1 constr +| "pattern" LIST1 pattern_occ SEP "," +| IDENT +] + +hypident: [ +| id_or_meta +| "(" "type" "of" id_or_meta ")" +| "(" "value" "of" id_or_meta ")" +| "(" "type" "of" Prim.identref ")" (* ssr plugin *) +| "(" "value" "of" Prim.identref ")" (* ssr plugin *) +] + +hypident_occ: [ +| hypident occs +] + +clause_dft_concl: [ +| "in" in_clause +| occs +| +] + +clause_dft_all: [ +| "in" in_clause +| +] + +opt_clause: [ +| "in" in_clause +| "at" occs_nums +| +] + +concl_occ: [ +| "*" occs +| +] + +in_hyp_list: [ +| "in" LIST1 id_or_meta +| +] + +in_hyp_as: [ +| "in" id_or_meta as_ipat +| +] + +simple_binder: [ +| name +| "(" LIST1 name ":" lconstr ")" +] + +fixdecl: [ +| "(" ident LIST0 simple_binder fixannot ":" lconstr ")" +] + +cofixdecl: [ +| "(" ident LIST0 simple_binder ":" lconstr ")" +] + +bindings_with_parameters: [ +| check_for_coloneq "(" ident LIST0 simple_binder ":=" lconstr ")" +] + +eliminator: [ +| "using" constr_with_bindings +] + +as_ipat: [ +| "as" simple_intropattern +| +] + +or_and_intropattern_loc: [ +| or_and_intropattern +| identref +] + +as_or_and_ipat: [ +| "as" or_and_intropattern_loc +| +] + +eqn_ipat: [ +| "eqn" ":" naming_intropattern +| "_eqn" ":" naming_intropattern +| "_eqn" +| +] + +as_name: [ +| "as" ident +| +] + +by_tactic: [ +| "by" tactic_expr3 +| +] + +rewriter: [ +| "!" constr_with_bindings_arg +| [ "?" | LEFTQMARK ] constr_with_bindings_arg +| natural "!" constr_with_bindings_arg +| natural [ "?" | LEFTQMARK ] constr_with_bindings_arg +| natural constr_with_bindings_arg +| constr_with_bindings_arg +] + +oriented_rewriter: [ +| orient rewriter +] + +induction_clause: [ +| destruction_arg as_or_and_ipat eqn_ipat opt_clause +] + +induction_clause_list: [ +| LIST1 induction_clause SEP "," OPT eliminator opt_clause +] + +ring_mod: [ +| "decidable" constr (* setoid_ring plugin *) +| "abstract" (* setoid_ring plugin *) +| "morphism" constr (* setoid_ring plugin *) +| "constants" "[" tactic "]" (* setoid_ring plugin *) +| "closed" "[" LIST1 global "]" (* setoid_ring plugin *) +| "preprocess" "[" tactic "]" (* setoid_ring plugin *) +| "postprocess" "[" tactic "]" (* setoid_ring plugin *) +| "setoid" constr constr (* setoid_ring plugin *) +| "sign" constr (* setoid_ring plugin *) +| "power" constr "[" LIST1 global "]" (* setoid_ring plugin *) +| "power_tac" constr "[" tactic "]" (* setoid_ring plugin *) +| "div" constr (* setoid_ring plugin *) +] + +ring_mods: [ +| "(" LIST1 ring_mod SEP "," ")" (* setoid_ring plugin *) +] + +field_mod: [ +| ring_mod (* setoid_ring plugin *) +| "completeness" constr (* setoid_ring plugin *) +] + +field_mods: [ +| "(" LIST1 field_mod SEP "," ")" (* setoid_ring plugin *) +] + +ssrtacarg: [ +| tactic_expr5 (* ssr plugin *) +] + +ssrtac3arg: [ +| tactic_expr3 (* ssr plugin *) +] + +ssrtclarg: [ +| ssrtacarg (* ssr plugin *) +] + +ssrhyp: [ +| ident (* ssr plugin *) +] + +ssrhoi_hyp: [ +| ident (* ssr plugin *) +] + +ssrhoi_id: [ +| ident (* ssr plugin *) +] + +ssrsimpl_ne: [ +| "//=" (* ssr plugin *) +| "/=" (* ssr plugin *) +| test_ssrslashnum11 "/" natural "/" natural "=" (* ssr plugin *) +| test_ssrslashnum10 "/" natural "/" (* ssr plugin *) +| test_ssrslashnum10 "/" natural "=" (* ssr plugin *) +| test_ssrslashnum10 "/" natural "/=" (* ssr plugin *) +| test_ssrslashnum10 "/" natural "/" "=" (* ssr plugin *) +| test_ssrslashnum01 "//" natural "=" (* ssr plugin *) +| test_ssrslashnum00 "//" (* ssr plugin *) +] + +ssrclear_ne: [ +| "{" LIST1 ssrhyp "}" (* ssr plugin *) +] + +ssrclear: [ +| ssrclear_ne (* ssr plugin *) +| (* ssr plugin *) +] + +ssrindex: [ +| int_or_var (* ssr plugin *) +] + +ssrocc: [ +| natural LIST0 natural (* ssr plugin *) +| "-" LIST0 natural (* ssr plugin *) +| "+" LIST0 natural (* ssr plugin *) +] + +ssrmmod: [ +| "!" (* ssr plugin *) +| LEFTQMARK (* ssr plugin *) +| "?" (* ssr plugin *) +] + +ssrmult_ne: [ +| natural ssrmmod (* ssr plugin *) +| ssrmmod (* ssr plugin *) +] + +ssrmult: [ +| ssrmult_ne (* ssr plugin *) +| (* ssr plugin *) +] + +ssrdocc: [ +| "{" ssrocc "}" (* ssr plugin *) +| "{" LIST0 ssrhyp "}" (* ssr plugin *) +] + +ssrterm: [ +| "YouShouldNotTypeThis" constr (* ssr plugin *) +| ssrtermkind Pcoq.Constr.constr (* ssr plugin *) +] + +ast_closure_term: [ +| term_annotation constr (* ssr plugin *) +] + +ast_closure_lterm: [ +| term_annotation lconstr (* ssr plugin *) +] + +ssrbwdview: [ +| "YouShouldNotTypeThis" (* ssr plugin *) +| test_not_ssrslashnum "/" Pcoq.Constr.constr (* ssr plugin *) +| test_not_ssrslashnum "/" Pcoq.Constr.constr ssrbwdview (* ssr plugin *) +] + +ssrfwdview: [ +| "YouShouldNotTypeThis" (* ssr plugin *) +| test_not_ssrslashnum "/" ast_closure_term (* ssr plugin *) +| test_not_ssrslashnum "/" ast_closure_term ssrfwdview (* ssr plugin *) +] + +ident_no_do: [ +| "YouShouldNotTypeThis" ident (* ssr plugin *) +| test_ident_no_do IDENT (* ssr plugin *) +] + +ssripat: [ +| "_" (* ssr plugin *) +| "*" (* ssr plugin *) +| ">" (* ssr plugin *) +| ident_no_do (* ssr plugin *) +| "?" (* ssr plugin *) +| "+" (* ssr plugin *) +| "++" (* ssr plugin *) +| ssrsimpl_ne (* ssr plugin *) +| ssrdocc "->" (* ssr plugin *) +| ssrdocc "<-" (* ssr plugin *) +| ssrdocc (* ssr plugin *) +| "->" (* ssr plugin *) +| "<-" (* ssr plugin *) +| "-" (* ssr plugin *) +| "-/" "=" (* ssr plugin *) +| "-/=" (* ssr plugin *) +| "-/" "/" (* ssr plugin *) +| "-//" (* ssr plugin *) +| "-/" integer "/" (* ssr plugin *) +| "-/" "/=" (* ssr plugin *) +| "-//" "=" (* ssr plugin *) +| "-//=" (* ssr plugin *) +| "-/" integer "/=" (* ssr plugin *) +| "-/" integer "/" integer "=" (* ssr plugin *) +| ssrfwdview (* ssr plugin *) +| "[" ":" LIST0 ident "]" (* ssr plugin *) +| "[:" LIST0 ident "]" (* ssr plugin *) +| ssrcpat (* ssr plugin *) +] + +ssripats: [ +| ssripat ssripats (* ssr plugin *) +| (* ssr plugin *) +] + +ssriorpat: [ +| ssripats "|" ssriorpat (* ssr plugin *) +| ssripats "|-" ">" ssriorpat (* ssr plugin *) +| ssripats "|-" ssriorpat (* ssr plugin *) +| ssripats "|->" ssriorpat (* ssr plugin *) +| ssripats "||" ssriorpat (* ssr plugin *) +| ssripats "|||" ssriorpat (* ssr plugin *) +| ssripats "||||" ssriorpat (* ssr plugin *) +| ssripats (* ssr plugin *) +] + +ssrcpat: [ +| "YouShouldNotTypeThis" ssriorpat (* ssr plugin *) +| test_nohidden "[" hat "]" (* ssr plugin *) +| test_nohidden "[" ssriorpat "]" (* ssr plugin *) +| test_nohidden "[=" ssriorpat "]" (* ssr plugin *) +] + +hat: [ +| "^" ident (* ssr plugin *) +| "^" "~" ident (* ssr plugin *) +| "^" "~" natural (* ssr plugin *) +| "^~" ident (* ssr plugin *) +| "^~" natural (* ssr plugin *) +] + +ssripats_ne: [ +| ssripat ssripats (* ssr plugin *) +] + +ssrhpats: [ +| ssripats (* ssr plugin *) +] + +ssrhpats_wtransp: [ +| ssripats (* ssr plugin *) +| ssripats "@" ssripats (* ssr plugin *) +] + +ssrhpats_nobs: [ +| ssripats (* ssr plugin *) +] + +ssrrpat: [ +| "->" (* ssr plugin *) +| "<-" (* ssr plugin *) +] + +ssrintros_ne: [ +| "=>" ssripats_ne (* ssr plugin *) +] + +ssrintros: [ +| ssrintros_ne (* ssr plugin *) +| (* ssr plugin *) +] + +ssrintrosarg: [ +| "YouShouldNotTypeThis" ssrtacarg ssrintros_ne (* ssr plugin *) +] + +ssrfwdid: [ +| test_ssrfwdid Prim.ident (* ssr plugin *) +] + +ssrortacs: [ +| ssrtacarg "|" ssrortacs (* ssr plugin *) +| ssrtacarg "|" (* ssr plugin *) +| ssrtacarg (* ssr plugin *) +| "|" ssrortacs (* ssr plugin *) +| "|" (* ssr plugin *) +] + +ssrhintarg: [ +| "[" "]" (* ssr plugin *) +| "[" ssrortacs "]" (* ssr plugin *) +| ssrtacarg (* ssr plugin *) +] + +ssrhint3arg: [ +| "[" "]" (* ssr plugin *) +| "[" ssrortacs "]" (* ssr plugin *) +| ssrtac3arg (* ssr plugin *) +] + +ssrortacarg: [ +| "[" ssrortacs "]" (* ssr plugin *) +] + +ssrhint: [ +| (* ssr plugin *) +| "by" ssrhintarg (* ssr plugin *) +] + +ssrwgen: [ +| ssrclear_ne (* ssr plugin *) +| ssrhoi_hyp (* ssr plugin *) +| "@" ssrhoi_hyp (* ssr plugin *) +| "(" ssrhoi_id ":=" lcpattern ")" (* ssr plugin *) +| "(" ssrhoi_id ")" (* ssr plugin *) +| "(@" ssrhoi_id ":=" lcpattern ")" (* ssr plugin *) +| "(" "@" ssrhoi_id ":=" lcpattern ")" (* ssr plugin *) +] + +ssrclausehyps: [ +| ssrwgen "," ssrclausehyps (* ssr plugin *) +| ssrwgen ssrclausehyps (* ssr plugin *) +| ssrwgen (* ssr plugin *) +] + +ssrclauses: [ +| "in" ssrclausehyps "|-" "*" (* ssr plugin *) +| "in" ssrclausehyps "|-" (* ssr plugin *) +| "in" ssrclausehyps "*" (* ssr plugin *) +| "in" ssrclausehyps (* ssr plugin *) +| "in" "|-" "*" (* ssr plugin *) +| "in" "*" (* ssr plugin *) +| "in" "*" "|-" (* ssr plugin *) +| (* ssr plugin *) +] + +ssrfwd: [ +| ":=" ast_closure_lterm (* ssr plugin *) +| ":" ast_closure_lterm ":=" ast_closure_lterm (* ssr plugin *) +] + +ssrbvar: [ +| ident (* ssr plugin *) +| "_" (* ssr plugin *) +] + +ssrbinder: [ +| ssrbvar (* ssr plugin *) +| "(" ssrbvar ")" (* ssr plugin *) +| "(" ssrbvar ":" lconstr ")" (* ssr plugin *) +| "(" ssrbvar LIST1 ssrbvar ":" lconstr ")" (* ssr plugin *) +| "(" ssrbvar ":" lconstr ":=" lconstr ")" (* ssr plugin *) +| "(" ssrbvar ":=" lconstr ")" (* ssr plugin *) +| [ "of" | "&" ] operconstr99 (* ssr plugin *) +] + +ssrstruct: [ +| "{" "struct" ident "}" (* ssr plugin *) +| (* ssr plugin *) +] + +ssrposefwd: [ +| LIST0 ssrbinder ssrfwd (* ssr plugin *) +] + +ssrfixfwd: [ +| "fix" ssrbvar LIST0 ssrbinder ssrstruct ssrfwd (* ssr plugin *) +] + +ssrcofixfwd: [ +| "cofix" ssrbvar LIST0 ssrbinder ssrfwd (* ssr plugin *) +] + +ssrsetfwd: [ +| ":" ast_closure_lterm ":=" "{" ssrocc "}" cpattern (* ssr plugin *) +| ":" ast_closure_lterm ":=" lcpattern (* ssr plugin *) +| ":=" "{" ssrocc "}" cpattern (* ssr plugin *) +| ":=" lcpattern (* ssr plugin *) +] + +ssrhavefwd: [ +| ":" ast_closure_lterm ssrhint (* ssr plugin *) +| ":" ast_closure_lterm ":=" ast_closure_lterm (* ssr plugin *) +| ":" ast_closure_lterm ":=" (* ssr plugin *) +| ":=" ast_closure_lterm (* ssr plugin *) +] + +ssrhavefwdwbinders: [ +| ssrhpats_wtransp LIST0 ssrbinder ssrhavefwd (* ssr plugin *) +] + +ssrdoarg: [ +] + +ssrseqarg: [ +| ssrswap (* ssr plugin *) +| ssrseqidx ssrortacarg OPT ssrorelse (* ssr plugin *) +| ssrseqidx ssrswap (* ssr plugin *) +| tactic_expr3 (* ssr plugin *) +] + +ssrseqidx: [ +| test_ssrseqvar Prim.ident (* ssr plugin *) +| Prim.natural (* ssr plugin *) +] + +ssrswap: [ +| "first" (* ssr plugin *) +| "last" (* ssr plugin *) +] + +ssrorelse: [ +| "||" tactic_expr2 (* ssr plugin *) +] + +Prim.ident: [ +| IDENT ssr_null_entry (* ssr plugin *) +] + +ssrparentacarg: [ +| "(" tactic_expr5 ")" (* ssr plugin *) +] + +ssrdotac: [ +| tactic_expr3 (* ssr plugin *) +| ssrortacarg (* ssr plugin *) +] + +ssrseqdir: [ +] + +ssr_first: [ +| ssr_first ssrintros_ne (* ssr plugin *) +| "[" LIST0 tactic_expr5 SEP "|" "]" (* ssr plugin *) +] + +ssr_first_else: [ +| ssr_first ssrorelse (* ssr plugin *) +| ssr_first (* ssr plugin *) +] + +ssrgen: [ +| ssrdocc cpattern (* ssr plugin *) +| cpattern (* ssr plugin *) +] + +ssrdgens_tl: [ +| "{" LIST1 ssrhyp "}" cpattern ssrdgens_tl (* ssr plugin *) +| "{" LIST1 ssrhyp "}" (* ssr plugin *) +| "{" ssrocc "}" cpattern ssrdgens_tl (* ssr plugin *) +| "/" ssrdgens_tl (* ssr plugin *) +| cpattern ssrdgens_tl (* ssr plugin *) +| (* ssr plugin *) +] + +ssrdgens: [ +| ":" ssrgen ssrdgens_tl (* ssr plugin *) +] + +ssreqid: [ +| test_ssreqid ssreqpat (* ssr plugin *) +| test_ssreqid (* ssr plugin *) +] + +ssreqpat: [ +| Prim.ident (* ssr plugin *) +| "_" (* ssr plugin *) +| "?" (* ssr plugin *) +| "+" (* ssr plugin *) +| ssrdocc "->" (* ssr plugin *) +| ssrdocc "<-" (* ssr plugin *) +| "->" (* ssr plugin *) +| "<-" (* ssr plugin *) +] + +ssrarg: [ +| ssrfwdview ssreqid ssrdgens ssrintros (* ssr plugin *) +| ssrfwdview ssrclear ssrintros (* ssr plugin *) +| ssreqid ssrdgens ssrintros (* ssr plugin *) +| ssrclear_ne ssrintros (* ssr plugin *) +| ssrintros_ne (* ssr plugin *) +] + +ssrmovearg: [ +| ssrarg (* ssr plugin *) +] + +ssrcasearg: [ +| ssrarg (* ssr plugin *) +] + +ssragen: [ +| "{" LIST1 ssrhyp "}" ssrterm (* ssr plugin *) +| ssrterm (* ssr plugin *) +] + +ssragens: [ +| "{" LIST1 ssrhyp "}" ssrterm ssragens (* ssr plugin *) +| "{" LIST1 ssrhyp "}" (* ssr plugin *) +| ssrterm ssragens (* ssr plugin *) +| (* ssr plugin *) +] + +ssrapplyarg: [ +| ":" ssragen ssragens ssrintros (* ssr plugin *) +| ssrclear_ne ssrintros (* ssr plugin *) +| ssrintros_ne (* ssr plugin *) +| ssrbwdview ":" ssragen ssragens ssrintros (* ssr plugin *) +| ssrbwdview ssrclear ssrintros (* ssr plugin *) +] + +ssrexactarg: [ +| ":" ssragen ssragens (* ssr plugin *) +| ssrbwdview ssrclear (* ssr plugin *) +| ssrclear_ne (* ssr plugin *) +] + +ssrcongrarg: [ +| natural constr ssrdgens (* ssr plugin *) +| natural constr (* ssr plugin *) +| constr ssrdgens (* ssr plugin *) +| constr (* ssr plugin *) +] + +ssrrwocc: [ +| "{" LIST0 ssrhyp "}" (* ssr plugin *) +| "{" ssrocc "}" (* ssr plugin *) +| (* ssr plugin *) +] + +ssrrule_ne: [ +| test_not_ssrslashnum [ "/" ssrterm | ssrterm | ssrsimpl_ne ] (* ssr plugin *) +| ssrsimpl_ne (* ssr plugin *) +] + +ssrrule: [ +| ssrrule_ne (* ssr plugin *) +| (* ssr plugin *) +] + +ssrpattern_squarep: [ +| "[" rpattern "]" (* ssr plugin *) +| (* ssr plugin *) +] + +ssrpattern_ne_squarep: [ +| "[" rpattern "]" (* ssr plugin *) +] + +ssrrwarg: [ +| "-" ssrmult ssrrwocc ssrpattern_squarep ssrrule_ne (* ssr plugin *) +| "-/" ssrterm (* ssr plugin *) +| ssrmult_ne ssrrwocc ssrpattern_squarep ssrrule_ne (* ssr plugin *) +| "{" LIST1 ssrhyp "}" ssrpattern_ne_squarep ssrrule_ne (* ssr plugin *) +| "{" LIST1 ssrhyp "}" ssrrule (* ssr plugin *) +| "{" ssrocc "}" ssrpattern_squarep ssrrule_ne (* ssr plugin *) +| "{" "}" ssrpattern_squarep ssrrule_ne (* ssr plugin *) +| ssrpattern_ne_squarep ssrrule_ne (* ssr plugin *) +| ssrrule_ne (* ssr plugin *) +] + +ssrrwargs: [ +| test_ssr_rw_syntax LIST1 ssrrwarg (* ssr plugin *) +] + +ssrunlockarg: [ +| "{" ssrocc "}" ssrterm (* ssr plugin *) +| ssrterm (* ssr plugin *) +] + +ssrunlockargs: [ +| LIST0 ssrunlockarg (* ssr plugin *) +] + +ssrsufffwd: [ +| ssrhpats LIST0 ssrbinder ":" ast_closure_lterm ssrhint (* ssr plugin *) +] + +ssrwlogfwd: [ +| ":" LIST0 ssrwgen "/" ast_closure_lterm (* ssr plugin *) +] + +ssr_idcomma: [ +| (* ssr plugin *) +| test_idcomma [ IDENT | "_" ] "," (* ssr plugin *) +] + +ssr_rtype: [ +| "return" operconstr100 (* ssr plugin *) +] + +ssr_mpat: [ +| pattern200 (* ssr plugin *) +] + +ssr_dpat: [ +| ssr_mpat "in" pattern200 ssr_rtype (* ssr plugin *) +| ssr_mpat ssr_rtype (* ssr plugin *) +| ssr_mpat (* ssr plugin *) +] + +ssr_dthen: [ +| ssr_dpat "then" lconstr (* ssr plugin *) +] + +ssr_elsepat: [ +| "else" (* ssr plugin *) +] + +ssr_else: [ +| ssr_elsepat lconstr (* ssr plugin *) +] + +ssr_search_item: [ +| string (* ssr plugin *) +| string "%" preident (* ssr plugin *) +| constr_pattern (* ssr plugin *) +] + +ssr_search_arg: [ +| "-" ssr_search_item ssr_search_arg (* ssr plugin *) +| ssr_search_item ssr_search_arg (* ssr plugin *) +| (* ssr plugin *) +] + +ssr_modlocs: [ +| (* ssr plugin *) +| "in" LIST1 modloc (* ssr plugin *) +] + +modloc: [ +| "-" global (* ssr plugin *) +| global (* ssr plugin *) +] + +ssrhintref: [ +| constr (* ssr plugin *) +| constr "|" natural (* ssr plugin *) +] + +ssrviewpos: [ +| "for" "move" "/" (* ssr plugin *) +| "for" "apply" "/" (* ssr plugin *) +| "for" "apply" "/" "/" (* ssr plugin *) +| "for" "apply" "//" (* ssr plugin *) +| (* ssr plugin *) +] + +ssrviewposspc: [ +| ssrviewpos (* ssr plugin *) +] + +rpattern: [ +| lconstr (* ssrmatching plugin *) +| "in" lconstr (* ssrmatching plugin *) +| lconstr "in" lconstr (* ssrmatching plugin *) +| "in" lconstr "in" lconstr (* ssrmatching plugin *) +| lconstr "in" lconstr "in" lconstr (* ssrmatching plugin *) +| lconstr "as" lconstr "in" lconstr (* ssrmatching plugin *) +] + +cpattern: [ +| "Qed" constr (* ssrmatching plugin *) +| ssrtermkind constr (* ssrmatching plugin *) +] + +lcpattern: [ +| "Qed" lconstr (* ssrmatching plugin *) +| ssrtermkind lconstr (* ssrmatching plugin *) +] + +ssrpatternarg: [ +| rpattern (* ssrmatching plugin *) +] + +numnotoption: [ +| +| "(" "warning" "after" bigint ")" +| "(" "abstract" "after" bigint ")" +] + diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar new file mode 100644 index 0000000000..cd6e11505c --- /dev/null +++ b/doc/tools/docgram/orderedGrammar @@ -0,0 +1,4170 @@ +(* Defines the order to apply to editedGrammar to get productionlistGrammar. +doc_grammar will modify this file to add/remove nonterminals and productions +to match editedGrammar, which will remove comments. Not compiled into Coq *) +DOC_GRAMMAR + +global: [ +| reference +] + +constr_pattern: [ +| term +] + +sort: [ +| "Set" +| "Prop" +| "SProp" +| "Type" +| "Type" "@{" "_" "}" +| "Type" "@{" universe "}" +] + +sort_family: [ +| "Set" +| "Prop" +| "SProp" +| "Type" +] + +universe_increment: [ +| "+" natural +| empty +] + +universe_name: [ +| global +| "Set" +| "Prop" +] + +universe_expr: [ +| universe_name universe_increment +] + +universe: [ +| "max" "(" universe_expr_list_comma ")" +| universe_expr +] + +universe_expr_list_comma: [ +| universe_expr_list_comma "," universe_expr +| universe_expr +] + +lconstr: [ +| operconstr200 +| lconstr +] + +term: [ +| operconstr8 +| "@" global instance +] + +operconstr200: [ +| binder_constr +| operconstr100 +] + +operconstr100: [ +| operconstr99 "<:" binder_constr +| operconstr99 "<:" operconstr100 +| operconstr99 "<<:" binder_constr +| operconstr99 "<<:" operconstr100 +| operconstr99 ":" binder_constr +| operconstr99 ":" operconstr100 +| operconstr99 ":>" +| operconstr99 +] + +operconstr99: [ +| operconstr90 +] + +operconstr90: [ +| operconstr10 +] + +operconstr10: [ +| operconstr9 appl_arg_list +| "@" global instance operconstr9_list_opt +| "@" pattern_identref ident_list +| operconstr9 +] + +appl_arg_list: [ +| appl_arg_list appl_arg +| appl_arg +] + +operconstr9: [ +| ".." operconstr0 ".." +| operconstr8 +] + +operconstr8: [ +| operconstr1 +] + +operconstr1: [ +| operconstr0 ".(" global appl_arg_list_opt ")" +| operconstr0 ".(" "@" global operconstr9_list_opt ")" +| operconstr0 "%" IDENT +| operconstr0 +] + +appl_arg_list_opt: [ +| appl_arg_list_opt appl_arg +| empty +] + +operconstr9_list_opt: [ +| operconstr9_list_opt operconstr9 +| empty +] + +operconstr0: [ +| atomic_constr +| match_constr +| "(" operconstr200 ")" +| "{|" record_declaration bar_cbrace +| "{" binder_constr "}" +| "`{" operconstr200 "}" +| "`(" operconstr200 ")" +| "ltac" ":" "(" ltac_expr ")" +] + +record_declaration: [ +| record_fields +] + +record_fields: [ +| record_field_declaration ";" record_fields +| record_field_declaration +| empty +| record_field ";" record_fields +| record_field ";" +| record_field +] + +record_field_declaration: [ +| global binders ":=" lconstr +] + +binder_constr: [ +| "forall" open_binders "," operconstr200 +| "fun" open_binders "=>" operconstr200 +| "let" name binders type_cstr ":=" operconstr200 "in" operconstr200 +| "let" single_fix "in" operconstr200 +| "let" name_alt return_type ":=" operconstr200 "in" operconstr200 +| "let" "'" pattern200 ":=" operconstr200 "in" operconstr200 +| "let" "'" pattern200 ":=" operconstr200 case_type "in" operconstr200 +| "let" "'" pattern200 "in" pattern200 ":=" operconstr200 case_type "in" operconstr200 +| "if" operconstr200 return_type "then" operconstr200 "else" operconstr200 +| fix_constr +| "if" operconstr200 "is" ssr_dthen ssr_else (* ssr plugin *) +| "if" operconstr200 "isn't" ssr_dthen ssr_else (* ssr plugin *) +| "let" ":" ssr_mpat ":=" lconstr "in" lconstr (* ssr plugin *) +| "let" ":" ssr_mpat ":=" lconstr ssr_rtype "in" lconstr (* ssr plugin *) +| "let" ":" ssr_mpat "in" pattern200 ":=" lconstr ssr_rtype "in" lconstr (* ssr plugin *) +] + +name_alt: [ +| "(" name_list_comma_opt ")" +| "()" +] + +name_list_comma_opt: [ +| name_list_comma +| empty +] + +name_list_comma: [ +| name_list_comma "," name +| name +] + +name_list_opt: [ +| name_list_opt name +| empty +] + +name_list: [ +| name_list name +| name +] + +appl_arg: [ +| lpar_id_coloneq lconstr ")" +| operconstr9 +] + +atomic_constr: [ +| global instance +| sort +| NUMERAL +| string +| "_" +| "?" "[" ident "]" +| "?" "[" "?" ident "]" +| "?" ident evar_instance +] + +inst: [ +| ident ":=" lconstr +] + +evar_instance: [ +| "@{" inst_list_semi "}" +| empty +] + +inst_list_semi: [ +| inst_list_semi ";" inst +| inst +] + +instance: [ +| "@{" universe_level_list_opt "}" +| empty +] + +universe_level_list_opt: [ +| universe_level_list_opt universe_level +| empty +] + +universe_level: [ +| "Set" +| "Prop" +| "Type" +| "_" +| global +] + +fix_constr: [ +| single_fix +| single_fix "with" fix_decl_list "for" ident +] + +fix_decl_list: [ +| fix_decl_list "with" fix_decl +| fix_decl +] + +single_fix: [ +| fix_kw fix_decl +] + +fix_kw: [ +| "fix" +| "cofix" +] + +fix_decl: [ +| ident binders_fixannot type_cstr ":=" operconstr200 +] + +match_constr: [ +| "match" case_item_list_comma case_type_opt "with" branches "end" +] + +case_item_list_comma: [ +| case_item_list_comma "," case_item +| case_item +] + +case_type_opt: [ +| case_type +| empty +] + +case_item: [ +| operconstr100 as_opt in_opt +] + +as_opt2: [ +| as_opt case_type +| empty +] + +in_opt: [ +| "in" pattern200 +| empty +] + +case_type: [ +| "return" operconstr100 +] + +return_type: [ +| as_opt2 +] + +as_opt3: [ +| "as" dirpath +| empty +] + +branches: [ +| or_opt eqn_list_or_opt +] + +mult_pattern: [ +| pattern200_list_comma +] + +pattern200_list_comma: [ +| pattern200_list_comma "," pattern200 +| pattern200 +] + +eqn: [ +| mult_pattern_list_or "=>" lconstr +] + +mult_pattern_list_or: [ +| mult_pattern_list_or "|" mult_pattern +| mult_pattern +] + +record_pattern: [ +| global ":=" pattern200 +] + +record_patterns: [ +| record_pattern ";" record_patterns +| record_pattern ";" +| record_pattern +| empty +] + +pattern200: [ +| pattern100 +] + +pattern100: [ +| pattern99 ":" binder_constr +| pattern99 ":" operconstr100 +| pattern99 +] + +pattern99: [ +| pattern90 +] + +pattern90: [ +| pattern10 +] + +pattern10: [ +| pattern1 "as" name +| pattern1 pattern1_list +| "@" reference pattern1_list_opt +| pattern1 +] + +pattern1_list: [ +| pattern1_list pattern1 +| pattern1 +] + +pattern1_list_opt: [ +| pattern1_list_opt pattern1 +| empty +] + +pattern1: [ +| pattern0 "%" IDENT +| pattern0 +] + +pattern0: [ +| reference +| "{|" record_patterns bar_cbrace +| "_" +| "(" pattern200 ")" +| "(" pattern200 "|" pattern200_list_or ")" +| NUMERAL +| string +] + +pattern200_list_or: [ +| pattern200_list_or "|" pattern200 +| pattern200 +] + +impl_ident_tail: [ +| "}" +| name_list ":" lconstr "}" +| name_list "}" +| ":" lconstr "}" +] + +fixannot: [ +| "{" "struct" ident "}" +| "{" "wf" term ident "}" +| "{" "measure" term ident_opt term_opt "}" +| "{" "struct" name "}" +| empty +] + +term_opt: [ +| term +| empty +] + +impl_name_head: [ +| empty +] + +binders_fixannot: [ +| impl_name_head impl_ident_tail binders_fixannot +| fixannot +| binder binders_fixannot +| empty +] + +open_binders: [ +| name name_list_opt ":" lconstr +| name name_list_opt binders +| name ".." name +| closed_binder binders +] + +binders: [ +| binder_list_opt +] + +binder_list_opt: [ +| binder_list_opt binder +| empty +] + +binder: [ +| name +| closed_binder +] + +typeclass_constraint: [ +| "!" operconstr200 +| "{" name "}" ":" exclam_opt operconstr200 +| name_colon exclam_opt operconstr200 +| operconstr200 +] + +type_cstr: [ +| lconstr_opt +| ":" lconstr +| empty +] + +preident: [ +| IDENT +] + +pattern_identref: [ +| "?" ident +] + +var: [ +| ident +] + +field: [ +| FIELD +] + +fields: [ +| field fields +| field +] + +fullyqualid: [ +| ident fields +| ident +] + +basequalid: [ +| ident fields +| ident +] + +name: [ +| "_" +| ident +] + +reference: [ +| ident fields +| ident +] + +by_notation: [ +| ne_string IDENT_opt +] + +IDENT_opt: [ +| "%" IDENT +| empty +] + +smart_global: [ +| reference +| by_notation +] + +qualid: [ +| basequalid +] + +ne_string: [ +| STRING +] + +ne_lstring: [ +| ne_string +] + +dirpath: [ +| ident field_list_opt +] + +field_list_opt: [ +| field_list_opt field +| empty +] + +string: [ +| STRING +] + +lstring: [ +| string +] + +integer: [ +| NUMERAL +| "-" NUMERAL +] + +natural: [ +| NUMERAL +] + +bigint: [ +| NUMERAL +] + +bar_cbrace: [ +| "|" "}" +] + +vernac_control: [ +| "Time" vernac_control +| "Redirect" ne_string vernac_control +| "Timeout" natural vernac_control +| "Fail" vernac_control +| decorated_vernac +] + +decorated_vernac: [ +| quoted_attributes_list_opt vernac +] + +quoted_attributes_list_opt: [ +| quoted_attributes_list_opt quoted_attributes +| empty +] + +quoted_attributes: [ +| "#[" attribute_list_comma_opt "]" +] + +attribute_list_comma_opt: [ +| attribute_list_comma +| empty +] + +attribute_list_comma: [ +| attribute_list_comma "," attribute +| attribute +] + +attribute: [ +| ident attribute_value +] + +attribute_value: [ +| "=" string +| "(" attribute_list_comma_opt ")" +| empty +] + +vernac: [ +| "Local" vernac_poly +| "Global" vernac_poly +| vernac_poly +] + +vernac_poly: [ +| "Polymorphic" vernac_aux +| "Monomorphic" vernac_aux +| vernac_aux +] + +vernac_aux: [ +| "Program" gallina "." +| "Program" gallina_ext "." +| gallina "." +| gallina_ext "." +| command "." +| syntax "." +| subprf +| command_entry +] + +noedit_mode: [ +| query_command +] + +subprf: [ +| BULLET +| "{" +| "}" +] + +gallina: [ +| thm_token ident_decl binders ":" lconstr with_list_opt +| assumption_token inline assum_list +| assumptions_token inline assum_list +| def_token ident_decl def_body +| "Let" ident def_body +| cumulativity_token_opt private_token finite_token inductive_definition_list +| "Fixpoint" rec_definition_list +| "Let" "Fixpoint" rec_definition_list +| "CoFixpoint" corec_definition_list +| "Let" "CoFixpoint" corec_definition_list +| "Scheme" scheme_list +| "Combined" "Scheme" ident "from" ident_list_comma +| "Register" global "as" qualid +| "Register" "Inline" global +| "Primitive" ident lconstr_opt ":=" register_token +| "Universe" ident_list +| "Universes" ident_list +| "Constraint" univ_constraint_list_comma +] + +with_list_opt: [ +| with_list_opt "with" ident_decl binders ":" lconstr +| empty +] + +cumulativity_token_opt: [ +| cumulativity_token +| empty +] + +inductive_definition_list: [ +| inductive_definition_list "with" inductive_definition +| inductive_definition +] + +rec_definition_list: [ +| rec_definition_list "with" rec_definition +| rec_definition +] + +corec_definition_list: [ +| corec_definition_list "with" corec_definition +| corec_definition +] + +scheme_list: [ +| scheme_list "with" scheme +| scheme +] + +ident_list_comma: [ +| ident_list_comma "," ident +| ident +] + +univ_constraint_list_comma: [ +| univ_constraint_list_comma "," univ_constraint +| univ_constraint +] + +lconstr_opt2: [ +| ":=" lconstr +| empty +] + +register_token: [ +| register_prim_token +| register_type_token +] + +register_type_token: [ +| "#int63_type" +] + +register_prim_token: [ +| "#int63_head0" +| "#int63_tail0" +| "#int63_add" +| "#int63_sub" +| "#int63_mul" +| "#int63_div" +| "#int63_mod" +| "#int63_lsr" +| "#int63_lsl" +| "#int63_land" +| "#int63_lor" +| "#int63_lxor" +| "#int63_addc" +| "#int63_subc" +| "#int63_addcarryc" +| "#int63_subcarryc" +| "#int63_mulc" +| "#int63_diveucl" +| "#int63_div21" +| "#int63_addmuldiv" +| "#int63_eq" +| "#int63_lt" +| "#int63_le" +| "#int63_compare" +] + +thm_token: [ +| "Theorem" +| "Lemma" +| "Fact" +| "Remark" +| "Corollary" +| "Proposition" +| "Property" +] + +def_token: [ +| "Definition" +| "Example" +| "SubClass" +] + +assumption_token: [ +| "Hypothesis" +| "Variable" +| "Axiom" +| "Parameter" +| "Conjecture" +] + +assumptions_token: [ +| "Hypotheses" +| "Variables" +| "Axioms" +| "Parameters" +| "Conjectures" +] + +inline: [ +| "Inline" "(" natural ")" +| "Inline" +| empty +] + +univ_constraint: [ +| universe_name lt_alt universe_name +] + +lt_alt: [ +| "<" +| "=" +| "<=" +] + +univ_decl: [ +| "@{" ident_list_opt plus_opt univ_constraint_alt +] + +plus_opt: [ +| "+" +| empty +] + +univ_constraint_alt: [ +| "|" univ_constraint_list_comma_opt plus_opt "}" +| rbrace_alt +] + +univ_constraint_list_comma_opt: [ +| univ_constraint_list_comma +| empty +] + +rbrace_alt: [ +| "}" +| bar_cbrace +] + +ident_decl: [ +| ident univ_decl_opt +] + +finite_token: [ +| "Inductive" +| "CoInductive" +| "Variant" +| "Record" +| "Structure" +| "Class" +] + +cumulativity_token: [ +| "Cumulative" +| "NonCumulative" +] + +private_token: [ +| "Private" +| empty +] + +def_body: [ +| binders ":=" reduce lconstr +| binders ":" lconstr ":=" reduce lconstr +| binders ":" lconstr +] + +reduce: [ +| "Eval" red_expr "in" +| empty +] + +one_decl_notation: [ +| ne_lstring ":=" term IDENT_opt2 +] + +IDENT_opt2: [ +| ":" IDENT +| empty +] + +decl_sep: [ +| "and" +] + +decl_notation: [ +| "where" one_decl_notation_list +| empty +] + +one_decl_notation_list: [ +| one_decl_notation_list decl_sep one_decl_notation +| one_decl_notation +] + +opt_constructors_or_fields: [ +| ":=" constructor_list_or_record_decl +| empty +] + +inductive_definition: [ +| opt_coercion ident_decl binders lconstr_opt opt_constructors_or_fields decl_notation +] + +constructor_list_or_record_decl: [ +| "|" constructor_list_or +| ident constructor_type "|" constructor_list_or_opt +| ident constructor_type +| ident "{" record_fields "}" +| "{" record_fields "}" +| empty +] + +constructor_list_or: [ +| constructor_list_or "|" constructor +| constructor +] + +constructor_list_or_opt: [ +| constructor_list_or +| empty +] + +opt_coercion: [ +| ">" +| empty +] + +rec_definition: [ +| ident_decl binders_fixannot type_cstr lconstr_opt2 decl_notation +] + +corec_definition: [ +| ident_decl binders type_cstr lconstr_opt2 decl_notation +] + +lconstr_opt: [ +| ":" lconstr +| empty +] + +scheme: [ +| scheme_kind +| ident ":=" scheme_kind +] + +scheme_kind: [ +| "Induction" "for" smart_global "Sort" sort_family +| "Minimality" "for" smart_global "Sort" sort_family +| "Elimination" "for" smart_global "Sort" sort_family +| "Case" "for" smart_global "Sort" sort_family +| "Equality" "for" smart_global +] + +record_field: [ +| quoted_attributes_list_opt record_binder natural_opt2 decl_notation +] + +record_binder_body: [ +| binders of_type_with_opt_coercion lconstr +| binders of_type_with_opt_coercion lconstr ":=" lconstr +| binders ":=" lconstr +] + +record_binder: [ +| name +| name record_binder_body +] + +assum_list: [ +| assum_coe_list +| simple_assum_coe +] + +assum_coe_list: [ +| assum_coe_list assum_coe +| assum_coe +] + +assum_coe: [ +| "(" simple_assum_coe ")" +] + +simple_assum_coe: [ +| ident_decl_list of_type_with_opt_coercion lconstr +] + +ident_decl_list: [ +| ident_decl_list ident_decl +| ident_decl +] + +constructor_type: [ +| binders of_type_with_opt_coercion_opt +] + +of_type_with_opt_coercion_opt: [ +| of_type_with_opt_coercion lconstr +| empty +] + +constructor: [ +| ident constructor_type +] + +of_type_with_opt_coercion: [ +| ":>>" +| ":>" ">" +| ":>" +| ":" ">" ">" +| ":" ">" +| ":" +] + +gallina_ext: [ +| "Module" export_token ident module_binder_list_opt of_module_type is_module_expr +| "Module" "Type" ident module_binder_list_opt check_module_types is_module_type +| "Declare" "Module" export_token ident module_binder_list_opt ":" module_type_inl +| "Section" ident +| "Chapter" ident +| "End" ident +| "Collection" ident ":=" section_subset_expr +| "Require" export_token global_list +| "From" global "Require" export_token global_list +| "Import" global_list +| "Export" global_list +| "Include" module_type_inl ext_module_expr_list_opt +| "Include" "Type" module_type_inl ext_module_type_list_opt +| "Transparent" smart_global_list +| "Opaque" smart_global_list +| "Strategy" strategy_level_list +| "Canonical" Structure_opt global univ_decl_opt2 +| "Canonical" Structure_opt by_notation +| "Coercion" global univ_decl_opt def_body +| "Identity" "Coercion" ident ":" class_rawexpr ">->" class_rawexpr +| "Coercion" global ":" class_rawexpr ">->" class_rawexpr +| "Coercion" by_notation ":" class_rawexpr ">->" class_rawexpr +| "Context" binder_list +| "Instance" instance_name ":" operconstr200 hint_info record_declaration_opt +| "Existing" "Instance" global hint_info +| "Existing" "Instances" global_list natural_opt2 +| "Existing" "Class" global +| "Arguments" smart_global argument_spec_block_list_opt more_implicits_block_opt arguments_modifier_opt +| "Implicit" "Type" reserv_list +| "Implicit" "Types" reserv_list +| "Generalizable" All_alt +| "Export" "Set" option_table option_setting +| "Export" "Unset" option_table +| "Import" "Prenex" "Implicits" (* ssr plugin *) +] + +module_binder_list_opt: [ +| module_binder_list_opt module_binder +| empty +] + +ext_module_expr_list_opt: [ +| ext_module_expr_list_opt ext_module_expr +| empty +] + +ext_module_type_list_opt: [ +| ext_module_type_list_opt ext_module_type +| empty +] + +strategy_level_list: [ +| strategy_level_list strategy_level "[" smart_global_list "]" +| strategy_level "[" smart_global_list "]" +] + +Structure_opt: [ +| "Structure" +| empty +] + +univ_decl_opt: [ +| univ_decl +| empty +] + +binder_list: [ +| binder_list binder +| binder +] + +record_declaration_opt: [ +| ":=" "{" record_declaration "}" +| ":=" lconstr +| empty +] + +natural_opt: [ +| natural +| empty +] + +argument_spec_block_list_opt: [ +| argument_spec_block_list_opt argument_spec_block +| empty +] + +more_implicits_block_opt: [ +| "," more_implicits_block_list_comma +| empty +] + +more_implicits_block_list_comma: [ +| more_implicits_block_list_comma "," more_implicits_block_list_opt +| more_implicits_block_list_opt +] + +arguments_modifier_opt: [ +| ":" arguments_modifier_list_comma +| empty +] + +arguments_modifier_list_comma: [ +| arguments_modifier_list_comma "," arguments_modifier +| arguments_modifier +] + +All_alt: [ +| "All" "Variables" +| "No" "Variables" +| Variable_alt ident_list +] + +Variable_alt: [ +| "Variable" +| "Variables" +] + +more_implicits_block_list_opt: [ +| more_implicits_block_list_opt more_implicits_block +| empty +] + +univ_decl_opt2: [ +| univ_decl_opt def_body +| empty +] + +export_token: [ +| "Import" +| "Export" +| empty +] + +ext_module_type: [ +| "<+" module_type_inl +] + +ext_module_expr: [ +| "<+" module_expr_inl +] + +check_module_type: [ +| "<:" module_type_inl +] + +check_module_types: [ +| check_module_type_list_opt +] + +check_module_type_list_opt: [ +| check_module_type_list_opt check_module_type +| empty +] + +of_module_type: [ +| ":" module_type_inl +| check_module_types +] + +is_module_type: [ +| ":=" module_type_inl ext_module_type_list_opt +| empty +] + +is_module_expr: [ +| ":=" module_expr_inl ext_module_expr_list_opt +| empty +] + +functor_app_annot: [ +| "[" "inline" "at" "level" natural "]" +| "[" "no" "inline" "]" +| empty +] + +module_expr_inl: [ +| "!" module_expr +| module_expr functor_app_annot +] + +module_type_inl: [ +| "!" module_type +| module_type functor_app_annot +] + +module_binder: [ +| "(" export_token ident_list ":" module_type_inl ")" +] + +module_expr: [ +| module_expr_atom +| module_expr module_expr_atom +] + +module_expr_atom: [ +| qualid +| "(" module_expr ")" +] + +with_declaration: [ +| "Definition" fullyqualid univ_decl_opt ":=" lconstr +| "Module" fullyqualid ":=" qualid +] + +module_type: [ +| qualid +| "(" module_type ")" +| module_type module_expr_atom +| module_type "with" with_declaration +] + +section_subset_expr: [ +| starredidentref_list_opt +| ssexpr35 +] + +starredidentref_list_opt: [ +| starredidentref_list_opt starredidentref +| empty +] + +starredidentref: [ +| ident +| ident "*" +| "Type" +| "Type" "*" +] + +ssexpr35: [ +| "-" ssexpr50 +| ssexpr50 +] + +ssexpr50: [ +| ssexpr0 "-" ssexpr0 +| ssexpr0 "+" ssexpr0 +| ssexpr0 +] + +ssexpr0: [ +| starredidentref +| "(" starredidentref_list_opt ")" +| "(" starredidentref_list_opt ")" "*" +| "(" ssexpr35 ")" +| "(" ssexpr35 ")" "*" +] + +arguments_modifier: [ +| "simpl" "nomatch" +| "simpl" "never" +| "default" "implicits" +| "clear" "implicits" +| "clear" "scopes" +| "clear" "bidirectionality" "hint" +| "rename" +| "assert" +| "extra" "scopes" +| "clear" "scopes" "and" "implicits" +| "clear" "implicits" "and" "scopes" +] + +scope: [ +| "%" IDENT +] + +argument_spec: [ +| exclam_opt name scope_opt +] + +exclam_opt: [ +| "!" +| empty +] + +scope_opt: [ +| scope +| empty +] + +argument_spec_block: [ +| argument_spec +| "/" +| "&" +| "(" argument_spec_list ")" scope_opt +| "[" argument_spec_list "]" scope_opt +| "{" argument_spec_list "}" scope_opt +] + +argument_spec_list: [ +| argument_spec_list argument_spec +| argument_spec +] + +more_implicits_block: [ +| name +| "[" name_list "]" +| "{" name_list "}" +] + +strategy_level: [ +| "expand" +| "opaque" +| integer +| "transparent" +] + +instance_name: [ +| ident_decl binders +| empty +] + +hint_info: [ +| "|" natural_opt constr_pattern_opt +| empty +] + +reserv_list: [ +| reserv_tuple_list +| simple_reserv +] + +reserv_tuple_list: [ +| reserv_tuple_list reserv_tuple +| reserv_tuple +] + +reserv_tuple: [ +| "(" simple_reserv ")" +] + +simple_reserv: [ +| ident_list ":" lconstr +] + +command: [ +| "Comments" comment_list_opt +| "Declare" "Instance" ident_decl binders ":" operconstr200 hint_info +| "Declare" "Scope" IDENT +| "Pwd" +| "Cd" +| "Cd" ne_string +| "Load" Verbose_opt ne_string_alt +| "Declare" "ML" "Module" ne_string_list +| "Locate" locatable +| "Add" "LoadPath" ne_string as_dirpath +| "Add" "Rec" "LoadPath" ne_string as_dirpath +| "Remove" "LoadPath" ne_string +| "AddPath" ne_string "as" as_dirpath +| "AddRecPath" ne_string "as" as_dirpath +| "DelPath" ne_string +| "Type" lconstr +| "Print" printable +| "Print" smart_global univ_name_list_opt +| "Print" "Module" "Type" global +| "Print" "Module" global +| "Print" "Namespace" dirpath +| "Inspect" natural +| "Add" "ML" "Path" ne_string +| "Add" "Rec" "ML" "Path" ne_string +| "Set" option_table option_setting +| "Unset" option_table +| "Print" "Table" option_table +| "Add" IDENT IDENT option_ref_value_list +| "Add" IDENT option_ref_value_list +| "Test" option_table "for" option_ref_value_list +| "Test" option_table +| "Remove" IDENT IDENT option_ref_value_list +| "Remove" IDENT option_ref_value_list +| "Write" "State" IDENT +| "Write" "State" ne_string +| "Restore" "State" IDENT +| "Restore" "State" ne_string +| "Reset" "Initial" +| "Reset" ident +| "Back" +| "Back" natural +| "BackTo" natural +| "Debug" "On" +| "Debug" "Off" +| "Declare" "Reduction" IDENT; ":=" red_expr +| "Declare" "Custom" "Entry" IDENT +| "Goal" lconstr +| "Proof" +| "Proof" "Mode" string +| "Proof" lconstr +| "Abort" +| "Abort" "All" +| "Abort" ident +| "Existential" natural constr_body +| "Admitted" +| "Qed" +| "Save" ident +| "Defined" +| "Defined" ident +| "Restart" +| "Undo" +| "Undo" natural +| "Undo" "To" natural +| "Focus" +| "Focus" natural +| "Unfocus" +| "Unfocused" +| "Show" +| "Show" natural +| "Show" ident +| "Show" "Existentials" +| "Show" "Universes" +| "Show" "Conjectures" +| "Show" "Proof" +| "Show" "Intro" +| "Show" "Intros" +| "Show" "Match" reference +| "Guarded" +| "Create" "HintDb" IDENT discriminated_opt +| "Remove" "Hints" global_list opt_hintbases +| "Hint" hint opt_hintbases +| "Obligation" integer "of" ident ":" lglob withtac +| "Obligation" integer "of" ident withtac +| "Obligation" integer ":" lglob withtac +| "Obligation" integer withtac +| "Next" "Obligation" "of" ident withtac +| "Next" "Obligation" withtac +| "Solve" "Obligation" integer "of" ident "with" tactic +| "Solve" "Obligation" integer "with" tactic +| "Solve" "Obligations" "of" ident "with" tactic +| "Solve" "Obligations" "with" tactic +| "Solve" "Obligations" +| "Solve" "All" "Obligations" "with" tactic +| "Solve" "All" "Obligations" +| "Admit" "Obligations" "of" ident +| "Admit" "Obligations" +| "Obligation" "Tactic" ":=" tactic +| "Show" "Obligation" "Tactic" +| "Obligations" "of" ident +| "Obligations" +| "Preterm" "of" ident +| "Preterm" +| "Hint" "Rewrite" orient term_list ":" preident_list_opt +| "Hint" "Rewrite" orient term_list "using" tactic ":" preident_list_opt +| "Hint" "Rewrite" orient term_list +| "Hint" "Rewrite" orient term_list "using" tactic +| "Derive" "Inversion_clear" ident "with" term "Sort" sort_family +| "Derive" "Inversion_clear" ident "with" term +| "Derive" "Inversion" ident "with" term "Sort" sort_family +| "Derive" "Inversion" ident "with" term +| "Derive" "Dependent" "Inversion" ident "with" term "Sort" sort_family +| "Derive" "Dependent" "Inversion_clear" ident "with" term "Sort" sort_family +| "Declare" "Left" "Step" term +| "Declare" "Right" "Step" term +| "Grab" "Existential" "Variables" +| "Unshelve" +| "Declare" "Equivalent" "Keys" term term +| "Print" "Equivalent" "Keys" +| "Optimize" "Proof" +| "Optimize" "Heap" +| "Reset" "Ltac" "Profile" +| "Show" "Ltac" "Profile" +| "Show" "Ltac" "Profile" "CutOff" int +| "Show" "Ltac" "Profile" string +| "Hint" "Cut" "[" hints_path "]" opthints +| "Typeclasses" "Transparent" reference_list_opt +| "Typeclasses" "Opaque" reference_list_opt +| "Typeclasses" "eauto" ":=" debug eauto_search_strategy int_opt +| "Add" "Relation" term term "reflexivity" "proved" "by" term "symmetry" "proved" "by" term "as" ident +| "Add" "Relation" term term "reflexivity" "proved" "by" term "as" ident +| "Add" "Relation" term term "as" ident +| "Add" "Relation" term term "symmetry" "proved" "by" term "as" ident +| "Add" "Relation" term term "symmetry" "proved" "by" term "transitivity" "proved" "by" term "as" ident +| "Add" "Relation" term term "reflexivity" "proved" "by" term "transitivity" "proved" "by" term "as" ident +| "Add" "Relation" term term "reflexivity" "proved" "by" term "symmetry" "proved" "by" term "transitivity" "proved" "by" term "as" ident +| "Add" "Relation" term term "transitivity" "proved" "by" term "as" ident +| "Add" "Parametric" "Relation" binders ":" term term "reflexivity" "proved" "by" term "symmetry" "proved" "by" term "as" ident +| "Add" "Parametric" "Relation" binders ":" term term "reflexivity" "proved" "by" term "as" ident +| "Add" "Parametric" "Relation" binders ":" term term "as" ident +| "Add" "Parametric" "Relation" binders ":" term term "symmetry" "proved" "by" term "as" ident +| "Add" "Parametric" "Relation" binders ":" term term "symmetry" "proved" "by" term "transitivity" "proved" "by" term "as" ident +| "Add" "Parametric" "Relation" binders ":" term term "reflexivity" "proved" "by" term "transitivity" "proved" "by" term "as" ident +| "Add" "Parametric" "Relation" binders ":" term term "reflexivity" "proved" "by" term "symmetry" "proved" "by" term "transitivity" "proved" "by" term "as" ident +| "Add" "Parametric" "Relation" binders ":" term term "transitivity" "proved" "by" term "as" ident +| "Add" "Setoid" term term term "as" ident +| "Add" "Parametric" "Setoid" binders ":" term term term "as" ident +| "Add" "Morphism" term ":" ident +| "Declare" "Morphism" term ":" ident +| "Add" "Morphism" term "with" "signature" lconstr "as" ident +| "Add" "Parametric" "Morphism" binders ":" term "with" "signature" lconstr "as" ident +| "Print" "Rewrite" "HintDb" preident +| "Proof" "with" tactic using_opt +| "Proof" "using" section_subset_expr with_opt +| "Tactic" "Notation" ltac_tactic_level_opt ltac_production_item_list ":=" tactic +| "Print" "Ltac" reference +| "Locate" "Ltac" reference +| "Ltac" ltac_tacdef_body_list +| "Print" "Ltac" "Signatures" +| "String" "Notation" reference reference reference ":" ident +| "Set" "Firstorder" "Solver" tactic +| "Print" "Firstorder" "Solver" +| "Numeral" "Notation" reference reference reference ":" ident numnotoption +| "Derive" ident "SuchThat" term "As" ident (* derive plugin *) +| "Extraction" global (* extraction plugin *) +| "Recursive" "Extraction" global_list (* extraction plugin *) +| "Extraction" string global_list (* extraction plugin *) +| "Extraction" "TestCompile" global_list (* extraction plugin *) +| "Separate" "Extraction" global_list (* extraction plugin *) +| "Extraction" "Library" ident (* extraction plugin *) +| "Recursive" "Extraction" "Library" ident (* extraction plugin *) +| "Extraction" "Language" language (* extraction plugin *) +| "Extraction" "Inline" global_list (* extraction plugin *) +| "Extraction" "NoInline" global_list (* extraction plugin *) +| "Print" "Extraction" "Inline" (* extraction plugin *) +| "Reset" "Extraction" "Inline" (* extraction plugin *) +| "Extraction" "Implicit" global "[" int_or_id_list_opt "]" (* extraction plugin *) +| "Extraction" "Blacklist" ident_list (* extraction plugin *) +| "Print" "Extraction" "Blacklist" (* extraction plugin *) +| "Reset" "Extraction" "Blacklist" (* extraction plugin *) +| "Extract" "Constant" global string_list_opt "=>" mlname (* extraction plugin *) +| "Extract" "Inlined" "Constant" global "=>" mlname (* extraction plugin *) +| "Extract" "Inductive" global "=>" mlname "[" mlname_list_opt "]" string_opt (* extraction plugin *) +| "Show" "Extraction" (* extraction plugin *) +| "Function" function_rec_definition_loc_list (* funind plugin *) +| "Functional" "Scheme" fun_scheme_arg_list (* funind plugin *) +| "Functional" "Case" fun_scheme_arg (* funind plugin *) +| "Generate" "graph" "for" reference (* funind plugin *) +| "Add" "Ring" ident ":" term ring_mods_opt (* setoid_ring plugin *) +| "Print" "Rings" (* setoid_ring plugin *) +| "Add" "Field" ident ":" term field_mods_opt (* setoid_ring plugin *) +| "Print" "Fields" (* setoid_ring plugin *) +| "Prenex" "Implicits" global_list (* ssr plugin *) +| "Search" ssr_search_arg ssr_modlocs (* ssr plugin *) +| "Print" "Hint" "View" ssrviewpos (* ssr plugin *) +| "Hint" "View" ssrviewposspc ssrhintref_list (* ssr plugin *) +] + +comment_list_opt: [ +| comment_list_opt comment +| empty +] + +Verbose_opt: [ +| "Verbose" +| empty +] + +ne_string_alt: [ +| ne_string +| IDENT +] + +ne_string_list: [ +| ne_string_list ne_string +| ne_string +] + +univ_name_list_opt: [ +| univ_name_list +| empty +] + +option_ref_value_list: [ +| option_ref_value_list option_ref_value +| option_ref_value +] + +discriminated_opt: [ +| "discriminated" +| empty +] + +global_list: [ +| global_list global +| global +] + +preident_list_opt: [ +| preident_list_opt preident +| empty +] + +reference_list_opt: [ +| reference_list_opt reference +| empty +] + +int_opt: [ +| int +| empty +] + +using_opt: [ +| "using" section_subset_expr +| empty +] + +with_opt: [ +| "with" tactic +| empty +] + +ltac_tactic_level_opt: [ +| ltac_tactic_level +| empty +] + +ltac_production_item_list: [ +| ltac_production_item_list ltac_production_item +| ltac_production_item +] + +ltac_tacdef_body_list: [ +| ltac_tacdef_body_list "with" ltac_tacdef_body +| ltac_tacdef_body +] + +int_or_id_list_opt: [ +| int_or_id_list_opt int_or_id +| empty +] + +ident_list: [ +| ident_list ident +| ident +] + +string_list_opt: [ +| string_list_opt string +| empty +] + +mlname_list_opt: [ +| mlname_list_opt mlname +| empty +] + +string_opt: [ +| string +| empty +] + +function_rec_definition_loc_list: [ +| function_rec_definition_loc_list "with" function_rec_definition_loc +| function_rec_definition_loc +] + +fun_scheme_arg_list: [ +| fun_scheme_arg_list "with" fun_scheme_arg +| fun_scheme_arg +] + +ring_mods_opt: [ +| ring_mods +| empty +] + +field_mods_opt: [ +| field_mods +| empty +] + +ssrhintref_list: [ +| ssrhintref_list ssrhintref +| ssrhintref +] + +query_command: [ +| "Eval" red_expr "in" lconstr "." +| "Compute" lconstr "." +| "Check" lconstr "." +| "About" smart_global univ_name_list_opt "." +| "SearchHead" constr_pattern in_or_out_modules "." +| "SearchPattern" constr_pattern in_or_out_modules "." +| "SearchRewrite" constr_pattern in_or_out_modules "." +| "Search" searchabout_query searchabout_queries "." +| "SearchAbout" searchabout_query searchabout_queries "." +| "SearchAbout" "[" searchabout_query_list "]" in_or_out_modules "." +] + +searchabout_query_list: [ +| searchabout_query_list searchabout_query +| searchabout_query +] + +printable: [ +| "Term" smart_global univ_name_list_opt +| "All" +| "Section" global +| "Grammar" IDENT +| "Custom" "Grammar" IDENT +| "LoadPath" dirpath_opt +| "Modules" +| "Libraries" +| "ML" "Path" +| "ML" "Modules" +| "Debug" "GC" +| "Graph" +| "Classes" +| "TypeClasses" +| "Instances" smart_global +| "Coercions" +| "Coercion" "Paths" class_rawexpr class_rawexpr +| "Canonical" "Projections" +| "Tables" +| "Options" +| "Hint" +| "Hint" smart_global +| "Hint" "*" +| "HintDb" IDENT +| "Scopes" +| "Scope" IDENT +| "Visibility" IDENT_opt3 +| "Implicit" smart_global +| Sorted_opt "Universes" printunivs_subgraph_opt ne_string_opt +| "Assumptions" smart_global +| "Opaque" "Dependencies" smart_global +| "Transparent" "Dependencies" smart_global +| "All" "Dependencies" smart_global +| "Strategy" smart_global +| "Strategies" +| "Registered" +] + +dirpath_opt: [ +| dirpath +| empty +] + +IDENT_opt3: [ +| IDENT +| empty +] + +Sorted_opt: [ +| "Sorted" +| empty +] + +printunivs_subgraph_opt: [ +| printunivs_subgraph +| empty +] + +ne_string_opt: [ +| ne_string +| empty +] + +printunivs_subgraph: [ +| "Subgraph" "(" reference_list_opt ")" +] + +class_rawexpr: [ +| "Funclass" +| "Sortclass" +| smart_global +] + +locatable: [ +| smart_global +| "Term" smart_global +| "File" ne_string +| "Library" global +| "Module" global +] + +option_setting: [ +| empty +| integer +| STRING +] + +option_ref_value: [ +| global +| STRING +] + +option_table: [ +| IDENT_list +] + +as_dirpath: [ +| as_opt3 +] + +as_opt: [ +| "as" name +| empty +] + +ne_in_or_out_modules: [ +| "inside" global_list +| "outside" global_list +] + +in_or_out_modules: [ +| ne_in_or_out_modules +| empty +] + +comment: [ +| term +| STRING +| natural +] + +positive_search_mark: [ +| "-" +| empty +] + +searchabout_query: [ +| positive_search_mark ne_string scope_opt +| positive_search_mark constr_pattern +] + +searchabout_queries: [ +| ne_in_or_out_modules +| searchabout_query searchabout_queries +| empty +] + +univ_name_list: [ +| "@{" name_list_opt "}" +] + +syntax: [ +| "Open" "Scope" IDENT +| "Close" "Scope" IDENT +| "Delimit" "Scope" IDENT; "with" IDENT +| "Undelimit" "Scope" IDENT +| "Bind" "Scope" IDENT; "with" class_rawexpr_list +| "Infix" ne_lstring ":=" term syntax_modifier_opt IDENT_opt2 +| "Notation" ident ident_list_opt ":=" term only_parsing +| "Notation" lstring ":=" term syntax_modifier_opt IDENT_opt2 +| "Format" "Notation" STRING STRING STRING +| "Reserved" "Infix" ne_lstring syntax_modifier_opt +| "Reserved" "Notation" ne_lstring syntax_modifier_opt +] + +class_rawexpr_list: [ +| class_rawexpr_list class_rawexpr +| class_rawexpr +] + +syntax_modifier_opt: [ +| "(" syntax_modifier_list_comma ")" +| empty +] + +syntax_modifier_list_comma: [ +| syntax_modifier_list_comma "," syntax_modifier +| syntax_modifier +] + +only_parsing: [ +| "(" "only" "parsing" ")" +| "(" "compat" STRING ")" +| empty +] + +level: [ +| "level" natural +| "next" "level" +] + +syntax_modifier: [ +| "at" "level" natural +| "in" "custom" IDENT +| "in" "custom" IDENT; "at" "level" natural +| "left" "associativity" +| "right" "associativity" +| "no" "associativity" +| "only" "printing" +| "only" "parsing" +| "compat" STRING +| "format" STRING STRING_opt +| IDENT; "," IDENT_list_comma "at" level +| IDENT; "at" level +| IDENT; "at" level constr_as_binder_kind +| IDENT constr_as_binder_kind +| IDENT syntax_extension_type +] + +STRING_opt: [ +| STRING +| empty +] + +IDENT_list_comma: [ +| IDENT_list_comma "," IDENT +| IDENT +] + +syntax_extension_type: [ +| "ident" +| "global" +| "bigint" +| "binder" +| "constr" +| "constr" at_level_opt constr_as_binder_kind_opt +| "pattern" +| "pattern" "at" "level" natural +| "strict" "pattern" +| "strict" "pattern" "at" "level" natural +| "closed" "binder" +| "custom" IDENT at_level_opt constr_as_binder_kind_opt +] + +at_level_opt: [ +| at_level +| empty +] + +constr_as_binder_kind_opt: [ +| constr_as_binder_kind +| empty +] + +at_level: [ +| "at" level +] + +constr_as_binder_kind: [ +| "as" "ident" +| "as" "pattern" +| "as" "strict" "pattern" +] + +opt_hintbases: [ +| empty +| ":" IDENT_list +] + +IDENT_list: [ +| IDENT_list IDENT +| IDENT +] + +reference_or_constr: [ +| global +| term +] + +hint: [ +| "Resolve" reference_or_constr_list hint_info +| "Resolve" "->" global_list natural_opt +| "Resolve" "<-" global_list natural_opt +| "Immediate" reference_or_constr_list +| "Variables" "Transparent" +| "Variables" "Opaque" +| "Constants" "Transparent" +| "Constants" "Opaque" +| "Transparent" global_list +| "Opaque" global_list +| "Mode" global mode +| "Unfold" global_list +| "Constructors" global_list +| "Extern" natural constr_pattern_opt "=>" tactic +] + +reference_or_constr_list: [ +| reference_or_constr_list reference_or_constr +| reference_or_constr +] + +natural_opt2: [ +| "|" natural +| empty +] + +constr_pattern_opt: [ +| constr_pattern +| empty +] + +constr_body: [ +| ":=" lconstr +| ":" lconstr ":=" lconstr +] + +mode: [ +| plus_list +] + +plus_list: [ +| plus_list plus_alt +| plus_alt +] + +plus_alt: [ +| "+" +| "!" +| "-" +] + +vernac_toplevel: [ +| "Drop" "." +| "Quit" "." +| "Backtrack" natural natural natural "." +| "Show" "Goal" natural "at" natural "." +| vernac_control +] + +orient: [ +| "->" +| "<-" +| empty +] + +occurrences: [ +| integer_list +| var +] + +integer_list: [ +| integer_list integer +| integer +] + +glob: [ +| term +] + +lglob: [ +| lconstr +] + +casted_constr: [ +| term +] + +hloc: [ +| empty +| "in" "|-" "*" +| "in" ident +| "in" "(" "Type" "of" ident ")" +| "in" "(" "Value" "of" ident ")" +| "in" "(" "type" "of" ident ")" +| "in" "(" "value" "of" ident ")" +] + +rename: [ +| ident "into" ident +] + +by_arg_tac: [ +| "by" ltac_expr3 +| empty +] + +in_clause: [ +| in_clause +| "*" occs +| "*" "|-" concl_occ +| hypident_occ_list_comma_opt "|-" concl_occ +| hypident_occ_list_comma_opt +] + +hypident_occ_list_comma_opt: [ +| hypident_occ_list_comma +| empty +] + +hypident_occ_list_comma: [ +| hypident_occ_list_comma "," hypident_occ +| hypident_occ +] + +test_lpar_id_colon: [ +| empty +] + +withtac: [ +| "with" tactic +| empty +] + +closed_binder: [ +| "(" name name_list ":" lconstr ")" +| "(" name ":" lconstr ")" +| "(" name ":=" lconstr ")" +| "(" name ":" lconstr ":=" lconstr ")" +| "{" name "}" +| "{" name name_list ":" lconstr "}" +| "{" name ":" lconstr "}" +| "{" name name_list "}" +| "`(" typeclass_constraint_list_comma ")" +| "`{" typeclass_constraint_list_comma "}" +| "'" pattern0 +| of_alt operconstr99 (* ssr plugin *) +| "(" "_" ":" lconstr "|" lconstr ")" +] + +typeclass_constraint_list_comma: [ +| typeclass_constraint_list_comma "," typeclass_constraint +| typeclass_constraint +] + +of_alt: [ +| "of" +| "&" +] + +simple_tactic: [ +| "reflexivity" +| "exact" casted_constr +| "assumption" +| "etransitivity" +| "cut" term +| "exact_no_check" term +| "vm_cast_no_check" term +| "native_cast_no_check" term +| "casetype" term +| "elimtype" term +| "lapply" term +| "transitivity" term +| "left" +| "eleft" +| "left" "with" bindings +| "eleft" "with" bindings +| "right" +| "eright" +| "right" "with" bindings +| "eright" "with" bindings +| "constructor" +| "constructor" int_or_var +| "constructor" int_or_var "with" bindings +| "econstructor" +| "econstructor" int_or_var +| "econstructor" int_or_var "with" bindings +| "specialize" constr_with_bindings +| "specialize" constr_with_bindings "as" simple_intropattern +| "symmetry" +| "symmetry" "in" in_clause +| "split" +| "esplit" +| "split" "with" bindings +| "esplit" "with" bindings +| "exists" +| "exists" bindings_list_comma +| "eexists" +| "eexists" bindings_list_comma +| "intros" "until" quantified_hypothesis +| "intro" +| "intro" ident +| "intro" ident "at" "top" +| "intro" ident "at" "bottom" +| "intro" ident "after" var +| "intro" ident "before" var +| "intro" "at" "top" +| "intro" "at" "bottom" +| "intro" "after" var +| "intro" "before" var +| "move" var "at" "top" +| "move" var "at" "bottom" +| "move" var "after" var +| "move" var "before" var +| "rename" rename_list_comma +| "revert" var_list +| "simple" "induction" quantified_hypothesis +| "simple" "destruct" quantified_hypothesis +| "double" "induction" quantified_hypothesis quantified_hypothesis +| "admit" +| "fix" ident natural +| "cofix" ident +| "clear" var_list_opt +| "clear" "-" var_list +| "clearbody" var_list +| "generalize" "dependent" term +| "replace" uconstr "with" term clause_dft_concl by_arg_tac +| "replace" "->" uconstr clause_dft_concl +| "replace" "<-" uconstr clause_dft_concl +| "replace" uconstr clause_dft_concl +| "simplify_eq" +| "simplify_eq" destruction_arg +| "esimplify_eq" +| "esimplify_eq" destruction_arg +| "discriminate" +| "discriminate" destruction_arg +| "ediscriminate" +| "ediscriminate" destruction_arg +| "injection" +| "injection" destruction_arg +| "einjection" +| "einjection" destruction_arg +| "injection" "as" simple_intropattern_list_opt +| "injection" destruction_arg "as" simple_intropattern_list_opt +| "einjection" "as" simple_intropattern_list_opt +| "einjection" destruction_arg "as" simple_intropattern_list_opt +| "simple" "injection" +| "simple" "injection" destruction_arg +| "dependent" "rewrite" orient term +| "dependent" "rewrite" orient term "in" var +| "cutrewrite" orient term +| "cutrewrite" orient term "in" var +| "decompose" "sum" term +| "decompose" "record" term +| "absurd" term +| "contradiction" constr_with_bindings_opt +| "autorewrite" "with" preident_list clause_dft_concl +| "autorewrite" "with" preident_list clause_dft_concl "using" tactic +| "autorewrite" "*" "with" preident_list clause_dft_concl +| "autorewrite" "*" "with" preident_list clause_dft_concl "using" tactic +| "rewrite" "*" orient uconstr "in" var "at" occurrences by_arg_tac +| "rewrite" "*" orient uconstr "at" occurrences "in" var by_arg_tac +| "rewrite" "*" orient uconstr "in" var by_arg_tac +| "rewrite" "*" orient uconstr "at" occurrences by_arg_tac +| "rewrite" "*" orient uconstr by_arg_tac +| "refine" uconstr +| "simple" "refine" uconstr +| "notypeclasses" "refine" uconstr +| "simple" "notypeclasses" "refine" uconstr +| "solve_constraints" +| "subst" var_list +| "subst" +| "simple" "subst" +| "evar" test_lpar_id_colon "(" ident ":" lconstr ")" +| "evar" term +| "instantiate" "(" ident ":=" lglob ")" +| "instantiate" "(" integer ":=" lglob ")" hloc +| "instantiate" +| "stepl" term "by" tactic +| "stepl" term +| "stepr" term "by" tactic +| "stepr" term +| "generalize_eqs" var +| "dependent" "generalize_eqs" var +| "generalize_eqs_vars" var +| "dependent" "generalize_eqs_vars" var +| "specialize_eqs" var +| "hresolve_core" "(" ident ":=" term ")" "at" int_or_var "in" term +| "hresolve_core" "(" ident ":=" term ")" "in" term +| "hget_evar" int_or_var +| "destauto" +| "destauto" "in" var +| "transparent_abstract" ltac_expr3 +| "transparent_abstract" ltac_expr3 "using" ident +| "constr_eq" term term +| "constr_eq_strict" term term +| "constr_eq_nounivs" term term +| "is_evar" term +| "has_evar" term +| "is_var" term +| "is_fix" term +| "is_cofix" term +| "is_ind" term +| "is_constructor" term +| "is_proj" term +| "is_const" term +| "shelve" +| "shelve_unifiable" +| "unshelve" ltac_expr1 +| "give_up" +| "cycle" int_or_var +| "swap" int_or_var int_or_var +| "revgoals" +| "guard" test +| "decompose" "[" term_list "]" term +| "optimize_heap" +| "start" "ltac" "profiling" +| "stop" "ltac" "profiling" +| "reset" "ltac" "profile" +| "show" "ltac" "profile" +| "show" "ltac" "profile" "cutoff" int +| "show" "ltac" "profile" string +| "restart_timer" string_opt +| "finish_timing" string_opt +| "finish_timing" "(" string ")" string_opt +| "eassumption" +| "eexact" term +| "trivial" auto_using hintbases +| "info_trivial" auto_using hintbases +| "debug" "trivial" auto_using hintbases +| "auto" int_or_var_opt auto_using hintbases +| "info_auto" int_or_var_opt auto_using hintbases +| "debug" "auto" int_or_var_opt auto_using hintbases +| "prolog" "[" uconstr_list_opt "]" int_or_var +| "eauto" int_or_var_opt int_or_var_opt auto_using hintbases +| "new" "auto" int_or_var_opt auto_using hintbases +| "debug" "eauto" int_or_var_opt int_or_var_opt auto_using hintbases +| "info_eauto" int_or_var_opt int_or_var_opt auto_using hintbases +| "dfs" "eauto" int_or_var_opt auto_using hintbases +| "autounfold" hintbases clause_dft_concl +| "autounfold_one" hintbases "in" var +| "autounfold_one" hintbases +| "unify" term term +| "unify" term term "with" preident +| "convert_concl_no_check" term +| "typeclasses" "eauto" "bfs" int_or_var_opt "with" preident_list +| "typeclasses" "eauto" int_or_var_opt "with" preident_list +| "typeclasses" "eauto" int_or_var_opt +| "head_of_constr" ident term +| "not_evar" term +| "is_ground" term +| "autoapply" term "using" preident +| "autoapply" term "with" preident +| "progress_evars" tactic +| "rewrite_strat" rewstrategy "in" var +| "rewrite_strat" rewstrategy +| "rewrite_db" preident "in" var +| "rewrite_db" preident +| "substitute" orient glob_constr_with_bindings +| "setoid_rewrite" orient glob_constr_with_bindings +| "setoid_rewrite" orient glob_constr_with_bindings "in" var +| "setoid_rewrite" orient glob_constr_with_bindings "at" occurrences +| "setoid_rewrite" orient glob_constr_with_bindings "at" occurrences "in" var +| "setoid_rewrite" orient glob_constr_with_bindings "in" var "at" occurrences +| "setoid_symmetry" +| "setoid_symmetry" "in" var +| "setoid_reflexivity" +| "setoid_transitivity" term +| "setoid_etransitivity" +| "decide" "equality" +| "compare" term term +| "intros" intropattern_list_opt +| "eintros" intropattern_list_opt +| "apply" constr_with_bindings_arg_list_comma in_hyp_as +| "eapply" constr_with_bindings_arg_list_comma in_hyp_as +| "simple" "apply" constr_with_bindings_arg_list_comma in_hyp_as +| "simple" "eapply" constr_with_bindings_arg_list_comma in_hyp_as +| "elim" constr_with_bindings_arg eliminator_opt +| "eelim" constr_with_bindings_arg eliminator_opt +| "case" induction_clause_list +| "ecase" induction_clause_list +| "fix" ident natural "with" fixdecl_list +| "cofix" ident "with" cofixdecl_list +| "pose" bindings_with_parameters +| "pose" term as_name +| "epose" bindings_with_parameters +| "epose" term as_name +| "set" bindings_with_parameters clause_dft_concl +| "set" term as_name clause_dft_concl +| "eset" bindings_with_parameters clause_dft_concl +| "eset" term as_name clause_dft_concl +| "remember" term as_name eqn_ipat clause_dft_all +| "eremember" term as_name eqn_ipat clause_dft_all +| "assert" "(" ident ":=" lconstr ")" +| "eassert" "(" ident ":=" lconstr ")" +| "assert" test_lpar_id_colon "(" ident ":" lconstr ")" by_tactic +| "eassert" test_lpar_id_colon "(" ident ":" lconstr ")" by_tactic +| "enough" test_lpar_id_colon "(" ident ":" lconstr ")" by_tactic +| "eenough" test_lpar_id_colon "(" ident ":" lconstr ")" by_tactic +| "assert" term as_ipat by_tactic +| "eassert" term as_ipat by_tactic +| "pose" "proof" lconstr as_ipat +| "epose" "proof" lconstr as_ipat +| "enough" term as_ipat by_tactic +| "eenough" term as_ipat by_tactic +| "generalize" term +| "generalize" term term_list +| "generalize" term occs as_name pattern_occ_list_opt +| "induction" induction_clause_list +| "einduction" induction_clause_list +| "destruct" induction_clause_list +| "edestruct" induction_clause_list +| "rewrite" oriented_rewriter_list_comma clause_dft_concl by_tactic +| "erewrite" oriented_rewriter_list_comma clause_dft_concl by_tactic +| "dependent" simple_alt quantified_hypothesis as_or_and_ipat with_opt2 +| "simple" "inversion" quantified_hypothesis as_or_and_ipat in_hyp_list +| "inversion" quantified_hypothesis as_or_and_ipat in_hyp_list +| "inversion_clear" quantified_hypothesis as_or_and_ipat in_hyp_list +| "inversion" quantified_hypothesis "using" term in_hyp_list +| "red" clause_dft_concl +| "hnf" clause_dft_concl +| "simpl" delta_flag ref_or_pattern_occ_opt clause_dft_concl +| "cbv" strategy_flag clause_dft_concl +| "cbn" strategy_flag clause_dft_concl +| "lazy" strategy_flag clause_dft_concl +| "compute" delta_flag clause_dft_concl +| "vm_compute" ref_or_pattern_occ_opt clause_dft_concl +| "native_compute" ref_or_pattern_occ_opt clause_dft_concl +| "unfold" unfold_occ_list_comma clause_dft_concl +| "fold" term_list clause_dft_concl +| "pattern" pattern_occ_list_comma clause_dft_concl +| "change" conversion clause_dft_concl +| "change_no_check" conversion clause_dft_concl +| "btauto" +| "rtauto" +| "congruence" +| "congruence" integer +| "congruence" "with" term_list +| "congruence" integer "with" term_list +| "f_equal" +| "firstorder" tactic_opt firstorder_using +| "firstorder" tactic_opt "with" preident_list +| "firstorder" tactic_opt firstorder_using "with" preident_list +| "gintuition" tactic_opt +| "functional" "inversion" quantified_hypothesis reference_opt (* funind plugin *) +| "functional" "induction" term_list fun_ind_using with_names (* funind plugin *) +| "soft" "functional" "induction" term_list fun_ind_using with_names (* funind plugin *) +| "myred" (* micromega plugin *) +| "psatz_Z" int_or_var tactic (* micromega plugin *) +| "psatz_Z" tactic (* micromega plugin *) +| "xlia" tactic (* micromega plugin *) +| "xnlia" tactic (* micromega plugin *) +| "xnra" tactic (* micromega plugin *) +| "xnqa" tactic (* micromega plugin *) +| "sos_Z" tactic (* micromega plugin *) +| "sos_Q" tactic (* micromega plugin *) +| "sos_R" tactic (* micromega plugin *) +| "lra_Q" tactic (* micromega plugin *) +| "lra_R" tactic (* micromega plugin *) +| "psatz_R" int_or_var tactic (* micromega plugin *) +| "psatz_R" tactic (* micromega plugin *) +| "psatz_Q" int_or_var tactic (* micromega plugin *) +| "psatz_Q" tactic (* micromega plugin *) +| "nsatz_compute" term (* nsatz plugin *) +| "omega" (* omega plugin *) +| "omega" "with" ident_list (* omega plugin *) +| "omega" "with" "*" (* omega plugin *) +| "protect_fv" string "in" ident (* setoid_ring plugin *) +| "protect_fv" string (* setoid_ring plugin *) +| "ring_lookup" ltac_expr0 "[" term_list_opt "]" term_list (* setoid_ring plugin *) +| "field_lookup" tactic "[" term_list_opt "]" term_list (* setoid_ring plugin *) +| "YouShouldNotTypeThis" ssrintrosarg (* ssr plugin *) +| "by" ssrhintarg (* ssr plugin *) +| "YouShouldNotTypeThis" "do" (* ssr plugin *) +| "YouShouldNotTypeThis" ssrtclarg ssrseqarg (* ssr plugin *) +| "clear" natural (* ssr plugin *) +| "move" ssrmovearg ssrrpat (* ssr plugin *) +| "move" ssrmovearg ssrclauses (* ssr plugin *) +| "move" ssrrpat (* ssr plugin *) +| "move" (* ssr plugin *) +| "case" ssrcasearg ssrclauses (* ssr plugin *) +| "case" (* ssr plugin *) +| "elim" ssrarg ssrclauses (* ssr plugin *) +| "elim" (* ssr plugin *) +| "apply" ssrapplyarg (* ssr plugin *) +| "apply" (* ssr plugin *) +| "exact" ssrexactarg (* ssr plugin *) +| "exact" (* ssr plugin *) +| "exact" "<:" lconstr (* ssr plugin *) +| "congr" ssrcongrarg (* ssr plugin *) +| "ssrinstancesofruleL2R" ssrterm (* ssr plugin *) +| "ssrinstancesofruleR2L" ssrterm (* ssr plugin *) +| "rewrite" ssrrwargs ssrclauses (* ssr plugin *) +| "unlock" ssrunlockargs ssrclauses (* ssr plugin *) +| "pose" ssrfixfwd (* ssr plugin *) +| "pose" ssrcofixfwd (* ssr plugin *) +| "pose" ssrfwdid ssrposefwd (* ssr plugin *) +| "set" ssrfwdid ssrsetfwd ssrclauses (* ssr plugin *) +| "abstract" ssrdgens (* ssr plugin *) +| "have" ssrhavefwdwbinders (* ssr plugin *) +| "have" "suff" ssrhpats_nobs ssrhavefwd (* ssr plugin *) +| "have" "suffices" ssrhpats_nobs ssrhavefwd (* ssr plugin *) +| "suff" "have" ssrhpats_nobs ssrhavefwd (* ssr plugin *) +| "suffices" "have" ssrhpats_nobs ssrhavefwd (* ssr plugin *) +| "suff" ssrsufffwd (* ssr plugin *) +| "suffices" ssrsufffwd (* ssr plugin *) +| "wlog" ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "wlog" "suff" ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "wlog" "suffices" ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "without" "loss" ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "without" "loss" "suff" ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "without" "loss" "suffices" ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "gen" "have" ssrclear ssr_idcomma ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "generally" "have" ssrclear ssr_idcomma ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "under" ssrrwarg (* ssr plugin *) +| "under" ssrrwarg ssrintros_ne (* ssr plugin *) +| "under" ssrrwarg ssrintros_ne "do" ssrhint3arg (* ssr plugin *) +| "under" ssrrwarg "do" ssrhint3arg (* ssr plugin *) +| "ssrinstancesoftpat" cpattern (* ssrmatching plugin *) +] + +var_list: [ +| var_list var +| var +] + +var_list_opt: [ +| var_list_opt var +| empty +] + +constr_with_bindings_opt: [ +| constr_with_bindings +| empty +] + +int_or_var_opt: [ +| int_or_var +| empty +] + +uconstr_list_opt: [ +| uconstr_list_opt uconstr +| empty +] + +constr_with_bindings_arg_list_comma: [ +| constr_with_bindings_arg_list_comma "," constr_with_bindings_arg +| constr_with_bindings_arg +] + +fixdecl_list: [ +| fixdecl_list fixdecl +| fixdecl +] + +cofixdecl_list: [ +| cofixdecl_list cofixdecl +| cofixdecl +] + +pattern_occ_list_opt: [ +| pattern_occ_list_opt "," pattern_occ as_name +| empty +] + +oriented_rewriter_list_comma: [ +| oriented_rewriter_list_comma "," oriented_rewriter +| oriented_rewriter +] + +simple_alt: [ +| "simple" "inversion" +| "inversion" +| "inversion_clear" +] + +with_opt2: [ +| "with" term +| empty +] + +tactic_opt: [ +| tactic +| empty +] + +reference_opt: [ +| reference +| empty +] + +bindings_list_comma: [ +| bindings_list_comma "," bindings +| bindings +] + +rename_list_comma: [ +| rename_list_comma "," rename +| rename +] + +orient_string: [ +| orient preident +] + +comparison: [ +| "=" +| "<" +| "<=" +| ">" +| ">=" +] + +test: [ +| int_or_var comparison int_or_var +] + +hintbases: [ +| "with" "*" +| "with" preident_list +| empty +] + +preident_list: [ +| preident_list preident +| preident +] + +auto_using: [ +| "using" uconstr_list_comma +| empty +] + +uconstr_list_comma: [ +| uconstr_list_comma "," uconstr +| uconstr +] + +hints_path_atom: [ +| global_list +| "_" +] + +hints_path: [ +| "(" hints_path ")" +| hints_path "*" +| "emp" +| "eps" +| hints_path "|" hints_path +| hints_path_atom +| hints_path hints_path +] + +opthints: [ +| ":" preident_list +| empty +] + +debug: [ +| "debug" +| empty +] + +eauto_search_strategy: [ +| "(bfs)" +| "(dfs)" +| empty +] + +glob_constr_with_bindings: [ +| constr_with_bindings +] + +rewstrategy: [ +| glob +| "<-" term +| "subterms" rewstrategy +| "subterm" rewstrategy +| "innermost" rewstrategy +| "outermost" rewstrategy +| "bottomup" rewstrategy +| "topdown" rewstrategy +| "id" +| "fail" +| "refl" +| "progress" rewstrategy +| "try" rewstrategy +| "any" rewstrategy +| "repeat" rewstrategy +| rewstrategy ";" rewstrategy +| "(" rewstrategy ")" +| "choice" rewstrategy rewstrategy +| "old_hints" preident +| "hints" preident +| "terms" term_list_opt +| "eval" red_expr +| "fold" term +] + +term_list_opt: [ +| term_list_opt term +| empty +] + +int_or_var: [ +| integer +| ident +] + +nat_or_var: [ +| natural +| ident +] + +id_or_meta: [ +| ident +] + +open_constr: [ +| term +] + +uconstr: [ +| term +] + +destruction_arg: [ +| natural +| constr_with_bindings +| constr_with_bindings_arg +] + +constr_with_bindings_arg: [ +| ">" constr_with_bindings +| constr_with_bindings +] + +quantified_hypothesis: [ +| ident +| natural +] + +conversion: [ +| term +| term "with" term +| term "at" occs_nums "with" term +] + +occs_nums: [ +| nat_or_var_list +| "-" nat_or_var int_or_var_list_opt +] + +nat_or_var_list: [ +| nat_or_var_list nat_or_var +| nat_or_var +] + +int_or_var_list_opt: [ +| int_or_var_list_opt int_or_var +| empty +] + +occs: [ +| "at" occs_nums +| empty +] + +pattern_occ: [ +| term occs +] + +ref_or_pattern_occ: [ +| smart_global occs +| term occs +] + +unfold_occ: [ +| smart_global occs +] + +intropattern_list_opt: [ +| intropattern_list_opt intropattern +| empty +] + +or_and_intropattern: [ +| "[" intropattern_or_list_or "]" +| "(" simple_intropattern_list_comma_opt ")" +| "(" simple_intropattern "&" simple_intropattern_list_ ")" +] + +simple_intropattern_list_comma_opt: [ +| simple_intropattern_list_comma +| empty +] + +simple_intropattern_list_comma: [ +| simple_intropattern_list_comma "," simple_intropattern +| simple_intropattern +] + +simple_intropattern_list_: [ +| simple_intropattern_list_ "&" simple_intropattern +| simple_intropattern +] + +intropattern_or_list_or: [ +| intropattern_or_list_or "|" intropattern_list_opt +| intropattern_list_opt +] + +simple_intropattern_list_opt: [ +| simple_intropattern_list_opt simple_intropattern +| empty +] + +equality_intropattern: [ +| "->" +| "<-" +| "[=" intropattern_list_opt "]" +] + +naming_intropattern: [ +| "?" ident +| "?" +| ident +] + +intropattern: [ +| simple_intropattern +| "*" +| "**" +] + +simple_intropattern: [ +| simple_intropattern_closed operconstr0_list_opt +] + +operconstr0_list_opt: [ +| operconstr0_list_opt "%" operconstr0 +| empty +] + +simple_intropattern_closed: [ +| or_and_intropattern +| equality_intropattern +| "_" +| naming_intropattern +] + +simple_binding: [ +| "(" ident ":=" lconstr ")" +| "(" natural ":=" lconstr ")" +] + +bindings: [ +| simple_binding_list +| term_list +] + +simple_binding_list: [ +| simple_binding_list simple_binding +| simple_binding +] + +term_list: [ +| term_list term +| term +] + +constr_with_bindings: [ +| term with_bindings +] + +with_bindings: [ +| "with" bindings +| empty +] + +red_flags: [ +| "beta" +| "iota" +| "match" +| "fix" +| "cofix" +| "zeta" +| "delta" delta_flag +] + +delta_flag: [ +| "-" "[" smart_global_list "]" +| "[" smart_global_list "]" +| empty +] + +smart_global_list: [ +| smart_global_list smart_global +| smart_global +] + +strategy_flag: [ +| red_flags_list +| delta_flag +] + +red_flags_list: [ +| red_flags_list red_flags +| red_flags +] + +red_expr: [ +| "red" +| "hnf" +| "simpl" delta_flag ref_or_pattern_occ_opt +| "cbv" strategy_flag +| "cbn" strategy_flag +| "lazy" strategy_flag +| "compute" delta_flag +| "vm_compute" ref_or_pattern_occ_opt +| "native_compute" ref_or_pattern_occ_opt +| "unfold" unfold_occ_list_comma +| "fold" term_list +| "pattern" pattern_occ_list_comma +| IDENT +] + +ref_or_pattern_occ_opt: [ +| ref_or_pattern_occ +| empty +] + +unfold_occ_list_comma: [ +| unfold_occ_list_comma "," unfold_occ +| unfold_occ +] + +pattern_occ_list_comma: [ +| pattern_occ_list_comma "," pattern_occ +| pattern_occ +] + +hypident: [ +| id_or_meta +| "(" "type" "of" id_or_meta ")" +| "(" "value" "of" id_or_meta ")" +| "(" "type" "of" ident ")" (* ssr plugin *) +| "(" "value" "of" ident ")" (* ssr plugin *) +] + +hypident_occ: [ +| hypident occs +] + +clause_dft_concl: [ +| "in" in_clause +| occs +| empty +] + +clause_dft_all: [ +| "in" in_clause +| empty +] + +opt_clause: [ +| "in" in_clause +| "at" occs_nums +| empty +] + +concl_occ: [ +| "*" occs +| empty +] + +in_hyp_list: [ +| "in" id_or_meta_list +| empty +] + +id_or_meta_list: [ +| id_or_meta_list id_or_meta +| id_or_meta +] + +in_hyp_as: [ +| "in" id_or_meta as_ipat +| empty +] + +simple_binder: [ +| name +| "(" name_list ":" lconstr ")" +] + +fixdecl: [ +| "(" ident simple_binder_list_opt fixannot ":" lconstr ")" +] + +cofixdecl: [ +| "(" ident simple_binder_list_opt ":" lconstr ")" +] + +bindings_with_parameters: [ +| "(" ident simple_binder_list_opt ":=" lconstr ")" +] + +simple_binder_list_opt: [ +| simple_binder_list_opt simple_binder +| empty +] + +eliminator: [ +| "using" constr_with_bindings +] + +as_ipat: [ +| "as" simple_intropattern +| empty +] + +or_and_intropattern_loc: [ +| or_and_intropattern +| ident +] + +as_or_and_ipat: [ +| "as" or_and_intropattern_loc +| empty +] + +eqn_ipat: [ +| "eqn" ":" naming_intropattern +| "_eqn" ":" naming_intropattern +| "_eqn" +| empty +] + +as_name: [ +| "as" ident +| empty +] + +by_tactic: [ +| "by" ltac_expr3 +| empty +] + +rewriter: [ +| "!" constr_with_bindings_arg +| qmark_alt constr_with_bindings_arg +| natural "!" constr_with_bindings_arg +| natural qmark_alt constr_with_bindings_arg +| natural constr_with_bindings_arg +| constr_with_bindings_arg +] + +qmark_alt: [ +| "?" +| "?" +] + +oriented_rewriter: [ +| orient rewriter +] + +induction_clause: [ +| destruction_arg as_or_and_ipat eqn_ipat opt_clause +] + +induction_clause_list: [ +| induction_clause_list_comma eliminator_opt opt_clause +] + +induction_clause_list_comma: [ +| induction_clause_list_comma "," induction_clause +| induction_clause +] + +eliminator_opt: [ +| eliminator +| empty +] + +ltac_expr: [ +| binder_tactic +| ltac_expr4 +] + +binder_tactic: [ +| "fun" input_fun_list "=>" ltac_expr +| "let" rec_opt let_clause_list "in" ltac_expr +| "info" ltac_expr +] + +input_fun_list: [ +| input_fun_list input_fun +| input_fun +] + +input_fun: [ +| "_" +| ident +] + +rec_opt: [ +| "rec" +| empty +] + +let_clause_list: [ +| let_clause_list "with" let_clause +| let_clause +] + +let_clause: [ +| ident ":=" ltac_expr +| "_" ":=" ltac_expr +| ident input_fun_list ":=" ltac_expr +] + +ltac_expr4: [ +| ltac_expr3 ";" binder_tactic +| ltac_expr3 ";" ltac_expr3 +| ltac_expr3 ";" "[" gt_opt tactic_then_gen "]" +| ltac_expr3 +| ltac_expr ";" "first" ssr_first_else (* ssr plugin *) +| ltac_expr ";" "first" ssrseqarg (* ssr plugin *) +| ltac_expr ";" "last" ssrseqarg (* ssr plugin *) +] + +gt_opt: [ +| ">" +| empty +] + +tactic_then_gen: [ +| ltac_expr_opt "|" tactic_then_gen +| ltac_expr_opt ".." or_opt ltac_expr_list2 +| ltac_expr +| empty +] + +ltac_expr_opt: [ +| ltac_expr +| empty +] + +ltac_expr_list_or2_opt: [ +| ltac_expr_list_or2 +| empty +] + +ltac_expr_list_or2: [ +| ltac_expr_list_or2 "|" ltac_expr_opt +| ltac_expr_opt +] + +ltac_expr3: [ +| "try" ltac_expr3 +| "do" int_or_var ltac_expr3 +| "timeout" int_or_var ltac_expr3 +| "time" string_opt ltac_expr3 +| "repeat" ltac_expr3 +| "progress" ltac_expr3 +| "once" ltac_expr3 +| "exactly_once" ltac_expr3 +| "infoH" ltac_expr3 +| "abstract" ltac_expr2 +| "abstract" ltac_expr2 "using" ident +| selector ltac_expr3 +| "do" ssrmmod ssrdotac ssrclauses (* ssr plugin *) +| "do" ssrortacarg ssrclauses (* ssr plugin *) +| "do" int_or_var ssrmmod ssrdotac ssrclauses (* ssr plugin *) +| "abstract" ssrdgens (* ssr plugin *) +| ltac_expr2 +] + +tactic_mode: [ +| toplevel_selector_opt query_command +| toplevel_selector_opt "{" +| toplevel_selector_opt ltac_info_opt tactic ltac_use_default +| "par" ":" ltac_info_opt tactic ltac_use_default +] + +toplevel_selector_opt: [ +| toplevel_selector +| empty +] + +toplevel_selector: [ +| selector_body ":" +| "!" ":" +| "all" ":" +] + +selector: [ +| "only" selector_body ":" +] + +selector_body: [ +| range_selector_list_comma +| "[" ident "]" +] + +range_selector_list_comma: [ +| range_selector_list_comma "," range_selector +| range_selector +] + +range_selector: [ +| natural "-" natural +| natural +] + +ltac_expr2: [ +| ltac_expr1 "+" binder_tactic +| ltac_expr1 "+" ltac_expr2 +| "tryif" ltac_expr "then" ltac_expr "else" ltac_expr2 +| ltac_expr1 "||" binder_tactic +| ltac_expr1 "||" ltac_expr2 +| ltac_expr1 +] + +ltac_expr1: [ +| match_key reverse_opt "goal" "with" match_context_list "end" +| match_key ltac_expr "with" match_list "end" +| "first" "[" ltac_expr_list_or_opt "]" +| "solve" "[" ltac_expr_list_or_opt "]" +| "idtac" message_token_list_opt +| failkw int_or_var_opt message_token_list_opt +| simple_tactic +| tactic_arg +| reference tactic_arg_compat_list_opt +| ltac_expr ssrintros_ne (* ssr plugin *) +| ltac_expr0 +] + +match_key: [ +| "match" +| "lazymatch" +| "multimatch" +] + +reverse_opt: [ +| "reverse" +| empty +] + +ltac_expr_list_or_opt: [ +| ltac_expr_list_or +| empty +] + +ltac_expr_list_or: [ +| ltac_expr_list_or "|" ltac_expr +| ltac_expr +] + +match_context_list: [ +| or_opt match_context_rule_list_or +] + +match_context_rule_list_or: [ +| match_context_rule_list_or "|" match_context_rule +| match_context_rule +] + +or_opt: [ +| "|" +| empty +] + +eqn_list_or_opt: [ +| eqn_list_or +| empty +] + +eqn_list_or: [ +| eqn_list_or "|" eqn +| eqn +] + +match_context_rule: [ +| match_hyps_list_comma_opt "|-" match_pattern "=>" ltac_expr +| "[" match_hyps_list_comma_opt "|-" match_pattern "]" "=>" ltac_expr +| "_" "=>" ltac_expr +] + +match_hyps_list_comma_opt: [ +| match_hyps_list_comma +| empty +] + +match_hyps_list_comma: [ +| match_hyps_list_comma "," match_hyps +| match_hyps +] + +match_hyps: [ +| name ":" match_pattern +| name ":=" match_pattern_opt match_pattern +] + +match_pattern: [ +| "context" ident_opt "[" lconstr_pattern "]" +| lconstr_pattern +] + +ident_opt: [ +| ident +| empty +] + +lconstr_pattern: [ +| lconstr +] + +match_pattern_opt: [ +| "[" match_pattern "]" ":" +| empty +] + +match_list: [ +| or_opt match_rule_list_or +] + +match_rule_list_or: [ +| match_rule_list_or "|" match_rule +| match_rule +] + +match_rule: [ +| match_pattern "=>" ltac_expr +| "_" "=>" ltac_expr +] + +message_token_list_opt: [ +| message_token_list_opt message_token +| empty +] + +message_token: [ +| ident +| STRING +| integer +] + +failkw: [ +| "fail" +| "gfail" +] + +tactic_arg: [ +| "eval" red_expr "in" term +| "context" ident "[" lconstr "]" +| "type" "of" term +| "fresh" fresh_id_list_opt +| "type_term" uconstr +| "numgoals" +] + +fresh_id_list_opt: [ +| fresh_id_list_opt fresh_id +| empty +] + +fresh_id: [ +| STRING +| qualid +] + +tactic_arg_compat_list_opt: [ +| tactic_arg_compat_list_opt tactic_arg_compat +| empty +] + +tactic_arg_compat: [ +| tactic_arg +| term +| "()" +] + +ltac_expr0: [ +| "(" ltac_expr ")" +| "[" ">" tactic_then_gen "]" +| tactic_atom +| ssrparentacarg (* ssr plugin *) +] + +tactic_atom: [ +| integer +| reference +| "()" +] + +constr_may_eval: [ +| "eval" red_expr "in" term +| "context" ident "[" lconstr "]" +| "type" "of" term +| term +] + +ltac_def_kind: [ +| ":=" +| "::=" +] + +tacdef_body: [ +| global input_fun_list ltac_def_kind ltac_expr +| global ltac_def_kind ltac_expr +] + +tactic: [ +| ltac_expr +] + +ltac_info_opt: [ +| ltac_info +| empty +] + +ltac_info: [ +| "Info" natural +] + +ltac_use_default: [ +| "." +| "..." +] + +ltac_tactic_level: [ +| "(" "at" "level" natural ")" +] + +ltac_production_sep: [ +| "," string +] + +ltac_production_item: [ +| string +| ident "(" ident ltac_production_sep_opt ")" +| ident +] + +ltac_production_sep_opt: [ +| ltac_production_sep +| empty +] + +ltac_tacdef_body: [ +| tacdef_body +] + +firstorder_using: [ +| "using" reference +| "using" reference "," reference_list_comma +| "using" reference reference reference_list_opt +| empty +] + +reference_list_comma: [ +| reference_list_comma "," reference +| reference +] + +numnotoption: [ +| empty +| "(" "warning" "after" bigint ")" +| "(" "abstract" "after" bigint ")" +] + +mlname: [ +| preident (* extraction plugin *) +| string (* extraction plugin *) +] + +int_or_id: [ +| preident (* extraction plugin *) +| integer (* extraction plugin *) +] + +language: [ +| "Ocaml" (* extraction plugin *) +| "OCaml" (* extraction plugin *) +| "Haskell" (* extraction plugin *) +| "Scheme" (* extraction plugin *) +| "JSON" (* extraction plugin *) +] + +fun_ind_using: [ +| "using" constr_with_bindings (* funind plugin *) +| empty (* funind plugin *) +] + +with_names: [ +| "as" simple_intropattern (* funind plugin *) +| empty (* funind plugin *) +] + +constr_comma_sequence': [ +| term "," constr_comma_sequence' (* funind plugin *) +| term (* funind plugin *) +] + +auto_using': [ +| "using" constr_comma_sequence' (* funind plugin *) +| empty (* funind plugin *) +] + +function_rec_definition_loc: [ +| rec_definition (* funind plugin *) +] + +fun_scheme_arg: [ +| ident ":=" "Induction" "for" reference "Sort" sort_family (* funind plugin *) +] + +ring_mod: [ +| "decidable" term (* setoid_ring plugin *) +| "abstract" (* setoid_ring plugin *) +| "morphism" term (* setoid_ring plugin *) +| "constants" "[" tactic "]" (* setoid_ring plugin *) +| "closed" "[" global_list "]" (* setoid_ring plugin *) +| "preprocess" "[" tactic "]" (* setoid_ring plugin *) +| "postprocess" "[" tactic "]" (* setoid_ring plugin *) +| "setoid" term term (* setoid_ring plugin *) +| "sign" term (* setoid_ring plugin *) +| "power" term "[" global_list "]" (* setoid_ring plugin *) +| "power_tac" term "[" tactic "]" (* setoid_ring plugin *) +| "div" term (* setoid_ring plugin *) +] + +ring_mods: [ +| "(" ring_mod_list_comma ")" (* setoid_ring plugin *) +] + +ring_mod_list_comma: [ +| ring_mod_list_comma "," ring_mod +| ring_mod +] + +field_mod: [ +| ring_mod (* setoid_ring plugin *) +| "completeness" term (* setoid_ring plugin *) +] + +field_mods: [ +| "(" field_mod_list_comma ")" (* setoid_ring plugin *) +] + +field_mod_list_comma: [ +| field_mod_list_comma "," field_mod +| field_mod +] + +ssrtacarg: [ +| ltac_expr (* ssr plugin *) +] + +ssrtac3arg: [ +| ltac_expr3 (* ssr plugin *) +] + +ssrtclarg: [ +| ssrtacarg (* ssr plugin *) +] + +ssrhyp: [ +| ident (* ssr plugin *) +] + +ssrhoi_hyp: [ +| ident (* ssr plugin *) +] + +ssrhoi_id: [ +| ident (* ssr plugin *) +] + +ssrsimpl_ne: [ +| "//=" (* ssr plugin *) +| "/=" (* ssr plugin *) +| "/" natural "/" natural "=" (* ssr plugin *) +| "/" natural "/" (* ssr plugin *) +| "/" natural "=" (* ssr plugin *) +| "/" natural "/=" (* ssr plugin *) +| "/" natural "/" "=" (* ssr plugin *) +| "//" natural "=" (* ssr plugin *) +| "//" (* ssr plugin *) +] + +ssrclear_ne: [ +| "{" ssrhyp_list "}" (* ssr plugin *) +] + +ssrclear: [ +| ssrclear_ne (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssrindex: [ +| int_or_var (* ssr plugin *) +] + +ssrocc: [ +| natural natural_list_opt (* ssr plugin *) +| "-" natural_list_opt (* ssr plugin *) +| "+" natural_list_opt (* ssr plugin *) +] + +natural_list_opt: [ +| natural_list_opt natural +| empty +] + +ssrmmod: [ +| "!" (* ssr plugin *) +| "?" (* ssr plugin *) +| "?" (* ssr plugin *) +] + +ssrmult_ne: [ +| natural ssrmmod (* ssr plugin *) +| ssrmmod (* ssr plugin *) +] + +ssrmult: [ +| ssrmult_ne (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssrdocc: [ +| "{" ssrocc "}" (* ssr plugin *) +| "{" ssrhyp_list_opt "}" (* ssr plugin *) +] + +ssrhyp_list_opt: [ +| ssrhyp_list_opt ssrhyp +| empty +] + +ssrterm: [ +| "YouShouldNotTypeThis" term (* ssr plugin *) +| term (* ssr plugin *) +] + +ast_closure_term: [ +| term (* ssr plugin *) +] + +ast_closure_lterm: [ +| lconstr (* ssr plugin *) +] + +ssrbwdview: [ +| "YouShouldNotTypeThis" (* ssr plugin *) +| "/" term (* ssr plugin *) +| "/" term ssrbwdview (* ssr plugin *) +] + +ssrfwdview: [ +| "YouShouldNotTypeThis" (* ssr plugin *) +| "/" ast_closure_term (* ssr plugin *) +| "/" ast_closure_term ssrfwdview (* ssr plugin *) +] + +ident_no_do: [ +| "YouShouldNotTypeThis" ident (* ssr plugin *) +| IDENT (* ssr plugin *) +] + +ssripat: [ +| "_" (* ssr plugin *) +| "*" (* ssr plugin *) +| ">" (* ssr plugin *) +| ident_no_do (* ssr plugin *) +| "?" (* ssr plugin *) +| "+" (* ssr plugin *) +| "++" (* ssr plugin *) +| ssrsimpl_ne (* ssr plugin *) +| ssrdocc "->" (* ssr plugin *) +| ssrdocc "<-" (* ssr plugin *) +| ssrdocc (* ssr plugin *) +| "->" (* ssr plugin *) +| "<-" (* ssr plugin *) +| "-" (* ssr plugin *) +| "-/" "=" (* ssr plugin *) +| "-/=" (* ssr plugin *) +| "-/" "/" (* ssr plugin *) +| "-//" (* ssr plugin *) +| "-/" integer "/" (* ssr plugin *) +| "-/" "/=" (* ssr plugin *) +| "-//" "=" (* ssr plugin *) +| "-//=" (* ssr plugin *) +| "-/" integer "/=" (* ssr plugin *) +| "-/" integer "/" integer "=" (* ssr plugin *) +| ssrfwdview (* ssr plugin *) +| "[" ":" ident_list_opt "]" (* ssr plugin *) +| "[:" ident_list_opt "]" (* ssr plugin *) +| ssrcpat (* ssr plugin *) +] + +ident_list_opt: [ +| ident_list_opt ident +| empty +] + +ssripats: [ +| ssripat ssripats (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssriorpat: [ +| ssripats "|" ssriorpat (* ssr plugin *) +| ssripats "|-" ">" ssriorpat (* ssr plugin *) +| ssripats "|-" ssriorpat (* ssr plugin *) +| ssripats "|->" ssriorpat (* ssr plugin *) +| ssripats "||" ssriorpat (* ssr plugin *) +| ssripats "|||" ssriorpat (* ssr plugin *) +| ssripats "||||" ssriorpat (* ssr plugin *) +| ssripats (* ssr plugin *) +] + +ssrcpat: [ +| "YouShouldNotTypeThis" ssriorpat (* ssr plugin *) +| "[" hat "]" (* ssr plugin *) +| "[" ssriorpat "]" (* ssr plugin *) +| "[=" ssriorpat "]" (* ssr plugin *) +] + +hat: [ +| "^" ident (* ssr plugin *) +| "^" "~" ident (* ssr plugin *) +| "^" "~" natural (* ssr plugin *) +| "^~" ident (* ssr plugin *) +| "^~" natural (* ssr plugin *) +] + +ssripats_ne: [ +| ssripat ssripats (* ssr plugin *) +] + +ssrhpats: [ +| ssripats (* ssr plugin *) +] + +ssrhpats_wtransp: [ +| ssripats (* ssr plugin *) +| ssripats "@" ssripats (* ssr plugin *) +] + +ssrhpats_nobs: [ +| ssripats (* ssr plugin *) +] + +ssrrpat: [ +| "->" (* ssr plugin *) +| "<-" (* ssr plugin *) +] + +ssrintros_ne: [ +| "=>" ssripats_ne (* ssr plugin *) +] + +ssrintros: [ +| ssrintros_ne (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssrintrosarg: [ +| "YouShouldNotTypeThis" ssrtacarg ssrintros_ne (* ssr plugin *) +] + +ssrfwdid: [ +| ident (* ssr plugin *) +] + +ssrortacs: [ +| ssrtacarg "|" ssrortacs (* ssr plugin *) +| ssrtacarg "|" (* ssr plugin *) +| ssrtacarg (* ssr plugin *) +| "|" ssrortacs (* ssr plugin *) +| "|" (* ssr plugin *) +] + +ssrhintarg: [ +| "[" "]" (* ssr plugin *) +| "[" ssrortacs "]" (* ssr plugin *) +| ssrtacarg (* ssr plugin *) +] + +ssrhint3arg: [ +| "[" "]" (* ssr plugin *) +| "[" ssrortacs "]" (* ssr plugin *) +| ssrtac3arg (* ssr plugin *) +] + +ssrortacarg: [ +| "[" ssrortacs "]" (* ssr plugin *) +] + +ssrhint: [ +| empty (* ssr plugin *) +| "by" ssrhintarg (* ssr plugin *) +] + +ssrwgen: [ +| ssrclear_ne (* ssr plugin *) +| ssrhoi_hyp (* ssr plugin *) +| "@" ssrhoi_hyp (* ssr plugin *) +| "(" ssrhoi_id ":=" lcpattern ")" (* ssr plugin *) +| "(" ssrhoi_id ")" (* ssr plugin *) +| "(@" ssrhoi_id ":=" lcpattern ")" (* ssr plugin *) +| "(" "@" ssrhoi_id ":=" lcpattern ")" (* ssr plugin *) +] + +ssrclausehyps: [ +| ssrwgen "," ssrclausehyps (* ssr plugin *) +| ssrwgen ssrclausehyps (* ssr plugin *) +| ssrwgen (* ssr plugin *) +] + +ssrclauses: [ +| "in" ssrclausehyps "|-" "*" (* ssr plugin *) +| "in" ssrclausehyps "|-" (* ssr plugin *) +| "in" ssrclausehyps "*" (* ssr plugin *) +| "in" ssrclausehyps (* ssr plugin *) +| "in" "|-" "*" (* ssr plugin *) +| "in" "*" (* ssr plugin *) +| "in" "*" "|-" (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssrfwd: [ +| ":=" ast_closure_lterm (* ssr plugin *) +| ":" ast_closure_lterm ":=" ast_closure_lterm (* ssr plugin *) +] + +ssrbvar: [ +| ident (* ssr plugin *) +| "_" (* ssr plugin *) +] + +ssrbinder: [ +| ssrbvar (* ssr plugin *) +| "(" ssrbvar ")" (* ssr plugin *) +| "(" ssrbvar ":" lconstr ")" (* ssr plugin *) +| "(" ssrbvar ssrbvar_list ":" lconstr ")" (* ssr plugin *) +| "(" ssrbvar ":" lconstr ":=" lconstr ")" (* ssr plugin *) +| "(" ssrbvar ":=" lconstr ")" (* ssr plugin *) +| of_alt operconstr99 (* ssr plugin *) +] + +ssrbvar_list: [ +| ssrbvar_list ssrbvar +| ssrbvar +] + +ssrstruct: [ +| "{" "struct" ident "}" (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssrposefwd: [ +| ssrbinder_list_opt ssrfwd (* ssr plugin *) +] + +ssrfixfwd: [ +| "fix" ssrbvar ssrbinder_list_opt ssrstruct ssrfwd (* ssr plugin *) +] + +ssrcofixfwd: [ +| "cofix" ssrbvar ssrbinder_list_opt ssrfwd (* ssr plugin *) +] + +ssrbinder_list_opt: [ +| ssrbinder_list_opt ssrbinder +| empty +] + +ssrsetfwd: [ +| ":" ast_closure_lterm ":=" "{" ssrocc "}" cpattern (* ssr plugin *) +| ":" ast_closure_lterm ":=" lcpattern (* ssr plugin *) +| ":=" "{" ssrocc "}" cpattern (* ssr plugin *) +| ":=" lcpattern (* ssr plugin *) +] + +ssrhavefwd: [ +| ":" ast_closure_lterm ssrhint (* ssr plugin *) +| ":" ast_closure_lterm ":=" ast_closure_lterm (* ssr plugin *) +| ":" ast_closure_lterm ":=" (* ssr plugin *) +| ":=" ast_closure_lterm (* ssr plugin *) +] + +ssrhavefwdwbinders: [ +| ssrhpats_wtransp ssrbinder_list_opt ssrhavefwd (* ssr plugin *) +] + +ssrseqarg: [ +| ssrswap (* ssr plugin *) +| ssrseqidx ssrortacarg ssrorelse_opt (* ssr plugin *) +| ssrseqidx ssrswap (* ssr plugin *) +| ltac_expr3 (* ssr plugin *) +] + +ssrorelse_opt: [ +| ssrorelse +| empty +] + +ssrseqidx: [ +| ident (* ssr plugin *) +| natural (* ssr plugin *) +] + +ssrswap: [ +| "first" (* ssr plugin *) +| "last" (* ssr plugin *) +] + +ssrorelse: [ +| "||" ltac_expr2 (* ssr plugin *) +] + +ident: [ +| IDENT +] + +ssrparentacarg: [ +| "(" ltac_expr ")" (* ssr plugin *) +] + +ssrdotac: [ +| ltac_expr3 (* ssr plugin *) +| ssrortacarg (* ssr plugin *) +] + +ssr_first: [ +| ssr_first ssrintros_ne (* ssr plugin *) +| "[" ltac_expr_list_or_opt "]" (* ssr plugin *) +] + +ssr_first_else: [ +| ssr_first ssrorelse (* ssr plugin *) +| ssr_first (* ssr plugin *) +] + +ssrgen: [ +| ssrdocc cpattern (* ssr plugin *) +| cpattern (* ssr plugin *) +] + +ssrdgens_tl: [ +| "{" ssrhyp_list "}" cpattern ssrdgens_tl (* ssr plugin *) +| "{" ssrhyp_list "}" (* ssr plugin *) +| "{" ssrocc "}" cpattern ssrdgens_tl (* ssr plugin *) +| "/" ssrdgens_tl (* ssr plugin *) +| cpattern ssrdgens_tl (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssrdgens: [ +| ":" ssrgen ssrdgens_tl (* ssr plugin *) +] + +ssreqid: [ +| ssreqpat (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssreqpat: [ +| ident (* ssr plugin *) +| "_" (* ssr plugin *) +| "?" (* ssr plugin *) +| "+" (* ssr plugin *) +| ssrdocc "->" (* ssr plugin *) +| ssrdocc "<-" (* ssr plugin *) +| "->" (* ssr plugin *) +| "<-" (* ssr plugin *) +] + +ssrarg: [ +| ssrfwdview ssreqid ssrdgens ssrintros (* ssr plugin *) +| ssrfwdview ssrclear ssrintros (* ssr plugin *) +| ssreqid ssrdgens ssrintros (* ssr plugin *) +| ssrclear_ne ssrintros (* ssr plugin *) +| ssrintros_ne (* ssr plugin *) +] + +ssrmovearg: [ +| ssrarg (* ssr plugin *) +] + +ssrcasearg: [ +| ssrarg (* ssr plugin *) +] + +ssragen: [ +| "{" ssrhyp_list "}" ssrterm (* ssr plugin *) +| ssrterm (* ssr plugin *) +] + +ssrhyp_list: [ +| ssrhyp_list ssrhyp +| ssrhyp +] + +ssragens: [ +| "{" ssrhyp_list "}" ssrterm ssragens (* ssr plugin *) +| "{" ssrhyp_list "}" (* ssr plugin *) +| ssrterm ssragens (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssrapplyarg: [ +| ":" ssragen ssragens ssrintros (* ssr plugin *) +| ssrclear_ne ssrintros (* ssr plugin *) +| ssrintros_ne (* ssr plugin *) +| ssrbwdview ":" ssragen ssragens ssrintros (* ssr plugin *) +| ssrbwdview ssrclear ssrintros (* ssr plugin *) +] + +ssrexactarg: [ +| ":" ssragen ssragens (* ssr plugin *) +| ssrbwdview ssrclear (* ssr plugin *) +| ssrclear_ne (* ssr plugin *) +] + +ssrcongrarg: [ +| natural term ssrdgens (* ssr plugin *) +| natural term (* ssr plugin *) +| term ssrdgens (* ssr plugin *) +| term (* ssr plugin *) +] + +ssrrwocc: [ +| "{" ssrhyp_list_opt "}" (* ssr plugin *) +| "{" ssrocc "}" (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssrrule_ne: [ +| ssrterm_alt (* ssr plugin *) +| ssrsimpl_ne (* ssr plugin *) +] + +ssrterm_alt: [ +| "/" ssrterm +| ssrterm +| ssrsimpl_ne +] + +ssrrule: [ +| ssrrule_ne (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssrpattern_squarep: [ +| "[" rpattern "]" (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssrpattern_ne_squarep: [ +| "[" rpattern "]" (* ssr plugin *) +] + +ssrrwarg: [ +| "-" ssrmult ssrrwocc ssrpattern_squarep ssrrule_ne (* ssr plugin *) +| "-/" ssrterm (* ssr plugin *) +| ssrmult_ne ssrrwocc ssrpattern_squarep ssrrule_ne (* ssr plugin *) +| "{" ssrhyp_list "}" ssrpattern_ne_squarep ssrrule_ne (* ssr plugin *) +| "{" ssrhyp_list "}" ssrrule (* ssr plugin *) +| "{" ssrocc "}" ssrpattern_squarep ssrrule_ne (* ssr plugin *) +| "{" "}" ssrpattern_squarep ssrrule_ne (* ssr plugin *) +| ssrpattern_ne_squarep ssrrule_ne (* ssr plugin *) +| ssrrule_ne (* ssr plugin *) +] + +ssrrwargs: [ +| ssrrwarg_list (* ssr plugin *) +] + +ssrrwarg_list: [ +| ssrrwarg_list ssrrwarg +| ssrrwarg +] + +ssrunlockarg: [ +| "{" ssrocc "}" ssrterm (* ssr plugin *) +| ssrterm (* ssr plugin *) +] + +ssrunlockargs: [ +| ssrunlockarg_list_opt (* ssr plugin *) +] + +ssrunlockarg_list_opt: [ +| ssrunlockarg_list_opt ssrunlockarg +| empty +] + +ssrsufffwd: [ +| ssrhpats ssrbinder_list_opt ":" ast_closure_lterm ssrhint (* ssr plugin *) +] + +ssrwlogfwd: [ +| ":" ssrwgen_list_opt "/" ast_closure_lterm (* ssr plugin *) +] + +ssrwgen_list_opt: [ +| ssrwgen_list_opt ssrwgen +| empty +] + +ssr_idcomma: [ +| empty (* ssr plugin *) +| IDENT_alt "," (* ssr plugin *) +] + +IDENT_alt: [ +| IDENT +| "_" +] + +ssr_rtype: [ +| "return" operconstr100 (* ssr plugin *) +] + +ssr_mpat: [ +| pattern200 (* ssr plugin *) +] + +ssr_dpat: [ +| ssr_mpat "in" pattern200 ssr_rtype (* ssr plugin *) +| ssr_mpat ssr_rtype (* ssr plugin *) +| ssr_mpat (* ssr plugin *) +] + +ssr_dthen: [ +| ssr_dpat "then" lconstr (* ssr plugin *) +] + +ssr_elsepat: [ +| "else" (* ssr plugin *) +] + +ssr_else: [ +| ssr_elsepat lconstr (* ssr plugin *) +] + +ssr_search_item: [ +| string (* ssr plugin *) +| string "%" preident (* ssr plugin *) +| constr_pattern (* ssr plugin *) +] + +ssr_search_arg: [ +| "-" ssr_search_item ssr_search_arg (* ssr plugin *) +| ssr_search_item ssr_search_arg (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssr_modlocs: [ +| empty (* ssr plugin *) +| "in" modloc_list (* ssr plugin *) +] + +modloc_list: [ +| modloc_list modloc +| modloc +] + +modloc: [ +| "-" global (* ssr plugin *) +| global (* ssr plugin *) +] + +ssrhintref: [ +| term (* ssr plugin *) +| term "|" natural (* ssr plugin *) +] + +ssrviewpos: [ +| "for" "move" "/" (* ssr plugin *) +| "for" "apply" "/" (* ssr plugin *) +| "for" "apply" "/" "/" (* ssr plugin *) +| "for" "apply" "//" (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssrviewposspc: [ +| ssrviewpos (* ssr plugin *) +] + +rpattern: [ +| lconstr (* ssrmatching plugin *) +| "in" lconstr (* ssrmatching plugin *) +| lconstr "in" lconstr (* ssrmatching plugin *) +| "in" lconstr "in" lconstr (* ssrmatching plugin *) +| lconstr "in" lconstr "in" lconstr (* ssrmatching plugin *) +| lconstr "as" lconstr "in" lconstr (* ssrmatching plugin *) +] + +cpattern: [ +| "Qed" term (* ssrmatching plugin *) +| term (* ssrmatching plugin *) +] + +lcpattern: [ +| "Qed" lconstr (* ssrmatching plugin *) +| lconstr (* ssrmatching plugin *) +] + +ssrpatternarg: [ +| rpattern (* ssrmatching plugin *) +] + +empty: [ +| +] + +lpar_id_coloneq: [ +| "(" IDENT; ":=" +] + +name_colon: [ +| IDENT; ":" +| "_" ":" +] + +int: [ +| integer +] + +command_entry: [ +| noedit_mode +] + diff --git a/doc/tools/docgram/prodn.edit_mlg b/doc/tools/docgram/prodn.edit_mlg new file mode 100644 index 0000000000..a28d07636a --- /dev/null +++ b/doc/tools/docgram/prodn.edit_mlg @@ -0,0 +1,14 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \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) *) +(************************************************************************) + +(* Defines additional productions and edits for use in documentation. Not compiled into Coq *) +(* Contents used to generate prodn in doc *) + +DOC_GRAMMAR diff --git a/doc/tools/docgram/productionlist.edit_mlg b/doc/tools/docgram/productionlist.edit_mlg new file mode 100644 index 0000000000..84acd07075 --- /dev/null +++ b/doc/tools/docgram/productionlist.edit_mlg @@ -0,0 +1,25 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \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) *) +(************************************************************************) + +(* Defines additional productions and edits for use in documentation. Not compiled into Coq *) +(* Contents used to generate productionlists in doc *) + +DOC_GRAMMAR + +EXPAND: [ | ] + +(* ugh todo: try to handle before expansion *) +tactic_then_gen : [ +| REPLACE ltac_expr_opt ".." ltac_expr_opt2 +| WITH ltac_expr_opt ".." or_opt ltac_expr_list2 +] + +ltac_expr_opt2 : [ | DELETENT ] +ltac_expr_list2_opt : [ | DELETENT ] |