Update grammar in the Terms section of Gallina chapter

Update doc_grammar tool

The grammar in the doc is generated semi-automatically with doc_grammar:
- the grammar is automatically extracted from the mlg files
- developer-prepared editing scripts *.mlg_edit modify the extracted
  grammar for clarity, simplicity and ordering of productions
- chunks of the resulting grammar are automatically inserted into the
  rsts using instructions embedded in the rsts

Running doc_grammar is currently a manual step.

The grammar updates in the rst files have been manually reviewed.

1 files changed, 588 insertions, 85 deletions

diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index ea94e21ff3..06b49a0a18 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -12,41 +12,10 @@
 
 DOC_GRAMMAR
 
-(* additional nts to be spliced *)
-
-LEFTQMARK: [
-| "?"
-]
-
-SPLICE: [
-| LEFTQMARK
-]
-
-hyp: [
-| var
-]
-
-tactic_then_gen: [
-| EDIT ADD_OPT tactic_expr5 "|" tactic_then_gen
-| EDIT ADD_OPT tactic_expr5 ".." tactic_then_last
-]
-
-SPLICE: [
-| hyp
-| identref
-| pattern_ident (* depends on previous LEFTQMARK splice todo: improve *)
-| constr_eval  (* splices as multiple prods *)
-| tactic_then_last  (* todo: dependency on c.edit_mlg edit?? really useful? *)
-| Prim.name
-| ltac_selector
-| Constr.ident
-| tactic_then_locality  (* todo: cleanup *)
-| attribute_list
-]
-
+(* renames to eliminate qualified names
+   put other renames at the end *)
 RENAME: [
   (* map missing names for rhs *)
-| _binders binders
 | Constr.constr term
 | Constr.constr_pattern constr_pattern
 | Constr.global global
@@ -54,58 +23,52 @@ RENAME: [
 | Constr.lconstr_pattern lconstr_pattern
 | G_vernac.query_command query_command
 | G_vernac.section_subset_expr section_subset_expr
-| nonsimple_intropattern intropattern
 | Pltac.tactic tactic
-| Pltac.tactic_expr ltac_expr
+| Pltac.tactic_expr tactic_expr5
 | Prim.ident ident
 | Prim.reference reference
 | Pvernac.Vernac_.main_entry vernac_control
 | Tactic.tactic tactic
-| tactic3 ltac_expr3  (* todo: can't figure out how this gets mapped by coqpp *)
-| tactic1 ltac_expr1  (* todo: can't figure out how this gets mapped by coqpp *)
-| tactic0 ltac_expr0  (* todo: can't figure out how this gets mapped by coqpp *)
-| tactic_expr5 ltac_expr
-| tactic_expr4 ltac_expr4
-| tactic_expr3 ltac_expr3
-| tactic_expr2 ltac_expr2
-| tactic_expr1 ltac_expr1
-| tactic_expr0 ltac_expr0
-
-  (* elementary renaming/OCaml-defined productions *)
-| clause clause_dft_concl
-| in_clause' in_clause
-| l_constr lconstr  (* todo: should delete the production *)
 
   (* SSR *)
+(*
 | G_vernac.def_body def_body
 | Pcoq.Constr.constr term
 | Prim.by_notation by_notation
 | Prim.identref ident
 | Prim.natural natural
+*)
 | Vernac.rec_definition rec_definition
 
-  (* rename on lhs *)
-| intropatterns intropattern_list_opt
 | Constr.closed_binder closed_binder
+]
 
-  (* historical name *)
-| constr term
+(* written in OCaml *)
+impl_ident_head: [
+| "{" ident
 ]
 
+lpar_id_coloneq: [
+| "(" ident; ":="
+]
+
+(* lookahead symbols *)
 DELETE: [
 | check_for_coloneq
-| impl_ident_head
 | local_test_lpar_id_colon
 | lookup_at_as_comma
 | only_starredidentrefs
 | test_bracket_ident
-| test_lpar_id_coloneq
+| test_lpar_id_colon
+| test_lpar_id_coloneq  (* todo: grammar seems incorrect, repeats the "(" IDENT ":=" *)
 | test_lpar_id_rpar
 | test_lpar_idnum_coloneq
+| test_nospace_pipe_closedcurly
 | test_show_goal
 
   (* SSR *)
 (* | ssr_null_entry *)
+(*
 | ssrtermkind  (* todo: rename as "test..." *)
 | term_annotation  (* todo: rename as "test..." *)
 | test_idcomma
@@ -122,48 +85,410 @@ DELETE: [
 | test_ident_no_do
 | ssrdoarg  (* todo: this and the next one should be removed from the grammar? *)
 | ssrseqdir
+*)
+
+(* unused *)
+| constr_comma_sequence'
+| auto_using'
+| constr_may_eval
 ]
 
-ident: [
-| DELETE IDENT ssr_null_entry
+(* ssrintrosarg: [ | DELETENT ] *)
+
+(* additional nts to be spliced *)
+
+hyp: [
+| var
 ]
 
-natural: [
-| DELETE _natural
+empty: [
+|
 ]
 
+or_opt: [
+| "|"
+| empty
+]
 
-  (* added productions *)
+ltac_expr_opt: [
+| tactic_expr5
+| empty
+]
 
-empty: [  (* todo: (bug) this is getting converted to empty -> empty *)
-|
+ltac_expr_opt_list_or: [
+| ltac_expr_opt_list_or "|" ltac_expr_opt
+| ltac_expr_opt
 ]
 
-lpar_id_coloneq: [
-| "(" IDENT; ":="
+tactic_then_gen: [
+| EDIT ADD_OPT tactic_expr5 "|" tactic_then_gen
+| EDIT ADD_OPT tactic_expr5 ".." tactic_then_last
+| REPLACE OPT tactic_expr5 ".." tactic_then_last
+| WITH ltac_expr_opt ".." or_opt ltac_expr_opt_list_or
 ]
 
-name_colon: [
-| IDENT; ":"
-| "_" ":"  (* todo: should "_" be a keyword or an identifier? *)
+ltac_expr_opt_list_or: [
+| ltac_expr_opt_list_or "|" OPT tactic_expr5
+| OPT tactic_expr5
 ]
 
-int: [ (* todo: probably should be NUMERAL *)
-| integer
+reference: [ | DELETENT ]
+
+reference: [
+| qualid
 ]
 
-command_entry: [
-| noedit_mode
+fullyqualid: [ | DELETENT ]
+
+fullyqualid: [
+| qualid
+]
+
+
+field: [ | DELETENT ]
+
+field: [
+| "." ident
+]
+
+basequalid: [
+| REPLACE ident fields
+| WITH qualid field
+]
+
+fields: [ | DELETENT ]
+
+dirpath: [
+| REPLACE ident LIST0 field
+| WITH ident
+| dirpath field
 ]
 
 binders: [
 | DELETE Pcoq.Constr.binders  (* todo: not sure why there are 2 "binders:" *)
 ]
 
-(* edits to simplify *)
+lconstr: [
+| DELETE l_constr
+]
+
+let_type_cstr: [
+| DELETE OPT [ ":" lconstr ]
+| rec_type_cstr
+]
+
+as_name_opt: [
+| "as" name
+| empty
+]
+
+(* rename here because we want to use "return_type" for something else *)
+RENAME: [
+| return_type as_return_type_opt
+]
+
+as_return_type_opt: [
+| REPLACE OPT [ OPT [ "as" name ] case_type ]
+| WITH as_name_opt case_type
+| empty
+]
+
+case_item: [
+| REPLACE operconstr100 OPT [ "as" name ] OPT [ "in" pattern200 ]
+| WITH operconstr100 as_name_opt OPT [ "in" pattern200 ]
+]
+
+as_dirpath: [
+| DELETE OPT [ "as" dirpath ]
+| "as" dirpath
+| empty
+]
+
+binder_constr: [
+| MOVETO term_let "let" name binders let_type_cstr ":=" operconstr200 "in" operconstr200
+| MOVETO term_let "let" single_fix "in" operconstr200
+| MOVETO term_let "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type_opt ":=" operconstr200 "in" operconstr200
+| MOVETO term_let "let" "'" pattern200 ":=" operconstr200 "in" operconstr200
+| MOVETO term_let "let" "'" pattern200 ":=" operconstr200 case_type "in" operconstr200
+| MOVETO term_let "let" "'" pattern200 "in" pattern200 ":=" operconstr200 case_type "in" operconstr200
+]
+
+term_let: [
+| REPLACE "let" name binders let_type_cstr ":=" operconstr200 "in" operconstr200
+| WITH "let" name let_type_cstr ":=" operconstr200 "in" operconstr200
+| "let" name LIST1 binder let_type_cstr ":=" operconstr200 "in" operconstr200
+(* Don't need to document that "( )" is equivalent to "()" *)
+| REPLACE "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type_opt ":=" operconstr200 "in" operconstr200
+| WITH "let" [ "(" LIST1 name SEP "," ")" | "()" ] as_return_type_opt ":=" operconstr200 "in" operconstr200
+| REPLACE "let" "'" pattern200 ":=" operconstr200 "in" operconstr200
+| WITH  "let" "'" pattern200 ":=" operconstr200 OPT case_type "in" operconstr200
+| DELETE "let" "'" pattern200 ":=" operconstr200 case_type "in" operconstr200
+]
+
+atomic_constr: [
+(* @Zimmi48: "string" used only for notations, but keep to be consistent with patterns *)
+(* | DELETE string *)
+| REPLACE "?" "[" ident "]"
+| WITH "?[" ident "]"
+| MOVETO term_evar "?[" ident "]"
+| REPLACE "?" "[" pattern_ident "]"
+| WITH "?[" pattern_ident "]"
+| MOVETO term_evar "?[" pattern_ident "]"
+| MOVETO term_evar pattern_ident evar_instance
+]
+
+tactic_expr0: [
+| REPLACE "[" ">" tactic_then_gen "]"
+| WITH "[>" tactic_then_gen "]"
+]
+
+operconstr100: [
+| MOVETO term_cast operconstr99 "<:" operconstr200
+| MOVETO term_cast operconstr99 "<<:" operconstr200
+| MOVETO term_cast operconstr99 ":" operconstr200
+| MOVETO term_cast operconstr99 ":>"
+]
+
+operconstr10: [
+(* fixme: add in as a prodn somewhere *)
+| MOVETO dangling_pattern_extension_rule "@" pattern_identref LIST1 identref
+| DELETE dangling_pattern_extension_rule
+]
+
+operconstr9: [
+(* @Zimmi48: Special token .. is for use in the Notation command. (see bug_3304.v) *)
+| DELETE ".." operconstr0 ".."
+]
+
+arg_list: [
+| arg_list appl_arg
+| appl_arg
+]
+
+arg_list_opt: [
+| arg_list
+| empty
+]
+
+operconstr1: [
+| REPLACE operconstr0 ".(" global LIST0 appl_arg ")"
+| WITH operconstr0 ".(" global arg_list_opt ")"
+| MOVETO term_projection operconstr0 ".(" global arg_list_opt ")"
+| MOVETO term_projection operconstr0 ".(" "@" global LIST0 ( operconstr9 ) ")"
+]
+
+operconstr0: [
+(* @Zimmi48: This rule is a hack, according to Hugo, and should not be shown in the manual. *)
+| DELETE "{" binder_constr "}"
+]
+
+single_fix: [
+| DELETE fix_kw fix_decl
+| "fix" fix_decl
+| "cofix" fix_decl
+]
+
+fix_kw: [ | DELETENT ]
+
+binders_fixannot: [
+(*
+| REPLACE impl_name_head impl_ident_tail binders_fixannot
+| WITH impl_name_head impl_ident_tail "}" binders_fixannot
+*)
+(* Omit this complex detail.  See https://github.com/coq/coq/pull/10614#discussion_r344118146 *)
+| DELETE impl_name_head impl_ident_tail binders_fixannot
+
+| DELETE fixannot
+| DELETE binder binders_fixannot
+| DELETE (* empty *)
+
+| LIST0 binder OPT fixannot
+]
 
-ltac_expr1: [
+impl_ident_tail: [
+| DELETENT
+(*
+| REPLACE "}"
+| WITH empty
+| REPLACE LIST1 name ":" lconstr "}"
+| WITH LIST1 name ":" lconstr
+| REPLACE LIST1 name "}"
+| WITH LIST1 name
+| REPLACE ":" lconstr "}"
+| WITH ":" lconstr
+*)
+]
+
+of_type_with_opt_coercion: [
+| DELETE ":>" ">"
+| DELETE ":" ">" ">"
+| DELETE ":" ">"
+]
+
+binder: [
+| DELETE name
+]
+
+open_binders: [
+| REPLACE name LIST0 name ":" lconstr
+| WITH LIST1 name ":" lconstr
+(* @Zimmi48: Special token .. is for use in the Notation command. (see bug_3304.v) *)
+| DELETE name ".." name
+| REPLACE name LIST0 name binders
+| WITH LIST1 binder
+| DELETE closed_binder binders
+]
+
+closed_binder: [
+| name
+
+| REPLACE "(" name LIST1 name ":" lconstr ")"
+| WITH "(" LIST1 name ":" lconstr ")"
+| DELETE "(" name ":" lconstr ")"
+
+| DELETE "(" name ":=" lconstr ")"
+| REPLACE "(" name ":" lconstr ":=" lconstr ")"
+| WITH "(" name rec_type_cstr ":=" lconstr ")"
+
+| DELETE "{" name LIST1 name "}"
+
+| REPLACE "{" name LIST1 name ":" lconstr "}"
+| WITH "{" LIST1 name rec_type_cstr "}"
+| DELETE "{" name ":" lconstr  "}"
+]
+
+typeclass_constraint: [
+| EDIT ADD_OPT "!" operconstr200
+]
+
+(* ?? From the grammar, Prim.name seems to be only "_" but ident is also accepted "*)
+Prim.name: [
+| REPLACE "_"
+| WITH name
+]
+
+oriented_rewriter: [
+| REPLACE orient_rw rewriter
+| WITH orient rewriter
+]
+
+DELETE: [
+| orient_rw
+]
+
+pattern1_list: [
+| pattern1_list pattern1
+| pattern1
+]
+
+pattern1_list_opt: [
+| pattern1_list
+| empty
+]
+
+pattern10: [
+| REPLACE pattern1 LIST1 pattern1
+| WITH LIST1 pattern1
+| REPLACE "@" reference LIST0 pattern1
+| WITH "@" reference pattern1_list_opt
+]
+
+pattern0: [
+| REPLACE "(" pattern200 ")"
+| WITH "(" LIST1 pattern200 SEP "|" ")"
+| DELETE "(" pattern200 "|" LIST1 pattern200 SEP "|" ")"
+]
+
+patterns_comma: [
+| patterns_comma "," pattern100
+| pattern100
+]
+
+patterns_comma_list_or: [
+| patterns_comma_list_or "|" patterns_comma
+| patterns_comma
+]
+
+eqn: [
+| REPLACE LIST1 mult_pattern SEP "|" "=>" lconstr
+| WITH patterns_comma_list_or "=>" lconstr
+]
+
+record_patterns: [
+| REPLACE record_pattern ";" record_patterns
+| WITH record_patterns ";" record_pattern
+]
+
+(* todo: binders should be binders_opt *)
+
+
+(* lexer stuff *)
+bigint: [
+| DELETE NUMERAL
+| num
+]
+
+ident: [
+| DELETENT
+]
+
+IDENT: [
+| ident
+]
+
+integer: [ | DELETENT ]
+RENAME: [
+| integer int (* todo: review uses in .mlg files, some should be "natural" *)
+]
+
+LEFTQMARK: [
+| "?"
+]
+
+natural: [ | DELETENT ]
+natural: [
+| num  (* todo: or should it be "nat"? *)
+]
+
+NUMERAL: [
+| numeral
+]
+
+(* todo: QUOTATION only used in a test suite .mlg files, is it documented/useful? *)
+
+string: [ | DELETENT ]
+STRING: [
+| string
+]
+
+
+(* todo: is "bigint" useful?? *)
+(* todo: "check_int" in g_prim.mlg should be "check_num" *)
+
+  (* added productions *)
+
+name_colon: [
+| name ":"
+]
+
+command_entry: [
+| noedit_mode
+]
+
+tactic_expr1: [
 | EDIT match_key ADD_OPT "reverse" "goal" "with" match_context_list "end"
+| MOVETO ltac_match_goal match_key OPT "reverse" "goal" "with" match_context_list "end"
+| MOVETO ltac_match_term match_key tactic_expr5 "with" match_list "end"
+]
+
+DELETE: [
+| tactic_then_locality
+]
+
+tactic_expr4: [
+| REPLACE tactic_expr3 ";" tactic_then_gen "]"
+| WITH tactic_expr3 ";" "[" tactic_then_gen "]"
+| tactic_expr3 ";" "[" ">" tactic_then_gen "]"
 ]
 
 match_context_list: [
@@ -180,35 +505,37 @@ match_list: [
 | EDIT ADD_OPT "|" LIST1 match_rule SEP "|"
 ]
 
+match_rule: [
+| REPLACE match_pattern "=>" tactic_expr5
+| WITH [ match_pattern | "_" ] "=>" tactic_expr5
+| DELETE "_" "=>" tactic_expr5
+]
+
 
 selector_body: [
 | REPLACE range_selector_or_nth  (* depends on whether range_selector_or_nth is deleted first *)
 | WITH LIST1 range_selector SEP ","
 ]
 
-range_selector_or_nth: [
-| DELETENT
-]
+range_selector_or_nth: [ | DELETENT ]
 
 simple_tactic: [
 | DELETE "intros"
 | REPLACE "intros" ne_intropatterns
-| WITH "intros" intropattern_list_opt
+| WITH "intros" intropatterns
 | DELETE "eintros"
 | REPLACE "eintros" ne_intropatterns
-| WITH "eintros" intropattern_list_opt
+| WITH "eintros" intropatterns
 ]
 
-intropattern_list_opt: [
+intropatterns: [
 | DELETE LIST0 intropattern
-| intropattern_list_opt intropattern
+| intropatterns intropattern
 | empty
 ]
 
-
-ne_intropatterns: [
-| DELETENT  (* todo: don't use DELETENT for this *)
-]
+(* todo: don't use DELETENT for this *)
+ne_intropatterns: [ | DELETENT ]
 
 
 or_and_intropattern: [
@@ -216,5 +543,181 @@ or_and_intropattern: [
 | DELETE "(" simple_intropattern ")"
 | REPLACE "(" simple_intropattern "," LIST1 simple_intropattern SEP "," ")"
 |   WITH  "(" LIST0 simple_intropattern SEP "," ")"
-| EDIT "[" USE_NT intropattern_or LIST1 intropattern_list_opt SEP "|" "]"
+| EDIT "[" USE_NT intropattern_or LIST1 intropatterns SEP "|" "]"
 ]
+
+bar_cbrace: [
+| REPLACE "|" "}"
+| WITH "|}"
+]
+
+(* todo: is this really correct? Search for "Pvernac.register_proof_mode" *)
+(* consider tactic_command vs tac2mode *)
+vernac_aux: [
+| tactic_mode "."
+]
+
+SPLICE: [
+| noedit_mode
+| command_entry
+| bigint
+| match_list
+| match_context_list
+| IDENT
+| LEFTQMARK
+| natural
+| NUMERAL
+| STRING
+| hyp
+| var
+| identref
+| pattern_ident
+| constr_eval  (* splices as multiple prods *)
+| tactic_then_last  (* todo: dependency on c.edit_mlg edit?? really useful? *)
+| Prim.name
+| ltac_selector
+| Constr.ident
+| attribute_list
+| operconstr99
+| operconstr90
+| operconstr9
+| operconstr8
+| pattern200
+| pattern99
+| pattern90
+| ne_lstring
+| ne_string
+| lstring
+| basequalid
+| fullyqualid
+| global
+| reference
+| bar_cbrace
+| lconstr
+| impl_name_head
+
+(*
+| ast_closure_term
+| ast_closure_lterm
+| ident_no_do
+| ssrterm
+| ssrtacarg
+| ssrtac3arg
+| ssrtclarg
+| ssrhyp
+| ssrhoi_hyp
+| ssrhoi_id
+| ssrindex
+| ssrhpats
+| ssrhpats_nobs
+| ssrfwdid
+| ssrmovearg
+| ssrcasearg
+| ssrrwargs
+| ssrviewposspc
+| ssrpatternarg
+| ssr_elsepat
+| ssr_mpat
+| ssrunlockargs
+| ssrcofixfwd
+| ssrfixfwd
+| ssrhavefwdwbinders
+| ssripats_ne
+| ssrparentacarg
+| ssrposefwd
+*)
+
+| preident
+| lpar_id_coloneq
+| binders
+| casted_constr
+| check_module_types
+| constr_pattern
+| decl_sep
+| function_rec_definition_loc (* loses funind annotation *)
+| glob
+| glob_constr_with_bindings
+| id_or_meta
+| lconstr_pattern
+| lglob
+| ltac_tacdef_body
+| mode
+| mult_pattern
+| open_constr
+| option_table
+| record_declaration
+| register_type_token
+| tactic
+| uconstr
+| impl_ident_head
+| argument_spec
+| at_level
+| branches
+| check_module_type
+| decorated_vernac
+| ext_module_expr
+| ext_module_type
+| pattern_identref
+| test
+| binder_constr
+| atomic_constr
+| let_type_cstr
+| name_colon
+| closed_binder
+| binders_fixannot
+]
+
+RENAME: [
+| clause clause_dft_concl
+| in_clause' in_clause
+
+| tactic3 ltac_expr3  (* todo: can't figure out how this gets mapped by coqpp *)
+| tactic1 ltac_expr1  (* todo: can't figure out how this gets mapped by coqpp *)
+| tactic0 ltac_expr0  (* todo: can't figure out how this gets mapped by coqpp *)
+| tactic_expr5 ltac_expr
+| tactic_expr4 ltac_expr4
+| tactic_expr3 ltac_expr3
+| tactic_expr2 ltac_expr2
+| tactic_expr1 ltac_expr1
+| tactic_expr0 ltac_expr0
+
+(* | nonsimple_intropattern intropattern (* ltac2 *) *)
+| intropatterns intropattern_list_opt
+
+| operconstr200 term   (* historical name *)
+| operconstr100 term100
+| operconstr10 term10
+| operconstr1 term1
+| operconstr0 term0
+| pattern100 pattern
+| match_constr term_match
+(*| impl_ident_tail impl_ident*)
+| ssexpr35 ssexpr (* strange in mlg, ssexpr50 is after this *)
+
+| tactic_then_gen multi_goal_tactics
+| selector only_selector
+| selector_body selector
+| input_fun fun_var
+| match_hyps match_hyp
+
+| BULLET bullet
+| nat_or_var num_or_var
+| fix_decl fix_body
+| instance universe_annot_opt
+| rec_type_cstr colon_term_opt
+| fix_constr term_fix
+| constr term1_extended
+| case_type return_type
+| appl_arg arg
+| record_patterns record_patterns_opt
+| universe_increment universe_increment_opt
+| rec_definition fix_definition
+| corec_definition cofix_definition
+| record_field_instance field_def
+| record_fields_instance fields_def
+| evar_instance evar_bindings_opt
+| inst evar_binding
+]
+
+
+(* todo: ssrreflect*.rst ref to fix_body is incorrect *)