diff options
Diffstat (limited to 'doc/tools')
| -rw-r--r-- | doc/tools/docgram/README.md | 2 | ||||
| -rw-r--r-- | doc/tools/docgram/common.edit_mlg | 727 | ||||
| -rw-r--r-- | doc/tools/docgram/doc_grammar.ml | 84 | ||||
| -rw-r--r-- | doc/tools/docgram/fullGrammar | 568 | ||||
| -rw-r--r-- | doc/tools/docgram/orderedGrammar | 209 |
5 files changed, 779 insertions, 811 deletions
diff --git a/doc/tools/docgram/README.md b/doc/tools/docgram/README.md index 4d38955fa8..dbb04bb6a6 100644 --- a/doc/tools/docgram/README.md +++ b/doc/tools/docgram/README.md @@ -42,7 +42,7 @@ for documentation purposes: First, nonterminals that use levels (`"5" RIGHTA` below) are modified, for example: ``` - tactic_expr: + ltac_expr: [ "5" RIGHTA [ te = binder_tactic -> { te } ] [ "4" ... diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 1e9be8dded..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_subset_expr +| 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 ] @@ -182,24 +186,20 @@ DELETE: [ (* additional nts to be spliced *) -hyp: [ -| var -] - 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: [ @@ -207,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: [ @@ -261,60 +261,55 @@ 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 "_" -| REPLACE "?" "[" ident "]" -| WITH "?[" ident "]" -| MOVETO term_evar "?[" ident "]" +| REPLACE "?" "[" identref "]" +| WITH "?[" identref "]" +| MOVETO term_evar "?[" identref "]" | 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 "]" +ltac_expr0: [ +| REPLACE "[" ">" for_each_goal "]" +| WITH "[>" for_each_goal "]" ] (* lexer token *) @@ -341,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_identref LIST1 identref +| 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: [ @@ -412,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: [ @@ -485,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 "*) @@ -545,7 +540,13 @@ evar_instance: [ (* 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 +| opt_coercion ident_decl binders OPT [ ":" sort ] OPT ( ":=" OPT [ identref ] "{" record_fields "}" ) +] + +(* No mutual recursion, no inductive classes, type must be a sort *) +(* constructor is optional but "Class record_definition" covers that case *) +singleton_class_definition: [ +| opt_coercion ident_decl binders OPT [ ":" sort ] ":=" constructor ] (* No record syntax, opt_coercion not supported for Variant, := ... required *) @@ -562,15 +563,16 @@ gallina: [ | "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 ) -| 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 ) +| "Class" record_definition +| "Class" singleton_class_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 ) ] @@ -579,7 +581,7 @@ finite_token: [ | DELETENT ] -constructor_list_or_record_decl: [ +constructors_or_record: [ | OPTINREF ] @@ -601,7 +603,7 @@ inline: [ | OPTINREF ] -univ_instance: [ +univ_annot: [ | OPTINREF ] @@ -610,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 ] @@ -654,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 @@ -694,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 @@ -713,6 +707,10 @@ gallina_ext: [ | REPLACE "Coercion" by_notation ":" class_rawexpr ">->" class_rawexpr | WITH "Coercion" smart_global ":" class_rawexpr ">->" class_rawexpr +(* semantically restricted per https://github.com/coq/coq/pull/12936#discussion_r492705820 *) +| REPLACE "Coercion" global OPT univ_decl def_body +| WITH "Coercion" ident OPT univ_decl def_body + | REPLACE "Include" "Type" module_type_inl LIST0 ext_module_type | WITH "Include" "Type" LIST1 module_type_inl SEP "<+" @@ -720,12 +718,12 @@ 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 | ] -| WITH "Instance" instance_name ":" operconstr200 hint_info OPT [ ":=" "{" 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 | WITH "From" dirpath "Require" export_token LIST1 global @@ -815,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: [ @@ -913,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 "," ] @@ -1083,8 +1081,8 @@ simple_tactic: [ | 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 ) +| REPLACE "subst" LIST1 hyp +| WITH "subst" LIST0 hyp | DELETE "subst" | DELETE "congruence" | DELETE "congruence" natural @@ -1095,10 +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 ) +| 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" ltac_expr3 ) ] (* todo: don't use DELETENT for this *) @@ -1130,14 +1136,31 @@ printable: [ | INSERTALL "Print" ] +add_zify: [ +| [ "InjTyp" | "BinOp" | "UnOp" | "CstOp" | "BinRel" | "UnOpSpec" | "BinOpSpec" ] TAG Micromega +| [ "PropOp" | "PropBinOp" | "PropUOp" | "Saturate" ]TAG Micromega +] + +show_zify: [ +| [ "InjTyp" | "BinOp" | "UnOp" | "CstOp" | "BinRel" | "UnOpSpec" | "BinOpSpec" | "Spec" ] TAG Micromega +] + +scheme_kind: [ +| DELETE "Induction" "for" smart_global "Sort" sort_family +| DELETE "Minimality" "for" smart_global "Sort" sort_family +| DELETE "Elimination" "for" smart_global "Sort" sort_family +| DELETE "Case" "for" smart_global "Sort" sort_family +| [ "Induction" | "Minimality" | "Elimination" | "Case" ] "for" smart_global "Sort" sort_family +] + command: [ | REPLACE "Print" printable | WITH printable | "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" @@ -1148,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 @@ -1202,7 +1225,7 @@ command: [ | WITH "Next" "Obligation" OPT ( "of" ident ) withtac | DELETE "Next" "Obligation" withtac | REPLACE "Obligation" natural "of" ident ":" lglob withtac -| WITH "Obligation" natural OPT ( "of" ident ) OPT ( ":" lglob withtac ) +| WITH "Obligation" natural OPT ( "of" ident ) OPT ( ":" type withtac ) | DELETE "Obligation" natural "of" ident withtac | DELETE "Obligation" natural ":" lglob withtac | DELETE "Obligation" natural withtac @@ -1215,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 @@ -1232,13 +1255,14 @@ command: [ | REPLACE "Solve" "All" "Obligations" "with" tactic | WITH "Solve" "All" "Obligations" OPT ( "with" tactic ) | DELETE "Solve" "All" "Obligations" +| DELETE "Solve" "Obligations" "of" ident "with" tactic +| DELETE "Solve" "Obligations" "of" ident +| DELETE "Solve" "Obligations" "with" tactic +| DELETE "Solve" "Obligations" +| "Solve" "Obligations" OPT ( "of" ident ) OPT ( "with" tactic ) | REPLACE "Solve" "Obligation" natural "of" ident "with" tactic | WITH "Solve" "Obligation" natural OPT ( "of" ident ) "with" tactic -| DELETE "Solve" "Obligations" | DELETE "Solve" "Obligation" natural "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 @@ -1261,12 +1285,38 @@ 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 "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 | DELETE "Ltac2" ltac2_entry (* was split up *) +| DELETE "Add" "Zify" "InjTyp" constr (* micromega plugin *) +| DELETE "Add" "Zify" "BinOp" constr (* micromega plugin *) +| DELETE "Add" "Zify" "UnOp" constr (* micromega plugin *) +| DELETE "Add" "Zify" "CstOp" constr (* micromega plugin *) +| DELETE "Add" "Zify" "BinRel" constr (* micromega plugin *) +| DELETE "Add" "Zify" "PropOp" constr (* micromega plugin *) +| DELETE "Add" "Zify" "PropBinOp" constr (* micromega plugin *) +| DELETE "Add" "Zify" "PropUOp" constr (* micromega plugin *) +| DELETE "Add" "Zify" "BinOpSpec" constr (* micromega plugin *) +| DELETE "Add" "Zify" "UnOpSpec" constr (* micromega plugin *) +| DELETE "Add" "Zify" "Saturate" constr (* micromega plugin *) +| "Add" "Zify" add_zify constr TAG Micromega + +| DELETE "Show" "Zify" "InjTyp" (* micromega plugin *) +| DELETE "Show" "Zify" "BinOp" (* micromega plugin *) +| DELETE "Show" "Zify" "UnOp" (* micromega plugin *) +| DELETE "Show" "Zify" "CstOp" (* micromega plugin *) +| DELETE "Show" "Zify" "BinRel" (* micromega plugin *) +| DELETE "Show" "Zify" "UnOpSpec" (* micromega plugin *) +| DELETE "Show" "Zify" "BinOpSpec" (* micromega plugin *) +(* keep this one | "Show" "Zify" "Spec" (* micromega plugin *)*) +| "Show" "Zify" show_zify TAG Micromega +| REPLACE "Goal" lconstr +| WITH "Goal" type ] option_setting: [ @@ -1298,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" @@ -1308,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" *) @@ -1376,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 ] @@ -1394,11 +1444,11 @@ type_cstr: [ inductive_definition: [ | REPLACE opt_coercion ident_decl binders OPT [ "|" binders ] OPT [ ":" lconstr ] opt_constructors_or_fields decl_notations -| WITH opt_coercion ident_decl binders OPT [ "|" binders ] OPT [ ":" type ] opt_constructors_or_fields decl_notations +| 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: [ +constructors_or_record: [ | DELETE "|" LIST1 constructor SEP "|" | REPLACE identref constructor_type "|" LIST1 constructor SEP "|" | WITH OPT "|" LIST1 constructor SEP "|" @@ -1409,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 ] @@ -1577,7 +1627,7 @@ ltac2_rewriter: [ | OPT natural OPT [ "?" | "!" ] ltac2_constr_with_bindings ] -tac2expr0: [ +ltac2_expr0: [ | DELETE "(" ")" ] @@ -1617,7 +1667,7 @@ eauto_search_strategy: [ constr_body: [ | DELETE ":=" lconstr | REPLACE ":" lconstr ":=" lconstr -| WITH OPT ( ":" lconstr ) ":=" lconstr +| WITH OPT ( ":" type ) ":=" lconstr ] opt_hintbases: [ @@ -1754,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: [ @@ -1769,13 +1819,20 @@ tactic_mode: [ | ltac_info tactic | MOVETO command ltac_info tactic | DELETE command +| REPLACE OPT toplevel_selector "{" +(* semantically restricted *) +| WITH OPT ( [ natural | "[" ident "]" ] ":" ) "{" +| MOVETO simple_tactic OPT ( [ natural | "[" ident "]" ] ":" ) "{" +| DELETE simple_tactic ] -sexpr: [ +tactic_mode: [ | DELETENT ] + +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 ] @@ -1785,7 +1842,7 @@ RENAME: [ ] toplevel_selector: [ -| selector_body +| selector | "all" | "!" (* par is accepted even though it's not in the .mlg *) @@ -1793,7 +1850,7 @@ toplevel_selector: [ ] toplevel_selector_temp: [ -| DELETE selector_body ":" +| DELETE selector ":" | DELETE "all" ":" | DELETE "!" ":" | toplevel_selector ":" @@ -1834,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 ] @@ -1858,27 +1915,27 @@ 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 -| "field" OPT ( "[" LIST1 operconstr200 "]" ) -| "field_simplify" OPT ( "[" LIST1 operconstr200 "]" ) LIST1 operconstr200 OPT ( "in" ident ) -| "field_simplify_eq" OPT ( "[" LIST1 operconstr200 "]" ) OPT ( "in" ident ) -| "intuition" OPT tactic_expr5 -| "nsatz" OPT ( "with" "radicalmax" ":=" operconstr200 "strategy" ":=" operconstr200 "parameters" ":=" operconstr200 "variables" ":=" operconstr200 ) -| "psatz" operconstr200 OPT int_or_var -| "ring" OPT ( "[" LIST1 operconstr200 "]" ) -| "ring_simplify" OPT ( "[" LIST1 operconstr200 "]" ) LIST1 operconstr200 OPT ( "in" ident ) (* todo: ident was "hyp", worth keeping? *) +| "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 ltac_expr5 +| "nsatz" OPT ( "with" "radicalmax" ":=" constr "strategy" ":=" constr "parameters" ":=" constr "variables" ":=" constr ) +| "psatz" constr OPT int_or_var +| "ring" OPT ( "[" LIST1 constr "]" ) +| "ring_simplify" OPT ( "[" LIST1 constr "]" ) LIST1 constr OPT ( "in" ident ) (* todo: ident was "hyp", worth keeping? *) ] (* defined in OCaml outside of mlgs *) -tactic_arg: [ -| "uconstr" ":" "(" operconstr200 ")" +tactic_value: [ +| "uconstr" ":" "(" term200 ")" | MOVEALLBUT simple_tactic ] @@ -1886,10 +1943,6 @@ nonterminal: [ ] value_tactic: [ ] -RENAME: [ -| tactic_arg tactic_value -] - syn_value: [ | IDENT; ":" "(" nonterminal ")" ] @@ -1908,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: [ @@ -1921,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: [ @@ -2005,7 +2058,7 @@ atomic_tac2pat: [ | OPTINREF ] -tac2expr0: [ +ltac2_expr0: [ (* | DELETE "(" ")" (* covered by "()" prodn *) | REPLACE "{" [ | LIST1 tac2rec_fieldexpr OPT ";" ] "}" @@ -2018,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: [ @@ -2105,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 *) ] @@ -2141,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 *) ] @@ -2194,6 +2240,40 @@ ltac2_induction_clause: [ | WITH ltac2_destruction_arg OPT ltac2_as_or_and_ipat OPT ltac2_eqn_ipat OPT ltac2_clause TAG Ltac2 ] +starredidentref: [ +| EDIT identref ADD_OPT "*" +| EDIT "Type" ADD_OPT "*" +| "All" +] + +ssexpr0: [ +| DELETE "(" LIST0 starredidentref ")" +| DELETE "(" LIST0 starredidentref ")" "*" +| DELETE "(" ssexpr35 ")" +| DELETE "(" ssexpr35 ")" "*" +| "(" section_subset_expr ")" OPT "*" +] + +ssexpr35: [ +| EDIT ADD_OPT "-" ssexpr50 +] + +simple_binding: [ +| REPLACE "(" ident ":=" lconstr ")" +| WITH "(" [ ident | natural ] ":=" lconstr ")" +| DELETE "(" natural ":=" lconstr ")" +] + + +subprf: [ +| MOVEALLBUT simple_tactic +| "{" (* should be removed. See https://github.com/coq/coq/issues/12004 *) +] + +ltac2_expr: [ +| DELETE _ltac2_expr +] + SPLICE: [ | clause | noedit_mode @@ -2204,7 +2284,6 @@ SPLICE: [ | NUMBER | STRING | hyp -| var | identref | pattern_ident | constr_eval (* splices as multiple prods *) @@ -2214,10 +2293,10 @@ SPLICE: [ | ltac_selector | Constr.ident | attribute_list -| operconstr99 -| operconstr90 -| operconstr9 -| operconstr8 +| term99 +| term90 +| term9 +| term8 | pattern200 | pattern99 | pattern90 @@ -2268,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 @@ -2286,7 +2365,6 @@ SPLICE: [ | decorated_vernac | ext_module_expr | ext_module_type -| pattern_identref | test | binder_constr | atomic_constr @@ -2354,7 +2432,6 @@ SPLICE: [ | intropatterns | instance_name | failkw -| selector | ne_in_or_out_modules | search_queries | locatable @@ -2377,87 +2454,49 @@ SPLICE: [ | refglobals (* Ltac2 *) | syntax_modifiers | array_elems -| ltac2_expr | G_LTAC2_input_fun | ltac2_simple_intropattern_closed | ltac2_with_bindings +| int_or_id +| fun_ind_using +| with_names +| eauto_search_strategy_name +| constr_with_bindings +| simple_binding +| ssexpr35 (* strange in mlg, ssexpr50 is after this *) ] (* end SPLICE *) 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*) -| ssexpr35 ssexpr (* strange in mlg, ssexpr50 is after this *) - -| tactic_then_gen for_each_goal -| ltac2_tactic_then_gen ltac2_for_each_goal -| selector_body selector -| match_hyps match_hyp +| ssexpr50 section_var_expr50 +| ssexpr0 section_var_expr0 +| section_subset_expr section_var_expr +| fun_scheme_arg func_scheme_def | BULLET bullet -| fix_decl fix_body -| cofix_decl cofix_body -(* todo: it's confusing that Constr.constr and constr are 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 ] @@ -2479,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 @@ -2518,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: [ diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml index 0ac652c0db..b7f1e18d2b 100644 --- a/doc/tools/docgram/doc_grammar.ml +++ b/doc/tools/docgram/doc_grammar.ml @@ -909,14 +909,17 @@ let apply_splice g edit_map = List.iter (fun b -> let (nt0, prods0) = b in let rec splice_loop nt prods cnt = - let max_cnt = 10 in - let (nt', prods') = edit_rule g edit_map nt prods in - if cnt > max_cnt then - error "Splice for '%s' not done after %d iterations\n" nt0 max_cnt; - if nt' = nt && prods' = prods then - (nt', prods') - else - splice_loop nt' prods' (cnt+1) + if cnt >= 10 then begin + error "Splice for '%s' not done after %d iterations. Current value is:\n" nt0 cnt; + List.iter (fun prod -> Printf.eprintf " %s\n" (prod_to_str prod)) prods; + (nt, prods) + end else begin + let (nt', prods') = edit_rule g edit_map nt prods in + if nt' = nt && prods' = prods then + (nt, prods) + else + splice_loop nt' prods' (cnt+1) + end in let (nt', prods') = splice_loop nt0 prods0 0 in g_update_prods g nt' prods') @@ -1724,6 +1727,7 @@ let open_temp_bin file = let match_cmd_regex = Str.regexp "[a-zA-Z0-9_ ]+" let match_subscripts = Str.regexp "__[a-zA-Z0-9]+" +let remove_subscrs str = Str.global_replace match_subscripts "" str let find_longest_match prods str = let get_pfx str = String.trim (if Str.string_match match_cmd_regex str 0 then Str.matched_string str else "") in @@ -1737,7 +1741,6 @@ let find_longest_match prods str = in aux 0 in - let remove_subscrs str = Str.global_replace match_subscripts "" str in let slen = String.length str in let str_pfx = get_pfx str in @@ -1892,25 +1895,15 @@ let process_rst g file args seen tac_prods cmd_prods = (* "doc/sphinx/proof-engine/ssreflect-proof-language.rst"]*) (* in*) - let cmd_replace_files = [ - "doc/sphinx/language/core/records.rst"; - "doc/sphinx/language/core/sections.rst"; - "doc/sphinx/language/extensions/implicit-arguments.rst"; - "doc/sphinx/language/extensions/arguments-command.rst"; - "doc/sphinx/language/gallina-extensions.rst"; - "doc/sphinx/language/gallina-specification-language.rst"; - "doc/sphinx/language/using/libraries/funind.rst"; - "doc/sphinx/proof-engine/ltac.rst"; - "doc/sphinx/proof-engine/ltac2.rst"; - "doc/sphinx/proof-engine/vernacular-commands.rst"; - "doc/sphinx/user-extensions/syntax-extensions.rst"; - "doc/sphinx/proof-engine/vernacular-commands.rst" + let cmd_exclude_files = [ + "doc/sphinx/proof-engine/ssreflect-proof-language.rst"; + "doc/sphinx/proof-engine/tactics.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 + if StringSet.is_empty prods || (List.mem file cmd_exclude_files) then rhs (* no change *) else let mtch, multi, best = find_longest_match prods rhs in @@ -1918,12 +1911,15 @@ let process_rst g file args seen tac_prods cmd_prods = if mtch = rhs then rhs (* no change *) else if mtch = "" then begin - warn "%s line %d: NO MATCH `%s`\n" file !linenum rhs; - if best <> "" then - warn "%s line %d: BEST `%s`\n" file !linenum best; + error "%s line %d: NO MATCH for `%s`\n" file !linenum rhs; + if best <> "" then begin + Printf.eprintf " closest match is: `%s`\n" best; + Printf.eprintf " Please update the rst manually while preserving any subscripts, e.g. 'NT__sub'\n" + end; rhs end else if multi then begin - warn "%s line %d: MULTIMATCH `%s`\n" file !linenum rhs; + error "%s line %d: MULTIPLE MATCHES for `%s`\n" file !linenum rhs; + Printf.eprintf " Please update the rst manually while preserving any subscripts, e.g. 'NT__sub'\n"; rhs end else mtch (* update cmd/tacn *) @@ -1936,7 +1932,7 @@ let process_rst g file args seen tac_prods cmd_prods = fprintf new_rst "%s%s\n" pfx (replace first_rhs prods); - map := NTMap.add first_rhs (file, !linenum) !map; + map := NTMap.add (remove_subscrs first_rhs) (file, !linenum) !map; while let nextline = getline() in ignore (Str.string_match contin_regex nextline 0); @@ -2078,13 +2074,11 @@ let process_grammar args = print_in_order out g `MLG !g.order StringSet.empty; close_out out; finish_with_file (dir "orderedGrammar") args; - check_singletons g + 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 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 *) let plist nt = let list = (List.map (fun t -> String.trim (prod_to_prodn t)) (NTMap.find nt !g.map)) in @@ -2095,7 +2089,6 @@ let process_grammar args = report_omitted_prods g !seen.nts "Nonterminal" ""; let out = open_out (dir "updated_rsts") in close_out out; - end; (* if args.check_tacs then @@ -2104,7 +2097,6 @@ let process_grammar args = report_omitted_prods cmd_list !seen.cmds "Command" "\n "; *) - 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 @@ -2113,7 +2105,7 @@ let process_grammar args = 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 + let out = open_out_bin (dir outfile) in StringSet.iter (fun c -> let rsts = StringSet.mem c rstCmds in let gram = StringSet.mem c gramCmds in @@ -2127,7 +2119,6 @@ let process_grammar args = 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 @@ -2139,17 +2130,16 @@ let process_grammar args = let tac_nts = ["simple_tactic"] in if args.check_tacs then - cmdReport "prodnTactics" "tacs" tac_nts !seen.tacs !seen.tacvs - end; + cmdReport "prodnTactics" "tacs" tac_nts !seen.tacs !seen.tacvs; - (* generate prodnGrammar for reference *) - if !exit_code = 0 && not args.verify then begin - 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 - end - end + (* generate prodnGrammar for reference *) + if not args.verify then begin + let out = open_out_bin (dir "prodnGrammar") in + print_in_order out prodn_gram `PRODN !prodn_gram.order StringSet.empty; + close_out out; + end + end (* if !exit_code = 0 *) + end (* if not args.fullGrammar *) let parse_args () = let suffix_regex = Str.regexp ".*\\.\\([a-z]+\\)$" in diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 73641976e3..c764cb6f37 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -17,7 +17,7 @@ constr_pattern: [ | constr ] -lconstr_pattern: [ +cpattern: [ | lconstr ] @@ -58,67 +58,67 @@ universe: [ ] lconstr: [ -| operconstr200 +| term200 ] constr: [ -| operconstr8 -| "@" global univ_instance +| term8 +| "@" global univ_annot ] -operconstr200: [ +term200: [ | binder_constr -| operconstr100 +| term100 ] -operconstr100: [ -| operconstr99 "<:" operconstr200 -| operconstr99 "<<:" operconstr200 -| operconstr99 ":" operconstr200 -| operconstr99 ":>" -| operconstr99 +term100: [ +| term99 "<:" term200 +| term99 "<<:" term200 +| term99 ":" term200 +| term99 ":>" +| term99 ] -operconstr99: [ -| operconstr90 +term99: [ +| term90 ] -operconstr90: [ -| operconstr10 +term90: [ +| term10 ] -operconstr10: [ -| operconstr9 LIST1 appl_arg -| "@" global univ_instance LIST0 operconstr9 -| "@" pattern_identref LIST1 identref -| operconstr9 +term10: [ +| term9 LIST1 arg +| "@" global univ_annot LIST0 term9 +| "@" pattern_ident LIST1 identref +| term9 ] -operconstr9: [ -| ".." operconstr0 ".." -| operconstr8 +term9: [ +| ".." term0 ".." +| term8 ] -operconstr8: [ -| operconstr1 +term8: [ +| term1 ] -operconstr1: [ -| operconstr0 ".(" global LIST0 appl_arg ")" -| operconstr0 ".(" "@" global LIST0 ( operconstr9 ) ")" -| operconstr0 "%" IDENT -| operconstr0 +term1: [ +| term0 ".(" global LIST0 arg ")" +| term0 ".(" "@" global LIST0 ( term9 ) ")" +| term0 "%" IDENT +| term0 ] -operconstr0: [ +term0: [ | atomic_constr -| match_constr -| "(" operconstr200 ")" +| term_match +| "(" term200 ")" | "{|" record_declaration bar_cbrace | "{" binder_constr "}" -| "`{" operconstr200 "}" -| test_array_opening "[" "|" array_elems "|" lconstr type_cstr test_array_closing "|" "]" univ_instance -| "`(" operconstr200 ")" +| "`{" term200 "}" +| test_array_opening "[" "|" array_elems "|" lconstr type_cstr test_array_closing "|" "]" univ_annot +| "`(" term200 ")" ] array_elems: [ @@ -140,38 +140,38 @@ field_def: [ ] binder_constr: [ -| "forall" open_binders "," operconstr200 -| "fun" open_binders "=>" operconstr200 -| "let" name binders let_type_cstr ":=" operconstr200 "in" operconstr200 -| "let" "fix" fix_decl "in" operconstr200 -| "let" "cofix" cofix_decl "in" operconstr200 -| "let" [ "(" LIST0 name SEP "," ")" | "()" ] return_type ":=" operconstr200 "in" operconstr200 -| "let" "'" pattern200 ":=" operconstr200 "in" operconstr200 -| "let" "'" pattern200 ":=" operconstr200 case_type "in" operconstr200 -| "let" "'" pattern200 "in" pattern200 ":=" operconstr200 case_type "in" operconstr200 -| "if" operconstr200 return_type "then" operconstr200 "else" operconstr200 +| "forall" open_binders "," term200 +| "fun" open_binders "=>" term200 +| "let" name binders let_type_cstr ":=" term200 "in" term200 +| "let" "fix" fix_decl "in" term200 +| "let" "cofix" cofix_body "in" term200 +| "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" term200 "in" term200 +| "let" "'" pattern200 ":=" term200 "in" term200 +| "let" "'" pattern200 ":=" term200 case_type "in" term200 +| "let" "'" pattern200 "in" pattern200 ":=" term200 case_type "in" term200 +| "if" term200 as_return_type "then" term200 "else" term200 | "fix" fix_decls | "cofix" cofix_decls ] -appl_arg: [ -| test_lpar_id_coloneq "(" ident ":=" lconstr ")" -| operconstr9 +arg: [ +| test_lpar_id_coloneq "(" identref ":=" lconstr ")" +| term9 ] atomic_constr: [ -| global univ_instance +| global univ_annot | sort | NUMBER | string | "_" -| "?" "[" ident "]" +| "?" "[" identref "]" | "?" "[" pattern_ident "]" | pattern_ident evar_instance ] inst: [ -| ident ":=" lconstr +| identref ":=" lconstr ] evar_instance: [ @@ -179,7 +179,7 @@ evar_instance: [ | ] -univ_instance: [ +univ_annot: [ | "@{" LIST0 universe_level "}" | ] @@ -198,31 +198,31 @@ fix_decls: [ ] cofix_decls: [ -| cofix_decl -| cofix_decl "with" LIST1 cofix_decl SEP "with" "for" identref +| cofix_body +| cofix_body "with" LIST1 cofix_body SEP "with" "for" identref ] fix_decl: [ -| identref binders_fixannot type_cstr ":=" operconstr200 +| identref binders_fixannot type_cstr ":=" term200 ] -cofix_decl: [ -| identref binders type_cstr ":=" operconstr200 +cofix_body: [ +| identref binders type_cstr ":=" term200 ] -match_constr: [ +term_match: [ | "match" LIST1 case_item SEP "," OPT case_type "with" branches "end" ] case_item: [ -| operconstr100 OPT [ "as" name ] OPT [ "in" pattern200 ] +| term100 OPT [ "as" name ] OPT [ "in" pattern200 ] ] case_type: [ -| "return" operconstr100 +| "return" term100 ] -return_type: [ +as_return_type: [ | OPT [ OPT [ "as" name ] case_type ] ] @@ -253,7 +253,7 @@ pattern200: [ ] pattern100: [ -| pattern99 ":" operconstr200 +| pattern99 ":" term200 | pattern99 ] @@ -335,10 +335,10 @@ closed_binder: [ ] typeclass_constraint: [ -| "!" operconstr200 -| "{" name "}" ":" [ "!" | ] operconstr200 -| test_name_colon name ":" [ "!" | ] operconstr200 -| operconstr200 +| "!" term200 +| "{" name "}" ":" [ "!" | ] term200 +| test_name_colon name ":" [ "!" | ] term200 +| term200 ] type_cstr: [ @@ -362,16 +362,12 @@ pattern_ident: [ | LEFTQMARK ident ] -pattern_identref: [ -| pattern_ident -] - -var: [ +identref: [ | ident ] -identref: [ -| ident +hyp: [ +| identref ] field: [ @@ -510,7 +506,7 @@ command: [ | "Remove" "Hints" LIST1 global opt_hintbases | "Hint" hint opt_hintbases | "Comments" LIST0 comment -| "Declare" "Instance" ident_decl binders ":" operconstr200 hint_info +| "Declare" "Instance" ident_decl binders ":" term200 hint_info | "Declare" "Scope" IDENT | "Pwd" | "Cd" @@ -529,13 +525,13 @@ command: [ | "Print" "Namespace" dirpath | "Inspect" natural | "Add" "ML" "Path" ne_string -| "Set" option_table option_setting -| "Unset" option_table -| "Print" "Table" option_table +| "Set" setting_name option_setting +| "Unset" setting_name +| "Print" "Table" setting_name | "Add" IDENT IDENT LIST1 table_value | "Add" IDENT LIST1 table_value -| "Test" option_table "for" LIST1 table_value -| "Test" option_table +| "Test" setting_name "for" LIST1 table_value +| "Test" setting_name | "Remove" IDENT IDENT LIST1 table_value | "Remove" IDENT LIST1 table_value | "Write" "State" IDENT @@ -573,7 +569,7 @@ command: [ | "Show" "Extraction" (* extraction plugin *) | "Set" "Firstorder" "Solver" tactic | "Print" "Firstorder" "Solver" -| "Function" LIST1 function_rec_definition_loc SEP "with" (* funind plugin *) +| "Function" LIST1 function_fix_definition SEP "with" (* funind plugin *) | "Functional" "Scheme" LIST1 fun_scheme_arg SEP "with" (* funind plugin *) | "Functional" "Case" fun_scheme_arg (* funind plugin *) | "Generate" "graph" "for" reference (* funind plugin *) @@ -596,9 +592,9 @@ command: [ | "Optimize" "Proof" | "Optimize" "Heap" | "Hint" "Cut" "[" hints_path "]" opthints -| "Typeclasses" "Transparent" LIST0 reference -| "Typeclasses" "Opaque" LIST0 reference -| "Typeclasses" "eauto" ":=" debug eauto_search_strategy OPT integer +| "Typeclasses" "Transparent" LIST1 reference +| "Typeclasses" "Opaque" LIST1 reference +| "Typeclasses" "eauto" ":=" debug eauto_search_strategy OPT natural | "Proof" "with" Pltac.tactic OPT [ "using" G_vernac.section_subset_expr ] | "Proof" "using" G_vernac.section_subset_expr OPT [ "with" Pltac.tactic ] | "Tactic" "Notation" OPT ltac_tactic_level LIST1 ltac_production_item ":=" tactic @@ -615,6 +611,7 @@ command: [ | "Solve" "Obligation" natural "of" ident "with" tactic | "Solve" "Obligation" natural "with" tactic | "Solve" "Obligations" "of" ident "with" tactic +| "Solve" "Obligations" "of" ident | "Solve" "Obligations" "with" tactic | "Solve" "Obligations" | "Solve" "All" "Obligations" "with" tactic @@ -689,11 +686,11 @@ command: [ | "Print" "Rings" (* ring plugin *) | "Add" "Field" ident ":" constr OPT field_mods (* ring plugin *) | "Print" "Fields" (* ring plugin *) -| "Number" "Notation" reference reference reference ":" ident numnotoption -| "Numeral" "Notation" reference reference reference ":" ident numnotoption +| "Number" "Notation" reference reference reference ":" ident numeral_modifier +| "Numeral" "Notation" reference reference reference ":" ident numeral_modifier | "String" "Notation" reference reference reference ":" ident | "Ltac2" ltac2_entry (* Ltac2 plugin *) -| "Ltac2" "Eval" ltac2_expr (* Ltac2 plugin *) +| "Ltac2" "Eval" ltac2_expr6 (* Ltac2 plugin *) | "Print" "Ltac2" reference (* Ltac2 plugin *) ] @@ -748,10 +745,10 @@ attribute_list: [ ] attribute: [ -| ident attribute_value +| ident attr_value ] -attribute_value: [ +attr_value: [ | "=" string | "(" attribute_list ")" | @@ -798,10 +795,10 @@ gallina: [ | def_token ident_decl def_body | "Let" ident_decl def_body | finite_token LIST1 inductive_definition SEP "with" -| "Fixpoint" LIST1 rec_definition SEP "with" -| "Let" "Fixpoint" LIST1 rec_definition SEP "with" -| "CoFixpoint" LIST1 corec_definition SEP "with" -| "Let" "CoFixpoint" LIST1 corec_definition SEP "with" +| "Fixpoint" LIST1 fix_definition SEP "with" +| "Let" "Fixpoint" LIST1 fix_definition SEP "with" +| "CoFixpoint" LIST1 cofix_definition SEP "with" +| "Let" "CoFixpoint" LIST1 cofix_definition SEP "with" | "Scheme" LIST1 scheme SEP "with" | "Combined" "Scheme" identref "from" LIST1 identref SEP "," | "Register" global "as" qualid @@ -900,7 +897,7 @@ decl_notations: [ ] opt_constructors_or_fields: [ -| ":=" constructor_list_or_record_decl +| ":=" constructors_or_record | ] @@ -908,7 +905,7 @@ inductive_definition: [ | opt_coercion ident_decl binders OPT [ "|" binders ] OPT [ ":" lconstr ] opt_constructors_or_fields decl_notations ] -constructor_list_or_record_decl: [ +constructors_or_record: [ | "|" LIST1 constructor SEP "|" | identref constructor_type "|" LIST1 constructor SEP "|" | identref constructor_type @@ -922,11 +919,11 @@ opt_coercion: [ | ] -rec_definition: [ +fix_definition: [ | ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notations ] -corec_definition: [ +cofix_definition: [ | ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notations ] @@ -953,39 +950,39 @@ record_fields: [ | ] -record_binder_body: [ -| binders of_type_with_opt_coercion lconstr -| binders of_type_with_opt_coercion lconstr ":=" lconstr +field_body: [ +| binders of_type lconstr +| binders of_type lconstr ":=" lconstr | binders ":=" lconstr ] record_binder: [ | name -| name record_binder_body +| name field_body ] assum_list: [ | LIST1 assum_coe -| simple_assum_coe +| assumpt ] assum_coe: [ -| "(" simple_assum_coe ")" +| "(" assumpt ")" ] -simple_assum_coe: [ -| LIST1 ident_decl of_type_with_opt_coercion lconstr +assumpt: [ +| LIST1 ident_decl of_type lconstr ] constructor_type: [ -| binders [ of_type_with_opt_coercion lconstr | ] +| binders [ of_type lconstr | ] ] constructor: [ | identref constructor_type ] -of_type_with_opt_coercion: [ +of_type: [ | ":>" | ":" ">" | ":" @@ -1014,16 +1011,16 @@ gallina_ext: [ | "Coercion" global ":" class_rawexpr ">->" class_rawexpr | "Coercion" by_notation ":" class_rawexpr ">->" class_rawexpr | "Context" LIST1 binder -| "Instance" instance_name ":" operconstr200 hint_info [ ":=" "{" record_declaration "}" | ":=" lconstr | ] +| "Instance" instance_name ":" term200 hint_info [ ":=" "{" record_declaration "}" | ":=" lconstr | ] | "Existing" "Instance" global hint_info | "Existing" "Instances" LIST1 global OPT [ "|" natural ] | "Existing" "Class" global -| "Arguments" smart_global LIST0 argument_spec_block OPT [ "," LIST1 [ LIST0 more_implicits_block ] SEP "," ] OPT [ ":" LIST1 arguments_modifier SEP "," ] +| "Arguments" smart_global LIST0 arg_specs OPT [ "," LIST1 [ LIST0 implicits_alt ] SEP "," ] OPT [ ":" LIST1 args_modifier SEP "," ] | "Implicit" "Type" reserv_list | "Implicit" "Types" reserv_list | "Generalizable" [ "All" "Variables" | "No" "Variables" | [ "Variable" | "Variables" ] LIST1 identref ] -| "Export" "Set" option_table option_setting -| "Export" "Unset" option_table +| "Export" "Set" setting_name option_setting +| "Export" "Unset" setting_name ] filtered_import: [ @@ -1145,7 +1142,7 @@ ssexpr0: [ | "(" ssexpr35 ")" "*" ] -arguments_modifier: [ +args_modifier: [ | "simpl" "nomatch" | "simpl" "never" | "default" "implicits" @@ -1167,7 +1164,7 @@ argument_spec: [ | OPT "!" name OPT scope_delimiter ] -argument_spec_block: [ +arg_specs: [ | argument_spec | "/" | "&" @@ -1176,7 +1173,7 @@ argument_spec_block: [ | "{" LIST1 argument_spec "}" OPT scope_delimiter ] -more_implicits_block: [ +implicits_alt: [ | name | "[" LIST1 name "]" | "{" LIST1 name "}" @@ -1285,7 +1282,7 @@ table_value: [ | STRING ] -option_table: [ +setting_name: [ | LIST1 IDENT ] @@ -1394,9 +1391,9 @@ syntax_modifier: [ | "only" "parsing" | "format" STRING OPT STRING | IDENT; "," LIST1 IDENT SEP "," "at" level -| IDENT; "at" level OPT constr_as_binder_kind -| IDENT constr_as_binder_kind -| IDENT syntax_extension_type +| IDENT; "at" level OPT binder_interp +| IDENT binder_interp +| IDENT explicit_subentry ] syntax_modifiers: [ @@ -1404,19 +1401,19 @@ syntax_modifiers: [ | ] -syntax_extension_type: [ +explicit_subentry: [ | "ident" | "global" | "bigint" | "binder" | "constr" -| "constr" at_level_opt OPT constr_as_binder_kind +| "constr" at_level_opt OPT binder_interp | "pattern" | "pattern" "at" "level" natural | "strict" "pattern" | "strict" "pattern" "at" "level" natural | "closed" "binder" -| "custom" IDENT at_level_opt OPT constr_as_binder_kind +| "custom" IDENT at_level_opt OPT binder_interp ] at_level_opt: [ @@ -1424,7 +1421,7 @@ at_level_opt: [ | ] -constr_as_binder_kind: [ +binder_interp: [ | "as" "ident" | "as" "pattern" | "as" "strict" "pattern" @@ -1551,7 +1548,7 @@ simple_tactic: [ | "notypeclasses" "refine" uconstr | "simple" "notypeclasses" "refine" uconstr | "solve_constraints" -| "subst" LIST1 var +| "subst" LIST1 hyp | "subst" | "simple" "subst" | "evar" test_lpar_id_colon "(" ident ":" lconstr ")" @@ -1619,6 +1616,7 @@ simple_tactic: [ | "convert_concl_no_check" constr | "typeclasses" "eauto" "bfs" OPT int_or_var "with" LIST1 preident | "typeclasses" "eauto" OPT int_or_var "with" LIST1 preident +| "typeclasses" "eauto" "bfs" OPT int_or_var | "typeclasses" "eauto" OPT int_or_var | "head_of_constr" ident constr | "not_evar" constr @@ -1791,8 +1789,8 @@ auto_using': [ | (* funind plugin *) ] -function_rec_definition_loc: [ -| Vernac.rec_definition (* funind plugin *) +function_fix_definition: [ +| Vernac.fix_definition (* funind plugin *) ] fun_scheme_arg: [ @@ -1811,7 +1809,7 @@ EXTRAARGS_natural: [ occurrences: [ | LIST1 integer -| var +| hyp ] glob: [ @@ -1925,16 +1923,16 @@ eauto_search_strategy: [ ] tactic_then_last: [ -| "|" LIST0 ( OPT tactic_expr5 ) SEP "|" +| "|" LIST0 ( OPT ltac_expr5 ) SEP "|" | ] -tactic_then_gen: [ -| tactic_expr5 "|" tactic_then_gen -| tactic_expr5 ".." tactic_then_last +for_each_goal: [ +| ltac_expr5 "|" for_each_goal +| ltac_expr5 ".." tactic_then_last | ".." tactic_then_last -| tactic_expr5 -| "|" tactic_then_gen +| ltac_expr5 +| "|" for_each_goal | ] @@ -1942,60 +1940,60 @@ tactic_then_locality: [ | "[" OPT ">" ] -tactic_expr5: [ +ltac_expr5: [ | binder_tactic -| tactic_expr4 -] - -tactic_expr4: [ -| tactic_expr3 ";" binder_tactic -| tactic_expr3 ";" tactic_expr3 -| tactic_expr3 ";" tactic_then_locality tactic_then_gen "]" -| tactic_expr3 -] - -tactic_expr3: [ -| "try" tactic_expr3 -| "do" int_or_var tactic_expr3 -| "timeout" int_or_var tactic_expr3 -| "time" OPT string tactic_expr3 -| "repeat" tactic_expr3 -| "progress" tactic_expr3 -| "once" tactic_expr3 -| "exactly_once" tactic_expr3 -| "infoH" tactic_expr3 -| "abstract" tactic_expr2 -| "abstract" tactic_expr2 "using" ident -| selector tactic_expr3 -| tactic_expr2 -] - -tactic_expr2: [ -| tactic_expr1 "+" binder_tactic -| tactic_expr1 "+" tactic_expr2 -| "tryif" tactic_expr5 "then" tactic_expr5 "else" tactic_expr2 -| tactic_expr1 "||" binder_tactic -| tactic_expr1 "||" tactic_expr2 -| tactic_expr1 -] - -tactic_expr1: [ +| ltac_expr4 +] + +ltac_expr4: [ +| ltac_expr3 ";" binder_tactic +| ltac_expr3 ";" ltac_expr3 +| ltac_expr3 ";" tactic_then_locality for_each_goal "]" +| ltac_expr3 +] + +ltac_expr3: [ +| "try" ltac_expr3 +| "do" int_or_var ltac_expr3 +| "timeout" int_or_var ltac_expr3 +| "time" OPT string ltac_expr3 +| "repeat" ltac_expr3 +| "progress" ltac_expr3 +| "once" ltac_expr3 +| "exactly_once" ltac_expr3 +| "infoH" ltac_expr3 +| "abstract" ltac_expr2 +| "abstract" ltac_expr2 "using" ident +| "only" selector ":" ltac_expr3 +| ltac_expr2 +] + +ltac_expr2: [ +| ltac_expr1 "+" binder_tactic +| ltac_expr1 "+" ltac_expr2 +| "tryif" ltac_expr5 "then" ltac_expr5 "else" ltac_expr2 +| ltac_expr1 "||" binder_tactic +| ltac_expr1 "||" ltac_expr2 +| ltac_expr1 +] + +ltac_expr1: [ | match_key "goal" "with" match_context_list "end" | match_key "reverse" "goal" "with" match_context_list "end" -| match_key tactic_expr5 "with" match_list "end" -| "first" "[" LIST0 tactic_expr5 SEP "|" "]" -| "solve" "[" LIST0 tactic_expr5 SEP "|" "]" +| match_key ltac_expr5 "with" match_list "end" +| "first" "[" LIST0 ltac_expr5 SEP "|" "]" +| "solve" "[" LIST0 ltac_expr5 SEP "|" "]" | "idtac" LIST0 message_token | failkw [ int_or_var | ] LIST0 message_token | simple_tactic -| tactic_arg -| reference LIST0 tactic_arg_compat -| tactic_expr0 +| tactic_value +| reference LIST0 tactic_arg +| ltac_expr0 ] -tactic_expr0: [ -| "(" tactic_expr5 ")" -| "[" ">" tactic_then_gen "]" +ltac_expr0: [ +| "(" ltac_expr5 ")" +| "[" ">" for_each_goal "]" | tactic_atom ] @@ -2005,17 +2003,17 @@ failkw: [ ] binder_tactic: [ -| "fun" LIST1 input_fun "=>" tactic_expr5 -| "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" tactic_expr5 +| "fun" LIST1 input_fun "=>" ltac_expr5 +| "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" ltac_expr5 ] -tactic_arg_compat: [ -| tactic_arg +tactic_arg: [ +| tactic_value | Constr.constr | "()" ] -tactic_arg: [ +tactic_value: [ | constr_eval | "fresh" LIST0 fresh_id | "type_term" uconstr @@ -2056,26 +2054,26 @@ input_fun: [ ] let_clause: [ -| identref ":=" tactic_expr5 -| "_" ":=" tactic_expr5 -| identref LIST1 input_fun ":=" tactic_expr5 +| identref ":=" ltac_expr5 +| "_" ":=" ltac_expr5 +| identref LIST1 input_fun ":=" ltac_expr5 ] match_pattern: [ -| "context" OPT Constr.ident "[" Constr.lconstr_pattern "]" -| Constr.lconstr_pattern +| "context" OPT Constr.ident "[" Constr.cpattern "]" +| Constr.cpattern ] -match_hyps: [ +match_hyp: [ | name ":" match_pattern | name ":=" "[" match_pattern "]" ":" match_pattern | name ":=" match_pattern ] match_context_rule: [ -| LIST0 match_hyps SEP "," "|-" match_pattern "=>" tactic_expr5 -| "[" LIST0 match_hyps SEP "," "|-" match_pattern "]" "=>" tactic_expr5 -| "_" "=>" tactic_expr5 +| LIST0 match_hyp SEP "," "|-" match_pattern "=>" ltac_expr5 +| "[" LIST0 match_hyp SEP "," "|-" match_pattern "]" "=>" ltac_expr5 +| "_" "=>" ltac_expr5 ] match_context_list: [ @@ -2084,8 +2082,8 @@ match_context_list: [ ] match_rule: [ -| match_pattern "=>" tactic_expr5 -| "_" "=>" tactic_expr5 +| match_pattern "=>" ltac_expr5 +| "_" "=>" ltac_expr5 ] match_list: [ @@ -2105,12 +2103,12 @@ ltac_def_kind: [ ] tacdef_body: [ -| Constr.global LIST1 input_fun ltac_def_kind tactic_expr5 -| Constr.global ltac_def_kind tactic_expr5 +| Constr.global LIST1 input_fun ltac_def_kind ltac_expr5 +| Constr.global ltac_def_kind ltac_expr5 ] tactic: [ -| tactic_expr5 +| ltac_expr5 ] range_selector: [ @@ -2123,17 +2121,13 @@ range_selector_or_nth: [ | natural OPT [ "," LIST1 range_selector SEP "," ] ] -selector_body: [ +selector: [ | range_selector_or_nth | test_bracket_ident "[" ident "]" ] -selector: [ -| "only" selector_body ":" -] - toplevel_selector: [ -| selector_body ":" +| selector ":" | "!" ":" | "all" ":" ] @@ -2149,8 +2143,8 @@ G_LTAC_hint: [ | "Extern" natural OPT Constr.constr_pattern "=>" Pltac.tactic ] -G_LTAC_operconstr0: [ -| "ltac" ":" "(" Pltac.tactic_expr ")" +G_LTAC_term0: [ +| "ltac" ":" "(" Pltac.ltac_expr ")" ] ltac_selector: [ @@ -2329,7 +2323,7 @@ intropattern: [ ] simple_intropattern: [ -| simple_intropattern_closed LIST0 [ "%" operconstr0 ] +| simple_intropattern_closed LIST0 [ "%" term0 ] ] simple_intropattern_closed: [ @@ -2358,7 +2352,7 @@ with_bindings: [ | ] -red_flags: [ +red_flag: [ | "beta" | "iota" | "match" @@ -2375,7 +2369,7 @@ delta_flag: [ ] strategy_flag: [ -| LIST1 red_flags +| LIST1 red_flag | delta_flag ] @@ -2502,7 +2496,7 @@ as_name: [ ] by_tactic: [ -| "by" tactic_expr3 +| "by" ltac_expr3 | ] @@ -2555,7 +2549,7 @@ field_mods: [ | "(" LIST1 field_mod SEP "," ")" (* ring plugin *) ] -numnotoption: [ +numeral_modifier: [ | | "(" "warning" "after" bignat ")" | "(" "abstract" "after" bignat ")" @@ -2578,50 +2572,50 @@ tac2pat0: [ atomic_tac2pat: [ | (* Ltac2 plugin *) -| tac2pat1 ":" tac2type5 (* Ltac2 plugin *) +| tac2pat1 ":" ltac2_type5 (* Ltac2 plugin *) | tac2pat1 "," LIST0 tac2pat1 SEP "," (* Ltac2 plugin *) | tac2pat1 (* Ltac2 plugin *) ] -tac2expr6: [ -| tac2expr5 ";" tac2expr6 (* Ltac2 plugin *) -| tac2expr5 (* Ltac2 plugin *) +ltac2_expr6: [ +| ltac2_expr5 ";" ltac2_expr6 (* Ltac2 plugin *) +| ltac2_expr5 (* Ltac2 plugin *) ] -tac2expr5: [ -| "fun" LIST1 G_LTAC2_input_fun "=>" tac2expr6 (* Ltac2 plugin *) -| "let" rec_flag LIST1 G_LTAC2_let_clause SEP "with" "in" tac2expr6 (* Ltac2 plugin *) -| "match" tac2expr5 "with" G_LTAC2_branches "end" (* Ltac2 plugin *) -| tac2expr4 (* Ltac2 plugin *) +ltac2_expr5: [ +| "fun" LIST1 G_LTAC2_input_fun "=>" ltac2_expr6 (* Ltac2 plugin *) +| "let" rec_flag LIST1 G_LTAC2_let_clause SEP "with" "in" ltac2_expr6 (* Ltac2 plugin *) +| "match" ltac2_expr5 "with" G_LTAC2_branches "end" (* Ltac2 plugin *) +| ltac2_expr4 (* Ltac2 plugin *) ] -tac2expr4: [ -| tac2expr3 (* Ltac2 plugin *) +ltac2_expr4: [ +| ltac2_expr3 (* Ltac2 plugin *) ] -tac2expr3: [ -| tac2expr2 "," LIST1 tac2expr2 SEP "," (* Ltac2 plugin *) -| tac2expr2 (* Ltac2 plugin *) +ltac2_expr3: [ +| ltac2_expr2 "," LIST1 ltac2_expr2 SEP "," (* Ltac2 plugin *) +| ltac2_expr2 (* Ltac2 plugin *) ] -tac2expr2: [ -| tac2expr1 "::" tac2expr2 (* Ltac2 plugin *) -| tac2expr1 (* Ltac2 plugin *) +ltac2_expr2: [ +| ltac2_expr1 "::" ltac2_expr2 (* Ltac2 plugin *) +| ltac2_expr1 (* Ltac2 plugin *) ] -tac2expr1: [ -| tac2expr0 LIST1 tac2expr0 (* Ltac2 plugin *) -| tac2expr0 ".(" Prim.qualid ")" (* Ltac2 plugin *) -| tac2expr0 ".(" Prim.qualid ")" ":=" tac2expr5 (* Ltac2 plugin *) -| tac2expr0 (* Ltac2 plugin *) +ltac2_expr1: [ +| ltac2_expr0 LIST1 ltac2_expr0 (* Ltac2 plugin *) +| ltac2_expr0 ".(" Prim.qualid ")" (* Ltac2 plugin *) +| ltac2_expr0 ".(" Prim.qualid ")" ":=" ltac2_expr5 (* Ltac2 plugin *) +| ltac2_expr0 (* Ltac2 plugin *) ] -tac2expr0: [ -| "(" tac2expr6 ")" (* Ltac2 plugin *) -| "(" tac2expr6 ":" tac2type5 ")" (* Ltac2 plugin *) +ltac2_expr0: [ +| "(" ltac2_expr6 ")" (* Ltac2 plugin *) +| "(" ltac2_expr6 ":" ltac2_type5 ")" (* Ltac2 plugin *) | "()" (* Ltac2 plugin *) | "(" ")" (* Ltac2 plugin *) -| "[" LIST0 tac2expr5 SEP ";" "]" (* Ltac2 plugin *) +| "[" LIST0 ltac2_expr5 SEP ";" "]" (* Ltac2 plugin *) | "{" tac2rec_fieldexprs "}" (* Ltac2 plugin *) | G_LTAC2_tactic_atom (* Ltac2 plugin *) ] @@ -2633,7 +2627,7 @@ G_LTAC2_branches: [ ] branch: [ -| tac2pat1 "=>" tac2expr6 (* Ltac2 plugin *) +| tac2pat1 "=>" ltac2_expr6 (* Ltac2 plugin *) ] rec_flag: [ @@ -2646,7 +2640,7 @@ mut_flag: [ | (* Ltac2 plugin *) ] -typ_param: [ +ltac2_typevar: [ | "'" Prim.ident (* Ltac2 plugin *) ] @@ -2660,48 +2654,48 @@ G_LTAC2_tactic_atom: [ | "constr" ":" "(" Constr.lconstr ")" (* Ltac2 plugin *) | "open_constr" ":" "(" Constr.lconstr ")" (* Ltac2 plugin *) | "ident" ":" "(" lident ")" (* Ltac2 plugin *) -| "pattern" ":" "(" Constr.lconstr_pattern ")" (* Ltac2 plugin *) +| "pattern" ":" "(" Constr.cpattern ")" (* Ltac2 plugin *) | "reference" ":" "(" globref ")" (* Ltac2 plugin *) | "ltac1" ":" "(" ltac1_expr_in_env ")" (* Ltac2 plugin *) | "ltac1val" ":" "(" ltac1_expr_in_env ")" (* Ltac2 plugin *) ] ltac1_expr_in_env: [ -| test_ltac1_env LIST0 locident "|-" ltac1_expr (* Ltac2 plugin *) -| ltac1_expr (* Ltac2 plugin *) +| test_ltac1_env LIST0 locident "|-" ltac_expr5 (* Ltac2 plugin *) +| ltac_expr5 (* Ltac2 plugin *) ] tac2expr_in_env: [ -| test_ltac1_env LIST0 locident "|-" tac2expr6 (* Ltac2 plugin *) -| tac2expr6 (* Ltac2 plugin *) +| test_ltac1_env LIST0 locident "|-" ltac2_expr6 (* Ltac2 plugin *) +| ltac2_expr6 (* Ltac2 plugin *) ] G_LTAC2_let_clause: [ -| let_binder ":=" tac2expr6 (* Ltac2 plugin *) +| let_binder ":=" ltac2_expr6 (* Ltac2 plugin *) ] let_binder: [ | LIST1 G_LTAC2_input_fun (* Ltac2 plugin *) ] -tac2type5: [ -| tac2type2 "->" tac2type5 (* Ltac2 plugin *) -| tac2type2 (* Ltac2 plugin *) +ltac2_type5: [ +| ltac2_type2 "->" ltac2_type5 (* Ltac2 plugin *) +| ltac2_type2 (* Ltac2 plugin *) ] -tac2type2: [ -| tac2type1 "*" LIST1 tac2type1 SEP "*" (* Ltac2 plugin *) -| tac2type1 (* Ltac2 plugin *) +ltac2_type2: [ +| ltac2_type1 "*" LIST1 ltac2_type1 SEP "*" (* Ltac2 plugin *) +| ltac2_type1 (* Ltac2 plugin *) ] -tac2type1: [ -| tac2type0 Prim.qualid (* Ltac2 plugin *) -| tac2type0 (* Ltac2 plugin *) +ltac2_type1: [ +| ltac2_type0 Prim.qualid (* Ltac2 plugin *) +| ltac2_type0 (* Ltac2 plugin *) ] -tac2type0: [ -| "(" LIST1 tac2type5 SEP "," ")" OPT Prim.qualid (* Ltac2 plugin *) -| typ_param (* Ltac2 plugin *) +ltac2_type0: [ +| "(" LIST1 ltac2_type5 SEP "," ")" OPT Prim.qualid (* Ltac2 plugin *) +| ltac2_typevar (* Ltac2 plugin *) | "_" (* Ltac2 plugin *) | Prim.qualid (* Ltac2 plugin *) ] @@ -2720,7 +2714,7 @@ G_LTAC2_input_fun: [ ] tac2def_body: [ -| G_LTAC2_binder LIST0 G_LTAC2_input_fun ":=" tac2expr6 (* Ltac2 plugin *) +| G_LTAC2_binder LIST0 G_LTAC2_input_fun ":=" ltac2_expr6 (* Ltac2 plugin *) ] tac2def_val: [ @@ -2728,11 +2722,11 @@ tac2def_val: [ ] tac2def_mut: [ -| "Set" Prim.qualid OPT [ "as" locident ] ":=" tac2expr6 (* Ltac2 plugin *) +| "Set" Prim.qualid OPT [ "as" locident ] ":=" ltac2_expr6 (* Ltac2 plugin *) ] tac2typ_knd: [ -| tac2type5 (* Ltac2 plugin *) +| ltac2_type5 (* Ltac2 plugin *) | "[" ".." "]" (* Ltac2 plugin *) | "[" tac2alg_constructors "]" (* Ltac2 plugin *) | "{" tac2rec_fields "}" (* Ltac2 plugin *) @@ -2745,7 +2739,7 @@ tac2alg_constructors: [ tac2alg_constructor: [ | Prim.ident (* Ltac2 plugin *) -| Prim.ident "(" LIST0 tac2type5 SEP "," ")" (* Ltac2 plugin *) +| Prim.ident "(" LIST0 ltac2_type5 SEP "," ")" (* Ltac2 plugin *) ] tac2rec_fields: [ @@ -2756,7 +2750,7 @@ tac2rec_fields: [ ] tac2rec_field: [ -| mut_flag Prim.ident ":" tac2type5 (* Ltac2 plugin *) +| mut_flag Prim.ident ":" ltac2_type5 (* Ltac2 plugin *) ] tac2rec_fieldexprs: [ @@ -2767,13 +2761,13 @@ tac2rec_fieldexprs: [ ] tac2rec_fieldexpr: [ -| Prim.qualid ":=" tac2expr1 (* Ltac2 plugin *) +| Prim.qualid ":=" ltac2_expr1 (* Ltac2 plugin *) ] tac2typ_prm: [ | (* Ltac2 plugin *) -| typ_param (* Ltac2 plugin *) -| "(" LIST1 typ_param SEP "," ")" (* Ltac2 plugin *) +| ltac2_typevar (* Ltac2 plugin *) +| "(" LIST1 ltac2_typevar SEP "," ")" (* Ltac2 plugin *) ] tac2typ_def: [ @@ -2791,7 +2785,7 @@ tac2def_typ: [ ] tac2def_ext: [ -| "@" "external" locident ":" tac2type5 ":=" Prim.string Prim.string (* Ltac2 plugin *) +| "@" "external" locident ":" ltac2_type5 ":=" Prim.string Prim.string (* Ltac2 plugin *) ] syn_node: [ @@ -2799,11 +2793,11 @@ syn_node: [ | Prim.ident (* Ltac2 plugin *) ] -sexpr: [ +ltac2_scope: [ | Prim.string (* Ltac2 plugin *) | Prim.integer (* Ltac2 plugin *) | syn_node (* Ltac2 plugin *) -| syn_node "(" LIST1 sexpr SEP "," ")" (* Ltac2 plugin *) +| syn_node "(" LIST1 ltac2_scope SEP "," ")" (* Ltac2 plugin *) ] syn_level: [ @@ -2812,7 +2806,7 @@ syn_level: [ ] tac2def_syn: [ -| "Notation" LIST1 sexpr syn_level ":=" tac2expr6 (* Ltac2 plugin *) +| "Notation" LIST1 ltac2_scope syn_level ":=" ltac2_expr6 (* Ltac2 plugin *) ] lident: [ @@ -3030,28 +3024,28 @@ q_rewriting: [ ] G_LTAC2_tactic_then_last: [ -| "|" LIST0 ( OPT tac2expr6 ) SEP "|" (* Ltac2 plugin *) +| "|" LIST0 ( OPT ltac2_expr6 ) SEP "|" (* Ltac2 plugin *) | (* Ltac2 plugin *) ] -G_LTAC2_tactic_then_gen: [ -| tac2expr6 "|" G_LTAC2_tactic_then_gen (* Ltac2 plugin *) -| tac2expr6 ".." G_LTAC2_tactic_then_last (* Ltac2 plugin *) +G_LTAC2_for_each_goal: [ +| ltac2_expr6 "|" G_LTAC2_for_each_goal (* Ltac2 plugin *) +| ltac2_expr6 ".." G_LTAC2_tactic_then_last (* Ltac2 plugin *) | ".." G_LTAC2_tactic_then_last (* Ltac2 plugin *) -| tac2expr6 (* Ltac2 plugin *) -| "|" G_LTAC2_tactic_then_gen (* Ltac2 plugin *) +| ltac2_expr6 (* Ltac2 plugin *) +| "|" G_LTAC2_for_each_goal (* Ltac2 plugin *) | (* Ltac2 plugin *) ] q_dispatch: [ -| G_LTAC2_tactic_then_gen (* Ltac2 plugin *) +| G_LTAC2_for_each_goal (* Ltac2 plugin *) ] q_occurrences: [ | G_LTAC2_occs (* Ltac2 plugin *) ] -red_flag: [ +ltac2_red_flag: [ | "beta" (* Ltac2 plugin *) | "iota" (* Ltac2 plugin *) | "match" (* Ltac2 plugin *) @@ -3082,7 +3076,7 @@ G_LTAC2_delta_flag: [ ] G_LTAC2_strategy_flag: [ -| LIST1 red_flag (* Ltac2 plugin *) +| LIST1 ltac2_red_flag (* Ltac2 plugin *) | G_LTAC2_delta_flag (* Ltac2 plugin *) ] @@ -3100,12 +3094,12 @@ q_hintdb: [ ] G_LTAC2_match_pattern: [ -| "context" OPT Prim.ident "[" Constr.lconstr_pattern "]" (* Ltac2 plugin *) -| Constr.lconstr_pattern (* Ltac2 plugin *) +| "context" OPT Prim.ident "[" Constr.cpattern "]" (* Ltac2 plugin *) +| Constr.cpattern (* Ltac2 plugin *) ] G_LTAC2_match_rule: [ -| G_LTAC2_match_pattern "=>" tac2expr6 (* Ltac2 plugin *) +| G_LTAC2_match_pattern "=>" ltac2_expr6 (* Ltac2 plugin *) ] G_LTAC2_match_list: [ @@ -3126,16 +3120,16 @@ gmatch_pattern: [ ] gmatch_rule: [ -| gmatch_pattern "=>" tac2expr6 (* Ltac2 plugin *) +| gmatch_pattern "=>" ltac2_expr6 (* Ltac2 plugin *) ] -gmatch_list: [ +goal_match_list: [ | LIST1 gmatch_rule SEP "|" (* Ltac2 plugin *) | "|" LIST1 gmatch_rule SEP "|" (* Ltac2 plugin *) ] q_goal_matching: [ -| gmatch_list (* Ltac2 plugin *) +| goal_match_list (* Ltac2 plugin *) ] move_location: [ @@ -3169,7 +3163,7 @@ G_LTAC2_as_ipat: [ ] G_LTAC2_by_tactic: [ -| "by" tac2expr6 (* Ltac2 plugin *) +| "by" ltac2_expr6 (* Ltac2 plugin *) | (* Ltac2 plugin *) ] @@ -3192,11 +3186,11 @@ ltac2_entry: [ ] ltac2_expr: [ -| tac2expr6 (* Ltac2 plugin *) +| _ltac2_expr (* Ltac2 plugin *) ] tac2mode: [ -| ltac2_expr ltac_use_default (* Ltac2 plugin *) +| ltac2_expr6 ltac_use_default (* Ltac2 plugin *) | G_vernac.query_command (* Ltac2 plugin *) ] diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 61befe9f1f..12a7bc684d 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -3,10 +3,6 @@ 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 -tactic_mode: [ -| OPT ( toplevel_selector ":" ) "{" -] - term: [ | term_forall_or_fun | term_let @@ -191,6 +187,15 @@ where: [ | "before" ident ] +add_zify: [ +| [ "InjTyp" | "BinOp" | "UnOp" | "CstOp" | "BinRel" | "UnOpSpec" | "BinOpSpec" ] (* Micromega plugin *) +| [ "PropOp" | "PropBinOp" | "PropUOp" | "Saturate" ] (* Micromega plugin *) +] + +show_zify: [ +| [ "InjTyp" | "BinOp" | "UnOp" | "CstOp" | "BinRel" | "UnOpSpec" | "BinOpSpec" | "Spec" ] (* Micromega plugin *) +] + REACHABLE: [ | command | simple_tactic @@ -315,11 +320,11 @@ univ_constraint: [ ] term_fix: [ -| "let" "fix" fix_body "in" term -| "fix" fix_body OPT ( LIST1 ( "with" fix_body ) "for" ident ) +| "let" "fix" fix_decl "in" term +| "fix" fix_decl OPT ( LIST1 ( "with" fix_decl ) "for" ident ) ] -fix_body: [ +fix_decl: [ | ident LIST0 binder OPT fixannot OPT ( ":" type ) ":=" term ] @@ -448,9 +453,7 @@ vernac_aux: [ ] subprf: [ -| bullet | "{" -| "}" ] fix_definition: [ @@ -538,8 +541,12 @@ variant_definition: [ | ident_decl LIST0 binder OPT [ "|" LIST0 binder ] OPT [ ":" type ] ":=" OPT "|" LIST1 constructor SEP "|" OPT decl_notations ] +singleton_class_definition: [ +| OPT ">" ident_decl LIST0 binder OPT [ ":" sort ] ":=" constructor +] + record_definition: [ -| OPT ">" ident_decl LIST0 binder OPT [ ":" type ] OPT ident "{" LIST0 record_field SEP ";" OPT ";" "}" OPT decl_notations +| OPT ">" ident_decl LIST0 binder OPT [ ":" sort ] OPT ( ":=" OPT ident "{" LIST0 record_field SEP ";" OPT ";" "}" ) ] record_field: [ @@ -582,11 +589,8 @@ cofix_definition: [ ] scheme_kind: [ -| "Induction" "for" reference "Sort" sort_family -| "Minimality" "for" reference "Sort" sort_family -| "Elimination" "for" reference "Sort" sort_family -| "Case" "for" reference "Sort" sort_family | "Equality" "for" reference +| [ "Induction" | "Minimality" | "Elimination" | "Case" ] "for" reference "Sort" sort_family ] sort_family: [ @@ -714,7 +718,7 @@ simple_reserv: [ ] command: [ -| "Goal" term +| "Goal" type | "Pwd" | "Cd" OPT string | "Load" OPT "Verbose" [ string | ident ] @@ -723,6 +727,8 @@ command: [ | "Locate" "Term" reference | "Locate" "Module" qualid | "Info" natural ltac_expr +| "Add" "Zify" add_zify one_term (* Micromega plugin *) +| "Show" "Zify" show_zify (* Micromega plugin *) | "Locate" "Ltac" qualid | "Locate" "Library" qualid | "Locate" "File" string @@ -798,7 +804,7 @@ command: [ | "Extraction" "NoInline" LIST1 qualid (* extraction plugin *) | "Print" "Extraction" "Inline" (* extraction plugin *) | "Reset" "Extraction" "Inline" (* extraction plugin *) -| "Extraction" "Implicit" qualid "[" LIST0 int_or_id "]" (* extraction plugin *) +| "Extraction" "Implicit" qualid "[" LIST0 [ ident | integer ] "]" (* extraction plugin *) | "Extraction" "Blacklist" LIST1 ident (* extraction plugin *) | "Print" "Extraction" "Blacklist" (* extraction plugin *) | "Reset" "Extraction" "Blacklist" (* extraction plugin *) @@ -810,7 +816,7 @@ command: [ | "Proof" "Mode" string | "Proof" term | "Abort" OPT [ "All" | ident ] -| "Existential" natural OPT ( ":" term ) ":=" term +| "Existential" natural OPT ( ":" type ) ":=" term | "Admitted" | "Qed" | "Save" ident @@ -835,10 +841,10 @@ command: [ | "Comments" LIST0 [ one_term | string | natural ] | "Declare" "Instance" ident_decl LIST0 binder ":" term OPT hint_info | "Declare" "Scope" scope_name -| "Obligation" natural OPT ( "of" ident ) OPT ( ":" term OPT ( "with" ltac_expr ) ) +| "Obligation" natural OPT ( "of" ident ) OPT ( ":" type OPT ( "with" ltac_expr ) ) | "Next" "Obligation" OPT ( "of" ident ) OPT ( "with" ltac_expr ) | "Solve" "Obligation" natural OPT ( "of" ident ) "with" ltac_expr -| "Solve" "Obligations" OPT ( OPT ( "of" ident ) "with" ltac_expr ) +| "Solve" "Obligations" OPT ( "of" ident ) OPT ( "with" ltac_expr ) | "Solve" "All" "Obligations" OPT ( "with" ltac_expr ) | "Admit" "Obligations" OPT ( "of" ident ) | "Obligation" "Tactic" ":=" ltac_expr @@ -862,17 +868,6 @@ command: [ | "Reset" "Ltac" "Profile" | "Show" "Ltac" "Profile" OPT [ "CutOff" integer | string ] | "Show" "Lia" "Profile" (* micromega plugin *) -| "Add" "Zify" "InjTyp" one_term (* micromega plugin *) -| "Add" "Zify" "BinOp" one_term (* micromega plugin *) -| "Add" "Zify" "UnOp" one_term (* micromega plugin *) -| "Add" "Zify" "CstOp" one_term (* micromega plugin *) -| "Add" "Zify" "BinRel" one_term (* micromega plugin *) -| "Add" "Zify" "PropOp" one_term (* micromega plugin *) -| "Add" "Zify" "PropBinOp" one_term (* micromega plugin *) -| "Add" "Zify" "PropUOp" one_term (* micromega plugin *) -| "Add" "Zify" "BinOpSpec" one_term (* micromega plugin *) -| "Add" "Zify" "UnOpSpec" one_term (* micromega plugin *) -| "Add" "Zify" "Saturate" one_term (* micromega plugin *) | "Add" "InjTyp" one_term (* micromega plugin *) | "Add" "BinOp" one_term (* micromega plugin *) | "Add" "UnOp" one_term (* micromega plugin *) @@ -884,25 +879,19 @@ command: [ | "Add" "BinOpSpec" one_term (* micromega plugin *) | "Add" "UnOpSpec" one_term (* micromega plugin *) | "Add" "Saturate" one_term (* micromega plugin *) -| "Show" "Zify" "InjTyp" (* micromega plugin *) -| "Show" "Zify" "BinOp" (* micromega plugin *) -| "Show" "Zify" "UnOp" (* micromega plugin *) -| "Show" "Zify" "CstOp" (* micromega plugin *) -| "Show" "Zify" "BinRel" (* micromega plugin *) -| "Show" "Zify" "UnOpSpec" (* micromega plugin *) -| "Show" "Zify" "BinOpSpec" (* micromega plugin *) | "Show" "Zify" "Spec" (* micromega plugin *) | "Add" "Ring" ident ":" one_term OPT ( "(" LIST1 ring_mod SEP "," ")" ) (* ring plugin *) | "Print" "Rings" (* ring plugin *) | "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" ) (* ring plugin *) | "Print" "Fields" (* ring plugin *) -| "Number" "Notation" qualid qualid qualid ":" ident OPT numeral_modifier +| "Number" "Notation" qualid qualid qualid ":" scope_name OPT numeral_modifier +| "Numeral" "Notation" qualid qualid qualid ":" scope_name OPT numeral_modifier | "Hint" "Cut" "[" hints_path "]" OPT ( ":" LIST1 ident ) -| "Typeclasses" "Transparent" LIST0 qualid -| "Typeclasses" "Opaque" LIST0 qualid -| "Typeclasses" "eauto" ":=" OPT "debug" OPT ( "(" eauto_search_strategy_name ")" ) OPT integer -| "Proof" "with" ltac_expr OPT [ "using" section_subset_expr ] -| "Proof" "using" section_subset_expr OPT [ "with" ltac_expr ] +| "Typeclasses" "Transparent" LIST1 qualid +| "Typeclasses" "Opaque" LIST1 qualid +| "Typeclasses" "eauto" ":=" OPT "debug" OPT ( "(" [ "bfs" | "dfs" ] ")" ) OPT natural +| "Proof" "with" ltac_expr OPT [ "using" section_var_expr ] +| "Proof" "using" section_var_expr OPT [ "with" ltac_expr ] | "Tactic" "Notation" OPT ( "(" "at" "level" natural ")" ) LIST1 ltac_production_item ":=" ltac_expr | "Print" "Rewrite" "HintDb" ident | "Print" "Ltac" qualid @@ -911,8 +900,8 @@ command: [ | "Set" "Firstorder" "Solver" ltac_expr | "Print" "Firstorder" "Solver" | "Function" fix_definition LIST0 ( "with" fix_definition ) -| "Functional" "Scheme" fun_scheme_arg LIST0 ( "with" fun_scheme_arg ) -| "Functional" "Case" fun_scheme_arg (* funind plugin *) +| "Functional" "Scheme" func_scheme_def LIST0 ( "with" func_scheme_def ) +| "Functional" "Case" func_scheme_def (* funind plugin *) | "Generate" "graph" "for" qualid (* funind plugin *) | "Hint" "Rewrite" OPT [ "->" | "<-" ] LIST1 one_term OPT ( "using" ltac_expr ) OPT ( ":" LIST0 ident ) | "Derive" "Inversion_clear" ident "with" one_term OPT ( "Sort" sort_family ) @@ -921,7 +910,6 @@ command: [ | "Derive" "Dependent" "Inversion_clear" ident "with" one_term "Sort" sort_family | "Declare" "Left" "Step" one_term | "Declare" "Right" "Step" one_term -| "Numeral" "Notation" qualid qualid qualid ":" scope_name OPT numeral_modifier | "String" "Notation" qualid qualid qualid ":" scope_name | "SubClass" ident_decl def_body | thm_token ident_decl LIST0 binder ":" type LIST0 [ "with" ident_decl LIST0 binder ":" type ] @@ -944,13 +932,14 @@ command: [ | "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 ) +| "Class" record_definition +| "Class" singleton_class_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 | "End" ident -| "Collection" ident ":=" section_subset_expr +| "Collection" ident ":=" section_var_expr | "Require" OPT [ "Import" | "Export" ] LIST1 qualid | "From" dirpath "Require" OPT [ "Import" | "Export" ] LIST1 qualid | "Import" LIST1 filtered_import @@ -962,11 +951,11 @@ command: [ | "Strategy" LIST1 [ strategy_level "[" LIST1 reference "]" ] | "Canonical" OPT "Structure" ident_decl def_body | "Canonical" OPT "Structure" reference -| "Coercion" qualid OPT univ_decl def_body +| "Coercion" ident OPT univ_decl def_body | "Identity" "Coercion" ident ":" class ">->" class | "Coercion" reference ":" class ">->" class | "Context" LIST1 binder -| "Instance" OPT ( ident_decl LIST0 binder ) ":" term OPT hint_info OPT [ ":=" "{" LIST0 field_def "}" | ":=" term ] +| "Instance" OPT ( ident_decl LIST0 binder ) ":" type OPT hint_info OPT [ ":=" "{" LIST0 field_def "}" | ":=" term ] | "Existing" "Instance" qualid OPT hint_info | "Existing" "Instances" LIST1 qualid OPT [ "|" natural ] | "Existing" "Class" qualid @@ -1012,35 +1001,26 @@ command: [ | "Show" "Goal" natural "at" natural ] -section_subset_expr: [ -| LIST0 starredidentref -| ssexpr +section_var_expr: [ +| LIST0 starred_ident_ref +| OPT "-" section_var_expr50 ] -ssexpr: [ -| "-" ssexpr50 -| ssexpr50 +section_var_expr50: [ +| section_var_expr0 "-" section_var_expr0 +| section_var_expr0 "+" section_var_expr0 +| section_var_expr0 ] -ssexpr50: [ -| ssexpr0 "-" ssexpr0 -| ssexpr0 "+" ssexpr0 -| ssexpr0 +section_var_expr0: [ +| starred_ident_ref +| "(" section_var_expr ")" OPT "*" ] -ssexpr0: [ -| starredidentref -| "(" LIST0 starredidentref ")" -| "(" LIST0 starredidentref ")" "*" -| "(" ssexpr ")" -| "(" ssexpr ")" "*" -] - -starredidentref: [ -| ident -| ident "*" -| "Type" -| "Type" "*" +starred_ident_ref: [ +| ident OPT "*" +| "Type" OPT "*" +| "All" ] dirpath: [ @@ -1137,13 +1117,13 @@ lident: [ destruction_arg: [ | natural -| constr_with_bindings +| one_term OPT ( "with" bindings ) | constr_with_bindings_arg ] constr_with_bindings_arg: [ -| ">" constr_with_bindings -| constr_with_bindings +| ">" one_term OPT ( "with" bindings ) +| one_term OPT ( "with" bindings ) ] clause_dft_concl: [ @@ -1262,11 +1242,6 @@ qhyp: [ | lident (* Ltac2 plugin *) ] -int_or_id: [ -| ident -| integer (* extraction plugin *) -] - language: [ | "OCaml" (* extraction plugin *) | "Haskell" (* extraction plugin *) @@ -1274,10 +1249,6 @@ language: [ | "JSON" (* extraction plugin *) ] -fun_scheme_arg: [ -| ident ":=" "Induction" "for" qualid "Sort" sort_family (* funind plugin *) -] - ring_mod: [ | "decidable" one_term (* ring plugin *) | "abstract" (* ring plugin *) @@ -1314,11 +1285,6 @@ hints_path: [ | hints_path hints_path ] -eauto_search_strategy_name: [ -| "bfs" -| "dfs" -] - class: [ | "Funclass" | "Sortclass" @@ -1390,7 +1356,7 @@ simple_tactic: [ | "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 ) +| "specialize" one_term OPT ( "with" bindings ) OPT ( "as" simple_intropattern ) | "symmetry" OPT ( "in" in_clause ) | "split" OPT ( "with" bindings ) | "esplit" OPT ( "with" bindings ) @@ -1411,6 +1377,10 @@ simple_tactic: [ | "generalize" "dependent" one_term | "replace" one_term "with" one_term OPT clause_dft_concl OPT ( "by" ltac_expr3 ) | "replace" OPT [ "->" | "<-" ] one_term OPT clause_dft_concl +| "setoid_replace" one_term "with" one_term OPT ( "using" "relation" one_term ) OPT ( "in" ident ) OPT ( "at" LIST1 int_or_var ) OPT ( "by" ltac_expr3 ) +| OPT ( [ natural | "[" ident "]" ] ":" ) "{" +| bullet +| "}" | "try" ltac_expr3 | "do" int_or_var ltac_expr3 | "timeout" int_or_var ltac_expr3 @@ -1456,7 +1426,7 @@ simple_tactic: [ | "decompose" "sum" one_term | "decompose" "record" one_term | "absurd" one_term -| "contradiction" OPT constr_with_bindings +| "contradiction" OPT ( one_term OPT ( "with" bindings ) ) | "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 ) @@ -1465,7 +1435,7 @@ simple_tactic: [ | "notypeclasses" "refine" one_term | "simple" "notypeclasses" "refine" one_term | "solve_constraints" -| "subst" OPT ( LIST1 ident ) +| "subst" LIST0 ident | "simple" "subst" | "evar" "(" ident ":" term ")" | "evar" one_term @@ -1529,9 +1499,7 @@ simple_tactic: [ | "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 -| "typeclasses" "eauto" OPT int_or_var +| "typeclasses" "eauto" OPT "bfs" OPT int_or_var OPT ( "with" LIST1 ident ) | "head_of_constr" ident one_term | "not_evar" one_term | "is_ground" one_term @@ -1540,9 +1508,9 @@ simple_tactic: [ | "progress_evars" ltac_expr | "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 +| "substitute" OPT [ "->" | "<-" ] one_term OPT ( "with" bindings ) +| "setoid_rewrite" OPT [ "->" | "<-" ] one_term OPT ( "with" bindings ) OPT ( "at" occurrences ) OPT ( "in" ident ) +| "setoid_rewrite" OPT [ "->" | "<-" ] one_term OPT ( "with" bindings ) "in" ident "at" occurrences | "setoid_symmetry" OPT ( "in" ident ) | "setoid_reflexivity" | "setoid_transitivity" one_term @@ -1555,8 +1523,8 @@ simple_tactic: [ | "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 ) +| "elim" constr_with_bindings_arg OPT ( "using" one_term OPT ( "with" bindings ) ) +| "eelim" constr_with_bindings_arg OPT ( "using" one_term OPT ( "with" bindings ) ) | "case" induction_clause_list | "ecase" induction_clause_list | "fix" ident natural OPT ( "with" LIST1 fixdecl ) @@ -1619,8 +1587,8 @@ simple_tactic: [ | "firstorder" OPT ltac_expr firstorder_rhs | "gintuition" OPT ltac_expr | "functional" "inversion" [ ident | natural ] OPT qualid (* funind plugin *) -| "functional" "induction" 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 *) +| "functional" "induction" term OPT ( "using" one_term OPT ( "with" bindings ) ) OPT ( "as" simple_intropattern ) (* funind plugin *) +| "soft" "functional" "induction" LIST1 one_term OPT ( "using" one_term OPT ( "with" bindings ) ) OPT ( "as" simple_intropattern ) (* funind plugin *) | "psatz_Z" OPT int_or_var ltac_expr | "xlia" ltac_expr (* micromega plugin *) | "xnlia" ltac_expr (* micromega plugin *) @@ -1663,14 +1631,14 @@ simple_tactic: [ | "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 ) +| "field" OPT ( "[" LIST1 one_term "]" ) +| "field_simplify" OPT ( "[" LIST1 one_term "]" ) LIST1 one_term OPT ( "in" ident ) +| "field_simplify_eq" OPT ( "[" LIST1 one_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 ) +| "nsatz" OPT ( "with" "radicalmax" ":=" one_term "strategy" ":=" one_term "parameters" ":=" one_term "variables" ":=" one_term ) +| "psatz" one_term OPT int_or_var +| "ring" OPT ( "[" LIST1 one_term "]" ) +| "ring_simplify" OPT ( "[" LIST1 one_term "]" ) LIST1 one_term OPT ( "in" ident ) | "match" ltac2_expr5 "with" OPT ltac2_branches "end" | qualid LIST1 tactic_arg ] @@ -1718,7 +1686,7 @@ induction_clause: [ ] induction_clause_list: [ -| LIST1 induction_clause SEP "," OPT ( "using" constr_with_bindings ) OPT opt_clause +| LIST1 induction_clause SEP "," OPT ( "using" one_term OPT ( "with" bindings ) ) OPT opt_clause ] auto_using: [ @@ -1764,13 +1732,8 @@ simple_intropattern_closed: [ | naming_intropattern ] -simple_binding: [ -| "(" ident ":=" term ")" -| "(" natural ":=" term ")" -] - bindings: [ -| LIST1 simple_binding +| LIST1 ( "(" [ ident | natural ] ":=" term ")" ) | LIST1 one_term ] @@ -2184,10 +2147,6 @@ cofixdecl: [ | "(" ident LIST0 simple_binder ":" term ")" ] -constr_with_bindings: [ -| one_term OPT ( "with" bindings ) -] - conversion: [ | one_term | one_term "with" one_term @@ -2200,12 +2159,8 @@ firstorder_using: [ | "using" qualid qualid LIST0 qualid ] -fun_ind_using: [ -| "using" constr_with_bindings (* funind plugin *) -] - -with_names: [ -| "as" simple_intropattern (* funind plugin *) +func_scheme_def: [ +| ident ":=" "Induction" "for" qualid "Sort" sort_family (* funind plugin *) ] occurrences: [ |