diff options
Diffstat (limited to 'doc/tools')
23 files changed, 1343 insertions, 921 deletions
diff --git a/doc/tools/coqrst/__init__.py b/doc/tools/coqrst/__init__.py index 710a90a6f1..5720cd9be0 100644 --- a/doc/tools/coqrst/__init__.py +++ b/doc/tools/coqrst/__init__.py @@ -1,7 +1,7 @@ ########################################################################## ## # 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) ## +## v # Copyright INRIA, CNRS and contributors ## +## <O___,, # (see version control and CREDITS file for authors & dates) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## ## # GNU Lesser General Public License Version 2.1 ## diff --git a/doc/tools/coqrst/checkdeps.py b/doc/tools/coqrst/checkdeps.py index feafcba026..899c80fbe6 100644 --- a/doc/tools/coqrst/checkdeps.py +++ b/doc/tools/coqrst/checkdeps.py @@ -1,7 +1,7 @@ ########################################################################## ## # 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) ## +## v # Copyright INRIA, CNRS and contributors ## +## <O___,, # (see version control and CREDITS file for authors & dates) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## ## # GNU Lesser General Public License Version 2.1 ## diff --git a/doc/tools/coqrst/coqdoc/__init__.py b/doc/tools/coqrst/coqdoc/__init__.py index 8d19924df1..3fe6886897 100644 --- a/doc/tools/coqrst/coqdoc/__init__.py +++ b/doc/tools/coqrst/coqdoc/__init__.py @@ -1,7 +1,7 @@ ########################################################################## ## # 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) ## +## v # Copyright INRIA, CNRS and contributors ## +## <O___,, # (see version control and CREDITS file for authors & dates) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## ## # GNU Lesser General Public License Version 2.1 ## diff --git a/doc/tools/coqrst/coqdoc/main.py b/doc/tools/coqrst/coqdoc/main.py index adacba97cc..a3fc069e6c 100644 --- a/doc/tools/coqrst/coqdoc/main.py +++ b/doc/tools/coqrst/coqdoc/main.py @@ -1,7 +1,7 @@ ########################################################################## ## # 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) ## +## v # Copyright INRIA, CNRS and contributors ## +## <O___,, # (see version control and CREDITS file for authors & dates) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## ## # GNU Lesser General Public License Version 2.1 ## diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 4d5c837e5c..6332c4c81d 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -1,7 +1,7 @@ ########################################################################## ## # 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) ## +## v # Copyright INRIA, CNRS and contributors ## +## <O___,, # (see version control and CREDITS file for authors & dates) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## ## # GNU Lesser General Public License Version 2.1 ## @@ -34,7 +34,6 @@ from sphinx.util.logging import getLogger, get_node_location from sphinx.directives import ObjectDescription from sphinx.domains import Domain, ObjType, Index from sphinx.domains.std import token_xrefs -from sphinx.ext import mathbase from . import coqdoc from .repl import ansicolors @@ -74,8 +73,7 @@ def make_target(objtype, targetid): return "coq:{}.{}".format(objtype, targetid) def make_math_node(latex, docname, nowrap): - node = mathbase.displaymath() - node['latex'] = latex + node = nodes.math_block(latex, latex) node['label'] = None # Otherwise equations are numbered node['nowrap'] = nowrap node['docname'] = docname @@ -339,7 +337,7 @@ class TacticNotationObject(NotationObject): """ subdomain = "tacn" index_suffix = "(tactic)" - annotation = None + annotation = "Tactic" class AttributeNotationObject(NotationObject): """An attribute. @@ -493,9 +491,7 @@ class ProductionObject(CoqObject): pass def _target_id(self, name): - # Use `name[1]` instead of ``nodes.make_id(name[1])`` to work around - # https://github.com/sphinx-doc/sphinx/issues/4983 - return 'grammar-token-{}'.format(name[1]) + return 'grammar-token-{}'.format(nodes.make_id(name[1])) def _record_name(self, name, targetid): env = self.state.document.settings.env @@ -523,7 +519,7 @@ class ProductionObject(CoqObject): row = nodes.inline(classes=['prodn-row']) entry = nodes.inline(classes=['prodn-cell-nonterminal']) if lhs != "": - target_name = 'grammar-token-' + lhs + target_name = 'grammar-token-' + nodes.make_id(lhs) target = nodes.target('', '', ids=[target_name], names=[target_name]) # putting prodn-target on the target node won't appear in the tex file inline = nodes.inline(classes=['prodn-target']) diff --git a/doc/tools/coqrst/notations/Makefile b/doc/tools/coqrst/notations/Makefile index 29132f1cd7..dc3a647f9e 100644 --- a/doc/tools/coqrst/notations/Makefile +++ b/doc/tools/coqrst/notations/Makefile @@ -1,7 +1,7 @@ ########################################################################## ## # 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) ## +## v # Copyright INRIA, CNRS and contributors ## +## <O___,, # (see version control and CREDITS file for authors & dates) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## ## # GNU Lesser General Public License Version 2.1 ## diff --git a/doc/tools/coqrst/notations/TacticNotations.g b/doc/tools/coqrst/notations/TacticNotations.g index f9cf26a21e..f29c69eeaf 100644 --- a/doc/tools/coqrst/notations/TacticNotations.g +++ b/doc/tools/coqrst/notations/TacticNotations.g @@ -1,7 +1,7 @@ /************************************************************************/ /* * 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) */ +/* v * Copyright INRIA, CNRS and contributors */ +/* <O___,, * (see version control and CREDITS file for authors & dates) */ /* \VV/ **************************************************************/ /* // * This file is distributed under the terms of the */ /* * GNU Lesser General Public License Version 2.1 */ diff --git a/doc/tools/coqrst/notations/fontsupport.py b/doc/tools/coqrst/notations/fontsupport.py index c3ba2c1301..1ffd816ba7 100755 --- a/doc/tools/coqrst/notations/fontsupport.py +++ b/doc/tools/coqrst/notations/fontsupport.py @@ -2,8 +2,8 @@ # -*- coding: utf-8 -*- ########################################################################## ## # 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) ## +## v # Copyright INRIA, CNRS and contributors ## +## <O___,, # (see version control and CREDITS file for authors & dates) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## ## # GNU Lesser General Public License Version 2.1 ## diff --git a/doc/tools/coqrst/notations/html.py b/doc/tools/coqrst/notations/html.py index 1136ee4997..7219fc2e37 100644 --- a/doc/tools/coqrst/notations/html.py +++ b/doc/tools/coqrst/notations/html.py @@ -1,7 +1,7 @@ ########################################################################## ## # 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) ## +## v # Copyright INRIA, CNRS and contributors ## +## <O___,, # (see version control and CREDITS file for authors & dates) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## ## # GNU Lesser General Public License Version 2.1 ## diff --git a/doc/tools/coqrst/notations/parsing.py b/doc/tools/coqrst/notations/parsing.py index 7b7febe668..abefd97121 100644 --- a/doc/tools/coqrst/notations/parsing.py +++ b/doc/tools/coqrst/notations/parsing.py @@ -1,7 +1,7 @@ ########################################################################## ## # 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) ## +## v # Copyright INRIA, CNRS and contributors ## +## <O___,, # (see version control and CREDITS file for authors & dates) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## ## # GNU Lesser General Public License Version 2.1 ## diff --git a/doc/tools/coqrst/notations/plain.py b/doc/tools/coqrst/notations/plain.py index 23996b0d63..2a8bf76e75 100644 --- a/doc/tools/coqrst/notations/plain.py +++ b/doc/tools/coqrst/notations/plain.py @@ -1,7 +1,7 @@ ########################################################################## ## # 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) ## +## v # Copyright INRIA, CNRS and contributors ## +## <O___,, # (see version control and CREDITS file for authors & dates) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## ## # GNU Lesser General Public License Version 2.1 ## diff --git a/doc/tools/coqrst/notations/regexp.py b/doc/tools/coqrst/notations/regexp.py index 697201a5d5..5979fe8f82 100644 --- a/doc/tools/coqrst/notations/regexp.py +++ b/doc/tools/coqrst/notations/regexp.py @@ -1,7 +1,7 @@ ########################################################################## ## # 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) ## +## v # Copyright INRIA, CNRS and contributors ## +## <O___,, # (see version control and CREDITS file for authors & dates) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## ## # GNU Lesser General Public License Version 2.1 ## diff --git a/doc/tools/coqrst/notations/sphinx.py b/doc/tools/coqrst/notations/sphinx.py index 5659a64b84..158a703640 100644 --- a/doc/tools/coqrst/notations/sphinx.py +++ b/doc/tools/coqrst/notations/sphinx.py @@ -1,7 +1,7 @@ ########################################################################## ## # 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) ## +## v # Copyright INRIA, CNRS and contributors ## +## <O___,, # (see version control and CREDITS file for authors & dates) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## ## # GNU Lesser General Public License Version 2.1 ## diff --git a/doc/tools/coqrst/repl/ansicolors.py b/doc/tools/coqrst/repl/ansicolors.py index 6d9c79d16c..9e23be2409 100644 --- a/doc/tools/coqrst/repl/ansicolors.py +++ b/doc/tools/coqrst/repl/ansicolors.py @@ -1,7 +1,7 @@ ########################################################################## ## # 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) ## +## v # Copyright INRIA, CNRS and contributors ## +## <O___,, # (see version control and CREDITS file for authors & dates) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## ## # GNU Lesser General Public License Version 2.1 ## diff --git a/doc/tools/coqrst/repl/coqtop.py b/doc/tools/coqrst/repl/coqtop.py index 3dc20db82b..c306961550 100644 --- a/doc/tools/coqrst/repl/coqtop.py +++ b/doc/tools/coqrst/repl/coqtop.py @@ -1,7 +1,7 @@ ########################################################################## ## # 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) ## +## v # Copyright INRIA, CNRS and contributors ## +## <O___,, # (see version control and CREDITS file for authors & dates) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## ## # GNU Lesser General Public License Version 2.1 ## diff --git a/doc/tools/docgram/README.md b/doc/tools/docgram/README.md index fc6d0ace0d..4cde3809f0 100644 --- a/doc/tools/docgram/README.md +++ b/doc/tools/docgram/README.md @@ -1,12 +1,13 @@ # 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. +`doc_grammar` extracts Coq's grammar from `.mlg` files, edits it and inserts it +into `.rst` files. The tool inserts `prodn` directives for grammar productions. +(`productionlist` are gradually being replaced by `prodn` in the manual.) +It also updates `tacn` and `cmd` directives when they can be unambiguously matched to +productions of the grammar (in practice, that's probably almost always). +`tacv` and `cmdv` directives are not updated because matching them appears to require +human judgement. `doc_grammar` generates a few files that may be useful to +developers and documentors. The mlg grammars present several challenges to generating an accurate grammar for documentation purposes: @@ -33,46 +34,49 @@ for documentation purposes: ## 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`. +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 nonterminals and individual productions + in the documented grammar. Developers should edit this file only to reorder lines. + `doc_grammar` updates `orderedGrammar` so it has the same set of nonterminals and productions + as `editedGrammar` while retaining the previous ordering. Since the position of + new or renamed nonterminals is unspecified, they tend to show up in the wrong + place in `orderedGrammar`, therefore users should review the output and make + appropriate adjustments to the order. + + The update process removes manually-added comments from `orderedGrammar` while + automatically-generated comments will be regenerated. + +4. The tool updates the `.rst` files. Comments in the form + `.. insertprodn <first nt> <last nt>` indicate inserting the productions for a + range of nonterminals. `.. cmd::` and `.. tacn::` directives are updated using + prefixes in the form `[a-zA-Z0-9_ ]+` from the directive and the + grammar. If there is unique match in the grammar, the directive is updated, if needed. + Multiple matches or no match gives an error message. + +5. For reference, the tool generates `prodnGrammar`, which has the entire grammar in the form of `prodns`. ## How to use the tool @@ -106,6 +110,9 @@ Other command line arguments: * `-no-warn` suppresses printing of some warning messages +* `-no-update` puts updates to `fullGrammar` and `orderedGrammar` into new files named + `*.new`, leaving the originals unmodified. For use in Dune. + * `-short` limits processing to updating/verifying only the `fullGrammar` file * `-verbose` prints more messages about the grammar @@ -114,12 +121,12 @@ Other command line arguments: ### Grammar editing scripts -The grammar editing scripts `*.edit_mlg` are similar in format to `.mlg` files stripped +The grammar editing script `common.edit_mlg` is similar in format to `.mlg` files but 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. +signals the use of the streamlined syntax. -Each edit file has a series of items in the form of productions. Items are applied +The 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. @@ -136,7 +143,7 @@ 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 +the name of a non-terminal and adds a 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 @@ -191,7 +198,7 @@ that appear in the specified production: ``` `MOVETO <destination> <production>` - moves the production to `<destination>` and, - if needed, creates a new production <edited_nt> -> <destination>. + if needed, creates a new production <edited_nt> -> \<destination>. `OPTINREF` - verifies that <edited_nt> has an empty production. If so, it removes the empty production and replaces all references to <edited_nt> throughout the @@ -200,7 +207,7 @@ grammar with `OPT <edited_nt>` `PRINT` <nonterminal> - prints the nonterminal definition at that point in applying the edits. Most useful when the edits get a bit complicated to follow. -* (any other nonterminal name) - adds a new production (and possibly a new nonterminal) +`(any other nonterminal name)` - adds a new production (and possibly a new nonterminal) to the grammar. ### `.rst` file updates diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 7a165988a6..60b845c4be 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -140,10 +140,10 @@ field_ident: [ | "." ident ] -basequalid: [ -| REPLACE ident fields -| WITH ident LIST0 field_ident -| DELETE ident +qualid: [ | DELETENT ] + +qualid: [ +| ident LIST0 field_ident ] field: [ | DELETENT ] @@ -313,6 +313,7 @@ closed_binder: [ | REPLACE "{" name LIST1 name ":" lconstr "}" | WITH "{" LIST1 name type_cstr "}" | DELETE "{" name ":" lconstr "}" +| MOVETO implicit_binders "{" LIST1 name type_cstr "}" | DELETE "[" name "]" | DELETE "[" name LIST1 name "]" @@ -320,9 +321,14 @@ closed_binder: [ | REPLACE "[" name LIST1 name ":" lconstr "]" | WITH "[" LIST1 name type_cstr "]" | DELETE "[" name ":" lconstr "]" +| MOVETO implicit_binders "[" LIST1 name type_cstr "]" | REPLACE "(" Prim.name ":" lconstr "|" lconstr ")" | WITH "(" Prim.name ":" type "|" lconstr ")" + +| MOVETO generalizing_binder "`(" LIST1 typeclass_constraint SEP "," ")" +| MOVETO generalizing_binder "`{" LIST1 typeclass_constraint SEP "," "}" +| MOVETO generalizing_binder "`[" LIST1 typeclass_constraint SEP "," "]" ] name_colon: [ @@ -383,15 +389,25 @@ evar_instance: [ | OPTINREF ] +(* No constructor syntax, OPT [ "|" binders ] is not supported for Record *) +record_definition: [ +| opt_coercion ident_decl binders OPT [ ":" type ] OPT [ identref ] "{" record_fields "}" decl_notations +] + +(* No record syntax, opt_coercion not supported for Variant, := ... required *) +variant_definition: [ +| ident_decl binders OPT [ "|" binders ] OPT [ ":" type ] ":=" OPT "|" LIST1 constructor SEP "|" decl_notations +] + gallina: [ | REPLACE thm_token ident_decl binders ":" lconstr LIST0 [ "with" ident_decl binders ":" lconstr ] | WITH thm_token ident_decl binders ":" type LIST0 [ "with" ident_decl binders ":" type ] | DELETE assumptions_token inline assum_list -| REPLACE OPT cumulativity_token private_token finite_token LIST1 inductive_definition SEP "with" +| REPLACE finite_token LIST1 inductive_definition SEP "with" | WITH "Inductive" inductive_definition LIST0 ( "with" inductive_definition ) | "CoInductive" inductive_definition LIST0 ( "with" inductive_definition ) -| "Variant" inductive_definition LIST0 ( "with" inductive_definition ) -| [ "Record" | "Structure" ] inductive_definition LIST0 ( "with" inductive_definition ) +| "Variant" variant_definition LIST0 ( "with" variant_definition ) +| [ "Record" | "Structure" ] record_definition LIST0 ( "with" record_definition ) | "Class" inductive_definition LIST0 ( "with" inductive_definition ) | REPLACE "Fixpoint" LIST1 rec_definition SEP "with" | WITH "Fixpoint" rec_definition LIST0 ( "with" rec_definition ) @@ -405,18 +421,13 @@ gallina: [ | WITH "Scheme" scheme LIST0 ( "with" scheme ) ] -DELETE: [ -| private_token -| cumulativity_token -] - constructor_list_or_record_decl: [ | OPTINREF ] record_fields: [ | REPLACE record_field ";" record_fields -| WITH LIST1 record_field SEP ";" +| WITH LIST0 record_field SEP ";" | DELETE record_field | DELETE (* empty *) ] @@ -492,16 +503,46 @@ functor_app_annot: [ ] is_module_expr: [ +| REPLACE ":=" module_expr_inl LIST0 ext_module_expr +| WITH ":=" LIST1 module_expr_inl SEP "<+" | OPTINREF ] is_module_type: [ +| REPLACE ":=" module_type_inl LIST0 ext_module_type +| WITH ":=" LIST1 module_type_inl SEP "<+" | OPTINREF ] gallina_ext: [ | REPLACE "Arguments" smart_global LIST0 argument_spec_block OPT [ "," LIST1 [ LIST0 more_implicits_block ] SEP "," ] OPT [ ":" LIST1 arguments_modifier SEP "," ] | WITH "Arguments" smart_global LIST0 argument_spec_block LIST0 [ "," LIST0 more_implicits_block ] OPT [ ":" LIST1 arguments_modifier SEP "," ] +| REPLACE "Implicit" "Type" reserv_list +| WITH "Implicit" [ "Type" | "Types" ] reserv_list +| DELETE "Implicit" "Types" reserv_list + +(* Per @Zimmi48, the global (qualid) must be a simple identifier if def_body is present + Note that smart_global is "qualid | by_notation" and that + ident_decl is "ident OPT univ_decl"; move + *) +| REPLACE "Canonical" OPT "Structure" global OPT [ OPT univ_decl def_body ] +| WITH "Canonical" OPT "Structure" ident_decl def_body +| REPLACE "Canonical" OPT "Structure" by_notation +| WITH "Canonical" OPT "Structure" smart_global + +| REPLACE "Include" "Type" module_type_inl LIST0 ext_module_type +| WITH "Include" "Type" LIST1 module_type_inl SEP "<+" + +| REPLACE "Generalizable" [ "All" "Variables" | "No" "Variables" | [ "Variable" | "Variables" ] LIST1 identref ] +| WITH "Generalizable" [ [ "Variable" | "Variables" ] LIST1 identref | "All" "Variables" | "No" "Variables" ] + +| REPLACE "Export" "Set" option_table option_setting +| WITH OPT "Export" "Set" option_table option_setting +| REPLACE "Export" "Unset" option_table +| WITH OPT "Export" "Unset" option_table +| REPLACE "Instance" instance_name ":" operconstr200 hint_info [ ":=" "{" record_declaration "}" | ":=" lconstr | ] +| WITH "Instance" instance_name ":" operconstr200 hint_info OPT [ ":=" "{" record_declaration "}" | ":=" lconstr ] + ] (* lexer stuff *) @@ -624,6 +665,19 @@ selector_body: [ range_selector_or_nth: [ | DELETENT ] +firstorder_rhs: [ +| firstorder_using +| "with" LIST1 preident +| firstorder_using "with" LIST1 preident +] + +where: [ +| "at" "top" +| "at" "bottom" +| "after" ident +| "before" ident +] + simple_tactic: [ | DELETE "intros" | REPLACE "intros" ne_intropatterns @@ -631,6 +685,158 @@ simple_tactic: [ | DELETE "eintros" | REPLACE "eintros" ne_intropatterns | WITH "eintros" intropatterns +| DELETE "autorewrite" "with" LIST1 preident clause +| DELETE "autorewrite" "with" LIST1 preident clause "using" tactic +| DELETE "autorewrite" "*" "with" LIST1 preident clause +| REPLACE "autorewrite" "*" "with" LIST1 preident clause "using" tactic +| WITH "autorewrite" OPT "*" "with" LIST1 preident clause_dft_concl OPT ( "using" tactic ) +| DELETE "cofix" ident +| REPLACE "cofix" ident "with" LIST1 cofixdecl +| WITH "cofix" ident OPT ( "with" LIST1 cofixdecl ) +| DELETE "constructor" +| DELETE "constructor" int_or_var +| REPLACE "constructor" int_or_var "with" bindings +| WITH "constructor" OPT int_or_var OPT ( "with" bindings ) +| DELETE "econstructor" +| DELETE "econstructor" int_or_var +| REPLACE "econstructor" int_or_var "with" bindings +| WITH "econstructor" OPT ( int_or_var OPT ( "with" bindings ) ) +| DELETE "dependent" "rewrite" orient constr +| REPLACE "dependent" "rewrite" orient constr "in" hyp +| WITH "dependent" "rewrite" orient constr OPT ( "in" hyp ) +| "firstorder" OPT tactic firstorder_rhs +| DELETE "firstorder" OPT tactic firstorder_using +| DELETE "firstorder" OPT tactic "with" LIST1 preident +| DELETE "firstorder" OPT tactic firstorder_using "with" LIST1 preident +| DELETE "fix" ident natural +| REPLACE "fix" ident natural "with" LIST1 fixdecl +| WITH "fix" ident natural OPT ( "with" LIST1 fixdecl ) +| DELETE "generalize" constr +| REPLACE "generalize" constr LIST1 constr +| WITH "generalize" constr OPT ( LIST1 constr ) +| EDIT "simplify_eq" ADD_OPT destruction_arg +| EDIT "esimplify_eq" ADD_OPT destruction_arg +| EDIT "discriminate" ADD_OPT destruction_arg +| EDIT "ediscriminate" ADD_OPT destruction_arg +| DELETE "injection" +| DELETE "injection" destruction_arg +| DELETE "injection" "as" LIST0 simple_intropattern +| REPLACE "injection" destruction_arg "as" LIST0 simple_intropattern +| WITH "injection" OPT destruction_arg OPT ( "as" LIST0 simple_intropattern ) +| DELETE "einjection" +| DELETE "einjection" destruction_arg +| DELETE "einjection" "as" LIST0 simple_intropattern +| REPLACE "einjection" destruction_arg "as" LIST0 simple_intropattern +| WITH "einjection" OPT destruction_arg OPT ( "as" LIST0 simple_intropattern ) +| EDIT "simple" "injection" ADD_OPT destruction_arg +| DELETE "intro" (* todo: change the mlg to simplify! *) +| DELETE "intro" ident +| DELETE "intro" ident "at" "top" +| DELETE "intro" ident "at" "bottom" +| DELETE "intro" ident "after" hyp +| DELETE "intro" ident "before" hyp +| DELETE "intro" "at" "top" +| DELETE "intro" "at" "bottom" +| DELETE "intro" "after" hyp +| DELETE "intro" "before" hyp +| "intro" OPT ident OPT where +| DELETE "move" hyp "at" "top" +| DELETE "move" hyp "at" "bottom" +| DELETE "move" hyp "after" hyp +| DELETE "move" hyp "before" hyp +| "move" ident OPT where +| DELETE "replace" "->" uconstr clause +| DELETE "replace" "<-" uconstr clause +| DELETE "replace" uconstr clause +| "replace" orient uconstr clause_dft_concl (* todo: fix 'clause' *) +| REPLACE "rewrite" "*" orient uconstr "in" hyp "at" occurrences by_arg_tac +| WITH "rewrite" "*" orient uconstr OPT ( "in" hyp ) OPT ( "at" occurrences by_arg_tac ) +| DELETE "rewrite" "*" orient uconstr "in" hyp by_arg_tac +| DELETE "rewrite" "*" orient uconstr "at" occurrences by_arg_tac +| DELETE "rewrite" "*" orient uconstr by_arg_tac +| DELETE "setoid_rewrite" orient glob_constr_with_bindings +| DELETE "setoid_rewrite" orient glob_constr_with_bindings "in" hyp +| DELETE "setoid_rewrite" orient glob_constr_with_bindings "at" occurrences +| REPLACE "setoid_rewrite" orient glob_constr_with_bindings "at" occurrences "in" hyp +| WITH "setoid_rewrite" orient glob_constr_with_bindings OPT ( "at" occurrences ) OPT ( "in" hyp ) +| REPLACE "stepl" constr "by" tactic +| WITH "stepl" constr OPT ( "by" tactic ) +| DELETE "stepl" constr +| REPLACE "stepr" constr "by" tactic +| WITH "stepr" constr OPT ( "by" tactic ) +| DELETE "stepr" constr +| DELETE "unify" constr constr +| REPLACE "unify" constr constr "with" preident +| WITH "unify" constr constr OPT ( "with" preident ) +| DELETE "cutrewrite" orient constr +| REPLACE "cutrewrite" orient constr "in" hyp +| WITH "cutrewrite" orient constr OPT ( "in" hyp ) +| DELETE "destauto" +| REPLACE "destauto" "in" hyp +| WITH "destauto" OPT ( "in" hyp ) +| REPLACE "autounfold_one" hintbases "in" hyp +| WITH "autounfold_one" hintbases OPT ( "in" hyp ) +| DELETE "autounfold_one" hintbases +| REPLACE "rewrite_db" preident "in" hyp +| WITH "rewrite_db" preident OPT ( "in" hyp ) +| DELETE "rewrite_db" preident +| DELETE "setoid_symmetry" +| REPLACE "setoid_symmetry" "in" hyp +| WITH "setoid_symmetry" OPT ( "in" hyp ) +| REPLACE "rewrite_strat" rewstrategy "in" hyp +| WITH "rewrite_strat" rewstrategy OPT ( "in" hyp ) +| DELETE "rewrite_strat" rewstrategy +| REPLACE "protect_fv" string "in" ident +| WITH "protect_fv" string OPT ( "in" ident ) +| DELETE "protect_fv" string +| DELETE "symmetry" +| REPLACE "symmetry" "in" in_clause +| WITH "symmetry" OPT ( "in" in_clause ) +| DELETE "split" +| REPLACE "split" "with" bindings +| WITH "split" OPT ( "with" bindings ) +| DELETE "esplit" +| REPLACE "esplit" "with" bindings +| WITH "esplit" OPT ( "with" bindings ) +| DELETE "specialize" constr_with_bindings +| REPLACE "specialize" constr_with_bindings "as" simple_intropattern +| WITH "specialize" constr_with_bindings OPT ( "as" simple_intropattern ) +| DELETE "exists" +| REPLACE "exists" LIST1 bindings SEP "," +| WITH "exists" OPT ( LIST1 bindings SEP "," ) +| DELETE "eexists" +| REPLACE "eexists" LIST1 bindings SEP "," +| WITH "eexists" OPT ( LIST1 bindings SEP "," ) +| DELETE "left" +| REPLACE "left" "with" bindings +| WITH "left" OPT ( "with" bindings ) +| DELETE "eleft" +| REPLACE "eleft" "with" bindings +| WITH "eleft" OPT ( "with" bindings ) +| DELETE "right" +| REPLACE "right" "with" bindings +| WITH "right" OPT ( "with" bindings ) +| DELETE "eright" +| REPLACE "eright" "with" bindings +| WITH "eright" OPT ( "with" bindings ) +| DELETE "finish_timing" OPT string +| REPLACE "finish_timing" "(" string ")" OPT string +| WITH "finish_timing" OPT ( "(" string ")" ) OPT string +| REPLACE "hresolve_core" "(" ident ":=" constr ")" "at" int_or_var "in" constr +| WITH "hresolve_core" "(" ident ":=" constr ")" OPT ( "at" int_or_var ) "in" constr +| DELETE "hresolve_core" "(" ident ":=" constr ")" "in" constr +| EDIT "psatz_R" ADD_OPT int_or_var tactic +| EDIT "psatz_Q" ADD_OPT int_or_var tactic +| EDIT "psatz_Z" ADD_OPT int_or_var tactic +| REPLACE "subst" LIST1 var +| WITH "subst" OPT ( LIST1 var ) +| DELETE "subst" +| DELETE "congruence" +| DELETE "congruence" int +| DELETE "congruence" "with" LIST1 constr +| REPLACE "congruence" int "with" LIST1 constr +| WITH "congruence" OPT int OPT ( "with" LIST1 constr ) + ] (* todo: don't use DELETENT for this *) @@ -666,6 +872,109 @@ command: [ | WITH "Function" function_rec_definition_loc LIST0 ( "with" function_rec_definition_loc ) (* funind plugin *) | REPLACE "Functional" "Scheme" LIST1 fun_scheme_arg SEP "with" (* funind plugin *) | WITH "Functional" "Scheme" fun_scheme_arg LIST0 ( "with" fun_scheme_arg ) (* funind plugin *) +| DELETE "Cd" +| REPLACE "Cd" ne_string +| WITH "Cd" OPT ne_string +| DELETE "Back" +| REPLACE "Back" natural +| WITH "Back" OPT natural +| REPLACE "Test" option_table "for" LIST1 option_ref_value +| WITH "Test" option_table OPT ( "for" LIST1 option_ref_value ) +| DELETE "Test" option_table +| REPLACE "Load" [ "Verbose" | ] [ ne_string | IDENT ] +| WITH "Load" OPT "Verbose" [ ne_string | IDENT ] +| DELETE "Unset" option_table +| DELETE "Set" option_table option_setting +| REPLACE "Add" IDENT IDENT LIST1 option_ref_value +| WITH "Add" IDENT OPT IDENT LIST1 option_ref_value +| DELETE "Add" IDENT LIST1 option_ref_value +| DELETE "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "as" ident +| DELETE "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "as" ident +| DELETE "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident +| DELETE "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident +| DELETE "Add" "Parametric" "Relation" binders ":" constr constr "symmetry" "proved" "by" constr "as" ident +| DELETE "Add" "Parametric" "Relation" binders ":" constr constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident +| DELETE "Add" "Parametric" "Relation" binders ":" constr constr "transitivity" "proved" "by" constr "as" ident +| DELETE "Add" "Parametric" "Relation" binders ":" constr constr "as" ident +| "Add" "Parametric" "Relation" binders ":" constr constr OPT ( "reflexivity" "proved" "by" constr ) OPT ( "symmetry" "proved" "by" constr ) OPT ("transitivity" "proved" "by" constr ) "as" ident +| DELETE "Add" "Relation" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "as" ident +| DELETE "Add" "Relation" constr constr "reflexivity" "proved" "by" constr "as" ident +| DELETE "Add" "Relation" constr constr "as" ident +| DELETE "Add" "Relation" constr constr "symmetry" "proved" "by" constr "as" ident +| DELETE "Add" "Relation" constr constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident +| DELETE "Add" "Relation" constr constr "reflexivity" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident +| DELETE "Add" "Relation" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident +| DELETE "Add" "Relation" constr constr "transitivity" "proved" "by" constr "as" ident +| "Add" "Relation" constr constr OPT ( "reflexivity" "proved" "by" constr ) OPT ( "symmetry" "proved" "by" constr ) OPT ( "transitivity" "proved" "by" constr ) "as" ident +| REPLACE "Admit" "Obligations" "of" ident +| WITH "Admit" "Obligations" OPT ( "of" ident ) +| DELETE "Admit" "Obligations" +| REPLACE "Create" "HintDb" IDENT; [ "discriminated" | ] +| WITH "Create" "HintDb" IDENT; OPT "discriminated" +| DELETE "Debug" "On" +| REPLACE "Debug" "Off" +| WITH "Debug" [ "On" | "Off" ] +| EDIT "Defined" ADD_OPT identref +| REPLACE "Derive" "Inversion" ident "with" constr "Sort" sort_family +| WITH "Derive" "Inversion" ident "with" constr OPT ( "Sort" sort_family ) +| DELETE "Derive" "Inversion" ident "with" constr +| REPLACE "Derive" "Inversion_clear" ident "with" constr "Sort" sort_family +| WITH "Derive" "Inversion_clear" ident "with" constr OPT ( "Sort" sort_family ) +| DELETE "Derive" "Inversion_clear" ident "with" constr +| EDIT "Focus" ADD_OPT natural +| DELETE "Hint" "Rewrite" orient LIST1 constr ":" LIST0 preident +| REPLACE "Hint" "Rewrite" orient LIST1 constr "using" tactic ":" LIST0 preident +| WITH "Hint" "Rewrite" orient LIST1 constr OPT ( "using" tactic ) OPT ( ":" LIST0 preident ) +| DELETE "Hint" "Rewrite" orient LIST1 constr +| DELETE "Hint" "Rewrite" orient LIST1 constr "using" tactic +| REPLACE "Next" "Obligation" "of" ident withtac +| WITH "Next" "Obligation" OPT ( "of" ident ) withtac +| DELETE "Next" "Obligation" withtac +| REPLACE "Obligation" int "of" ident ":" lglob withtac +| WITH "Obligation" int OPT ( "of" ident ) OPT ( ":" lglob withtac ) +| DELETE "Obligation" int "of" ident withtac +| DELETE "Obligation" int ":" lglob withtac +| DELETE "Obligation" int withtac +| REPLACE "Obligations" "of" ident +| WITH "Obligations" OPT ( "of" ident ) +| DELETE "Obligations" +| REPLACE "Preterm" "of" ident +| WITH "Preterm" OPT ( "of" ident ) +| DELETE "Preterm" +| EDIT "Remove" ADD_OPT IDENT IDENT LIST1 option_ref_value +| DELETE "Restore" "State" IDENT +| DELETE "Restore" "State" ne_string +| "Restore" "State" [ IDENT | ne_string ] +| DELETE "Show" +| DELETE "Show" natural +| DELETE "Show" ident +| "Show" OPT [ ident | natural ] +| DELETE "Show" "Ltac" "Profile" +| REPLACE "Show" "Ltac" "Profile" "CutOff" int +| WITH "Show" "Ltac" "Profile" OPT [ "CutOff" int | string ] +| DELETE "Show" "Ltac" "Profile" string +| DELETE "Show" "Proof" (* combined with Show Proof Diffs in vernac_toplevel *) +| REPLACE "Solve" "All" "Obligations" "with" tactic +| WITH "Solve" "All" "Obligations" OPT ( "with" tactic ) +| DELETE "Solve" "All" "Obligations" +| REPLACE "Solve" "Obligation" int "of" ident "with" tactic +| WITH "Solve" "Obligation" int OPT ( "of" ident ) "with" tactic +| DELETE "Solve" "Obligations" +| DELETE "Solve" "Obligation" int "with" tactic +| REPLACE "Solve" "Obligations" "of" ident "with" tactic +| WITH "Solve" "Obligations" OPT ( OPT ( "of" ident ) "with" tactic ) +| DELETE "Solve" "Obligations" "with" tactic +| DELETE "Undo" +| DELETE "Undo" natural +| REPLACE "Undo" "To" natural +| WITH "Undo" OPT ( OPT "To" natural ) +| DELETE "Write" "State" IDENT +| REPLACE "Write" "State" ne_string +| WITH "Write" "State" [ IDENT | ne_string ] +| DELETE "Abort" +| DELETE "Abort" "All" +| REPLACE "Abort" identref +| WITH "Abort" OPT [ "All" | identref ] ] @@ -737,12 +1046,20 @@ assumption_token: [ | WITH [ "Variable" | "Variables" ] ] -legacy_attrs: [ -| OPT [ "Local" | "Global" ] OPT [ "Polymorphic" | "Monomorphic" ] OPT "Program" OPT [ "Cumulative" | "NonCumulative" ] OPT "Private" +all_attrs: [ +| LIST0 ( "#[" LIST0 attribute SEP "," "]" ) LIST0 legacy_attr ] -all_attrs: [ -| LIST0 ( "#[" LIST0 attribute SEP "," "]" ) OPT legacy_attrs +legacy_attr: [ +| REPLACE "Local" +| WITH [ "Local" | "Global" ] +| DELETE "Global" +| REPLACE "Polymorphic" +| WITH [ "Polymorphic" | "Monomorphic" ] +| DELETE "Monomorphic" +| REPLACE "Cumulative" +| WITH [ "Cumulative" | "NonCumulative" ] +| DELETE "NonCumulative" ] vernacular: [ @@ -770,6 +1087,7 @@ inductive_definition: [ | WITH opt_coercion ident_decl binders OPT [ "|" binders ] OPT [ ":" type ] opt_constructors_or_fields decl_notations ] +(* note that constructor -> identref constructor_type *) constructor_list_or_record_decl: [ | DELETE "|" LIST1 constructor SEP "|" | REPLACE identref constructor_type "|" LIST1 constructor SEP "|" @@ -786,6 +1104,222 @@ record_binder: [ | DELETE name ] +at_level_opt: [ +| OPTINREF +] + +query_command: [ +| REPLACE "Eval" red_expr "in" lconstr "." +| WITH "Eval" red_expr "in" lconstr +| REPLACE "Compute" lconstr "." +| WITH "Compute" lconstr +| REPLACE "Check" lconstr "." +| WITH "Check" lconstr +| REPLACE "About" smart_global OPT univ_name_list "." +| WITH "About" smart_global OPT univ_name_list +| REPLACE "SearchHead" constr_pattern in_or_out_modules "." +| WITH "SearchHead" constr_pattern in_or_out_modules +| REPLACE "SearchPattern" constr_pattern in_or_out_modules "." +| WITH "SearchPattern" constr_pattern in_or_out_modules +| REPLACE "SearchRewrite" constr_pattern in_or_out_modules "." +| WITH "SearchRewrite" constr_pattern in_or_out_modules +| REPLACE "Search" searchabout_query searchabout_queries "." +| WITH "Search" searchabout_query searchabout_queries +] + +vernac_toplevel: [ +(* note these commands can't be referenced by vernac_control commands *) +| REPLACE "Drop" "." +| WITH "Drop" +| REPLACE "Quit" "." +| WITH "Quit" +| REPLACE "BackTo" natural "." +| WITH "BackTo" natural +| REPLACE "Show" "Goal" natural "at" natural "." +| WITH "Show" "Goal" natural "at" natural +| REPLACE "Show" "Proof" "Diffs" OPT "removed" "." +| WITH "Show" "Proof" OPT ( "Diffs" OPT "removed" ) +| DELETE vernac_control +] + +positive_search_mark: [ +| OPTINREF +] + +in_or_out_modules: [ +| OPTINREF +] + +searchabout_queries: [ +| OPTINREF +] + +vernac_control: [ +(* replacing vernac_control with command is cheating a little; + they can't refer to the vernac_toplevel commands. + cover this the descriptions of these commands *) +| REPLACE "Time" vernac_control +| WITH "Time" command +| REPLACE "Redirect" ne_string vernac_control +| WITH "Redirect" ne_string command +| REPLACE "Timeout" natural vernac_control +| WITH "Timeout" natural command +| REPLACE "Fail" vernac_control +| WITH "Fail" command +| DELETE decorated_vernac +] + +option_setting: [ +| OPTINREF +] + +orient: [ +| OPTINREF +] + +in_hyp_as: [ +| OPTINREF +] + +as_name: [ +| OPTINREF +] + +hloc: [ +| OPTINREF +] + +as_or_and_ipat: [ +| OPTINREF +] + +hintbases: [ +| OPTINREF +] + +as_ipat: [ +| OPTINREF +] + +auto_using: [ +| OPTINREF +] + +with_bindings: [ +| OPTINREF +] + +eqn_ipat: [ +| OPTINREF +] + +withtac: [ +| OPTINREF +] + +of_module_type: [ +| (* empty *) +| OPTINREF +] + + +clause_dft_all: [ +| OPTINREF +] + +opt_clause: [ +| OPTINREF +] + +with_names: [ +| OPTINREF +] + +in_hyp_list: [ +| OPTINREF +] + +struct_annot: [ +| OPTINREF +] + +firstorder_using: [ +| OPTINREF +] + +fun_ind_using: [ +| OPTINREF +] + +by_arg_tac: [ +| OPTINREF +] + +by_tactic: [ +| OPTINREF +] + +rewriter: [ +| REPLACE [ "?" | LEFTQMARK ] constr_with_bindings_arg +| WITH "?" constr_with_bindings_arg +] + +intropattern_or_list_or: [ +(* todo: where does intropattern_or_list_or come from?? *) +| REPLACE intropattern_or_list_or "|" intropatterns +| WITH LIST0 intropattern LIST0 ( "|" intropatterns ) +| DELETE intropatterns +] + +record_declaration: [ +| DELETE fields_def +| LIST0 field_def +] + +fields_def: [ | DELETENT ] + +hint_info: [ +| OPTINREF +] + +debug: [ +| OPTINREF +] + +eauto_search_strategy: [ +| OPTINREF +] + + +constr_body: [ +| DELETE ":=" lconstr +| REPLACE ":" lconstr ":=" lconstr +| WITH OPT ( ":" lconstr ) ":=" lconstr +] + +opt_hintbases: [ +| OPTINREF +] + +opthints: [ +| OPTINREF +] + +scheme: [ +| DELETE scheme_kind +| REPLACE identref ":=" scheme_kind +| WITH OPT ( identref ":=" ) scheme_kind +] + +instance_name: [ +| OPTINREF +] + +simple_reserv: [ +| REPLACE LIST1 identref ":" lconstr +| WITH LIST1 identref ":" type +] + in_clause: [ | DELETE in_clause' | REPLACE LIST0 hypident_occ SEP "," "|-" concl_occ @@ -811,9 +1345,14 @@ decl_notations: [ | OPTINREF ] +module_expr: [ +| REPLACE module_expr_atom +| WITH LIST1 module_expr_atom +| DELETE module_expr module_expr_atom +] + SPLICE: [ | noedit_mode -| command_entry | bigint | match_list | match_context_list @@ -842,7 +1381,6 @@ SPLICE: [ | ne_lstring | ne_string | lstring -| basequalid | fullyqualid | global | reference @@ -918,7 +1456,6 @@ SPLICE: [ | binders_fixannot | as_return_type | case_type -| fields_def | universe_increment | type_cstr | record_pattern @@ -945,8 +1482,42 @@ SPLICE: [ | record_fields | constructor_type | record_binder +| at_level_opt +| option_ref_value +| positive_search_mark +| in_or_out_modules +| register_prim_token +| option_setting +| orient +| with_bindings +| by_arg_tac +| by_tactic +| quantified_hypothesis +| nat_or_var +| in_hyp_list +| rename +| export_token +| reserv_tuple +| inst | opt_coercion | opt_constructors_or_fields +| is_module_type +| is_module_expr +| module_expr +| mlname +| withtac +| debug +| eauto_search_strategy +| constr_body +| reference_or_constr +| opt_hintbases +| hints_path_atom +| opthints +| scheme +| fresh_id +| ltac_def_kind +| intropatterns +| instance_name ] (* end SPLICE *) RENAME: [ @@ -963,7 +1534,6 @@ RENAME: [ | tactic_expr0 ltac_expr0 (* | nonsimple_intropattern intropattern (* ltac2 *) *) -| intropatterns intropattern_list_opt | operconstr200 term (* historical name *) | operconstr100 term100 @@ -982,14 +1552,12 @@ RENAME: [ | match_hyps match_hyp | BULLET bullet -| nat_or_var num_or_var | fix_decl fix_body | cofix_decl cofix_body | constr one_term | appl_arg arg | rec_definition fix_definition | corec_definition cofix_definition -| inst evar_binding | univ_instance univ_annot | simple_assum_coe assumpt | of_type_with_opt_coercion of_type @@ -1001,5 +1569,90 @@ RENAME: [ | smart_global smart_qualid ] +(* todo: doesn't work if up above... maybe because 'clause' doesn't exist? *) +clause_dft_concl: [ +| OPTINREF +] + +(* add in ltac and Tactic Notation tactics that appear in the doc: *) +ltac_defined_tactics: [ +| "classical_left" +| "classical_right" +| "contradict" ident +| "discrR" +| "easy" +| "exfalso" +| "inversion_sigma" +| "lia" +| "lra" +| "nia" +| "nra" +| "split_Rabs" +| "split_Rmult" +| "tauto" +| "zify" +] + +(* todo: need careful review; assume that "[" ... "]" are literals *) +tactic_notation_tactics: [ +| "assert_fails" ltac_expr3 +| "assert_succeeds" ltac_expr3 +| "field" OPT ( "[" LIST1 term "]" ) +| "field_simplify" OPT ( "[" LIST1 term "]" ) LIST1 term OPT ( "in" ident ) +| "field_simplify_eq" OPT ( "[" LIST1 term "]" ) OPT ( "in" ident ) +| "intuition" OPT ltac_expr +| "nsatz" OPT ( "with" "radicalmax" ":=" term "strategy" ":=" term "parameters" ":=" term "variables" ":=" term ) +| "psatz" term OPT int_or_var +| "ring" OPT ( "[" LIST1 term "]" ) +| "ring_simplify" OPT ( "[" LIST1 term "]" ) LIST1 term OPT ( "in" ident ) (* todo: ident was "hyp", worth keeping? *) +] + +tacticals: [ +] + +simple_tactic: [ +| ltac_defined_tactics +| tactic_notation_tactics +] + +(* move all commands under "command" *) + +DELETE: [ +| vernac +] + +tactic_mode: [ +(* todo: make sure to document this production! *) +(* deleting to allow splicing query_command into command *) +| DELETE OPT toplevel_selector query_command +] +vernac_aux: [ +| DELETE gallina "." +| DELETE gallina_ext "." +| DELETE syntax "." +| DELETE command_entry +] + +command: [ +| gallina +| gallina_ext +| syntax +| query_command +| vernac_control +| vernac_toplevel +| command_entry +] + +SPLICE: [ +| gallina +| gallina_ext +| syntax +| query_command +| vernac_control +| vernac_toplevel +| command_entry +| ltac_defined_tactics +| tactic_notation_tactics +] (* todo: ssrreflect*.rst ref to fix_body is incorrect *) diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml index 366b70a1f7..eea1d5081d 100644 --- a/doc/tools/docgram/doc_grammar.ml +++ b/doc/tools/docgram/doc_grammar.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -32,6 +32,7 @@ type args = { fullGrammar : bool; check_tacs : bool; check_cmds : bool; + no_update: bool; show_warn : bool; verbose : bool; verify : bool; @@ -43,12 +44,13 @@ let default_args = { fullGrammar = false; check_tacs = false; check_cmds = false; + no_update = false; show_warn = true; verbose = false; verify = false; } -let start_symbols = ["vernac_toplevel"] +let start_symbols = ["vernacular"] let tokens = [ "bullet"; "string"; "unicode_id_part"; "unicode_letter" ] (* translated symbols *) @@ -1165,7 +1167,7 @@ let apply_edit_file g edits = in aux tl prods' add_nt | (Snterm "OPTINREF" :: _) :: tl -> - if not (List.mem [] prods) then + if not (has_match [] prods) then error "OPTINREF but no empty production for %s\n" nt; global_repl g [(Snterm nt)] [(Sopt (Snterm nt))]; aux tl (remove_prod [] prods nt) add_nt @@ -1574,7 +1576,7 @@ let reorder_grammar eg reordered_rules file = g_reorder eg !og.map !og.order -let finish_with_file old_file verify = +let finish_with_file old_file args = let files_eq f1 f2 = let chunksize = 8192 in (try @@ -1605,21 +1607,24 @@ let finish_with_file old_file verify = with Sys_error _ -> false) in - let temp_file = (old_file ^ "_temp") in + let temp_file = (old_file ^ ".new") in if !exit_code <> 0 then Sys.remove temp_file - else if verify then begin + else if args.verify then begin if not (files_eq old_file temp_file) then error "%s is not current\n" old_file; Sys.remove temp_file - end else + end else if not args.no_update then Sys.rename temp_file old_file let open_temp_bin file = - open_out_bin (sprintf "%s_temp" file) + open_out_bin (sprintf "%s.new" file) + +let match_cmd_regex = Str.regexp "[a-zA-Z0-9_ ]+" let find_longest_match prods str = - (* todo: require a minimum length? *) + let get_pfx str = String.trim (if Str.string_match match_cmd_regex str 0 then Str.matched_string str else "") in + let prods = StringSet.fold (fun a lst -> a :: lst) prods [] in (* todo: wasteful! *) let common_prefix_len s1 s2 = let limit = min (String.length s1) (String.length s2) in let rec aux off = @@ -1631,13 +1636,16 @@ let find_longest_match prods str = in let slen = String.length str in + let str_pfx = get_pfx 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 pstr = String.trim prod in (* todo: should be pretrimmed *) let clen = common_prefix_len str pstr in - if clen = slen && slen = String.length pstr then + if str_pfx = "" || str_pfx <> get_pfx pstr then + longest best multi best_len tl (* prefixes don't match *) + else 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 *) @@ -1651,6 +1659,7 @@ let find_longest_match prods str = type seen = { nts: (string * int) NTMap.t; tacs: (string * int) NTMap.t; + tacvs: (string * int) NTMap.t; cmds: (string * int) NTMap.t; cmdvs: (string * int) NTMap.t; } @@ -1659,8 +1668,9 @@ 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 dir_regex = Str.regexp "^\\([ \t]*\\)\\.\\.[ \t]*\\([a-zA-Z0-9:]* *\\)\\(.*\\)" in + let contin_regex = Str.regexp "^\\([ \t]*\\)\\(.*\\)" in + let ip_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 getline () = @@ -1692,7 +1702,7 @@ let process_rst g file args seen tac_prods cmd_prods = in let process_insertprodn line rhs = - if not (Str.string_match ig_args_regex rhs 0) then + if not (Str.string_match ip_args_regex rhs 0) then error "%s line %d: bad arguments '%s' for 'insertprodn'\n" file !linenum rhs else begin let start = Str.matched_group 1 rhs in @@ -1703,8 +1713,8 @@ let process_rst g file args seen tac_prods cmd_prods = error "%s line %d: '%s' is undefined in insertprodn\n" file !linenum start; if end_index = None then error "%s line %d: '%s' is undefined in insertprodn\n" file !linenum end_; - if start_index <> None && end_index <> None then - check_range_consistency g start end_; +(* if start_index <> None && end_index <> None then*) +(* check_range_consistency g start end_;*) match start_index, end_index with | Some start_index, Some end_index -> if start_index > end_index then @@ -1716,7 +1726,7 @@ let process_rst g file args seen tac_prods cmd_prods = error "%s line %d: expecting a blank line after 'insertprodn'\n" file !linenum else begin let line3 = getline() in - if not (Str.string_match dir_regex line3 0) || (Str.matched_group 2 line3) <> "prodn::" then + if not (Str.string_match dir_regex line3 0) || (String.trim (Str.matched_group 2 line3)) <> "prodn::" then error "%s line %d: expecting '.. prodn::' after 'insertprodn'\n" file !linenum else begin let indent = Str.matched_group 1 line3 in @@ -1736,38 +1746,82 @@ let process_rst g file args seen tac_prods cmd_prods = end | _ -> () end + in + +(* let skip_files = ["doc/sphinx/proof-engine/ltac.rst"; "doc/sphinx/proof-engine/ltac2.rst";*) +(* "doc/sphinx/proof-engine/ssreflect-proof-language.rst"]*) +(* in*) + let cmd_replace_files = [ + "doc/sphinx/language/gallina-specification-language.rst"; + "doc/sphinx/language/gallina-extensions.rst" + ] in + + let save_n_get_more direc pfx first_rhs seen_map prods = + let replace rhs prods = + if StringSet.is_empty prods || not (List.mem file cmd_replace_files) then + rhs (* no change *) + else + let mtch, multi, len = find_longest_match prods rhs in + if mtch = rhs then + rhs (* no change *) + else if mtch = "" then begin + warn "%s line %d: NO MATCH `%s`\n" file !linenum rhs; + rhs + end else if multi then begin + warn "%s line %d: MULTIMATCH `%s`\n" file !linenum rhs; + rhs + end else + mtch (* update cmd/tacn *) + in + let map = ref seen_map in + if NTMap.mem first_rhs !map then + warn "%s line %d: Repeated %s: '%s'\n" file !linenum direc first_rhs; +(* if not (StringSet.mem rhs seen_map) then*) +(* warn "%s line %d: Unknown tactic: '%s'\n" file !linenum rhs;*) + + fprintf new_rst "%s%s\n" pfx (replace first_rhs prods); + + map := NTMap.add first_rhs (file, !linenum) !map; + while + let nextline = getline() in + ignore (Str.string_match contin_regex nextline 0); + let indent = Str.matched_group 1 nextline in + let rhs = Str.matched_group 2 nextline in + let replaceable = rhs <> "" && rhs.[0] <> ':' in + let upd_rhs = if replaceable then (replace rhs prods) else rhs in + fprintf new_rst "%s%s\n" indent upd_rhs; + if replaceable then begin + map := NTMap.add rhs (file, !linenum) !map + end; + rhs <> "" + do + () + done; + !map + 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 + let dir = String.trim (Str.matched_group 2 line) in + let rhs = Str.matched_group 3 line in + let pfx = String.sub line 0 (Str.group_end 2) in match dir with | "prodn::" -> if rhs = "coq" then warn "%s line %d: Missing 'insertprodn' before 'prodn:: 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 + seen := { !seen with tacs = save_n_get_more "tacn" pfx rhs !seen.tacs tac_prods } + | "tacv::" when args.check_tacs -> + seen := { !seen with tacvs = save_n_get_more "tacv" pfx rhs !seen.tacvs StringSet.empty } | "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 + seen := { !seen with cmds = save_n_get_more "cmd" pfx rhs !seen.cmds cmd_prods } | "cmdv::" when args.check_cmds -> - seen := { !seen with cmdvs = (NTMap.add rhs (file, !linenum) !seen.cmdvs)}; - fprintf new_rst "%s\n" line + seen := { !seen with cmdvs = save_n_get_more "cmdv" pfx rhs !seen.cmdvs StringSet.empty } | "insertprodn" -> process_insertprodn line rhs | _ -> fprintf new_rst "%s\n" line @@ -1777,7 +1831,7 @@ let process_rst g file args seen tac_prods cmd_prods = with End_of_file -> (); close_in old_rst; close_out new_rst; - finish_with_file file args.verify + finish_with_file file args let report_omitted_prods entries seen label split = let maybe_warn first last n = @@ -1825,7 +1879,7 @@ let process_grammar args = "DOC_GRAMMAR"; print_in_order out g `MLG !g.order StringSet.empty; close_out out; - finish_with_file (dir "fullGrammar") args.verify; + finish_with_file (dir "fullGrammar") args; if args.verbose then print_special_tokens g; @@ -1835,19 +1889,7 @@ let process_grammar args = 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; + let prodn_gram = ref { map = !g.map; order = !g.order } in (* todo: should just be 'g', right? *) if !exit_code = 0 && not args.verify then begin let out = open_temp_bin (dir "editedGrammar") in @@ -1856,7 +1898,7 @@ let process_grammar args = "DOC_GRAMMAR"; print_in_order out g `MLG !g.order StringSet.empty; close_out out; - finish_with_file (dir "editedGrammar") args.verify; + finish_with_file (dir "editedGrammar") args; report_bad_nts g "editedGrammar" end; @@ -1864,18 +1906,20 @@ let process_grammar args = 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" ^ + ("(* Defines the order to apply to editedGrammar to get the final grammar for the doc.\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; + finish_with_file (dir "orderedGrammar") args; check_singletons g (* print_dominated g*) end; + let seen = ref { nts=NTMap.empty; tacs=NTMap.empty; tacvs=NTMap.empty; cmds=NTMap.empty; cmdvs=NTMap.empty } in + let args = { args with no_update = false } in (* always update rsts in place for now *) if !exit_code = 0 then begin let plist nt = let list = (List.map (fun t -> String.trim (prod_to_prodn t)) @@ -1883,11 +1927,12 @@ let process_grammar args = 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; cmdvs=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" ""; let out = open_out (dir "updated_rsts") in close_out out; + end; + (* if args.check_tacs then report_omitted_prods tac_list !seen.tacs "Tactic" "\n "; @@ -1895,41 +1940,48 @@ let process_grammar args = report_omitted_prods cmd_list !seen.cmds "Command" "\n "; *) - let rstCmds = StringSet.of_list (List.map (fun b -> let c, _ = b in c) (NTMap.bindings !seen.cmds)) in - let rstCmdvs = StringSet.of_list (List.map (fun b -> let c, _ = b in c) (NTMap.bindings !seen.cmdvs)) in - let command_nts = ["command"; "gallina"; "gallina_ext"; "query_command"; "syntax"] in + if !exit_code = 0 then begin + (* generate report on cmds or tacs *) + let cmdReport outfile cmdStr cmd_nts cmds cmdvs = + let rstCmds = StringSet.of_list (List.map (fun b -> let c, _ = b in c) (NTMap.bindings cmds)) in + let rstCmdvs = StringSet.of_list (List.map (fun b -> let c, _ = b in c) (NTMap.bindings cmdvs)) in + let gramCmds = List.fold_left (fun set nt -> + StringSet.union set (StringSet.of_list (List.map (fun p -> String.trim (prod_to_prodn p)) (NTMap.find nt !prodn_gram.map))) + ) StringSet.empty cmd_nts in + let allCmds = StringSet.union rstCmdvs (StringSet.union rstCmds gramCmds) in + let out = open_temp_bin (dir outfile) in + StringSet.iter (fun c -> + let rsts = StringSet.mem c rstCmds in + let gram = StringSet.mem c gramCmds in + let pfx = match rsts, gram with + | true, false -> "+" + | false, true -> "-" + | false, false -> "?" + | _, _ -> " " + in + let var = if StringSet.mem c rstCmdvs then "v" else " " in + fprintf out "%s%s %s\n" pfx var c) + allCmds; + close_out out; + finish_with_file (dir outfile) args; + Printf.printf "# %s in rsts, gram, total = %d %d %d\n" cmdStr (StringSet.cardinal gramCmds) + (StringSet.cardinal rstCmds) (StringSet.cardinal allCmds); + in + + let cmd_nts = ["command"] in (* TODO: need to handle tactic_mode (overlaps with query_command) and subprf *) - let gramCmds = List.fold_left (fun set nt -> - StringSet.union set (StringSet.of_list (List.map (fun p -> String.trim (prod_to_prodn p)) (NTMap.find nt !prodn_gram.map))) - ) StringSet.empty command_nts in - - let allCmds = StringSet.union rstCmdvs (StringSet.union rstCmds gramCmds) in - let out = open_out_bin (dir "prodnCommands") in - StringSet.iter (fun c -> - let rsts = StringSet.mem c rstCmds in - let gram = StringSet.mem c gramCmds in - let pfx = match rsts, gram with - | true, false -> "+" - | false, true -> "-" - | false, false -> "?" - | _, _ -> " " - in - let var = if StringSet.mem c rstCmdvs then "v" else " " in - fprintf out "%s%s %s\n" pfx var c) - allCmds; - close_out out; - Printf.printf "# cmds in rsts, gram, total = %d %d %d\n" (StringSet.cardinal gramCmds) - (StringSet.cardinal rstCmds) (StringSet.cardinal allCmds); + cmdReport "prodnCommands" "cmds" cmd_nts !seen.cmds !seen.cmdvs; + + let tac_nts = ["simple_tactic"] in + cmdReport "prodnTactics" "tacs" tac_nts !seen.tacs !seen.tacvs end; - (* generate output for prodn: simple_tactic, command, also for Ltac?? *) + (* generate prodnGrammar for reference *) 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 + finish_with_file (dir "prodnGrammar") args end end @@ -1941,6 +1993,7 @@ let parse_args () = | "-check-cmds" -> { args with check_cmds = true } | "-check-tacs" -> { args with check_tacs = true } | "-no-warn" -> show_warn := false; { args with show_warn = true } + | "-no-update" -> { args with no_update = true } | "-short" -> { args with fullGrammar = true } | "-verbose" -> { args with verbose = true } | "-verify" -> { args with verify = true } diff --git a/doc/tools/docgram/dune b/doc/tools/docgram/dune new file mode 100644 index 0000000000..fba4856241 --- /dev/null +++ b/doc/tools/docgram/dune @@ -0,0 +1,51 @@ +(executable + (name doc_grammar) + (libraries coq.clib coqpp)) + +(env (_ (binaries doc_grammar.exe))) + +(rule + (alias check-gram) + (deps + (:input + ; Main grammar + (glob_files %{project_root}/parsing/*.mlg) + (glob_files %{project_root}/toplevel/*.mlg) + (glob_files %{project_root}/vernac/*.mlg) + ; All plugins except SSReflect and Ltac2 for now (mimicking what is done in Makefile.doc) + (glob_files %{project_root}/plugins/btauto/*.mlg) + (glob_files %{project_root}/plugins/cc/*.mlg) + (glob_files %{project_root}/plugins/derive/*.mlg) + (glob_files %{project_root}/plugins/extraction/*.mlg) + (glob_files %{project_root}/plugins/firstorder/*.mlg) + (glob_files %{project_root}/plugins/funind/*.mlg) + (glob_files %{project_root}/plugins/ltac/*.mlg) + (glob_files %{project_root}/plugins/micromega/*.mlg) + (glob_files %{project_root}/plugins/nsatz/*.mlg) + (glob_files %{project_root}/plugins/omega/*.mlg) + (glob_files %{project_root}/plugins/rtauto/*.mlg) + (glob_files %{project_root}/plugins/setoid_ring/*.mlg) + (glob_files %{project_root}/plugins/syntax/*.mlg) + ; Sphinx files + (glob_files %{project_root}/doc/sphinx/language/*.rst) + (glob_files %{project_root}/doc/sphinx/proof-engine/*.rst) + (glob_files %{project_root}/doc/sphinx/user-extensions/*.rst) + (glob_files %{project_root}/doc/sphinx/practical-tools/*.rst) + (glob_files %{project_root}/doc/sphinx/addendum/*.rst) + (glob_files %{project_root}/doc/sphinx/language/core/*.rst) + (glob_files %{project_root}/doc/sphinx/language/extensions/*.rst) + (glob_files %{project_root}/doc/sphinx/proofs/writing-proofs/*.rst) + (glob_files %{project_root}/doc/sphinx/proofs/automatic-tactics/*.rst) + (glob_files %{project_root}/doc/sphinx/proofs/creating-tactics/*.rst) + (glob_files %{project_root}/doc/sphinx/using/libraries/*.rst) + (glob_files %{project_root}/doc/sphinx/using/tools/*.rst)) + common.edit_mlg + orderedGrammar) + (action + (progn + (bash "for f in fullGrammar orderedGrammar; do cp ${f} ${f}.old; done") + (chdir %{project_root} (run doc_grammar -check-cmds %{input})) + (bash "for f in fullGrammar orderedGrammar; do cp ${f} ${f}.new; done") + (bash "for f in fullGrammar orderedGrammar; do cp ${f}.old ${f}; done") + (diff? fullGrammar fullGrammar.new) + (diff? orderedGrammar orderedGrammar.new)))) diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 6897437457..272d17bb35 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -386,11 +386,6 @@ fullyqualid: [ | ident ] -basequalid: [ -| ident fields -| ident -] - name: [ | "_" | ident @@ -401,6 +396,10 @@ reference: [ | ident ] +qualid: [ +| reference +] + by_notation: [ | ne_string OPT [ "%" IDENT ] ] @@ -410,10 +409,6 @@ smart_global: [ | by_notation ] -qualid: [ -| basequalid -] - ne_string: [ | STRING ] @@ -435,17 +430,21 @@ lstring: [ ] integer: [ -| NUMERAL -| "-" NUMERAL +| bigint ] natural: [ -| NUMERAL +| bignat | _natural ] bigint: [ | NUMERAL +| test_minus_nat "-" NUMERAL +] + +bignat: [ +| NUMERAL ] bar_cbrace: [ @@ -735,21 +734,22 @@ attribute_value: [ | ] -vernac: [ -| "Local" vernac_poly -| "Global" vernac_poly -| vernac_poly +legacy_attr: [ +| "Local" +| "Global" +| "Polymorphic" +| "Monomorphic" +| "Cumulative" +| "NonCumulative" +| "Private" +| "Program" ] -vernac_poly: [ -| "Polymorphic" vernac_aux -| "Monomorphic" vernac_aux -| vernac_aux +vernac: [ +| LIST0 legacy_attr vernac_aux ] vernac_aux: [ -| "Program" gallina "." -| "Program" gallina_ext "." | gallina "." | gallina_ext "." | command "." @@ -774,7 +774,7 @@ gallina: [ | 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" +| 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" @@ -903,16 +903,6 @@ finite_token: [ | "Class" ] -cumulativity_token: [ -| "Cumulative" -| "NonCumulative" -] - -private_token: [ -| "Private" -| -] - def_body: [ | binders ":=" reduce lconstr | binders ":" lconstr ":=" reduce lconstr @@ -1254,8 +1244,6 @@ query_command: [ | "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: [ @@ -2464,8 +2452,6 @@ as_or_and_ipat: [ eqn_ipat: [ | "eqn" ":" naming_intropattern -| "_eqn" ":" naming_intropattern -| "_eqn" | ] @@ -2530,7 +2516,7 @@ field_mods: [ numnotoption: [ | -| "(" "warning" "after" bigint ")" -| "(" "abstract" "after" bigint ")" +| "(" "warning" "after" bignat ")" +| "(" "abstract" "after" bignat ")" ] diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index f26a174722..0c9d7a853b 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -1,19 +1,9 @@ -(* Defines the order to apply to editedGrammar to get productionlistGrammar. +(* Defines the order to apply to editedGrammar to get the final grammar for the doc. 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 -vernac_toplevel: [ -| "Drop" "." -| "Quit" "." -| "BackTo" num "." -| "Show" "Goal" num "at" num "." -| "Show" "Proof" "Diffs" OPT "removed" "." -| vernac_control -] - tactic_mode: [ -| OPT toplevel_selector query_command | OPT toplevel_selector "{" | OPT toplevel_selector OPT ( "Info" num ) ltac_expr ltac_use_default | "par" ":" OPT ( "Info" num ) ltac_expr ltac_use_default @@ -24,14 +14,6 @@ ltac_use_default: [ | "..." ] -vernac_control: [ -| "Time" vernac_control -| "Redirect" string vernac_control -| "Timeout" num vernac_control -| "Fail" vernac_control -| LIST0 ( "#[" LIST0 attr SEP "," "]" ) vernac -] - term: [ | "forall" open_binders "," term | "fun" open_binders "=>" term @@ -96,11 +78,7 @@ term_projection: [ term_evar: [ | "?[" ident "]" | "?[" "?" ident "]" -| "?" ident OPT ( "@{" LIST1 evar_binding SEP ";" "}" ) -] - -evar_binding: [ -| ident ":=" term +| "?" ident OPT ( "@{" LIST1 ( ident ":=" term ) SEP ";" "}" ) ] dangling_pattern_extension_rule: [ @@ -167,12 +145,28 @@ subsequent_letter: [ | [ first_letter | digit | "'" | unicode_id_part ] ] +firstorder_rhs: [ +| OPT firstorder_using +| "with" LIST1 ident +| OPT firstorder_using "with" LIST1 ident +] + +where: [ +| "at" "top" +| "at" "bottom" +| "after" ident +| "before" ident +] + vernacular: [ | LIST0 ( OPT all_attrs [ command | ltac_expr ] "." ) ] +tacticals: [ +] + all_attrs: [ -| LIST0 ( "#[" LIST0 attr SEP "," "]" ) OPT legacy_attrs +| LIST0 ( "#[" LIST0 attr SEP "," "]" ) LIST0 legacy_attr ] attr: [ @@ -184,8 +178,12 @@ attr_value: [ | "(" LIST0 attr SEP "," ")" ] -legacy_attrs: [ -| OPT [ "Local" | "Global" ] OPT [ "Polymorphic" | "Monomorphic" ] OPT "Program" OPT [ "Cumulative" | "NonCumulative" ] OPT "Private" +legacy_attr: [ +| [ "Local" | "Global" ] +| [ "Polymorphic" | "Monomorphic" ] +| [ "Cumulative" | "NonCumulative" ] +| "Private" +| "Program" ] sort: [ @@ -278,13 +276,21 @@ binder: [ | name | "(" LIST1 name ":" type ")" | "(" name OPT ( ":" type ) ":=" term ")" +| implicit_binders +| generalizing_binder | "(" name ":" type "|" term ")" +| "'" pattern0 +] + +implicit_binders: [ | "{" LIST1 name OPT ( ":" type ) "}" | "[" LIST1 name OPT ( ":" type ) "]" +] + +generalizing_binder: [ | "`(" LIST1 typeclass_constraint SEP "," ")" | "`{" LIST1 typeclass_constraint SEP "," "}" | "`[" LIST1 typeclass_constraint SEP "," "]" -| "'" pattern0 ] typeclass_constraint: [ @@ -337,28 +343,10 @@ pattern0: [ | string ] -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 "." | tactic_mode "." -| syntax "." | subprf -| query_command ] subprf: [ @@ -367,30 +355,6 @@ subprf: [ | "}" ] -gallina: [ -| thm_token ident_decl LIST0 binder ":" type LIST0 [ "with" ident_decl LIST0 binder ":" type ] -| assumption_token OPT ( "Inline" OPT ( "(" num ")" ) ) [ LIST1 ( "(" assumpt ")" ) | assumpt ] -| [ "Definition" | "Example" ] ident_decl def_body -| "Let" ident def_body -| "Inductive" inductive_definition LIST0 ( "with" inductive_definition ) -| "CoInductive" inductive_definition LIST0 ( "with" inductive_definition ) -| "Variant" inductive_definition LIST0 ( "with" inductive_definition ) -| [ "Record" | "Structure" ] inductive_definition LIST0 ( "with" inductive_definition ) -| "Class" inductive_definition LIST0 ( "with" inductive_definition ) -| "Fixpoint" fix_definition LIST0 ( "with" fix_definition ) -| "Let" "Fixpoint" fix_definition LIST0 ( "with" fix_definition ) -| "CoFixpoint" cofix_definition LIST0 ( "with" cofix_definition ) -| "Let" "CoFixpoint" cofix_definition LIST0 ( "with" cofix_definition ) -| "Scheme" scheme LIST0 ( "with" scheme ) -| "Combined" "Scheme" ident "from" LIST1 ident SEP "," -| "Register" qualid "as" qualid -| "Register" "Inline" qualid -| "Primitive" ident OPT [ ":" term ] ":=" register_token -| "Universe" LIST1 ident -| "Universes" LIST1 ident -| "Constraint" LIST1 univ_constraint SEP "," -] - fix_definition: [ | ident_decl LIST0 binder OPT fixannot OPT ( ":" type ) OPT [ ":=" term ] OPT decl_notations ] @@ -404,12 +368,8 @@ decl_notation: [ ] register_token: [ -| register_prim_token | "#int63_type" | "#float64_type" -] - -register_prim_token: [ | "#int63_head0" | "#int63_tail0" | "#int63_add" @@ -493,15 +453,6 @@ delta_flag: [ | OPT "-" "[" LIST1 smart_qualid "]" ] -smart_qualid: [ -| qualid -| by_notation -] - -by_notation: [ -| string OPT [ "%" ident ] -] - strategy_flag: [ | LIST1 red_flags | delta_flag @@ -523,13 +474,8 @@ ref_or_pattern_occ: [ ] occs_nums: [ -| LIST1 num_or_var -| "-" num_or_var LIST0 int_or_var -] - -num_or_var: [ -| num -| ident +| LIST1 [ num | ident ] +| "-" [ num | ident ] LIST0 int_or_var ] int_or_var: [ @@ -554,17 +500,12 @@ finite_token: [ | "Class" ] -inductive_definition: [ -| OPT ">" ident_decl LIST0 binder OPT [ "|" LIST0 binder ] OPT [ ":" type ] OPT ( ":=" OPT constructors_or_record ) OPT decl_notations +variant_definition: [ +| ident_decl LIST0 binder OPT [ "|" LIST0 binder ] OPT [ ":" type ] ":=" OPT "|" LIST1 constructor SEP "|" OPT decl_notations ] -constructors_or_record: [ -| OPT "|" LIST1 constructor SEP "|" -| OPT ident "{" LIST1 record_field SEP ";" "}" -] - -constructor: [ -| ident LIST0 binder OPT of_type +record_definition: [ +| OPT ">" ident_decl LIST0 binder OPT [ ":" type ] OPT ident "{" LIST0 record_field SEP ";" "}" OPT decl_notations ] record_field: [ @@ -577,13 +518,21 @@ field_body: [ | LIST0 binder ":=" term ] -cofix_definition: [ -| ident_decl LIST0 binder OPT ( ":" type ) OPT [ ":=" term ] OPT decl_notations +inductive_definition: [ +| OPT ">" ident_decl LIST0 binder OPT [ "|" LIST0 binder ] OPT [ ":" type ] OPT ( ":=" OPT constructors_or_record ) OPT decl_notations +] + +constructors_or_record: [ +| OPT "|" LIST1 constructor SEP "|" +| OPT ident "{" LIST0 record_field SEP ";" "}" +] + +constructor: [ +| ident LIST0 binder OPT of_type ] -scheme: [ -| scheme_kind -| ident ":=" scheme_kind +cofix_definition: [ +| ident_decl LIST0 binder OPT ( ":" type ) OPT [ ":=" term ] OPT decl_notations ] scheme_kind: [ @@ -601,60 +550,12 @@ sort_family: [ | "Type" ] -gallina_ext: [ -| "Module" OPT export_token ident LIST0 module_binder of_module_type OPT is_module_expr -| "Module" "Type" ident LIST0 module_binder LIST0 ( "<:" module_type_inl ) OPT is_module_type -| "Declare" "Module" OPT export_token ident LIST0 module_binder ":" module_type_inl -| "Section" ident -| "Chapter" ident -| "End" ident -| "Collection" ident ":=" section_subset_expr -| "Require" OPT export_token LIST1 qualid -| "From" qualid "Require" OPT export_token LIST1 qualid -| "Import" LIST1 qualid -| "Export" LIST1 qualid -| "Include" module_type_inl LIST0 ( "<+" module_expr_inl ) -| "Include" "Type" module_type_inl LIST0 ( "<+" module_type_inl ) -| "Transparent" LIST1 smart_qualid -| "Opaque" LIST1 smart_qualid -| "Strategy" LIST1 [ strategy_level "[" LIST1 smart_qualid "]" ] -| "Canonical" OPT "Structure" qualid OPT [ OPT univ_decl def_body ] -| "Canonical" OPT "Structure" by_notation -| "Coercion" qualid OPT univ_decl def_body -| "Identity" "Coercion" ident ":" class ">->" class -| "Coercion" qualid ":" class ">->" class -| "Coercion" by_notation ":" class ">->" class -| "Context" LIST1 binder -| "Instance" instance_name ":" term hint_info [ ":=" "{" [ LIST1 field_def SEP ";" | ] "}" | ":=" term | ] -| "Existing" "Instance" qualid hint_info -| "Existing" "Instances" LIST1 qualid OPT [ "|" num ] -| "Existing" "Class" qualid -| "Arguments" smart_qualid LIST0 argument_spec_block LIST0 [ "," LIST0 more_implicits_block ] OPT [ ":" LIST1 arguments_modifier SEP "," ] -| "Implicit" "Type" reserv_list -| "Implicit" "Types" reserv_list -| "Generalizable" [ "All" "Variables" | "No" "Variables" | [ "Variable" | "Variables" ] LIST1 ident ] -| "Export" "Set" LIST1 ident option_setting -| "Export" "Unset" LIST1 ident -] - -option_setting: [ -| -| int -| string -] - hint_info: [ | "|" OPT num OPT one_term -| -] - -export_token: [ -| "Import" -| "Export" ] module_binder: [ -| "(" OPT export_token LIST1 ident ":" module_type_inl ")" +| "(" OPT [ "Import" | "Export" ] LIST1 ident ":" module_type_inl ")" ] module_type_inl: [ @@ -662,6 +563,11 @@ module_type_inl: [ | module_type OPT functor_app_annot ] +functor_app_annot: [ +| "[" "inline" "at" "level" num "]" +| "[" "no" "inline" "]" +] + module_type: [ | qualid | "(" module_type ")" @@ -674,9 +580,9 @@ with_declaration: [ | "Module" qualid ":=" qualid ] -functor_app_annot: [ -| "[" "inline" "at" "level" num "]" -| "[" "no" "inline" "]" +module_expr_atom: [ +| qualid +| "(" LIST1 module_expr_atom ")" ] of_module_type: [ @@ -684,27 +590,18 @@ of_module_type: [ | LIST0 ( "<:" module_type_inl ) ] -is_module_type: [ -| ":=" module_type_inl LIST0 ( "<+" module_type_inl ) +module_expr_inl: [ +| "!" LIST1 module_expr_atom +| LIST1 module_expr_atom OPT functor_app_annot ] -module_expr_atom: [ +smart_qualid: [ | qualid -| "(" module_expr ")" -] - -module_expr: [ -| module_expr_atom -| module_expr module_expr_atom -] - -is_module_expr: [ -| ":=" module_expr_inl LIST0 ( "<+" module_expr_inl ) +| by_notation ] -module_expr_inl: [ -| "!" module_expr -| module_expr OPT functor_app_annot +by_notation: [ +| string OPT [ "%" ident ] ] argument_spec_block: [ @@ -747,31 +644,21 @@ strategy_level: [ | "transparent" ] -instance_name: [ -| ident_decl LIST0 binder -| -] - reserv_list: [ -| LIST1 reserv_tuple +| LIST1 ( "(" simple_reserv ")" ) | simple_reserv ] -reserv_tuple: [ -| "(" simple_reserv ")" -] - simple_reserv: [ -| LIST1 ident ":" term +| LIST1 ident ":" type ] command: [ | "Goal" term | "Declare" "Scope" ident | "Pwd" -| "Cd" -| "Cd" string -| "Load" [ "Verbose" | ] [ string | ident ] +| "Cd" OPT string +| "Load" OPT "Verbose" [ string | ident ] | "Declare" "ML" "Module" LIST1 string | "Locate" locatable | "Add" "LoadPath" string "as" dirpath @@ -821,101 +708,61 @@ command: [ | "Print" "Namespace" dirpath | "Inspect" num | "Add" "ML" "Path" string -| "Set" LIST1 ident option_setting -| "Unset" LIST1 ident +| OPT "Export" "Set" LIST1 ident OPT [ int | string ] +| OPT "Export" "Unset" LIST1 ident | "Print" "Table" LIST1 ident -| "Add" ident ident LIST1 option_ref_value -| "Add" ident LIST1 option_ref_value -| "Test" LIST1 ident "for" LIST1 option_ref_value -| "Test" LIST1 ident -| "Remove" ident ident LIST1 option_ref_value -| "Remove" ident LIST1 option_ref_value -| "Write" "State" ident -| "Write" "State" string -| "Restore" "State" ident -| "Restore" "State" string +| "Add" ident OPT ident LIST1 [ qualid | string ] +| "Test" LIST1 ident OPT ( "for" LIST1 [ qualid | string ] ) +| "Remove" OPT ident ident LIST1 [ qualid | string ] +| "Write" "State" [ ident | string ] +| "Restore" "State" [ ident | string ] | "Reset" "Initial" | "Reset" ident -| "Back" -| "Back" num -| "Debug" "On" -| "Debug" "Off" +| "Back" OPT num +| "Debug" [ "On" | "Off" ] | "Declare" "Reduction" ident ":=" red_expr | "Declare" "Custom" "Entry" ident | "Derive" ident "SuchThat" one_term "As" ident (* derive plugin *) | "Proof" | "Proof" "Mode" string | "Proof" term -| "Abort" -| "Abort" "All" -| "Abort" ident -| "Existential" num constr_body +| "Abort" OPT [ "All" | ident ] +| "Existential" num OPT ( ":" term ) ":=" term | "Admitted" | "Qed" | "Save" ident -| "Defined" -| "Defined" ident +| "Defined" OPT ident | "Restart" -| "Undo" -| "Undo" num -| "Undo" "To" num -| "Focus" -| "Focus" num +| "Undo" OPT ( OPT "To" num ) +| "Focus" OPT num | "Unfocus" | "Unfocused" -| "Show" -| "Show" num -| "Show" ident +| "Show" OPT [ ident | num ] | "Show" "Existentials" | "Show" "Universes" | "Show" "Conjectures" -| "Show" "Proof" +| "Show" "Proof" OPT ( "Diffs" OPT "removed" ) | "Show" "Intro" | "Show" "Intros" | "Show" "Match" qualid | "Guarded" -| "Create" "HintDb" ident [ "discriminated" | ] -| "Remove" "Hints" LIST1 qualid opt_hintbases -| "Hint" hint opt_hintbases +| "Create" "HintDb" ident OPT "discriminated" +| "Remove" "Hints" LIST1 qualid OPT ( ":" LIST1 ident ) +| "Hint" hint OPT ( ":" LIST1 ident ) | "Comments" LIST0 comment -| "Declare" "Instance" ident_decl LIST0 binder ":" term hint_info -| "Obligation" int "of" ident ":" term withtac -| "Obligation" int "of" ident withtac -| "Obligation" int ":" term withtac -| "Obligation" int withtac -| "Next" "Obligation" "of" ident withtac -| "Next" "Obligation" withtac -| "Solve" "Obligation" int "of" ident "with" ltac_expr -| "Solve" "Obligation" int "with" ltac_expr -| "Solve" "Obligations" "of" ident "with" ltac_expr -| "Solve" "Obligations" "with" ltac_expr -| "Solve" "Obligations" -| "Solve" "All" "Obligations" "with" ltac_expr -| "Solve" "All" "Obligations" -| "Admit" "Obligations" "of" ident -| "Admit" "Obligations" +| "Declare" "Instance" ident_decl LIST0 binder ":" term OPT hint_info +| "Obligation" int OPT ( "of" ident ) OPT ( ":" term OPT ( "with" ltac_expr ) ) +| "Next" "Obligation" OPT ( "of" ident ) OPT ( "with" ltac_expr ) +| "Solve" "Obligation" int OPT ( "of" ident ) "with" ltac_expr +| "Solve" "Obligations" OPT ( OPT ( "of" ident ) "with" ltac_expr ) +| "Solve" "All" "Obligations" OPT ( "with" ltac_expr ) +| "Admit" "Obligations" OPT ( "of" ident ) | "Obligation" "Tactic" ":=" ltac_expr | "Show" "Obligation" "Tactic" -| "Obligations" "of" ident -| "Obligations" -| "Preterm" "of" ident -| "Preterm" -| "Add" "Relation" one_term one_term "reflexivity" "proved" "by" one_term "symmetry" "proved" "by" one_term "as" ident -| "Add" "Relation" one_term one_term "reflexivity" "proved" "by" one_term "as" ident -| "Add" "Relation" one_term one_term "as" ident -| "Add" "Relation" one_term one_term "symmetry" "proved" "by" one_term "as" ident -| "Add" "Relation" one_term one_term "symmetry" "proved" "by" one_term "transitivity" "proved" "by" one_term "as" ident -| "Add" "Relation" one_term one_term "reflexivity" "proved" "by" one_term "transitivity" "proved" "by" one_term "as" ident -| "Add" "Relation" one_term one_term "reflexivity" "proved" "by" one_term "symmetry" "proved" "by" one_term "transitivity" "proved" "by" one_term "as" ident -| "Add" "Relation" one_term one_term "transitivity" "proved" "by" one_term "as" ident -| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "reflexivity" "proved" "by" one_term "symmetry" "proved" "by" one_term "as" ident -| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "reflexivity" "proved" "by" one_term "as" ident -| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "as" ident -| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "symmetry" "proved" "by" one_term "as" ident -| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "symmetry" "proved" "by" one_term "transitivity" "proved" "by" one_term "as" ident -| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "reflexivity" "proved" "by" one_term "transitivity" "proved" "by" one_term "as" ident -| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "reflexivity" "proved" "by" one_term "symmetry" "proved" "by" one_term "transitivity" "proved" "by" one_term "as" ident -| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "transitivity" "proved" "by" one_term "as" ident +| "Obligations" OPT ( "of" ident ) +| "Preterm" OPT ( "of" ident ) +| "Add" "Relation" one_term one_term OPT ( "reflexivity" "proved" "by" one_term ) OPT ( "symmetry" "proved" "by" one_term ) OPT ( "transitivity" "proved" "by" one_term ) "as" ident +| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term OPT ( "reflexivity" "proved" "by" one_term ) OPT ( "symmetry" "proved" "by" one_term ) OPT ( "transitivity" "proved" "by" one_term ) "as" ident | "Add" "Setoid" one_term one_term one_term "as" ident | "Add" "Parametric" "Setoid" LIST0 binder ":" one_term one_term one_term "as" ident | "Add" "Morphism" one_term ":" ident @@ -929,9 +776,7 @@ command: [ | "Optimize" "Proof" | "Optimize" "Heap" | "Reset" "Ltac" "Profile" -| "Show" "Ltac" "Profile" -| "Show" "Ltac" "Profile" "CutOff" int -| "Show" "Ltac" "Profile" string +| "Show" "Ltac" "Profile" OPT [ "CutOff" int | string ] | "Show" "Lia" "Profile" (* micromega plugin *) | "Add" "InjTyp" one_term (* micromega plugin *) | "Add" "BinOp" one_term (* micromega plugin *) @@ -952,10 +797,10 @@ command: [ | "Show" "Zify" "BinRel" (* micromega plugin *) | "Show" "Zify" "Spec" (* micromega plugin *) | "Add" "Ring" ident ":" one_term OPT ( "(" LIST1 ring_mod SEP "," ")" ) (* setoid_ring plugin *) -| "Hint" "Cut" "[" hints_path "]" opthints +| "Hint" "Cut" "[" hints_path "]" OPT ( ":" LIST1 ident ) | "Typeclasses" "Transparent" LIST0 qualid | "Typeclasses" "Opaque" LIST0 qualid -| "Typeclasses" "eauto" ":=" debug eauto_search_strategy OPT int +| "Typeclasses" "eauto" ":=" OPT "debug" OPT [ "(bfs)" | "(dfs)" ] OPT int | "Proof" "with" ltac_expr OPT [ "using" section_subset_expr ] | "Proof" "using" section_subset_expr OPT [ "with" ltac_expr ] | "Tactic" "Notation" OPT ( "(" "at" "level" num ")" ) LIST1 ltac_production_item ":=" ltac_expr @@ -984,20 +829,15 @@ command: [ | "Extraction" "Blacklist" LIST1 ident (* extraction plugin *) | "Print" "Extraction" "Blacklist" (* extraction plugin *) | "Reset" "Extraction" "Blacklist" (* extraction plugin *) -| "Extract" "Constant" qualid LIST0 string "=>" mlname (* extraction plugin *) -| "Extract" "Inlined" "Constant" qualid "=>" mlname (* extraction plugin *) -| "Extract" "Inductive" qualid "=>" mlname "[" LIST0 mlname "]" OPT string (* extraction plugin *) +| "Extract" "Constant" qualid LIST0 string "=>" [ ident | string ] (* extraction plugin *) +| "Extract" "Inlined" "Constant" qualid "=>" [ ident | string ] (* extraction plugin *) +| "Extract" "Inductive" qualid "=>" [ ident | string ] "[" LIST0 [ ident | string ] "]" OPT string (* extraction plugin *) | "Show" "Extraction" (* extraction plugin *) | "Functional" "Case" fun_scheme_arg (* funind plugin *) | "Generate" "graph" "for" qualid (* funind plugin *) -| "Hint" "Rewrite" orient LIST1 one_term ":" LIST0 ident -| "Hint" "Rewrite" orient LIST1 one_term "using" ltac_expr ":" LIST0 ident -| "Hint" "Rewrite" orient LIST1 one_term -| "Hint" "Rewrite" orient LIST1 one_term "using" ltac_expr -| "Derive" "Inversion_clear" ident "with" one_term "Sort" sort_family -| "Derive" "Inversion_clear" ident "with" one_term -| "Derive" "Inversion" ident "with" one_term "Sort" sort_family -| "Derive" "Inversion" ident "with" one_term +| "Hint" "Rewrite" OPT [ "->" | "<-" ] LIST1 one_term OPT ( "using" ltac_expr ) OPT ( ":" LIST0 ident ) +| "Derive" "Inversion_clear" ident "with" one_term OPT ( "Sort" sort_family ) +| "Derive" "Inversion" ident "with" one_term OPT ( "Sort" sort_family ) | "Derive" "Dependent" "Inversion" ident "with" one_term "Sort" sort_family | "Derive" "Dependent" "Inversion_clear" ident "with" one_term "Sort" sort_family | "Declare" "Left" "Step" one_term @@ -1008,12 +848,84 @@ command: [ | "Numeral" "Notation" qualid qualid qualid ":" ident OPT numnotoption | "String" "Notation" qualid qualid qualid ":" ident | "SubClass" ident_decl def_body -] - -orient: [ -| "->" -| "<-" -| +| thm_token ident_decl LIST0 binder ":" type LIST0 [ "with" ident_decl LIST0 binder ":" type ] +| assumption_token OPT ( "Inline" OPT ( "(" num ")" ) ) [ LIST1 ( "(" assumpt ")" ) | assumpt ] +| [ "Definition" | "Example" ] ident_decl def_body +| "Let" ident def_body +| "Inductive" inductive_definition LIST0 ( "with" inductive_definition ) +| "Fixpoint" fix_definition LIST0 ( "with" fix_definition ) +| "Let" "Fixpoint" fix_definition LIST0 ( "with" fix_definition ) +| "CoFixpoint" cofix_definition LIST0 ( "with" cofix_definition ) +| "Let" "CoFixpoint" cofix_definition LIST0 ( "with" cofix_definition ) +| "Scheme" OPT ( ident ":=" ) scheme_kind LIST0 ( "with" OPT ( ident ":=" ) scheme_kind ) +| "Combined" "Scheme" ident "from" LIST1 ident SEP "," +| "Register" qualid "as" qualid +| "Register" "Inline" qualid +| "Primitive" ident OPT [ ":" term ] ":=" register_token +| "Universe" LIST1 ident +| "Universes" LIST1 ident +| "Constraint" LIST1 univ_constraint SEP "," +| "CoInductive" inductive_definition LIST0 ( "with" inductive_definition ) +| "Variant" variant_definition LIST0 ( "with" variant_definition ) +| [ "Record" | "Structure" ] record_definition LIST0 ( "with" record_definition ) +| "Class" inductive_definition LIST0 ( "with" inductive_definition ) +| "Module" OPT [ "Import" | "Export" ] ident LIST0 module_binder OPT of_module_type OPT ( ":=" LIST1 module_expr_inl SEP "<+" ) +| "Module" "Type" ident LIST0 module_binder LIST0 ( "<:" module_type_inl ) OPT ( ":=" LIST1 module_type_inl SEP "<+" ) +| "Declare" "Module" OPT [ "Import" | "Export" ] ident LIST0 module_binder ":" module_type_inl +| "Section" ident +| "Chapter" ident +| "End" ident +| "Collection" ident ":=" section_subset_expr +| "Require" OPT [ "Import" | "Export" ] LIST1 qualid +| "From" qualid "Require" OPT [ "Import" | "Export" ] LIST1 qualid +| "Import" LIST1 qualid +| "Export" LIST1 qualid +| "Include" module_type_inl LIST0 ( "<+" module_expr_inl ) +| "Include" "Type" LIST1 module_type_inl SEP "<+" +| "Transparent" LIST1 smart_qualid +| "Opaque" LIST1 smart_qualid +| "Strategy" LIST1 [ strategy_level "[" LIST1 smart_qualid "]" ] +| "Canonical" OPT "Structure" ident_decl def_body +| "Canonical" OPT "Structure" smart_qualid +| "Coercion" qualid OPT univ_decl def_body +| "Identity" "Coercion" ident ":" class ">->" class +| "Coercion" qualid ":" class ">->" class +| "Coercion" by_notation ":" class ">->" class +| "Context" LIST1 binder +| "Instance" OPT ( ident_decl LIST0 binder ) ":" term OPT hint_info OPT [ ":=" "{" LIST0 field_def "}" | ":=" term ] +| "Existing" "Instance" qualid OPT hint_info +| "Existing" "Instances" LIST1 qualid OPT [ "|" num ] +| "Existing" "Class" qualid +| "Arguments" smart_qualid LIST0 argument_spec_block LIST0 [ "," LIST0 more_implicits_block ] OPT [ ":" LIST1 arguments_modifier SEP "," ] +| "Implicit" [ "Type" | "Types" ] reserv_list +| "Generalizable" [ [ "Variable" | "Variables" ] LIST1 ident | "All" "Variables" | "No" "Variables" ] +| "Open" "Scope" ident +| "Close" "Scope" ident +| "Delimit" "Scope" ident "with" ident +| "Undelimit" "Scope" ident +| "Bind" "Scope" ident "with" LIST1 class +| "Infix" string ":=" one_term OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" ident ] +| "Notation" ident LIST0 ident ":=" one_term OPT ( "(" "only" "parsing" ")" ) +| "Notation" string ":=" one_term OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" ident ] +| "Format" "Notation" string string string +| "Reserved" "Infix" string OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] +| "Reserved" "Notation" string OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] +| "Eval" red_expr "in" term +| "Compute" term +| "Check" term +| "About" smart_qualid OPT ( "@{" LIST0 name "}" ) +| "SearchHead" one_term OPT ne_in_or_out_modules +| "SearchPattern" one_term OPT ne_in_or_out_modules +| "SearchRewrite" one_term OPT ne_in_or_out_modules +| "Search" searchabout_query OPT searchabout_queries +| "Time" command +| "Redirect" string command +| "Timeout" num command +| "Fail" command +| "Drop" +| "Quit" +| "BackTo" num +| "Show" "Goal" num "at" num ] section_subset_expr: [ @@ -1052,6 +964,10 @@ dirpath: [ | dirpath field_ident ] +bignat: [ +| numeral +] + locatable: [ | smart_qualid | "Term" smart_qualid @@ -1060,27 +976,17 @@ locatable: [ | "Module" qualid ] -option_ref_value: [ -| qualid -| string -] - comment: [ | one_term | string | num ] -reference_or_constr: [ -| qualid -| one_term -] - hint: [ -| "Resolve" LIST1 reference_or_constr hint_info +| "Resolve" LIST1 [ qualid | one_term ] OPT hint_info | "Resolve" "->" LIST1 qualid OPT num | "Resolve" "<-" LIST1 qualid OPT num -| "Immediate" LIST1 reference_or_constr +| "Immediate" LIST1 [ qualid | one_term ] | "Variables" "Transparent" | "Variables" "Opaque" | "Constants" "Transparent" @@ -1093,24 +999,9 @@ hint: [ | "Extern" num OPT one_term "=>" ltac_expr ] -constr_body: [ -| ":=" term -| ":" term ":=" term -] - -withtac: [ -| "with" ltac_expr -| -] - -ltac_def_kind: [ -| ":=" -| "::=" -] - tacdef_body: [ -| qualid LIST1 fun_var ltac_def_kind ltac_expr -| qualid ltac_def_kind ltac_expr +| qualid LIST1 fun_var [ ":=" | "::=" ] ltac_expr +| qualid [ ":=" | "::=" ] ltac_expr ] ltac_production_item: [ @@ -1120,13 +1011,8 @@ ltac_production_item: [ ] numnotoption: [ -| "(" "warning" "after" num ")" -| "(" "abstract" "after" num ")" -] - -mlname: [ -| ident (* extraction plugin *) -| string (* extraction plugin *) +| "(" "warning" "after" bignat ")" +| "(" "abstract" "after" bignat ")" ] int_or_id: [ @@ -1166,55 +1052,17 @@ field_mod: [ | "completeness" one_term (* setoid_ring plugin *) ] -debug: [ -| "debug" -| -] - -eauto_search_strategy: [ -| "(bfs)" -| "(dfs)" -| -] - -hints_path_atom: [ -| LIST1 qualid -| "_" -] - hints_path: [ | "(" hints_path ")" | hints_path "*" | "emp" | "eps" | hints_path "|" hints_path -| hints_path_atom +| LIST1 qualid +| "_" | hints_path hints_path ] -opthints: [ -| ":" LIST1 ident -| -] - -opt_hintbases: [ -| -| ":" LIST1 ident -] - -query_command: [ -| "Eval" red_expr "in" term "." -| "Compute" term "." -| "Check" term "." -| "About" smart_qualid OPT ( "@{" LIST0 name "}" ) "." -| "SearchHead" one_term in_or_out_modules "." -| "SearchPattern" one_term in_or_out_modules "." -| "SearchRewrite" one_term in_or_out_modules "." -| "Search" searchabout_query searchabout_queries "." -| "SearchAbout" searchabout_query searchabout_queries "." -| "SearchAbout" "[" LIST1 searchabout_query "]" in_or_out_modules "." -] - class: [ | "Funclass" | "Sortclass" @@ -1226,39 +1074,14 @@ ne_in_or_out_modules: [ | "outside" LIST1 qualid ] -in_or_out_modules: [ -| ne_in_or_out_modules -| -] - -positive_search_mark: [ -| "-" -| -] - searchabout_query: [ -| positive_search_mark string OPT ( "%" ident ) -| positive_search_mark one_term +| OPT "-" string OPT ( "%" ident ) +| OPT "-" one_term ] searchabout_queries: [ | ne_in_or_out_modules | searchabout_query searchabout_queries -| -] - -syntax: [ -| "Open" "Scope" ident -| "Close" "Scope" ident -| "Delimit" "Scope" ident "with" ident -| "Undelimit" "Scope" ident -| "Bind" "Scope" ident "with" LIST1 class -| "Infix" string ":=" one_term OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" ident ] -| "Notation" ident LIST0 ident ":=" one_term OPT ( "(" "only" "parsing" ")" ) -| "Notation" string ":=" one_term OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" ident ] -| "Format" "Notation" string string string -| "Reserved" "Infix" string OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] -| "Reserved" "Notation" string OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] ] level: [ @@ -1294,18 +1117,13 @@ syntax_extension_type: [ | "bigint" | "binder" | "constr" -| "constr" at_level_opt OPT constr_as_binder_kind +| "constr" OPT ( "at" level ) OPT constr_as_binder_kind | "pattern" | "pattern" "at" "level" num | "strict" "pattern" | "strict" "pattern" "at" "level" num | "closed" "binder" -| "custom" ident at_level_opt OPT constr_as_binder_kind -] - -at_level_opt: [ -| "at" level -| +| "custom" ident OPT ( "at" level ) OPT constr_as_binder_kind ] simple_tactic: [ @@ -1321,125 +1139,71 @@ simple_tactic: [ | "elimtype" one_term | "lapply" one_term | "transitivity" one_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" 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" ident -| "intro" ident "before" ident -| "intro" "at" "top" -| "intro" "at" "bottom" -| "intro" "after" ident -| "intro" "before" ident -| "move" ident "at" "top" -| "move" ident "at" "bottom" -| "move" ident "after" ident -| "move" ident "before" ident -| "rename" LIST1 rename SEP "," +| "left" OPT ( "with" bindings ) +| "eleft" OPT ( "with" bindings ) +| "right" OPT ( "with" bindings ) +| "eright" OPT ( "with" bindings ) +| "constructor" OPT int_or_var OPT ( "with" bindings ) +| "econstructor" OPT ( int_or_var OPT ( "with" bindings ) ) +| "specialize" constr_with_bindings OPT ( "as" simple_intropattern ) +| "symmetry" OPT ( "in" in_clause ) +| "split" OPT ( "with" bindings ) +| "esplit" OPT ( "with" bindings ) +| "exists" OPT ( LIST1 bindings SEP "," ) +| "eexists" OPT ( LIST1 bindings SEP "," ) +| "intros" "until" [ ident | num ] +| "intro" OPT ident OPT where +| "move" ident OPT where +| "rename" LIST1 ( ident "into" ident ) SEP "," | "revert" LIST1 ident -| "simple" "induction" quantified_hypothesis -| "simple" "destruct" quantified_hypothesis -| "double" "induction" quantified_hypothesis quantified_hypothesis +| "simple" "induction" [ ident | num ] +| "simple" "destruct" [ ident | num ] +| "double" "induction" [ ident | num ] [ ident | num ] | "admit" -| "fix" ident num -| "cofix" ident | "clear" LIST0 ident | "clear" "-" LIST1 ident | "clearbody" LIST1 ident | "generalize" "dependent" one_term -| "replace" one_term "with" one_term clause_dft_concl by_arg_tac -| "replace" "->" one_term clause_dft_concl -| "replace" "<-" one_term clause_dft_concl -| "replace" one_term 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" 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 one_term -| "dependent" "rewrite" orient one_term "in" ident -| "cutrewrite" orient one_term -| "cutrewrite" orient one_term "in" ident +| "replace" one_term "with" one_term OPT clause_dft_concl OPT ( "by" ltac_expr3 ) +| "replace" OPT [ "->" | "<-" ] one_term OPT clause_dft_concl +| "simplify_eq" OPT destruction_arg +| "esimplify_eq" OPT destruction_arg +| "discriminate" OPT destruction_arg +| "ediscriminate" OPT destruction_arg +| "injection" OPT destruction_arg OPT ( "as" LIST0 simple_intropattern ) +| "einjection" OPT destruction_arg OPT ( "as" LIST0 simple_intropattern ) +| "simple" "injection" OPT destruction_arg +| "dependent" "rewrite" OPT [ "->" | "<-" ] one_term OPT ( "in" ident ) +| "cutrewrite" OPT [ "->" | "<-" ] one_term OPT ( "in" ident ) | "decompose" "sum" one_term | "decompose" "record" one_term | "absurd" one_term | "contradiction" OPT constr_with_bindings -| "autorewrite" "with" LIST1 ident clause_dft_concl -| "autorewrite" "with" LIST1 ident clause_dft_concl "using" ltac_expr -| "autorewrite" "*" "with" LIST1 ident clause_dft_concl -| "autorewrite" "*" "with" LIST1 ident clause_dft_concl "using" ltac_expr -| "rewrite" "*" orient one_term "in" ident "at" occurrences by_arg_tac -| "rewrite" "*" orient one_term "at" occurrences "in" ident by_arg_tac -| "rewrite" "*" orient one_term "in" ident by_arg_tac -| "rewrite" "*" orient one_term "at" occurrences by_arg_tac -| "rewrite" "*" orient one_term by_arg_tac +| "autorewrite" OPT "*" "with" LIST1 ident OPT clause_dft_concl OPT ( "using" ltac_expr ) +| "rewrite" "*" OPT [ "->" | "<-" ] one_term OPT ( "in" ident ) OPT ( "at" occurrences OPT ( "by" ltac_expr3 ) ) +| "rewrite" "*" OPT [ "->" | "<-" ] one_term "at" occurrences "in" ident OPT ( "by" ltac_expr3 ) | "refine" one_term | "simple" "refine" one_term | "notypeclasses" "refine" one_term | "simple" "notypeclasses" "refine" one_term | "solve_constraints" -| "subst" LIST1 ident -| "subst" +| "subst" OPT ( LIST1 ident ) | "simple" "subst" | "evar" "(" ident ":" term ")" | "evar" one_term | "instantiate" "(" ident ":=" term ")" -| "instantiate" "(" int ":=" term ")" hloc +| "instantiate" "(" int ":=" term ")" OPT hloc | "instantiate" -| "stepl" one_term "by" ltac_expr -| "stepl" one_term -| "stepr" one_term "by" ltac_expr -| "stepr" one_term +| "stepl" one_term OPT ( "by" ltac_expr ) +| "stepr" one_term OPT ( "by" ltac_expr ) | "generalize_eqs" ident | "dependent" "generalize_eqs" ident | "generalize_eqs_vars" ident | "dependent" "generalize_eqs_vars" ident | "specialize_eqs" ident -| "hresolve_core" "(" ident ":=" one_term ")" "at" int_or_var "in" one_term -| "hresolve_core" "(" ident ":=" one_term ")" "in" one_term +| "hresolve_core" "(" ident ":=" one_term ")" OPT ( "at" int_or_var ) "in" one_term | "hget_evar" int_or_var -| "destauto" -| "destauto" "in" ident +| "destauto" OPT ( "in" ident ) | "transparent_abstract" ltac_expr3 | "transparent_abstract" ltac_expr3 "using" ident | "constr_eq" one_term one_term @@ -1471,27 +1235,24 @@ simple_tactic: [ | "show" "ltac" "profile" "cutoff" int | "show" "ltac" "profile" string | "restart_timer" OPT string -| "finish_timing" OPT string -| "finish_timing" "(" string ")" OPT string +| "finish_timing" OPT ( "(" string ")" ) OPT string | "eassumption" | "eexact" one_term -| "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 +| "trivial" OPT auto_using OPT hintbases +| "info_trivial" OPT auto_using OPT hintbases +| "debug" "trivial" OPT auto_using OPT hintbases +| "auto" OPT int_or_var OPT auto_using OPT hintbases +| "info_auto" OPT int_or_var OPT auto_using OPT hintbases +| "debug" "auto" OPT int_or_var OPT auto_using OPT hintbases | "prolog" "[" LIST0 one_term "]" 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" ident -| "autounfold_one" hintbases -| "unify" one_term one_term -| "unify" one_term one_term "with" ident +| "eauto" OPT int_or_var OPT int_or_var OPT auto_using OPT hintbases +| "new" "auto" OPT int_or_var OPT auto_using OPT hintbases +| "debug" "eauto" OPT int_or_var OPT int_or_var OPT auto_using OPT hintbases +| "info_eauto" OPT int_or_var OPT int_or_var OPT auto_using OPT hintbases +| "dfs" "eauto" OPT int_or_var OPT auto_using OPT hintbases +| "autounfold" OPT hintbases OPT clause_dft_concl +| "autounfold_one" OPT hintbases OPT ( "in" ident ) +| "unify" one_term one_term OPT ( "with" ident ) | "convert_concl_no_check" one_term | "typeclasses" "eauto" "bfs" OPT int_or_var "with" LIST1 ident | "typeclasses" "eauto" OPT int_or_var "with" LIST1 ident @@ -1502,103 +1263,90 @@ simple_tactic: [ | "autoapply" one_term "using" ident | "autoapply" one_term "with" ident | "progress_evars" ltac_expr -| "rewrite_strat" rewstrategy -| "rewrite_db" ident "in" ident -| "rewrite_db" ident -| "substitute" orient constr_with_bindings -| "setoid_rewrite" orient constr_with_bindings -| "setoid_rewrite" orient constr_with_bindings "in" ident -| "setoid_rewrite" orient constr_with_bindings "at" occurrences -| "setoid_rewrite" orient constr_with_bindings "at" occurrences "in" ident -| "setoid_rewrite" orient constr_with_bindings "in" ident "at" occurrences -| "setoid_symmetry" -| "setoid_symmetry" "in" ident +| "rewrite_strat" rewstrategy OPT ( "in" ident ) +| "rewrite_db" ident OPT ( "in" ident ) +| "substitute" OPT [ "->" | "<-" ] constr_with_bindings +| "setoid_rewrite" OPT [ "->" | "<-" ] constr_with_bindings OPT ( "at" occurrences ) OPT ( "in" ident ) +| "setoid_rewrite" OPT [ "->" | "<-" ] constr_with_bindings "in" ident "at" occurrences +| "setoid_symmetry" OPT ( "in" ident ) | "setoid_reflexivity" | "setoid_transitivity" one_term | "setoid_etransitivity" | "decide" "equality" | "compare" one_term one_term -| "rewrite_strat" rewstrategy "in" ident -| "intros" intropattern_list_opt -| "eintros" intropattern_list_opt -| "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 +| "intros" LIST0 intropattern +| "eintros" LIST0 intropattern +| "apply" LIST1 constr_with_bindings_arg SEP "," OPT in_hyp_as +| "eapply" LIST1 constr_with_bindings_arg SEP "," OPT in_hyp_as +| "simple" "apply" LIST1 constr_with_bindings_arg SEP "," OPT in_hyp_as +| "simple" "eapply" LIST1 constr_with_bindings_arg SEP "," OPT in_hyp_as | "elim" constr_with_bindings_arg OPT ( "using" constr_with_bindings ) | "eelim" constr_with_bindings_arg OPT ( "using" constr_with_bindings ) | "case" induction_clause_list | "ecase" induction_clause_list -| "fix" ident num "with" LIST1 fixdecl -| "cofix" ident "with" LIST1 cofixdecl +| "fix" ident num OPT ( "with" LIST1 fixdecl ) +| "cofix" ident OPT ( "with" LIST1 cofixdecl ) | "pose" bindings_with_parameters -| "pose" one_term as_name +| "pose" one_term OPT as_name | "epose" bindings_with_parameters -| "epose" one_term as_name -| "set" bindings_with_parameters clause_dft_concl -| "set" one_term as_name clause_dft_concl -| "eset" bindings_with_parameters clause_dft_concl -| "eset" one_term as_name clause_dft_concl -| "remember" one_term as_name eqn_ipat clause_dft_all -| "eremember" one_term as_name eqn_ipat clause_dft_all +| "epose" one_term OPT as_name +| "set" bindings_with_parameters OPT clause_dft_concl +| "set" one_term OPT as_name OPT clause_dft_concl +| "eset" bindings_with_parameters OPT clause_dft_concl +| "eset" one_term OPT as_name OPT clause_dft_concl +| "remember" one_term OPT as_name OPT eqn_ipat OPT clause_dft_all +| "eremember" one_term OPT as_name OPT eqn_ipat OPT clause_dft_all | "assert" "(" ident ":=" term ")" | "eassert" "(" ident ":=" term ")" -| "assert" "(" ident ":" term ")" by_tactic -| "eassert" "(" ident ":" term ")" by_tactic -| "enough" "(" ident ":" term ")" by_tactic -| "eenough" "(" ident ":" term ")" by_tactic -| "assert" one_term as_ipat by_tactic -| "eassert" one_term as_ipat by_tactic +| "assert" "(" ident ":" term ")" OPT ( "by" ltac_expr3 ) +| "eassert" "(" ident ":" term ")" OPT ( "by" ltac_expr3 ) +| "enough" "(" ident ":" term ")" OPT ( "by" ltac_expr3 ) +| "eenough" "(" ident ":" term ")" OPT ( "by" ltac_expr3 ) +| "assert" one_term OPT as_ipat OPT ( "by" ltac_expr3 ) +| "eassert" one_term OPT as_ipat OPT ( "by" ltac_expr3 ) | "pose" "proof" "(" ident ":=" term ")" | "epose" "proof" "(" ident ":=" term ")" -| "pose" "proof" term as_ipat -| "epose" "proof" term as_ipat -| "enough" one_term as_ipat by_tactic -| "eenough" one_term as_ipat by_tactic -| "generalize" one_term -| "generalize" one_term LIST1 one_term -| "generalize" one_term OPT ( "at" occs_nums ) as_name LIST0 [ "," pattern_occ as_name ] +| "pose" "proof" term OPT as_ipat +| "epose" "proof" term OPT as_ipat +| "enough" one_term OPT as_ipat OPT ( "by" ltac_expr3 ) +| "eenough" one_term OPT as_ipat OPT ( "by" ltac_expr3 ) +| "generalize" one_term OPT ( LIST1 one_term ) +| "generalize" one_term OPT ( "at" occs_nums ) OPT as_name LIST0 [ "," pattern_occ OPT 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" one_term ] -| "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" one_term in_hyp_list -| "red" clause_dft_concl -| "hnf" clause_dft_concl -| "simpl" OPT delta_flag OPT ref_or_pattern_occ clause_dft_concl -| "cbv" OPT strategy_flag clause_dft_concl -| "cbn" OPT strategy_flag clause_dft_concl -| "lazy" OPT strategy_flag clause_dft_concl -| "compute" OPT 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 one_term clause_dft_concl -| "pattern" LIST1 pattern_occ SEP "," clause_dft_concl -| "change" conversion clause_dft_concl -| "change_no_check" conversion clause_dft_concl +| "rewrite" LIST1 oriented_rewriter SEP "," OPT clause_dft_concl OPT ( "by" ltac_expr3 ) +| "erewrite" LIST1 oriented_rewriter SEP "," OPT clause_dft_concl OPT ( "by" ltac_expr3 ) +| "dependent" [ "simple" "inversion" | "inversion" | "inversion_clear" ] [ ident | num ] OPT as_or_and_ipat OPT [ "with" one_term ] +| "simple" "inversion" [ ident | num ] OPT as_or_and_ipat OPT ( "in" LIST1 ident ) +| "inversion" [ ident | num ] OPT as_or_and_ipat OPT ( "in" LIST1 ident ) +| "inversion_clear" [ ident | num ] OPT as_or_and_ipat OPT ( "in" LIST1 ident ) +| "inversion" [ ident | num ] "using" one_term OPT ( "in" LIST1 ident ) +| "red" OPT clause_dft_concl +| "hnf" OPT clause_dft_concl +| "simpl" OPT delta_flag OPT ref_or_pattern_occ OPT clause_dft_concl +| "cbv" OPT strategy_flag OPT clause_dft_concl +| "cbn" OPT strategy_flag OPT clause_dft_concl +| "lazy" OPT strategy_flag OPT clause_dft_concl +| "compute" OPT delta_flag OPT clause_dft_concl +| "vm_compute" OPT ref_or_pattern_occ OPT clause_dft_concl +| "native_compute" OPT ref_or_pattern_occ OPT clause_dft_concl +| "unfold" LIST1 unfold_occ SEP "," OPT clause_dft_concl +| "fold" LIST1 one_term OPT clause_dft_concl +| "pattern" LIST1 pattern_occ SEP "," OPT clause_dft_concl +| "change" conversion OPT clause_dft_concl +| "change_no_check" conversion OPT clause_dft_concl | "btauto" | "rtauto" -| "congruence" -| "congruence" int -| "congruence" "with" LIST1 one_term -| "congruence" int "with" LIST1 one_term +| "congruence" OPT int OPT ( "with" LIST1 one_term ) | "f_equal" -| "firstorder" OPT ltac_expr firstorder_using -| "firstorder" OPT ltac_expr "with" LIST1 ident -| "firstorder" OPT ltac_expr firstorder_using "with" LIST1 ident +| "firstorder" OPT ltac_expr firstorder_rhs | "gintuition" OPT ltac_expr -| "functional" "inversion" quantified_hypothesis OPT qualid (* funind plugin *) -| "functional" "induction" LIST1 one_term fun_ind_using with_names (* funind plugin *) -| "soft" "functional" "induction" LIST1 one_term fun_ind_using with_names (* funind plugin *) -| "psatz_Z" int_or_var ltac_expr (* micromega plugin *) -| "psatz_Z" ltac_expr (* micromega plugin *) +| "functional" "inversion" [ ident | num ] OPT qualid (* funind plugin *) +| "functional" "induction" LIST1 one_term OPT fun_ind_using OPT with_names (* funind plugin *) +| "soft" "functional" "induction" LIST1 one_term OPT fun_ind_using OPT with_names (* funind plugin *) +| "psatz_Z" OPT int_or_var ltac_expr | "xlia" ltac_expr (* micromega plugin *) | "xnlia" ltac_expr (* micromega plugin *) | "xnra" ltac_expr (* micromega plugin *) @@ -1608,10 +1356,8 @@ simple_tactic: [ | "sos_R" ltac_expr (* micromega plugin *) | "lra_Q" ltac_expr (* micromega plugin *) | "lra_R" ltac_expr (* micromega plugin *) -| "psatz_R" int_or_var ltac_expr (* micromega plugin *) -| "psatz_R" ltac_expr (* micromega plugin *) -| "psatz_Q" int_or_var ltac_expr (* micromega plugin *) -| "psatz_Q" ltac_expr (* micromega plugin *) +| "psatz_R" OPT int_or_var ltac_expr +| "psatz_Q" OPT int_or_var ltac_expr | "zify_iter_specs" (* micromega plugin *) | "zify_op" (* micromega plugin *) | "zify_saturate" (* micromega plugin *) @@ -1619,14 +1365,37 @@ simple_tactic: [ | "zify_elim_let" (* micromega plugin *) | "nsatz_compute" one_term (* nsatz plugin *) | "omega" (* omega plugin *) -| "protect_fv" string "in" ident (* setoid_ring plugin *) -| "protect_fv" string (* setoid_ring plugin *) +| "protect_fv" string OPT ( "in" ident ) | "ring_lookup" ltac_expr0 "[" LIST0 one_term "]" LIST1 one_term (* setoid_ring plugin *) | "field_lookup" ltac_expr "[" LIST0 one_term "]" LIST1 one_term (* setoid_ring plugin *) +| "classical_left" +| "classical_right" +| "contradict" ident +| "discrR" +| "easy" +| "exfalso" +| "inversion_sigma" +| "lia" +| "lra" +| "nia" +| "nra" +| "split_Rabs" +| "split_Rmult" +| "tauto" +| "zify" +| "assert_fails" ltac_expr3 +| "assert_succeeds" ltac_expr3 +| "field" OPT ( "[" LIST1 term "]" ) +| "field_simplify" OPT ( "[" LIST1 term "]" ) LIST1 term OPT ( "in" ident ) +| "field_simplify_eq" OPT ( "[" LIST1 term "]" ) OPT ( "in" ident ) +| "intuition" OPT ltac_expr +| "nsatz" OPT ( "with" "radicalmax" ":=" term "strategy" ":=" term "parameters" ":=" term "variables" ":=" term ) +| "psatz" term OPT int_or_var +| "ring" OPT ( "[" LIST1 term "]" ) +| "ring_simplify" OPT ( "[" LIST1 term "]" ) LIST1 term OPT ( "in" ident ) ] hloc: [ -| | "in" "|-" "*" | "in" ident | "in" "(" "Type" "of" ident ")" @@ -1635,15 +1404,6 @@ hloc: [ | "in" "(" "value" "of" ident ")" ] -rename: [ -| ident "into" ident -] - -by_arg_tac: [ -| "by" ltac_expr3 -| -] - in_clause: [ | LIST0 hypident_occ SEP "," OPT ( "|-" OPT concl_occ ) | "*" "|-" OPT concl_occ @@ -1666,7 +1426,6 @@ hypident: [ as_ipat: [ | "as" simple_intropattern -| ] or_and_intropattern_loc: [ @@ -1676,29 +1435,19 @@ or_and_intropattern_loc: [ 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" ltac_expr3 -| ] rewriter: [ | "!" constr_with_bindings_arg -| [ "?" | "?" ] constr_with_bindings_arg +| "?" constr_with_bindings_arg | num "!" constr_with_bindings_arg | num [ "?" | "?" ] constr_with_bindings_arg | num constr_with_bindings_arg @@ -1706,24 +1455,19 @@ rewriter: [ ] oriented_rewriter: [ -| orient rewriter +| OPT [ "->" | "<-" ] rewriter ] induction_clause: [ -| destruction_arg as_or_and_ipat eqn_ipat opt_clause +| destruction_arg OPT as_or_and_ipat OPT eqn_ipat OPT opt_clause ] induction_clause_list: [ -| LIST1 induction_clause SEP "," OPT ( "using" constr_with_bindings ) opt_clause +| LIST1 induction_clause SEP "," OPT ( "using" constr_with_bindings ) OPT opt_clause ] auto_using: [ | "using" LIST1 one_term SEP "," -| -] - -intropattern_list_opt: [ -| LIST0 intropattern ] or_and_intropattern: [ @@ -1733,14 +1477,13 @@ or_and_intropattern: [ ] intropattern_or_list_or: [ -| intropattern_or_list_or "|" intropattern_list_opt -| intropattern_list_opt +| LIST0 intropattern LIST0 ( "|" LIST0 intropattern ) ] equality_intropattern: [ | "->" | "<-" -| "[=" intropattern_list_opt "]" +| "[=" LIST0 intropattern "]" ] naming_intropattern: [ @@ -1787,7 +1530,6 @@ comparison: [ hintbases: [ | "with" "*" | "with" LIST1 ident -| ] bindings_with_parameters: [ @@ -1797,28 +1539,19 @@ bindings_with_parameters: [ clause_dft_concl: [ | "in" in_clause | OPT ( "at" occs_nums ) -| ] clause_dft_all: [ | "in" in_clause -| ] opt_clause: [ | "in" in_clause | "at" occs_nums -| -] - -in_hyp_list: [ -| "in" LIST1 ident -| ] in_hyp_as: [ -| "in" ident as_ipat -| +| "in" ident OPT as_ipat ] simple_binder: [ @@ -1827,12 +1560,11 @@ simple_binder: [ ] fixdecl: [ -| "(" ident LIST0 simple_binder struct_annot ":" term ")" +| "(" ident LIST0 simple_binder OPT struct_annot ":" term ")" ] struct_annot: [ | "{" "struct" name "}" -| ] cofixdecl: [ @@ -1840,12 +1572,7 @@ cofixdecl: [ ] constr_with_bindings: [ -| one_term with_bindings -] - -with_bindings: [ -| "with" bindings -| +| one_term OPT ( "with" bindings ) ] destruction_arg: [ @@ -1859,11 +1586,6 @@ constr_with_bindings_arg: [ | constr_with_bindings ] -quantified_hypothesis: [ -| ident -| num -] - conversion: [ | one_term | one_term "with" one_term @@ -1874,17 +1596,14 @@ firstorder_using: [ | "using" qualid | "using" qualid "," LIST1 qualid SEP "," | "using" qualid qualid LIST0 qualid -| ] fun_ind_using: [ | "using" constr_with_bindings (* funind plugin *) -| (* funind plugin *) ] with_names: [ | "as" simple_intropattern (* funind plugin *) -| (* funind plugin *) ] occurrences: [ @@ -2032,16 +1751,11 @@ tactic_arg: [ | "eval" red_expr "in" term | "context" ident "[" term "]" | "type" "of" term -| "fresh" LIST0 fresh_id +| "fresh" LIST0 [ string | qualid ] | "type_term" one_term | "numgoals" ] -fresh_id: [ -| string -| qualid -] - tactic_arg_compat: [ | tactic_arg | term diff --git a/doc/tools/docgram/prodn.edit_mlg b/doc/tools/docgram/prodn.edit_mlg deleted file mode 100644 index 37197a1fec..0000000000 --- a/doc/tools/docgram/prodn.edit_mlg +++ /dev/null @@ -1,24 +0,0 @@ -(************************************************************************) -(* * 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 - -(* todo: doesn't work, gives -ltac_match: @match_key @ltac_expr with {? %| } {+| @ltac_expr } end -instead of -ltac_match: @match_key @ltac_expr with {? %| } {+| {| @match_pattern | _ } => @ltac_expr } end - -SPLICE: [ -| match_rule -] -*) diff --git a/doc/tools/docgram/productionlist.edit_mlg b/doc/tools/docgram/productionlist.edit_mlg deleted file mode 100644 index 93eb38d1a0..0000000000 --- a/doc/tools/docgram/productionlist.edit_mlg +++ /dev/null @@ -1,14 +0,0 @@ -(************************************************************************) -(* * 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 |