diff options
Diffstat (limited to 'doc/tools/docgram/common.edit_mlg')
| -rw-r--r-- | doc/tools/docgram/common.edit_mlg | 573 |
1 files changed, 248 insertions, 325 deletions
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index f9aba5b1e1..f6a684bbd7 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -28,15 +28,15 @@ strategy_level_or_var: [ | strategy_level ] -operconstr0: [ -| "ltac" ":" "(" tactic_expr5 ")" +term0: [ +| "ltac" ":" "(" ltac_expr5 ")" ] EXTRAARGS_natural: [ | DELETENT ] EXTRAARGS_lconstr: [ | DELETENT ] EXTRAARGS_strategy_level: [ | DELETENT ] G_LTAC_hint: [ | DELETENT ] -G_LTAC_operconstr0: [ | DELETENT ] +G_LTAC_term0: [ | DELETENT ] G_REWRITE_binders: [ | DELETE Pcoq.Constr.binders @@ -86,7 +86,7 @@ RENAME: [ | G_LTAC2_eqn_ipat ltac2_eqn_ipat | G_LTAC2_conversion ltac2_conversion | G_LTAC2_oriented_rewriter ltac2_oriented_rewriter -| G_LTAC2_tactic_then_gen ltac2_tactic_then_gen +| G_LTAC2_for_each_goal ltac2_for_each_goal | G_LTAC2_tactic_then_last ltac2_tactic_then_last | G_LTAC2_as_name ltac2_as_name | G_LTAC2_as_ipat ltac2_as_ipat @@ -94,18 +94,22 @@ RENAME: [ | G_LTAC2_match_list ltac2_match_list ] -(* renames to eliminate qualified names - put other renames at the end *) +(* Renames to eliminate qualified names. + Put other renames at the end *) RENAME: [ (* map missing names for rhs *) | Constr.constr term | Constr.global global | Constr.lconstr lconstr -| Constr.lconstr_pattern cpattern +| Constr.cpattern cpattern | G_vernac.query_command query_command | G_vernac.section_subset_expr section_var_expr | Prim.ident ident | Prim.reference reference +| Prim.string string +| Prim.integer integer +| Prim.qualid qualid +| Prim.natural natural | Pvernac.Vernac_.main_entry vernac_control | Tactic.tactic tactic @@ -117,7 +121,7 @@ RENAME: [ | Prim.identref ident | Prim.natural natural *) -| Vernac.rec_definition rec_definition +| Vernac.fix_definition fix_definition (* todo: hmm, rename adds 1 prodn to closed_binder?? *) | Constr.closed_binder closed_binder ] @@ -183,19 +187,19 @@ DELETE: [ (* additional nts to be spliced *) tactic_then_last: [ -| REPLACE "|" LIST0 ( OPT tactic_expr5 ) SEP "|" -| WITH LIST0 ( "|" ( OPT tactic_expr5 ) ) +| REPLACE "|" LIST0 ( OPT ltac_expr5 ) SEP "|" +| WITH LIST0 ( "|" ( OPT ltac_expr5 ) ) ] goal_tactics: [ -| LIST0 ( OPT tactic_expr5 ) SEP "|" +| LIST0 ( OPT ltac_expr5 ) SEP "|" ] -tactic_then_gen: [ | DELETENT ] +for_each_goal: [ | DELETENT ] -tactic_then_gen: [ +for_each_goal: [ | goal_tactics -| OPT ( goal_tactics "|" ) OPT tactic_expr5 ".." OPT ( "|" goal_tactics ) +| OPT ( goal_tactics "|" ) OPT ltac_expr5 ".." OPT ( "|" goal_tactics ) ] tactic_then_last: [ @@ -203,19 +207,19 @@ tactic_then_last: [ ] ltac2_tactic_then_last: [ -| REPLACE "|" LIST0 ( OPT tac2expr6 ) SEP "|" (* Ltac2 plugin *) -| WITH LIST0 ( "|" OPT tac2expr6 ) TAG Ltac2 +| REPLACE "|" LIST0 ( OPT ltac2_expr6 ) SEP "|" (* Ltac2 plugin *) +| WITH LIST0 ( "|" OPT ltac2_expr6 ) TAG Ltac2 ] ltac2_goal_tactics: [ -| LIST0 ( OPT tac2expr6 ) SEP "|" TAG Ltac2 +| LIST0 ( OPT ltac2_expr6 ) SEP "|" TAG Ltac2 ] -ltac2_tactic_then_gen: [ | DELETENT ] +ltac2_for_each_goal: [ | DELETENT ] -ltac2_tactic_then_gen: [ +ltac2_for_each_goal: [ | ltac2_goal_tactics TAG Ltac2 -| OPT ( ltac2_goal_tactics "|" ) OPT tac2expr6 ".." OPT ( "|" ltac2_goal_tactics ) TAG Ltac2 +| OPT ( ltac2_goal_tactics "|" ) OPT ltac2_expr6 ".." OPT ( "|" ltac2_goal_tactics ) TAG Ltac2 ] ltac2_tactic_then_last: [ @@ -257,45 +261,40 @@ let_type_cstr: [ | type_cstr ] -(* rename here because we want to use "return_type" for something else *) -RENAME: [ -| return_type as_return_type -] - case_item: [ -| REPLACE operconstr100 OPT [ "as" name ] OPT [ "in" pattern200 ] -| WITH operconstr100 OPT ("as" name) OPT [ "in" pattern200 ] +| REPLACE term100 OPT [ "as" name ] OPT [ "in" pattern200 ] +| WITH term100 OPT ("as" name) OPT [ "in" pattern200 ] ] binder_constr: [ -| MOVETO term_forall_or_fun "forall" open_binders "," operconstr200 -| MOVETO term_forall_or_fun "fun" open_binders "=>" operconstr200 -| MOVETO term_let "let" name binders let_type_cstr ":=" operconstr200 "in" operconstr200 -| MOVETO term_if "if" operconstr200 as_return_type "then" operconstr200 "else" operconstr200 -| MOVETO term_fix "let" "fix" fix_decl "in" operconstr200 -| MOVETO term_cofix "let" "cofix" cofix_decl "in" operconstr200 -| MOVETO term_let "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" 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 +| MOVETO term_forall_or_fun "forall" open_binders "," term200 +| MOVETO term_forall_or_fun "fun" open_binders "=>" term200 +| MOVETO term_let "let" name binders let_type_cstr ":=" term200 "in" term200 +| MOVETO term_if "if" term200 as_return_type "then" term200 "else" term200 +| MOVETO term_fix "let" "fix" fix_decl "in" term200 +| MOVETO term_cofix "let" "cofix" cofix_body "in" term200 +| MOVETO term_let "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" term200 "in" term200 +| MOVETO term_let "let" "'" pattern200 ":=" term200 "in" term200 +| MOVETO term_let "let" "'" pattern200 ":=" term200 case_type "in" term200 +| MOVETO term_let "let" "'" pattern200 "in" pattern200 ":=" term200 case_type "in" term200 | MOVETO term_fix "fix" fix_decls | MOVETO term_cofix "cofix" cofix_decls ] 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 +| REPLACE "let" name binders let_type_cstr ":=" term200 "in" term200 +| WITH "let" name let_type_cstr ":=" term200 "in" term200 +| "let" name LIST1 binder let_type_cstr ":=" term200 "in" term200 (* Don't need to document that "( )" is equivalent to "()" *) -| REPLACE "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" operconstr200 "in" operconstr200 -| WITH "let" "(" LIST0 name SEP "," ")" as_return_type ":=" 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 +| REPLACE "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" term200 "in" term200 +| WITH "let" "(" LIST0 name SEP "," ")" as_return_type ":=" term200 "in" term200 +| REPLACE "let" "'" pattern200 ":=" term200 "in" term200 +| WITH "let" "'" pattern200 ":=" term200 OPT case_type "in" term200 +| DELETE "let" "'" pattern200 ":=" term200 case_type "in" term200 ] atomic_constr: [ -| MOVETO qualid_annotated global univ_instance +| MOVETO qualid_annotated global univ_annot | MOVETO primitive_notations NUMBER | MOVETO primitive_notations string | MOVETO term_evar "_" @@ -308,9 +307,9 @@ atomic_constr: [ | MOVETO term_evar pattern_ident evar_instance ] -tactic_expr0: [ -| REPLACE "[" ">" tactic_then_gen "]" -| WITH "[>" tactic_then_gen "]" +ltac_expr0: [ +| REPLACE "[" ">" for_each_goal "]" +| WITH "[>" for_each_goal "]" ] (* lexer token *) @@ -337,68 +336,68 @@ scope_delimiter: [ ] type: [ -| operconstr200 +| term200 ] -operconstr100: [ -| REPLACE operconstr99 "<:" operconstr200 -| WITH operconstr99 "<:" type -| MOVETO term_cast operconstr99 "<:" type -| REPLACE operconstr99 "<<:" operconstr200 -| WITH operconstr99 "<<:" type -| MOVETO term_cast operconstr99 "<<:" type -| REPLACE operconstr99 ":" operconstr200 -| WITH operconstr99 ":" type -| MOVETO term_cast operconstr99 ":" type -| MOVETO term_cast operconstr99 ":>" +term100: [ +| REPLACE term99 "<:" term200 +| WITH term99 "<:" type +| MOVETO term_cast term99 "<:" type +| REPLACE term99 "<<:" term200 +| WITH term99 "<<:" type +| MOVETO term_cast term99 "<<:" type +| REPLACE term99 ":" term200 +| WITH term99 ":" type +| MOVETO term_cast term99 ":" type +| MOVETO term_cast term99 ":>" ] constr: [ -| REPLACE "@" global univ_instance +| REPLACE "@" global univ_annot | WITH "@" qualid_annotated | MOVETO term_explicit "@" qualid_annotated ] -operconstr10: [ +term10: [ (* Separate this LIST0 in the nonempty and the empty case *) (* The empty case is covered by constr *) -| REPLACE "@" global univ_instance LIST0 operconstr9 -| WITH "@" qualid_annotated LIST1 operconstr9 -| REPLACE operconstr9 +| REPLACE "@" global univ_annot LIST0 term9 +| WITH "@" qualid_annotated LIST1 term9 +| REPLACE term9 | WITH constr -| MOVETO term_application operconstr9 LIST1 appl_arg -| MOVETO term_application "@" qualid_annotated LIST1 operconstr9 +| MOVETO term_application term9 LIST1 arg +| MOVETO term_application "@" qualid_annotated LIST1 term9 (* fixme: add in as a prodn somewhere *) | MOVETO dangling_pattern_extension_rule "@" pattern_ident LIST1 identref | DELETE dangling_pattern_extension_rule ] -operconstr9: [ +term9: [ (* @Zimmi48: Special token .. is for use in the Notation command. (see bug_3304.v) *) -| DELETE ".." operconstr0 ".." +| DELETE ".." term0 ".." ] -operconstr1: [ -| REPLACE operconstr0 ".(" global LIST0 appl_arg ")" -| WITH operconstr0 ".(" global LIST0 appl_arg ")" (* huh? *) -| REPLACE operconstr0 "%" IDENT -| WITH operconstr0 "%" scope_key -| MOVETO term_scope operconstr0 "%" scope_key -| MOVETO term_projection operconstr0 ".(" global LIST0 appl_arg ")" -| MOVETO term_projection operconstr0 ".(" "@" global LIST0 ( operconstr9 ) ")" +term1: [ +| REPLACE term0 ".(" global LIST0 arg ")" +| WITH term0 ".(" global LIST0 arg ")" (* huh? *) +| REPLACE term0 "%" IDENT +| WITH term0 "%" scope_key +| MOVETO term_scope term0 "%" scope_key +| MOVETO term_projection term0 ".(" global LIST0 arg ")" +| MOVETO term_projection term0 ".(" "@" global LIST0 ( term9 ) ")" ] -operconstr0: [ +term0: [ (* @Zimmi48: This rule is a hack, according to Hugo, and should not be shown in the manual. *) | DELETE "{" binder_constr "}" | REPLACE "{|" record_declaration bar_cbrace | WITH "{|" LIST0 field_def SEP ";" OPT ";" bar_cbrace | MOVETO term_record "{|" LIST0 field_def SEP ";" OPT ";" bar_cbrace -| MOVETO term_generalizing "`{" operconstr200 "}" -| MOVETO term_generalizing "`(" operconstr200 ")" -| MOVETO term_ltac "ltac" ":" "(" tactic_expr5 ")" -| REPLACE "[" "|" array_elems "|" lconstr type_cstr "|" "]" univ_instance -| WITH "[|" array_elems "|" lconstr type_cstr "|]" univ_instance +| MOVETO term_generalizing "`{" term200 "}" +| MOVETO term_generalizing "`(" term200 ")" +| MOVETO term_ltac "ltac" ":" "(" ltac_expr5 ")" +| REPLACE "[" "|" array_elems "|" lconstr type_cstr "|" "]" univ_annot +| WITH "[|" array_elems "|" lconstr type_cstr "|]" univ_annot ] fix_decls: [ @@ -408,9 +407,9 @@ fix_decls: [ ] cofix_decls: [ -| DELETE cofix_decl -| REPLACE cofix_decl "with" LIST1 cofix_decl SEP "with" "for" identref -| WITH cofix_decl OPT ( LIST1 ( "with" cofix_decl ) "for" identref ) +| DELETE cofix_body +| REPLACE cofix_body "with" LIST1 cofix_body SEP "with" "for" identref +| WITH cofix_body OPT ( LIST1 ( "with" cofix_body ) "for" identref ) ] fields_def: [ @@ -481,11 +480,11 @@ name_colon: [ ] typeclass_constraint: [ -| EDIT ADD_OPT "!" operconstr200 -| REPLACE "{" name "}" ":" [ "!" | ] operconstr200 -| WITH "{" name "}" ":" OPT "!" operconstr200 -| REPLACE name ":" [ "!" | ] operconstr200 -| WITH name ":" OPT "!" operconstr200 +| EDIT ADD_OPT "!" term200 +| REPLACE "{" name "}" ":" [ "!" | ] term200 +| WITH "{" name "}" ":" OPT "!" term200 +| REPLACE name ":" [ "!" | ] term200 +| WITH name ":" OPT "!" term200 ] (* ?? From the grammar, Prim.name seems to be only "_" but ident is also accepted "*) @@ -566,14 +565,14 @@ gallina: [ | [ "Record" | "Structure" ] record_definition LIST0 ( "with" record_definition ) | "Class" record_definition | "Class" singleton_class_definition -| REPLACE "Fixpoint" LIST1 rec_definition SEP "with" -| WITH "Fixpoint" rec_definition LIST0 ( "with" rec_definition ) -| REPLACE "Let" "Fixpoint" LIST1 rec_definition SEP "with" -| WITH "Let" "Fixpoint" rec_definition LIST0 ( "with" rec_definition ) -| REPLACE "CoFixpoint" LIST1 corec_definition SEP "with" -| WITH "CoFixpoint" corec_definition LIST0 ( "with" corec_definition ) -| REPLACE "Let" "CoFixpoint" LIST1 corec_definition SEP "with" -| WITH "Let" "CoFixpoint" corec_definition LIST0 ( "with" corec_definition ) +| REPLACE "Fixpoint" LIST1 fix_definition SEP "with" +| WITH "Fixpoint" fix_definition LIST0 ( "with" fix_definition ) +| REPLACE "Let" "Fixpoint" LIST1 fix_definition SEP "with" +| WITH "Let" "Fixpoint" fix_definition LIST0 ( "with" fix_definition ) +| REPLACE "CoFixpoint" LIST1 cofix_definition SEP "with" +| WITH "CoFixpoint" cofix_definition LIST0 ( "with" cofix_definition ) +| REPLACE "Let" "CoFixpoint" LIST1 cofix_definition SEP "with" +| WITH "Let" "CoFixpoint" cofix_definition LIST0 ( "with" cofix_definition ) | REPLACE "Scheme" LIST1 scheme SEP "with" | WITH "Scheme" scheme LIST0 ( "with" scheme ) ] @@ -582,7 +581,7 @@ finite_token: [ | DELETENT ] -constructor_list_or_record_decl: [ +constructors_or_record: [ | OPTINREF ] @@ -604,7 +603,7 @@ inline: [ | OPTINREF ] -univ_instance: [ +univ_annot: [ | OPTINREF ] @@ -613,15 +612,15 @@ univ_decl: [ | WITH "@{" LIST0 identref OPT "+" OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}" ] -of_type_with_opt_coercion: [ +of_type: [ | DELETENT ] -of_type_with_opt_coercion: [ +of_type: [ | [ ":" | ":>" ] type ] -attribute_value: [ +attr_value: [ | OPTINREF ] @@ -657,14 +656,6 @@ ltac2_branches: [ | OPTINREF ] -RENAME: [ -| red_flag ltac2_red_flag -| red_flags red_flag -] - -RENAME: [ -] - strategy_flag: [ | REPLACE OPT delta_flag | WITH delta_flag @@ -697,8 +688,8 @@ is_module_type: [ ] 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 "Arguments" smart_global LIST0 arg_specs OPT [ "," LIST1 [ LIST0 implicits_alt ] SEP "," ] OPT [ ":" LIST1 args_modifier SEP "," ] +| WITH "Arguments" smart_global LIST0 arg_specs LIST0 [ "," LIST0 implicits_alt ] OPT [ ":" LIST1 args_modifier SEP "," ] | REPLACE "Implicit" "Type" reserv_list | WITH "Implicit" [ "Type" | "Types" ] reserv_list | DELETE "Implicit" "Types" reserv_list @@ -727,11 +718,11 @@ gallina_ext: [ | WITH "Generalizable" [ [ "Variable" | "Variables" ] LIST1 identref | "All" "Variables" | "No" "Variables" ] (* don't show Export for Set, Unset *) -| REPLACE "Export" "Set" option_table option_setting -| WITH "Set" option_table option_setting -| REPLACE "Export" "Unset" option_table -| WITH "Unset" option_table -| REPLACE "Instance" instance_name ":" operconstr200 hint_info [ ":=" "{" record_declaration "}" | ":=" lconstr | ] +| REPLACE "Export" "Set" setting_name option_setting +| WITH "Set" setting_name option_setting +| REPLACE "Export" "Unset" setting_name +| WITH "Unset" setting_name +| REPLACE "Instance" instance_name ":" term200 hint_info [ ":=" "{" record_declaration "}" | ":=" lconstr | ] | WITH "Instance" instance_name ":" type hint_info OPT [ ":=" "{" record_declaration "}" | ":=" lconstr ] | REPLACE "From" global "Require" export_token LIST1 global @@ -822,92 +813,92 @@ DELETE: [ | tactic_then_locality ] -tactic_expr5: [ -(* make these look consistent with use of binder_tactic in other tactic_expr* *) +ltac_expr5: [ +(* make these look consistent with use of binder_tactic in other ltac_expr* *) | DELETE binder_tactic -| DELETE tactic_expr4 -| [ tactic_expr4 | binder_tactic ] +| DELETE ltac_expr4 +| [ ltac_expr4 | binder_tactic ] ] ltac_constructs: [ (* repeated in main ltac grammar - need to create a COPY edit *) -| tactic_expr3 ";" [ tactic_expr3 | binder_tactic ] -| tactic_expr3 ";" "[" tactic_then_gen "]" +| ltac_expr3 ";" [ ltac_expr3 | binder_tactic ] +| ltac_expr3 ";" "[" for_each_goal "]" -| tactic_expr1 "+" [ tactic_expr2 | binder_tactic ] -| tactic_expr1 "||" [ tactic_expr2 | binder_tactic ] +| ltac_expr1 "+" [ ltac_expr2 | binder_tactic ] +| ltac_expr1 "||" [ ltac_expr2 | binder_tactic ] -(* | qualid LIST0 tactic_arg add later due renaming tactic_arg *) +(* | qualid LIST0 tactic_value add later due renaming tactic_value *) -| "[>" tactic_then_gen "]" -| toplevel_selector tactic_expr5 +| "[>" for_each_goal "]" +| toplevel_selector ltac_expr5 ] -tactic_expr4: [ -| REPLACE tactic_expr3 ";" tactic_then_gen "]" -| WITH tactic_expr3 ";" "[" tactic_then_gen "]" -| REPLACE tactic_expr3 ";" binder_tactic -| WITH tactic_expr3 ";" [ tactic_expr3 | binder_tactic ] -| DELETE tactic_expr3 ";" tactic_expr3 +ltac_expr4: [ +| REPLACE ltac_expr3 ";" for_each_goal "]" +| WITH ltac_expr3 ";" "[" for_each_goal "]" +| REPLACE ltac_expr3 ";" binder_tactic +| WITH ltac_expr3 ";" [ ltac_expr3 | binder_tactic ] +| DELETE ltac_expr3 ";" ltac_expr3 ] l3_tactic: [ ] -tactic_expr3: [ -| DELETE "abstract" tactic_expr2 -| REPLACE "abstract" tactic_expr2 "using" ident -| WITH "abstract" tactic_expr2 OPT ( "using" ident ) +ltac_expr3: [ +| DELETE "abstract" ltac_expr2 +| REPLACE "abstract" ltac_expr2 "using" ident +| WITH "abstract" ltac_expr2 OPT ( "using" ident ) | l3_tactic | MOVEALLBUT ltac_builtins | l3_tactic -| tactic_expr2 +| ltac_expr2 ] l2_tactic: [ ] -tactic_expr2: [ -| REPLACE tactic_expr1 "+" binder_tactic -| WITH tactic_expr1 "+" [ tactic_expr2 | binder_tactic ] -| DELETE tactic_expr1 "+" tactic_expr2 -| REPLACE tactic_expr1 "||" binder_tactic -| WITH tactic_expr1 "||" [ tactic_expr2 | binder_tactic ] -| DELETE tactic_expr1 "||" tactic_expr2 -| MOVETO ltac_builtins "tryif" tactic_expr5 "then" tactic_expr5 "else" tactic_expr2 +ltac_expr2: [ +| REPLACE ltac_expr1 "+" binder_tactic +| WITH ltac_expr1 "+" [ ltac_expr2 | binder_tactic ] +| DELETE ltac_expr1 "+" ltac_expr2 +| REPLACE ltac_expr1 "||" binder_tactic +| WITH ltac_expr1 "||" [ ltac_expr2 | binder_tactic ] +| DELETE ltac_expr1 "||" ltac_expr2 +| MOVETO ltac_builtins "tryif" ltac_expr5 "then" ltac_expr5 "else" ltac_expr2 | l2_tactic | DELETE ltac_builtins ] l1_tactic: [ ] -tactic_expr1: [ +ltac_expr1: [ | EDIT match_key ADD_OPT "reverse" "goal" "with" match_context_list "end" | MOVETO simple_tactic match_key OPT "reverse" "goal" "with" match_context_list "end" -| MOVETO simple_tactic match_key tactic_expr5 "with" match_list "end" +| MOVETO simple_tactic match_key ltac_expr5 "with" match_list "end" | REPLACE failkw [ int_or_var | ] LIST0 message_token | WITH failkw OPT int_or_var LIST0 message_token -| REPLACE reference LIST0 tactic_arg_compat -| WITH reference LIST1 tactic_arg_compat +| REPLACE reference LIST0 tactic_arg +| WITH reference LIST1 tactic_arg | l1_tactic | DELETE simple_tactic | MOVEALLBUT ltac_builtins | l1_tactic -| tactic_arg -| reference LIST1 tactic_arg_compat -| tactic_expr0 +| tactic_value +| reference LIST1 tactic_arg +| ltac_expr0 ] (* split match_context_rule *) goal_pattern: [ -| LIST0 match_hyps SEP "," "|-" match_pattern -| "[" LIST0 match_hyps SEP "," "|-" match_pattern "]" +| LIST0 match_hyp SEP "," "|-" match_pattern +| "[" LIST0 match_hyp SEP "," "|-" match_pattern "]" | "_" ] match_context_rule: [ -| DELETE LIST0 match_hyps SEP "," "|-" match_pattern "=>" tactic_expr5 -| DELETE "[" LIST0 match_hyps SEP "," "|-" match_pattern "]" "=>" tactic_expr5 -| DELETE "_" "=>" tactic_expr5 -| goal_pattern "=>" tactic_expr5 +| DELETE LIST0 match_hyp SEP "," "|-" match_pattern "=>" ltac_expr5 +| DELETE "[" LIST0 match_hyp SEP "," "|-" match_pattern "]" "=>" ltac_expr5 +| DELETE "_" "=>" ltac_expr5 +| goal_pattern "=>" ltac_expr5 ] match_context_list: [ @@ -920,10 +911,10 @@ match_list: [ match_rule: [ (* redundant; match_pattern -> term -> _ *) -| DELETE "_" "=>" tactic_expr5 +| DELETE "_" "=>" ltac_expr5 ] -selector_body: [ +selector: [ | REPLACE range_selector_or_nth (* depends on whether range_selector_or_nth is deleted first *) | WITH LIST1 range_selector SEP "," ] @@ -1091,7 +1082,7 @@ simple_tactic: [ | EDIT "psatz_Q" ADD_OPT int_or_var tactic | EDIT "psatz_Z" ADD_OPT int_or_var tactic | REPLACE "subst" LIST1 hyp -| WITH "subst" OPT ( LIST1 hyp ) +| WITH "subst" LIST0 hyp | DELETE "subst" | DELETE "congruence" | DELETE "congruence" natural @@ -1102,18 +1093,18 @@ simple_tactic: [ | REPLACE "show" "ltac" "profile" "cutoff" integer | WITH "show" "ltac" "profile" OPT [ "cutoff" integer | string ] | DELETE "show" "ltac" "profile" string -(* perversely, the mlg uses "tactic3" instead of "tactic_expr3" *) +(* perversely, the mlg uses "tactic3" instead of "ltac_expr3" *) | DELETE "transparent_abstract" tactic3 | REPLACE "transparent_abstract" tactic3 "using" ident -| WITH "transparent_abstract" tactic_expr3 OPT ( "using" ident ) -| REPLACE "typeclasses" "eauto" "bfs" OPT int_or_var "with" LIST1 preident -| WITH "typeclasses" "eauto" OPT "bfs" OPT int_or_var OPT ( "with" LIST1 preident ) +| WITH "transparent_abstract" ltac_expr3 OPT ( "using" ident ) +| "typeclasses" "eauto" OPT "bfs" OPT int_or_var OPT ( "with" LIST1 preident ) +| DELETE "typeclasses" "eauto" "bfs" OPT int_or_var "with" LIST1 preident | DELETE "typeclasses" "eauto" OPT int_or_var "with" LIST1 preident | DELETE "typeclasses" "eauto" "bfs" OPT int_or_var | DELETE "typeclasses" "eauto" OPT int_or_var (* in Tactic Notation: *) | "setoid_replace" constr "with" constr OPT ( "using" "relation" constr ) OPT ( "in" hyp ) - OPT ( "at" LIST1 int_or_var ) OPT ( "by" tactic_expr3 ) + OPT ( "at" LIST1 int_or_var ) OPT ( "by" ltac_expr3 ) ] (* todo: don't use DELETENT for this *) @@ -1168,8 +1159,8 @@ command: [ | "SubClass" ident_decl def_body | REPLACE "Ltac" LIST1 ltac_tacdef_body SEP "with" | WITH "Ltac" ltac_tacdef_body LIST0 ( "with" ltac_tacdef_body ) -| REPLACE "Function" LIST1 function_rec_definition_loc SEP "with" (* funind plugin *) -| WITH "Function" function_rec_definition_loc LIST0 ( "with" function_rec_definition_loc ) (* funind plugin *) +| REPLACE "Function" LIST1 function_fix_definition SEP "with" (* funind plugin *) +| WITH "Function" function_fix_definition LIST0 ( "with" function_fix_definition ) (* 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" @@ -1180,16 +1171,16 @@ command: [ | WITH "Back" OPT natural | REPLACE "Load" [ "Verbose" | ] [ ne_string | IDENT ] | WITH "Load" OPT "Verbose" [ ne_string | IDENT ] -| DELETE "Unset" option_table -| REPLACE "Set" option_table option_setting -| WITH OPT "Export" "Set" option_table (* set flag *) -| REPLACE "Test" option_table "for" LIST1 table_value -| WITH "Test" option_table OPT ( "for" LIST1 table_value ) -| DELETE "Test" option_table +| DELETE "Unset" setting_name +| REPLACE "Set" setting_name option_setting +| WITH OPT "Export" "Set" setting_name (* set flag *) +| REPLACE "Test" setting_name "for" LIST1 table_value +| WITH "Test" setting_name OPT ( "for" LIST1 table_value ) +| DELETE "Test" setting_name (* hide the fact that table names are limited to 2 IDENTs *) | REPLACE "Add" IDENT IDENT LIST1 table_value -| WITH "Add" option_table LIST1 table_value +| WITH "Add" setting_name LIST1 table_value | DELETE "Add" IDENT LIST1 table_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 @@ -1247,7 +1238,7 @@ command: [ (* hide the fact that table names are limited to 2 IDENTs *) | REPLACE "Remove" IDENT IDENT LIST1 table_value -| WITH "Remove" option_table LIST1 table_value +| WITH "Remove" setting_name LIST1 table_value | DELETE "Remove" IDENT LIST1 table_value | DELETE "Restore" "State" IDENT | DELETE "Restore" "State" ne_string @@ -1294,10 +1285,10 @@ command: [ | WITH "Declare" "Scope" scope_name (* odd that these are in command while other notation-related ones are in syntax *) -| REPLACE "Numeral" "Notation" reference reference reference ":" ident numnotoption -| WITH "Numeral" "Notation" reference reference reference ":" scope_name numnotoption -| REPLACE "Number" "Notation" reference reference reference ":" ident numnotoption -| WITH "Number" "Notation" reference reference reference ":" scope_name numnotoption +| REPLACE "Numeral" "Notation" reference reference reference ":" ident numeral_modifier +| WITH "Numeral" "Notation" reference reference reference ":" scope_name numeral_modifier +| REPLACE "Number" "Notation" reference reference reference ":" ident numeral_modifier +| WITH "Number" "Notation" reference reference reference ":" scope_name numeral_modifier | REPLACE "String" "Notation" reference reference reference ":" ident | WITH "String" "Notation" reference reference reference ":" scope_name @@ -1357,7 +1348,7 @@ syntax_modifier: [ | WITH LIST1 IDENT SEP "," "at" level ] -syntax_extension_type: [ +explicit_subentry: [ | REPLACE "strict" "pattern" "at" "level" natural | WITH "strict" "pattern" OPT ( "at" "level" natural ) | DELETE "strict" "pattern" @@ -1367,31 +1358,31 @@ syntax_extension_type: [ | DELETE "constr" (* covered by another prod *) ] -numnotoption: [ +numeral_modifier: [ | OPTINREF ] binder_tactic: [ -| REPLACE "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" tactic_expr5 -| WITH "let" OPT "rec" let_clause LIST0 ( "with" let_clause ) "in" tactic_expr5 +| REPLACE "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" ltac_expr5 +| WITH "let" OPT "rec" let_clause LIST0 ( "with" let_clause ) "in" ltac_expr5 | MOVEALLBUT ltac_builtins ] -record_binder_body: [ -| REPLACE binders of_type_with_opt_coercion lconstr -| WITH binders of_type_with_opt_coercion -| REPLACE binders of_type_with_opt_coercion lconstr ":=" lconstr -| WITH binders of_type_with_opt_coercion ":=" lconstr +field_body: [ +| REPLACE binders of_type lconstr +| WITH binders of_type +| REPLACE binders of_type lconstr ":=" lconstr +| WITH binders of_type ":=" lconstr ] -simple_assum_coe: [ -| REPLACE LIST1 ident_decl of_type_with_opt_coercion lconstr -| WITH LIST1 ident_decl of_type_with_opt_coercion +assumpt: [ +| REPLACE LIST1 ident_decl of_type lconstr +| WITH LIST1 ident_decl of_type ] constructor_type: [ -| REPLACE binders [ of_type_with_opt_coercion lconstr | ] -| WITH binders OPT of_type_with_opt_coercion +| REPLACE binders [ of_type lconstr | ] +| WITH binders OPT of_type ] (* todo: is this really correct? Search for "Pvernac.register_proof_mode" *) @@ -1435,12 +1426,12 @@ legacy_attr: [ sentence: [ ] (* productions defined below *) -rec_definition: [ +fix_definition: [ | REPLACE ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notations | WITH ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notations ] -corec_definition: [ +cofix_definition: [ | REPLACE ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notations | WITH ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notations ] @@ -1457,7 +1448,7 @@ inductive_definition: [ ] (* note that constructor -> identref constructor_type *) -constructor_list_or_record_decl: [ +constructors_or_record: [ | DELETE "|" LIST1 constructor SEP "|" | REPLACE identref constructor_type "|" LIST1 constructor SEP "|" | WITH OPT "|" LIST1 constructor SEP "|" @@ -1468,8 +1459,8 @@ constructor_list_or_record_decl: [ ] record_binder: [ -| REPLACE name record_binder_body -| WITH name OPT record_binder_body +| REPLACE name field_body +| WITH name OPT field_body | DELETE name ] @@ -1636,7 +1627,7 @@ ltac2_rewriter: [ | OPT natural OPT [ "?" | "!" ] ltac2_constr_with_bindings ] -tac2expr0: [ +ltac2_expr0: [ | DELETE "(" ")" ] @@ -1813,9 +1804,9 @@ input_fun: [ ] let_clause: [ -| DELETE identref ":=" tactic_expr5 -| REPLACE "_" ":=" tactic_expr5 -| WITH name ":=" tactic_expr5 +| DELETE identref ":=" ltac_expr5 +| REPLACE "_" ":=" ltac_expr5 +| WITH name ":=" ltac_expr5 ] tactic_mode: [ @@ -1837,11 +1828,11 @@ tactic_mode: [ tactic_mode: [ | DELETENT ] -sexpr: [ +ltac2_scope: [ | REPLACE syn_node (* Ltac2 plugin *) | WITH name TAG Ltac2 -| REPLACE syn_node "(" LIST1 sexpr SEP "," ")" (* Ltac2 plugin *) -| WITH name "(" LIST1 sexpr SEP "," ")" TAG Ltac2 +| REPLACE syn_node "(" LIST1 ltac2_scope SEP "," ")" (* Ltac2 plugin *) +| WITH name "(" LIST1 ltac2_scope SEP "," ")" TAG Ltac2 ] syn_node: [ | DELETENT ] @@ -1851,7 +1842,7 @@ RENAME: [ ] toplevel_selector: [ -| selector_body +| selector | "all" | "!" (* par is accepted even though it's not in the .mlg *) @@ -1859,7 +1850,7 @@ toplevel_selector: [ ] toplevel_selector_temp: [ -| DELETE selector_body ":" +| DELETE selector ":" | DELETE "all" ":" | DELETE "!" ":" | toplevel_selector ":" @@ -1900,7 +1891,7 @@ query_command: [ ] (* re-add as a placeholder *) sentence: [ | OPT attributes command "." | OPT attributes OPT ( natural ":" ) query_command "." -| OPT attributes OPT ( toplevel_selector ":" ) tactic_expr5 [ "." | "..." ] +| OPT attributes OPT ( toplevel_selector ":" ) ltac_expr5 [ "." | "..." ] | control_command ] @@ -1924,18 +1915,18 @@ ltac_defined_tactics: [ | "split_Rabs" | "split_Rmult" | "tauto" -| "time_constr" tactic_expr5 +| "time_constr" ltac_expr5 | "zify" ] (* todo: need careful review; assume that "[" ... "]" are literals *) tactic_notation_tactics: [ -| "assert_fails" tactic_expr3 -| "assert_succeeds" tactic_expr3 +| "assert_fails" ltac_expr3 +| "assert_succeeds" ltac_expr3 | "field" OPT ( "[" LIST1 constr "]" ) | "field_simplify" OPT ( "[" LIST1 constr "]" ) LIST1 constr OPT ( "in" ident ) | "field_simplify_eq" OPT ( "[" LIST1 constr "]" ) OPT ( "in" ident ) -| "intuition" OPT tactic_expr5 +| "intuition" OPT ltac_expr5 | "nsatz" OPT ( "with" "radicalmax" ":=" constr "strategy" ":=" constr "parameters" ":=" constr "variables" ":=" constr ) | "psatz" constr OPT int_or_var | "ring" OPT ( "[" LIST1 constr "]" ) @@ -1943,8 +1934,8 @@ tactic_notation_tactics: [ ] (* defined in OCaml outside of mlgs *) -tactic_arg: [ -| "uconstr" ":" "(" operconstr200 ")" +tactic_value: [ +| "uconstr" ":" "(" term200 ")" | MOVEALLBUT simple_tactic ] @@ -1952,10 +1943,6 @@ nonterminal: [ ] value_tactic: [ ] -RENAME: [ -| tactic_arg tactic_value -] - syn_value: [ | IDENT; ":" "(" nonterminal ")" ] @@ -1974,8 +1961,8 @@ ltac2_match_key: [ ] ltac2_constructs: [ -| ltac2_match_key tac2expr6 "with" ltac2_match_list "end" -| ltac2_match_key OPT "reverse" "goal" "with" gmatch_list "end" +| ltac2_match_key ltac2_expr6 "with" ltac2_match_list "end" +| ltac2_match_key OPT "reverse" "goal" "with" goal_match_list "end" ] simple_tactic: [ @@ -1987,9 +1974,9 @@ simple_tactic: [ ] tacdef_body: [ -| REPLACE global LIST1 input_fun ltac_def_kind tactic_expr5 -| WITH global LIST0 input_fun ltac_def_kind tactic_expr5 -| DELETE global ltac_def_kind tactic_expr5 +| REPLACE global LIST1 input_fun ltac_def_kind ltac_expr5 +| WITH global LIST0 input_fun ltac_def_kind ltac_expr5 +| DELETE global ltac_def_kind ltac_expr5 ] tac2def_typ: [ @@ -2071,7 +2058,7 @@ atomic_tac2pat: [ | OPTINREF ] -tac2expr0: [ +ltac2_expr0: [ (* | DELETE "(" ")" (* covered by "()" prodn *) | REPLACE "{" [ | LIST1 tac2rec_fieldexpr OPT ";" ] "}" @@ -2084,13 +2071,13 @@ tac2expr0: [ use LIST1? *) SPLICE: [ -| tac2expr4 +| ltac2_expr4 ] -tac2expr3: [ -| REPLACE tac2expr2 "," LIST1 tac2expr2 SEP "," (* Ltac2 plugin *) -| WITH LIST1 tac2expr2 SEP "," TAG Ltac2 -| DELETE tac2expr2 (* Ltac2 plugin *) +ltac2_expr3: [ +| REPLACE ltac2_expr2 "," LIST1 ltac2_expr2 SEP "," (* Ltac2 plugin *) +| WITH LIST1 ltac2_expr2 SEP "," TAG Ltac2 +| DELETE ltac2_expr2 (* Ltac2 plugin *) ] tac2rec_fieldexprs: [ @@ -2171,7 +2158,7 @@ ltac2_entry: [ | WITH "Ltac2" tac2def_val | REPLACE tac2def_ext (* Ltac2 plugin *) | WITH "Ltac2" tac2def_ext -| "Ltac2" "Notation" [ string | lident ] ":=" tac2expr6 TAG Ltac2 (* variant *) +| "Ltac2" "Notation" [ string | lident ] ":=" ltac2_expr6 TAG Ltac2 (* variant *) | MOVEALLBUT command (* todo: MOVEALLBUT should ignore tag on "but" prodns *) ] @@ -2207,21 +2194,14 @@ SPLICE: [ | anti ] -tac2expr5: [ -| REPLACE "let" OPT "rec" LIST1 ltac2_let_clause SEP "with" "in" tac2expr6 (* Ltac2 plugin *) -| WITH "let" OPT "rec" ltac2_let_clause LIST0 ( "with" ltac2_let_clause ) "in" tac2expr6 TAG Ltac2 -| MOVETO simple_tactic "match" tac2expr5 "with" OPT ltac2_branches "end" (* Ltac2 plugin *) +ltac2_expr5: [ +| REPLACE "let" OPT "rec" LIST1 ltac2_let_clause SEP "with" "in" ltac2_expr6 (* Ltac2 plugin *) +| WITH "let" OPT "rec" ltac2_let_clause LIST0 ( "with" ltac2_let_clause ) "in" ltac2_expr6 TAG Ltac2 +| MOVETO simple_tactic "match" ltac2_expr5 "with" OPT ltac2_branches "end" (* Ltac2 plugin *) | DELETE simple_tactic ] -RENAME: [ -| Prim.string string -| Prim.integer integer -| Prim.qualid qualid -| Prim.natural natural -] - -gmatch_list: [ +goal_match_list: [ | EDIT ADD_OPT "|" LIST1 gmatch_rule SEP "|" (* Ltac2 plugin *) ] @@ -2290,6 +2270,10 @@ subprf: [ | "{" (* should be removed. See https://github.com/coq/coq/issues/12004 *) ] +ltac2_expr: [ +| DELETE _ltac2_expr +] + SPLICE: [ | clause | noedit_mode @@ -2309,10 +2293,10 @@ SPLICE: [ | ltac_selector | Constr.ident | attribute_list -| operconstr99 -| operconstr90 -| operconstr9 -| operconstr8 +| term99 +| term90 +| term9 +| term8 | pattern200 | pattern99 | pattern90 @@ -2363,7 +2347,7 @@ SPLICE: [ | check_module_types | constr_pattern | decl_sep -| function_rec_definition_loc (* loses funind annotation *) +| function_fix_definition (* loses funind annotation *) | glob | glob_constr_with_bindings | id_or_meta @@ -2381,7 +2365,6 @@ SPLICE: [ | decorated_vernac | ext_module_expr | ext_module_type -| pattern_ident | test | binder_constr | atomic_constr @@ -2449,7 +2432,6 @@ SPLICE: [ | intropatterns | instance_name | failkw -| selector | ne_in_or_out_modules | search_queries | locatable @@ -2472,7 +2454,6 @@ SPLICE: [ | refglobals (* Ltac2 *) | syntax_modifiers | array_elems -| ltac2_expr | G_LTAC2_input_fun | ltac2_simple_intropattern_closed | ltac2_with_bindings @@ -2489,81 +2470,33 @@ RENAME: [ | 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 *) -| ltac1_expr ltac_expr -| tactic_expr5 ltac_expr -| tactic_expr4 ltac_expr4 -| tactic_expr3 ltac_expr3 -| tactic_expr2 ltac_expr2 -| tactic_expr1 ltac_expr1 -| tactic_expr0 ltac_expr0 +| ltac_expr5 ltac_expr (* | nonsimple_intropattern intropattern (* ltac2 *) *) -| operconstr200 term (* historical name *) -| operconstr100 term100 -| operconstr10 term10 -| operconstr1 term1 -| operconstr0 term0 +| term200 term | pattern100 pattern -| match_constr term_match (*| impl_ident_tail impl_ident*) | ssexpr50 section_var_expr50 | ssexpr0 section_var_expr0 | section_subset_expr section_var_expr | fun_scheme_arg func_scheme_def -| tactic_then_gen for_each_goal -| ltac2_tactic_then_gen ltac2_for_each_goal -| selector_body selector -| match_hyps match_hyp - | BULLET bullet -| fix_decl fix_body -| cofix_decl cofix_body -(* todo: it's confusing that Constr.constr and constr mean different things *) -| constr one_term -| appl_arg arg -| rec_definition fix_definition -| corec_definition cofix_definition -| univ_instance univ_annot -| simple_assum_coe assumpt -| of_type_with_opt_coercion of_type -| attribute_value attr_value -| constructor_list_or_record_decl constructors_or_record -| record_binder_body field_body -| class_rawexpr class -| smart_global reference +| constr one_term (* many, many, many *) +| class_rawexpr class (* OCaml reserved word *) +| smart_global reference (* many, many *) (* | searchabout_query search_item *) -| option_table setting_name -| argument_spec_block arg_specs -| more_implicits_block implicits_alt -| arguments_modifier args_modifier -| constr_as_binder_kind binder_interp -| syntax_extension_type explicit_subentry -| numnotoption numeral_modifier -| tactic_arg_compat tactic_arg -| lconstr_pattern cpattern -| Pltac.tactic ltac_expr -| sexpr ltac2_scope -| tac2type5 ltac2_type -| tac2type2 ltac2_type2 -| tac2type1 ltac2_type1 -| tac2type0 ltac2_type0 -| typ_param ltac2_typevar -| tac2expr6 ltac2_expr -| tac2expr5 ltac2_expr5 -| tac2expr3 ltac2_expr3 -| tac2expr2 ltac2_expr2 -| tac2expr1 ltac2_expr1 -| tac2expr0 ltac2_expr0 -| gmatch_list goal_match_list +| Pltac.tactic ltac_expr (* many uses in EXTENDs *) +| ltac2_type5 ltac2_type +| ltac2_expr6 ltac2_expr | starredidentref starred_ident_ref ] simple_tactic: [ -(* due to renaming of tactic_arg; Use LIST1 for function application *) +(* due to renaming of tactic_value; Use LIST1 for function application *) | qualid LIST1 tactic_arg ] @@ -2585,7 +2518,7 @@ SPLICE: [ | ltac_defined_tactics | tactic_notation_tactics ] -(* todo: ssrreflect*.rst ref to fix_body is incorrect *) +(* todo: ssrreflect*.rst ref to fix_decl is incorrect *) REACHABLE: [ | command @@ -2624,17 +2557,7 @@ NOTINRSTS: [ | q_constr_matching | q_goal_matching -(* todo: figure these out -(*Warning: editedGrammar: Undefined symbol 'ltac1_expr' *) -| dangling_pattern_extension_rule -| vernac_aux -| subprf -| tactic_mode -| tac2expr_in_env (* no refs *) -| tac2mode (* no refs *) -| ltac_use_default (* from tac2mode *) -| tacticals -*) + ] REACHABLE: [ |