diff options
Diffstat (limited to 'doc/tools/docgram')
| -rw-r--r-- | doc/tools/docgram/README.md | 37 | ||||
| -rw-r--r-- | doc/tools/docgram/common.edit_mlg | 540 | ||||
| -rw-r--r-- | doc/tools/docgram/doc_grammar.ml | 541 | ||||
| -rw-r--r-- | doc/tools/docgram/fullGrammar | 750 | ||||
| -rw-r--r-- | doc/tools/docgram/orderedGrammar | 688 |
5 files changed, 2175 insertions, 381 deletions
diff --git a/doc/tools/docgram/README.md b/doc/tools/docgram/README.md index 2d29743d78..14f87e5885 100644 --- a/doc/tools/docgram/README.md +++ b/doc/tools/docgram/README.md @@ -37,13 +37,16 @@ for documentation purposes: 1. The tool reads all the `mlg` files and generates `fullGrammar`, which includes all the grammar without the actions for each production or the OCaml code. This file is provided as a convenience to make it easier to examine the (mostly) - unprocessed grammar of the mlg files with less clutter. Nonterminals that use - levels (`"5" RIGHTA` below) are modified, for example: + unprocessed grammar of the mlg files with less clutter. This step includes two + transformations that rename some nonterminal symbols: + + First, nonterminals that use levels (`"5" RIGHTA` below) are modified, for example: ``` tactic_expr: [ "5" RIGHTA [ te = binder_tactic -> { te } ] + [ "4" ... ``` becomes @@ -55,6 +58,17 @@ for documentation purposes: ] ``` + Second, nonterminals that are local to an .mlg will be renamed, if necessary, to + make them unique. For example, `strategy_level` is defined as a local nonterminal + in both `g_prim.mlg` and in `extraargs.mlg`. The nonterminal defined in the former + remains `strategy_level` because it happens to be processed before the latter, + in which the nonterminal is renamed to `EXTRAARGS_strategy_level` to make the local + symbol unique. + + Nonterminals listed after `GLOBAL:` are global; otherwise they are local. + + References to renamed symbols are updated with the modified names. + 2. The tool applies grammar editing operations specified by `common.edit_mlg` to generate `editedGrammar`. @@ -227,9 +241,22 @@ to the grammar. The end of the existing `prodn` is recognized by a blank line. -### Other details +### Tagging productions + +`doc_grammar` tags the origin of productions from plugins that aren't automatically +loaded. In grammar files, they appear as `(* XXX plugin *)`. In rsts, productions +generated by `.. insertprodn` will include where relevant three spaces as (a delimiter) +and a tag name after each production, which Sphinx will show on the far right-hand side +of the production. + +The origin of a production can be specified explicitly in `common.edit_mlg` with the +`TAG name` appearing at the end of a production. `name` must be in quotes if it +contains whitespace characters. Some edit operations preserve the +tags, but others, such as `REPLACE ... WITH ...` do not. + +A mapping from filenames to tags (e.g. "g_ltac2.mlg" is "Ltac2") is hard-coded as is +filtering to avoid showing tags for, say, Ltac2 productions from appearing on every +production in that chapter. -The output identifies productions from plugins that aren't automatically loaded with -`(* XXX plugin *)` in grammar files and with `(XXX plugin)` in productionlists. If desired, this mechanism could be extended to tag certain productions as deprecated, perhaps in conjunction with a coqpp change. diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 80f825358f..6625e07d05 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -12,19 +12,98 @@ DOC_GRAMMAR +(* first, fixup symbols duplicated across files *) +lglob: [ +| lconstr +| DELETE EXTRAARGS_lconstr +] + +hint: [ +| "Extern" natural OPT constr_pattern "=>" tactic +] + +(* todo: does ARGUMENT EXTEND make the symbol global? It is in both extraargs and extratactics *) +strategy_level_or_var: [ +| DELETE EXTRAARGS_strategy_level +| strategy_level +] + +operconstr0: [ +| "ltac" ":" "(" tactic_expr5 ")" +] + +EXTRAARGS_natural: [ | DELETENT ] +EXTRAARGS_lconstr: [ | DELETENT ] +EXTRAARGS_strategy_level: [ | DELETENT ] +G_LTAC_hint: [ | DELETENT ] +G_LTAC_operconstr0: [ | DELETENT ] + +G_REWRITE_binders: [ +| DELETE Pcoq.Constr.binders +| binders +] + +G_TACTIC_in_clause: [ +| in_clause +| MOVEALLBUT in_clause +| in_clause +] + +SPLICE: [ +| G_REWRITE_binders +| G_TACTIC_in_clause +] + +RENAME: [ +| G_LTAC2_delta_flag ltac2_delta_flag +| G_LTAC2_strategy_flag ltac2_strategy_flag +| G_LTAC2_binder ltac2_binder +| G_LTAC2_branches ltac2_branches +| G_LTAC2_let_clause ltac2_let_clause +| G_LTAC2_tactic_atom ltac2_tactic_atom +| G_LTAC2_rewriter ltac2_rewriter +| G_LTAC2_constr_with_bindings ltac2_constr_with_bindings +| G_LTAC2_match_rule ltac2_match_rule +| G_LTAC2_match_pattern ltac2_match_pattern +| G_LTAC2_intropatterns ltac2_intropatterns +| G_LTAC2_simple_intropattern ltac2_simple_intropattern +| G_LTAC2_simple_intropattern_closed ltac2_simple_intropattern_closed +| G_LTAC2_or_and_intropattern ltac2_or_and_intropattern +| G_LTAC2_equality_intropattern ltac2_equality_intropattern +| G_LTAC2_naming_intropattern ltac2_naming_intropattern +| G_LTAC2_destruction_arg ltac2_destruction_arg +| G_LTAC2_with_bindings ltac2_with_bindings +| G_LTAC2_bindings ltac2_bindings +| G_LTAC2_simple_binding ltac2_simple_binding +| G_LTAC2_in_clause ltac2_in_clause +| G_LTAC2_occs ltac2_occs +| G_LTAC2_occs_nums ltac2_occs_nums +| G_LTAC2_concl_occ ltac2_concl_occ +| G_LTAC2_hypident_occ ltac2_hypident_occ +| G_LTAC2_hypident ltac2_hypident +| G_LTAC2_induction_clause ltac2_induction_clause +| G_LTAC2_as_or_and_ipat ltac2_as_or_and_ipat +| 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_tactic_then_last ltac2_tactic_then_last +| G_LTAC2_as_name ltac2_as_name +| G_LTAC2_as_ipat ltac2_as_ipat +| G_LTAC2_by_tactic ltac2_by_tactic +| G_LTAC2_match_list ltac2_match_list +] + (* renames to eliminate qualified names put other renames at the end *) RENAME: [ (* map missing names for rhs *) | Constr.constr term -| Constr.constr_pattern constr_pattern | Constr.global global | Constr.lconstr lconstr | Constr.lconstr_pattern cpattern | G_vernac.query_command query_command | G_vernac.section_subset_expr section_subset_expr -| Pltac.tactic tactic -| Pltac.tactic_expr tactic_expr5 | Prim.ident ident | Prim.reference reference | Pvernac.Vernac_.main_entry vernac_control @@ -69,6 +148,8 @@ DELETE: [ | test_name_colon | test_pipe_closedcurly | ensure_fixannot +| test_array_opening +| test_array_closing (* SSR *) (* | ssr_null_entry *) @@ -125,6 +206,26 @@ tactic_then_last: [ | OPTINREF ] +ltac2_tactic_then_last: [ +| REPLACE "|" LIST0 ( OPT tac2expr6 ) SEP "|" (* Ltac2 plugin *) +| WITH LIST0 ( "|" OPT tac2expr6 ) TAG Ltac2 +] + +ltac2_goal_tactics: [ +| LIST0 ( OPT tac2expr6 ) SEP "|" TAG Ltac2 +] + +ltac2_tactic_then_gen: [ | DELETENT ] + +ltac2_tactic_then_gen: [ +| ltac2_goal_tactics TAG Ltac2 +| OPT ( ltac2_goal_tactics "|" ) OPT tac2expr6 ".." OPT ( "|" ltac2_goal_tactics ) TAG Ltac2 +] + +ltac2_tactic_then_last: [ +| OPTINREF +] + reference: [ | DELETENT ] reference: [ @@ -155,15 +256,6 @@ dirpath: [ | WITH LIST0 ( ident "." ) ident ] -binders: [ -| DELETE Pcoq.Constr.binders (* todo: not sure why there are 2 "binders:" *) -] - -lconstr: [ -| DELETE l_constr -] - - let_type_cstr: [ | DELETE OPT [ ":" lconstr ] | type_cstr @@ -309,6 +401,8 @@ operconstr0: [ | 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 ] fix_decls: [ @@ -551,9 +645,28 @@ delta_flag: [ | OPTINREF ] +ltac2_delta_flag: [ +| EDIT ADD_OPT "-" "[" refglobals "]" (* Ltac2 plugin *) +] + +ltac2_branches: [ +| EDIT ADD_OPT "|" LIST1 branch SEP "|" (* Ltac2 plugin *) +| OPTINREF +] + +RENAME: [ +| red_flag ltac2_red_flag +| red_flags red_flag +] + +RENAME: [ +] + strategy_flag: [ | REPLACE OPT delta_flag | WITH delta_flag +(*| REPLACE LIST1 red_flags +| WITH LIST1 red_flag*) | (* empty *) | OPTINREF ] @@ -841,7 +954,7 @@ simple_tactic: [ | DELETE "autorewrite" "with" LIST1 preident clause "using" tactic | DELETE "autorewrite" "*" "with" LIST1 preident clause | REPLACE "autorewrite" "*" "with" LIST1 preident clause "using" tactic -| WITH "autorewrite" OPT "*" "with" LIST1 preident clause_dft_concl OPT ( "using" tactic ) +| WITH "autorewrite" OPT "*" "with" LIST1 preident clause OPT ( "using" tactic ) | DELETE "cofix" ident | REPLACE "cofix" ident "with" LIST1 cofixdecl | WITH "cofix" ident OPT ( "with" LIST1 cofixdecl ) @@ -900,7 +1013,7 @@ simple_tactic: [ | DELETE "replace" "->" uconstr clause | DELETE "replace" "<-" uconstr clause | DELETE "replace" uconstr clause -| "replace" orient uconstr clause_dft_concl (* todo: fix 'clause' *) +| "replace" orient uconstr clause | REPLACE "rewrite" "*" orient uconstr "in" hyp "at" occurrences by_arg_tac | WITH "rewrite" "*" orient uconstr OPT ( "in" hyp ) OPT ( "at" occurrences by_arg_tac ) | DELETE "rewrite" "*" orient uconstr "in" hyp by_arg_tac @@ -1163,6 +1276,7 @@ command: [ | REPLACE "String" "Notation" reference reference reference ":" ident | WITH "String" "Notation" reference reference reference ":" scope_name +| DELETE "Ltac2" ltac2_entry (* was split up *) ] option_setting: [ @@ -1180,14 +1294,10 @@ syntax: [ | WITH "Undelimit" "Scope" scope_name | REPLACE "Bind" "Scope" IDENT; "with" LIST1 class_rawexpr | WITH "Bind" "Scope" scope_name; "with" LIST1 class_rawexpr -| REPLACE "Infix" ne_lstring ":=" constr [ "(" LIST1 syntax_modifier SEP "," ")" | ] OPT [ ":" IDENT ] -| WITH "Infix" ne_lstring ":=" constr OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" scope_name ] -| REPLACE "Notation" lstring ":=" constr [ "(" LIST1 syntax_modifier SEP "," ")" | ] OPT [ ":" IDENT ] -| WITH "Notation" lstring ":=" constr OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" scope_name ] -| REPLACE "Reserved" "Infix" ne_lstring [ "(" LIST1 syntax_modifier SEP "," ")" | ] -| WITH "Reserved" "Infix" ne_lstring OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] -| REPLACE "Reserved" "Notation" ne_lstring [ "(" LIST1 syntax_modifier SEP "," ")" | ] -| WITH "Reserved" "Notation" ne_lstring OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] +| REPLACE "Infix" ne_lstring ":=" constr syntax_modifiers OPT [ ":" IDENT ] +| WITH "Infix" ne_lstring ":=" constr syntax_modifiers OPT [ ":" scope_name ] +| REPLACE "Notation" lstring ":=" constr syntax_modifiers OPT [ ":" IDENT ] +| WITH "Notation" lstring ":=" constr syntax_modifiers OPT [ ":" scope_name ] ] syntax_modifier: [ @@ -1458,8 +1568,33 @@ by_tactic: [ ] rewriter: [ -| REPLACE [ "?" | LEFTQMARK ] constr_with_bindings_arg -| WITH "?" constr_with_bindings_arg +| DELETE "!" constr_with_bindings_arg +| DELETE [ "?" | LEFTQMARK ] constr_with_bindings_arg +| DELETE natural "!" constr_with_bindings_arg +| DELETE natural [ "?" | LEFTQMARK ] constr_with_bindings_arg +| DELETE natural constr_with_bindings_arg +| DELETE constr_with_bindings_arg +| OPT natural OPT [ "?" | "!" ] constr_with_bindings_arg +] + +ltac2_rewriter: [ +| DELETE "!" ltac2_constr_with_bindings (* Ltac2 plugin *) +| DELETE [ "?" | LEFTQMARK ] ltac2_constr_with_bindings +| DELETE lnatural "!" ltac2_constr_with_bindings (* Ltac2 plugin *) +| DELETE lnatural [ "?" | LEFTQMARK ] ltac2_constr_with_bindings +| DELETE lnatural ltac2_constr_with_bindings (* Ltac2 plugin *) +| DELETE ltac2_constr_with_bindings (* Ltac2 plugin *) +| OPT natural OPT [ "?" | "!" ] ltac2_constr_with_bindings +] + +tac2expr0: [ +| DELETE "(" ")" +] + +tac2type_body: [ +| REPLACE ":=" tac2typ_knd (* Ltac2 plugin *) +| WITH [ ":=" | "::=" ] tac2typ_knd TAG Ltac2 +| DELETE "::=" tac2typ_knd (* Ltac2 plugin *) ] intropattern_or_list_or: [ @@ -1525,6 +1660,12 @@ in_clause: [ | DELETE LIST0 hypident_occ SEP "," ] +ltac2_in_clause: [ +| REPLACE LIST0 ltac2_hypident_occ SEP "," "|-" ltac2_concl_occ (* Ltac2 plugin *) +| WITH LIST0 ltac2_hypident_occ SEP "," OPT ( "|-" ltac2_concl_occ ) TAG Ltac2 +| DELETE LIST0 ltac2_hypident_occ SEP "," (* Ltac2 plugin *) +] + concl_occ: [ | OPTINREF ] @@ -1597,8 +1738,12 @@ by_notation: [ ] decl_notation: [ -| REPLACE ne_lstring ":=" constr only_parsing OPT [ ":" IDENT ] -| WITH ne_lstring ":=" constr only_parsing OPT [ ":" scope_name ] +| REPLACE ne_lstring ":=" constr syntax_modifiers OPT [ ":" IDENT ] +| WITH ne_lstring ":=" constr syntax_modifiers OPT [ ":" scope_name ] +] + +syntax_modifiers: [ +| OPTINREF ] @@ -1636,6 +1781,15 @@ tactic_mode: [ | DELETE command ] +sexpr: [ +| REPLACE syn_node (* Ltac2 plugin *) +| WITH name TAG Ltac2 +| REPLACE syn_node "(" LIST1 sexpr SEP "," ")" (* Ltac2 plugin *) +| WITH name "(" LIST1 sexpr SEP "," ")" TAG Ltac2 +] + +syn_node: [ | DELETENT ] + RENAME: [ | toplevel_selector toplevel_selector_temp ] @@ -1754,9 +1908,24 @@ tactic_value: [ | [ value_tactic | syn_value ] ] + +(* defined in Ltac2/Notations.v *) + +ltac2_match_key: [ +| "lazy_match!" +| "match!" +| "multi_match!" +] + +ltac2_constructs: [ +| ltac2_match_key tac2expr6 "with" ltac2_match_list "end" +| ltac2_match_key OPT "reverse" "goal" "with" gmatch_list "end" +] + simple_tactic: [ | ltac_builtins | ltac_constructs +| ltac2_constructs | ltac_defined_tactics | tactic_notation_tactics ] @@ -1767,6 +1936,24 @@ tacdef_body: [ | DELETE global ltac_def_kind tactic_expr5 ] +tac2def_typ: [ +| REPLACE "Type" rec_flag LIST1 tac2typ_def SEP "with" (* Ltac2 plugin *) +| WITH "Type" rec_flag tac2typ_def LIST0 ( "with" tac2typ_def ) TAG Ltac2 +] + +tac2def_val: [ +| REPLACE mut_flag rec_flag LIST1 tac2def_body SEP "with" (* Ltac2 plugin *) +| WITH mut_flag rec_flag tac2def_body LIST0 ( "with" tac2def_body ) TAG Ltac1 +] + +tac2alg_constructors: [ +| REPLACE "|" LIST1 tac2alg_constructor SEP "|" (* Ltac2 plugin *) +| WITH OPT "|" LIST1 tac2alg_constructor SEP "|" TAG Ltac2 +| DELETE LIST0 tac2alg_constructor SEP "|" (* Ltac2 plugin *) +| (* empty *) +| OPTINREF +] + SPLICE: [ | def_token | extended_def_token @@ -1792,7 +1979,233 @@ logical_kind: [ | [ "Field" | "Method" ] ] +(* ltac2 *) + +DELETE: [ +| test_ltac1_env +] + +mut_flag: [ +| OPTINREF +] + +rec_flag: [ +| OPTINREF +] + +ltac2_orient: [ | DELETENT ] + +ltac2_orient: [ +| orient +] + SPLICE: [ +| ltac2_orient +] + +tac2typ_prm: [ +| OPTINREF +] + +tac2type_body: [ +| OPTINREF +] + +atomic_tac2pat: [ +| OPTINREF +] + +tac2expr0: [ +(* +| DELETE "(" ")" (* covered by "()" prodn *) +| REPLACE "{" [ | LIST1 tac2rec_fieldexpr OPT ";" ] "}" +| WITH "{" OPT ( LIST1 tac2rec_fieldexpr OPT ";" ) "}" +*) +] + +(* todo: should +| tac2pat1 "," LIST0 tac2pat1 SEP "," +use LIST1? *) + +SPLICE: [ +| tac2expr4 +] + +tac2expr3: [ +| REPLACE tac2expr2 "," LIST1 tac2expr2 SEP "," (* Ltac2 plugin *) +| WITH LIST1 tac2expr2 SEP "," TAG Ltac2 +| DELETE tac2expr2 (* Ltac2 plugin *) +] + +tac2rec_fieldexprs: [ +| DELETE tac2rec_fieldexpr ";" tac2rec_fieldexprs +| DELETE tac2rec_fieldexpr ";" +| DELETE tac2rec_fieldexpr +| LIST1 tac2rec_fieldexpr OPT ";" +| OPTINREF +] + +tac2rec_fields: [ +| DELETE tac2rec_field ";" tac2rec_fields +| DELETE tac2rec_field ";" +| DELETE tac2rec_field +| LIST1 tac2rec_field SEP ";" OPT ";" TAG Ltac2 +| OPTINREF +] + +(* todo: weird productions, ints only after an initial "-"??: + occs_nums: [ + | LIST1 [ num | ident ] + | "-" [ num | ident ] LIST0 int_or_var +*) +ltac2_occs_nums: [ +| DELETE LIST1 nat_or_anti (* Ltac2 plugin *) +| REPLACE "-" nat_or_anti LIST0 nat_or_anti (* Ltac2 plugin *) +| WITH OPT "-" LIST1 nat_or_anti TAG Ltac2 +] + +syn_level: [ +| OPTINREF +] + +ltac2_delta_flag: [ +| OPTINREF +] + +ltac2_occs: [ +| OPTINREF +] + +ltac2_concl_occ: [ +| OPTINREF +] + +ltac2_with_bindings: [ +| OPTINREF +] + +ltac2_as_or_and_ipat: [ +| OPTINREF +] + +ltac2_eqn_ipat: [ +| OPTINREF +] + +ltac2_as_name: [ +| OPTINREF +] + +ltac2_as_ipat: [ +| OPTINREF +] + +ltac2_by_tactic: [ +| OPTINREF +] + +ltac2_entry: [ +| REPLACE tac2def_typ (* Ltac2 plugin *) +| WITH "Ltac2" tac2def_typ +| REPLACE tac2def_syn (* Ltac2 plugin *) +| WITH "Ltac2" tac2def_syn +| REPLACE tac2def_mut (* Ltac2 plugin *) +| WITH "Ltac2" tac2def_mut +| REPLACE tac2def_val (* Ltac2 plugin *) +| WITH "Ltac2" tac2def_val +| REPLACE tac2def_ext (* Ltac2 plugin *) +| WITH "Ltac2" tac2def_ext +| "Ltac2" "Notation" [ string | lident ] ":=" tac2expr6 TAG Ltac2 (* variant *) +| MOVEALLBUT command +(* todo: MOVEALLBUT should ignore tag on "but" prodns *) +] + +ltac2_match_list: [ +| EDIT ADD_OPT "|" LIST1 ltac2_match_rule SEP "|" (* Ltac2 plugin *) +] + +ltac2_or_and_intropattern: [ +| DELETE "(" ltac2_simple_intropattern ")" (* Ltac2 plugin *) +| REPLACE "(" ltac2_simple_intropattern "," LIST1 ltac2_simple_intropattern SEP "," ")" (* Ltac2 plugin *) +| WITH "(" LIST1 ltac2_simple_intropattern SEP "," ")" TAG Ltac2 +| REPLACE "(" ltac2_simple_intropattern "&" LIST1 ltac2_simple_intropattern SEP "&" ")" (* Ltac2 plugin *) +| WITH "(" LIST1 ltac2_simple_intropattern SEP "&" ")" TAG Ltac2 +] + +SPLICE: [ +| tac2def_val +| tac2def_typ +| tac2def_ext +| tac2def_syn +| tac2def_mut +| mut_flag +| rec_flag +| locident +| syn_level +| tac2rec_fieldexprs +| tac2type_body +| tac2alg_constructors +| tac2rec_fields +| ltac2_binder +| branch +| 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 *) +| DELETE simple_tactic +] + +RENAME: [ +| Prim.string string +| Prim.integer int +| Prim.qualid qualid +| Prim.natural num +] + +gmatch_list: [ +| EDIT ADD_OPT "|" LIST1 gmatch_rule SEP "|" (* Ltac2 plugin *) +] + +ltac2_quotations: [ + +] + +ltac2_tactic_atom: [ +| MOVETO ltac2_quotations "constr" ":" "(" lconstr ")" (* Ltac2 plugin *) +| MOVETO ltac2_quotations "open_constr" ":" "(" lconstr ")" (* Ltac2 plugin *) +| MOVETO ltac2_quotations "ident" ":" "(" lident ")" (* Ltac2 plugin *) +| MOVETO ltac2_quotations "pattern" ":" "(" cpattern ")" (* Ltac2 plugin *) +| MOVETO ltac2_quotations "reference" ":" "(" globref ")" (* Ltac2 plugin *) +| MOVETO ltac2_quotations "ltac1" ":" "(" ltac1_expr_in_env ")" (* Ltac2 plugin *) +| MOVETO ltac2_quotations "ltac1val" ":" "(" ltac1_expr_in_env ")" (* Ltac2 plugin *) +] + +(* non-Ltac2 "clause" is really clause_dft_concl + there is an ltac2 "clause" *) +ltac2_clause: [ ] + +clause: [ +| MOVEALLBUT ltac2_clause +] + +clause: [ +| clause_dft_concl +] + +q_clause: [ +| REPLACE clause +| WITH ltac2_clause TAG Ltac2 +] + +ltac2_induction_clause: [ +| REPLACE ltac2_destruction_arg OPT ltac2_as_or_and_ipat OPT ltac2_eqn_ipat OPT clause (* Ltac2 plugin *) +| WITH ltac2_destruction_arg OPT ltac2_as_or_and_ipat OPT ltac2_eqn_ipat OPT ltac2_clause TAG Ltac2 +] + +SPLICE: [ +| clause | noedit_mode | bigint | match_list @@ -1808,6 +2221,7 @@ SPLICE: [ | pattern_ident | constr_eval (* splices as multiple prods *) | tactic_then_last (* todo: dependency on c.edit_mlg edit?? really useful? *) +| ltac2_tactic_then_last | Prim.name | ltac_selector | Constr.ident @@ -1962,7 +2376,6 @@ SPLICE: [ | search_where | message_token | input_fun -| tactic_then_last | ltac_use_default | toplevel_selector_temp | comment @@ -1970,14 +2383,24 @@ SPLICE: [ | match_context_rule | match_rule | by_notation +| lnatural +| nat_or_anti +| globref +| let_binder +| refglobals (* Ltac2 *) +| syntax_modifiers +| array_elems +| ltac2_expr +| G_LTAC2_input_fun +| ltac2_simple_intropattern_closed +| ltac2_with_bindings ] (* end SPLICE *) RENAME: [ -| clause clause_dft_concl - | 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 @@ -1998,6 +2421,7 @@ RENAME: [ | 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 @@ -2029,6 +2453,20 @@ RENAME: [ | 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 ] simple_tactic: [ @@ -2050,6 +2488,7 @@ SPLICE: [ | command_entry | ltac_builtins | ltac_constructs +| ltac2_constructs | ltac_defined_tactics | tactic_notation_tactics ] @@ -2064,12 +2503,47 @@ NOTINRSTS: [ | simple_tactic | REACHABLE | NOTINRSTS +| l1_tactic +| l2_tactic +| l3_tactic +| binder_tactic +| value_tactic +| ltac2_entry +(* ltac2 syntactic classes *) +| q_intropatterns +| q_intropattern +| q_ident +| q_destruction_arg +| q_with_bindings +| q_bindings +| q_strategy_flag +| q_reference +| q_clause +| q_occurrences +| q_induction_clause +| q_conversion +| q_rewriting +| q_dispatch +| q_hintdb +| q_move_location +| q_pose +| q_assert +| 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: [ | NOTINRSTS ] - -strategy_level: [ -| DELETE strategy_level0 -] diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml index 33c4bd3e01..0ac652c0db 100644 --- a/doc/tools/docgram/doc_grammar.ml +++ b/doc/tools/docgram/doc_grammar.ml @@ -82,6 +82,138 @@ type gram = { order: string list; } + +(*** Print routines ***) + +let sprintf = Printf.sprintf + +let map_and_concat f ?(delim="") l = + String.concat delim (List.map f l) + +let rec db_output_prodn = function + | Sterm s -> sprintf "(Sterm %s) " s + | Snterm s -> sprintf "(Snterm %s) " s + | Slist1 sym -> sprintf "(Slist1 %s) " (db_output_prodn sym) + | Slist1sep (sym, sep) -> sprintf "(Slist1sep %s %s) " (db_output_prodn sep) (db_output_prodn sym) + | Slist0 sym -> sprintf "(Slist0 %s) " (db_output_prodn sym) + | Slist0sep (sym, sep) -> sprintf "(Slist0sep %s %s) " (db_output_prodn sep) (db_output_prodn sym) + | Sopt sym -> sprintf "(Sopt %s) " (db_output_prodn sym) + | Sparen prod -> sprintf "(Sparen %s) " (db_out_list prod) + | Sprod prods -> sprintf "(Sprod %s) " (db_out_prods prods) + | Sedit s -> sprintf "(Sedit %s) " s + | Sedit2 (s, s2) -> sprintf "(Sedit2 %s %s) " s s2 +and db_out_list prod = sprintf "(%s)" (map_and_concat db_output_prodn prod) +and db_out_prods prods = sprintf "( %s )" (map_and_concat ~delim:" | " db_out_list prods) + +(* identify special chars that don't get a trailing space in output *) +let omit_space s = List.mem s ["?"; "."; "#"] + +let rec output_prod plist need_semi = function + | Sterm s -> if plist then sprintf "%s" s else sprintf "\"%s\"" s + | Snterm s -> + if plist then sprintf "`%s`" s else + sprintf "%s%s" s (if s = "IDENT" && need_semi then ";" else "") + | Slist1 sym -> sprintf "LIST1 %s" (prod_to_str ~plist [sym]) + | Slist1sep (sym, sep) -> sprintf "LIST1 %s SEP %s" (prod_to_str ~plist [sym]) (prod_to_str ~plist [sep]) + | Slist0 sym -> sprintf "LIST0 %s" (prod_to_str ~plist [sym]) + | Slist0sep (sym, sep) -> sprintf "LIST0 %s SEP %s" (prod_to_str ~plist [sym]) (prod_to_str ~plist [sep]) + | Sopt sym -> sprintf "OPT %s" (prod_to_str ~plist [sym]) + | Sparen sym_list -> sprintf "( %s )" (prod_to_str sym_list) + | Sprod sym_list_list -> + sprintf "[ %s ]" (String.concat " " (List.mapi (fun i r -> + let prod = (prod_to_str r) in + let sep = if i = 0 then "" else + if prod <> "" then "| " else "|" in + sprintf "%s%s" sep prod) + sym_list_list)) + | Sedit s -> sprintf "%s" s + (* todo: make TAG info output conditional on the set of prods? *) + | Sedit2 ("TAG", plugin) -> + if plist then + sprintf " (%s plugin)" plugin + else + sprintf " (* %s plugin *)" plugin + | Sedit2 ("FILE", file) -> + let file_suffix_regex = Str.regexp ".*/\\([a-zA-Z0-9_\\.]+\\)" in + let suffix = if Str.string_match file_suffix_regex file 0 then Str.matched_group 1 file else file in + if plist then + sprintf " (%s)" suffix + else + sprintf " (* %s *)" suffix + | Sedit2 (s, s2) -> sprintf "%s \"%s\"" s s2 + +and prod_to_str_r plist prod = + match prod with + | Sterm s :: Snterm "ident" :: tl when omit_space s && plist -> + (sprintf "%s`ident`" s) :: (prod_to_str_r plist tl) + | p :: tl -> + let need_semi = + match prod with + | Snterm "IDENT" :: Sterm _ :: _ + | Snterm "IDENT" :: Sprod _ :: _ -> true + | _ -> false in + (output_prod plist need_semi p) :: (prod_to_str_r plist tl) + | [] -> [] + +and prod_to_str ?(plist=false) prod = + String.concat " " (prod_to_str_r plist prod) + +(* Determine if 2 productions are equal ignoring Sedit and Sedit2 *) +let ematch prod edit = + let rec ematchr prod edit = + (*Printf.printf "%s and\n %s\n\n" (prod_to_str prod) (prod_to_str edit);*) + match (prod, edit) with + | (_, Sedit _ :: tl) + | (_, Sedit2 _ :: tl) + -> ematchr prod tl + | (Sedit _ :: tl, _) + | (Sedit2 _ :: tl, _) + -> ematchr tl edit + | (phd :: ptl, hd :: tl) -> + let m = match (phd, hd) with + | (Slist1 psym, Slist1 sym) + | (Slist0 psym, Slist0 sym) + | (Sopt psym, Sopt sym) + -> ematchr [psym] [sym] + | (Slist1sep (psym, psep), Slist1sep (sym, sep)) + | (Slist0sep (psym, psep), Slist0sep (sym, sep)) + -> ematchr [psym] [sym] && ematchr [psep] [sep] + | (Sparen psyml, Sparen syml) + -> ematchr psyml syml + | (Sprod psymll, Sprod symll) -> + if List.compare_lengths psymll symll != 0 then false + else + List.fold_left (&&) true (List.map2 ematchr psymll symll) + | _, _ -> phd = hd + in + m && ematchr ptl tl + | ([], hd :: tl) -> false + | (phd :: ptl, []) -> false + | ([], []) -> true +in + (*Printf.printf "\n";*) + let rv = ematchr prod edit in + (*Printf.printf "%b\n" rv;*) + rv + +let get_first m_prod prods = + let rec find_first_r prods i = + match prods with + | [] -> + raise Not_found + | prod :: tl -> + if ematch prod m_prod then i + else find_first_r tl (i+1) + in + find_first_r prods 0 + +let find_first edit prods nt = + try + get_first edit prods + with Not_found -> + error "Can't find '%s' in edit for '%s'\n" (prod_to_str edit) nt; + raise Not_found + module DocGram = struct (* these guarantee that order and map have a 1-1 relationship on the nt name. They don't guarantee that nts on rhs of a production @@ -90,6 +222,8 @@ module DocGram = struct exception Duplicate exception Invalid + let g_empty () = ref { map = NTMap.empty; order = [] } + (* add an nt at the end (if not already present) then set its prods *) let g_maybe_add g nt prods = if not (NTMap.mem nt !g.map) then @@ -167,81 +301,6 @@ module DocGram = struct end open DocGram -(*** Print routines ***) - -let sprintf = Printf.sprintf - -let map_and_concat f ?(delim="") l = - String.concat delim (List.map f l) - -let rec db_output_prodn = function - | Sterm s -> sprintf "(Sterm %s) " s - | Snterm s -> sprintf "(Snterm %s) " s - | Slist1 sym -> sprintf "(Slist1 %s) " (db_output_prodn sym) - | Slist1sep (sym, sep) -> sprintf "(Slist1sep %s %s) " (db_output_prodn sep) (db_output_prodn sym) - | Slist0 sym -> sprintf "(Slist0 %s) " (db_output_prodn sym) - | Slist0sep (sym, sep) -> sprintf "(Slist0sep %s %s) " (db_output_prodn sep) (db_output_prodn sym) - | Sopt sym -> sprintf "(Sopt %s) " (db_output_prodn sym) - | Sparen prod -> sprintf "(Sparen %s) " (db_out_list prod) - | Sprod prods -> sprintf "(Sprod %s) " (db_out_prods prods) - | Sedit s -> sprintf "(Sedit %s) " s - | Sedit2 (s, s2) -> sprintf "(Sedit2 %s %s) " s s2 -and db_out_list prod = sprintf "(%s)" (map_and_concat db_output_prodn prod) -and db_out_prods prods = sprintf "( %s )" (map_and_concat ~delim:" | " db_out_list prods) - -(* identify special chars that don't get a trailing space in output *) -let omit_space s = List.mem s ["?"; "."; "#"] - -let rec output_prod plist need_semi = function - | Sterm s -> if plist then sprintf "%s" s else sprintf "\"%s\"" s - | Snterm s -> - if plist then sprintf "`%s`" s else - sprintf "%s%s" s (if s = "IDENT" && need_semi then ";" else "") - | Slist1 sym -> sprintf "LIST1 %s" (prod_to_str ~plist [sym]) - | Slist1sep (sym, sep) -> sprintf "LIST1 %s SEP %s" (prod_to_str ~plist [sym]) (prod_to_str ~plist [sep]) - | Slist0 sym -> sprintf "LIST0 %s" (prod_to_str ~plist [sym]) - | Slist0sep (sym, sep) -> sprintf "LIST0 %s SEP %s" (prod_to_str ~plist [sym]) (prod_to_str ~plist [sep]) - | Sopt sym -> sprintf "OPT %s" (prod_to_str ~plist [sym]) - | Sparen sym_list -> sprintf "( %s )" (prod_to_str sym_list) - | Sprod sym_list_list -> - sprintf "[ %s ]" (String.concat " " (List.mapi (fun i r -> - let prod = (prod_to_str r) in - let sep = if i = 0 then "" else - if prod <> "" then "| " else "|" in - sprintf "%s%s" sep prod) - sym_list_list)) - | Sedit s -> sprintf "%s" s - (* todo: make PLUGIN info output conditional on the set of prods? *) - | Sedit2 ("PLUGIN", plugin) -> - if plist then - sprintf " (%s plugin)" plugin - else - sprintf " (* %s plugin *)" plugin - | Sedit2 ("FILE", file) -> - let file_suffix_regex = Str.regexp ".*/\\([a-zA-Z0-9_\\.]+\\)" in - let suffix = if Str.string_match file_suffix_regex file 0 then Str.matched_group 1 file else file in - if plist then - sprintf " (%s)" suffix - else - sprintf " (* %s *)" suffix - | Sedit2 (s, s2) -> sprintf "%s \"%s\"" s s2 - -and prod_to_str_r plist prod = - match prod with - | Sterm s :: Snterm "ident" :: tl when omit_space s && plist -> - (sprintf "%s`ident`" s) :: (prod_to_str_r plist tl) - | p :: tl -> - let need_semi = - match prod with - | Snterm "IDENT" :: Sterm _ :: _ - | Snterm "IDENT" :: Sprod _ :: _ -> true - | _ -> false in - (output_prod plist need_semi p) :: (prod_to_str_r plist tl) - | [] -> [] - -and prod_to_str ?(plist=false) prod = - String.concat " " (prod_to_str_r plist prod) - let rec output_prodn = function | Sterm s -> @@ -275,7 +334,7 @@ let rec output_prodn = function sym_list)) rcurly | Sedit s -> sprintf "%s" s - | Sedit2 ("PLUGIN", s2) -> "" + | Sedit2 ("TAG", s2) -> "" | Sedit2 (s, s2) -> sprintf "%s \"%s\"" s s2 and output_sep sep = @@ -292,6 +351,16 @@ and prod_to_prodn_r prod = and prod_to_prodn prod = String.concat " " (prod_to_prodn_r prod) +let get_tag file prod = + List.fold_left (fun rv sym -> + match sym with + (* todo: temporarily limited to Ltac2 tags in prodn when not in ltac2.rst *) + | Sedit2 ("TAG", s2) + when (s2 = "Ltac2" || s2 = "not Ltac2") && + file <> "doc/sphinx/proof-engine/ltac2.rst" -> " " ^ s2 + | _ -> rv + ) "" prod + let pr_prods nt prods = (* duplicative *) Printf.printf "%s: [\n" nt; List.iter (fun prod -> @@ -397,6 +466,10 @@ and cvt_gram_sym_list l = (Sedit2 ("NOTE", s2)) :: cvt_gram_sym_list tl | GSymbQualid ("USE_NT", _) :: GSymbQualid (s2, l) :: tl -> (Sedit2 ("USE_NT", s2)) :: cvt_gram_sym_list tl + | GSymbQualid ("TAG", _) :: GSymbQualid (s2, l) :: tl -> + (Sedit2 ("TAG", s2)) :: cvt_gram_sym_list tl + | GSymbQualid ("TAG", _) :: GSymbString (s2) :: tl -> + (Sedit2 ("TAG", s2)) :: cvt_gram_sym_list tl | GSymbString s :: tl -> (* todo: not seeing "(bfs)" here for some reason *) keywords := StringSet.add s !keywords; @@ -474,59 +547,36 @@ let autoloaded_mlgs = [ (* in the order they are loaded by Coq *) ] -let ematch prod edit = - let rec ematchr prod edit = - (*Printf.printf "%s and\n %s\n\n" (prod_to_str prod) (prod_to_str edit);*) - match (prod, edit) with - | (_, Sedit _ :: tl) - | (_, Sedit2 _ :: tl) - -> ematchr prod tl - | (Sedit _ :: tl, _) - | (Sedit2 _ :: tl, _) - -> ematchr tl edit - | (phd :: ptl, hd :: tl) -> - let m = match (phd, hd) with - | (Slist1 psym, Slist1 sym) - | (Slist0 psym, Slist0 sym) - | (Sopt psym, Sopt sym) - -> ematchr [psym] [sym] - | (Slist1sep (psym, psep), Slist1sep (sym, sep)) - | (Slist0sep (psym, psep), Slist0sep (sym, sep)) - -> ematchr [psym] [sym] && ematchr [psep] [sep] - | (Sparen psyml, Sparen syml) - -> ematchr psyml syml - | (Sprod psymll, Sprod symll) -> - if List.compare_lengths psymll symll != 0 then false - else - List.fold_left (&&) true (List.map2 ematchr psymll symll) - | _, _ -> phd = hd - in - m && ematchr ptl tl - | ([], hd :: tl) -> false - | (phd :: ptl, []) -> false - | ([], []) -> true -in - (*Printf.printf "\n";*) - let rv = ematchr prod edit in - (*Printf.printf "%b\n" rv;*) - rv - let has_match p prods = List.exists (fun p2 -> ematch p p2) prods let plugin_regex = Str.regexp "^plugins/\\([a-zA-Z0-9_]+\\)/" let level_regex = Str.regexp "[a-zA-Z0-9_]*$" -let read_mlg is_edit ast file level_renames symdef_map = +let get_plugin_name file = + if file = "user-contrib/Ltac2/g_ltac2.mlg" then + "Ltac2" + else if Str.string_match plugin_regex file 0 then + Str.matched_group 1 file + else + "" + +let read_mlg g is_edit ast file level_renames symdef_map = let res = ref [] in let locals = ref StringSet.empty in + let dup_renames = ref StringMap.empty in let add_prods nt prods = if not is_edit then + if NTMap.mem nt !g.map && nt <> "command" && nt <> "simple_tactic" then begin + let new_name = String.uppercase_ascii (Filename.remove_extension (Filename.basename file)) ^ "_" ^ nt in + dup_renames := StringMap.add nt new_name !dup_renames; + Printf.printf "** dup sym %s -> %s in %s\n" nt new_name file + end; add_symdef nt file symdef_map; + let plugin = get_plugin_name file in let prods = if not is_edit && not (List.mem file autoloaded_mlgs) && - Str.string_match plugin_regex file 0 then - let plugin = Str.matched_group 1 file in - List.map (fun p -> p @ [Sedit2 ("PLUGIN", plugin)]) prods + plugin <> "" then + List.map (fun p -> p @ [Sedit2 ("TAG", plugin)]) prods else prods in @@ -600,7 +650,7 @@ let read_mlg is_edit ast file level_renames symdef_map = in List.iter prod_loop ast; - List.rev !res, !locals + List.rev !res, !locals, !dup_renames let dir s = "doc/tools/docgram/" ^ s @@ -608,7 +658,7 @@ let read_mlg_edit file = let fdir = dir file in let level_renames = ref StringMap.empty in (* ignored *) let symdef_map = ref StringMap.empty in (* ignored *) - let prods, _ = read_mlg true (parse_file fdir) fdir level_renames symdef_map in + let prods, _, _ = read_mlg (g_empty ()) true (parse_file fdir) fdir level_renames symdef_map in prods let add_rule g nt prods file = @@ -623,17 +673,99 @@ let add_rule g nt prods file = prods) in g_maybe_add_begin g nt (ent @ nodups) + +let remove_Sedit2 p = + List.filter (fun sym -> match sym with | Sedit2 _ -> false | _ -> true) p + +(* edit a production: rename nonterminals, drop nonterminals, substitute nonterminals *) +let rec edit_prod g top edit_map prod = + let edit_nt edit_map sym0 nt = + try + let binding = StringMap.find nt edit_map in + match binding with + | "DELETE" -> [] + | "SPLICE" -> + begin + try let splice_prods = NTMap.find nt !g.map in + match splice_prods with + | [] -> error "Empty splice for '%s'\n" nt; [] + | [p] -> List.rev (remove_Sedit2 p) + | _ -> [Sprod (List.map remove_Sedit2 splice_prods)] (* todo? check if we create a dup *) + with Not_found -> error "Missing nt '%s' for splice\n" nt; [Snterm nt] + end + | _ -> [Snterm binding] + with Not_found -> [sym0] + in + let maybe_wrap syms = + match syms with + | s :: [] -> List.hd syms + | s -> Sparen (List.rev syms) + in + + let rec edit_symbol sym0 = + match sym0 with + | Sterm s -> [sym0] + | Snterm s -> edit_nt edit_map sym0 s + | Slist1 sym -> [Slist1 (maybe_wrap (edit_symbol sym))] + (* you'll get a run-time failure deleting a SEP symbol *) + | Slist1sep (sym, sep) -> [Slist1sep (maybe_wrap (edit_symbol sym), (List.hd (edit_symbol sep)))] + | Slist0 sym -> [Slist0 (maybe_wrap (edit_symbol sym))] + | Slist0sep (sym, sep) -> [Slist0sep (maybe_wrap (edit_symbol sym), (List.hd (edit_symbol sep)))] + | Sopt sym -> [Sopt (maybe_wrap (edit_symbol sym))] + | Sparen slist -> [Sparen (List.hd (edit_prod g false edit_map slist))] + | Sprod slistlist -> let (_, prods) = edit_rule g edit_map "" slistlist in + [Sprod prods] + | Sedit _ + | Sedit2 _ -> [sym0] (* these constructors not used here *) + in + let is_splice nt = + try + StringMap.find nt edit_map = "SPLICE" + with Not_found -> false + in + let get_splice_prods nt = + try NTMap.find nt !g.map + with Not_found -> (error "Missing nt '%s' for splice\n" nt; []) + in + + (* special case splice creating multiple new productions *) + let splice_prods = match prod with + | Snterm nt :: [] when is_splice nt -> + get_splice_prods nt + | Snterm nt :: Sedit2 ("TAG", _) :: [] when is_splice nt -> + get_splice_prods nt + | _ -> [] + in + if top && splice_prods <> [] then + splice_prods + else + [List.rev (List.concat (List.rev (List.map (fun sym -> edit_symbol sym) prod)))] + +and edit_rule g edit_map nt rule = + let nt = + try let new_name = StringMap.find nt edit_map in + match new_name with + | "SPLICE" -> nt + | "DELETE" -> "" + | _ -> new_name + with Not_found -> nt + in + (nt, (List.concat (List.map (edit_prod g true edit_map) rule))) + let read_mlg_files g args symdef_map = let level_renames = ref StringMap.empty in let last_autoloaded = List.hd (List.rev autoloaded_mlgs) in List.iter (fun file -> - (* does nt renaming, deletion and splicing *) - let rules, locals = read_mlg false (parse_file file) file level_renames symdef_map in + (* todo: ??? does nt renaming, deletion and splicing *) + let rules, locals, dup_renames = read_mlg g false (parse_file file) file level_renames symdef_map in let numprods = List.fold_left (fun num rule -> let nt, prods = rule in - if NTMap.mem nt !g.map && (StringSet.mem nt locals) && - StringSet.cardinal (StringSet.of_list (StringMap.find nt !symdef_map)) > 1 then - warn "%s: local nonterminal '%s' already defined\n" file nt; + (* rename local duplicates *) + let prods = List.map (fun prod -> List.hd (edit_prod g true dup_renames prod)) prods in + let nt = try StringMap.find nt dup_renames with Not_found -> nt in +(* if NTMap.mem nt !g.map && (StringSet.mem nt locals) &&*) +(* StringSet.cardinal (StringSet.of_list (StringMap.find nt !symdef_map)) > 1 then*) +(* warn "%s: local nonterminal '%s' already defined\n" file nt; (* todo: goes away *)*) add_rule g nt prods file; num + List.length prods) 0 rules @@ -701,7 +833,12 @@ let create_edit_map g op edits = | "RENAME" -> if not (StringSet.mem key all_nts_ref || (StringSet.mem key all_nts_def)) then error "Unused/undefined nt `%s` in RENAME\n" key; -(* todo: could not get the following codeto type check + | "MERGE" -> + if not (StringSet.mem key all_nts_ref || (StringSet.mem key all_nts_def)) then + error "Unused/undefined nt `%s` in MERGE\n" key; + if not (StringSet.mem binding all_nts_ref || (StringSet.mem binding all_nts_def)) then + error "Unused/undefined nt `%s` in MERGE\n" key; +(* todo: could not get the following code to type check (match binding with | _ :: Snterm new_nt :: _ -> if not (StringSet.mem new_nt all_nts_ref) then @@ -713,9 +850,6 @@ let create_edit_map g op edits = in aux edits StringMap.empty -let remove_Sedit2 p = - List.filter (fun sym -> match sym with | Sedit2 _ -> false | _ -> true) p - (* don't deal with Sedit, Sedit2 yet (ever?) *) let rec pmatch fullprod fullpat repl = let map_prod prod = List.concat (List.map (fun s -> pmatch [s] fullpat repl) prod) in @@ -768,88 +902,15 @@ let global_repl g pat repl = g_update_prods g nt (List.map (fun prod -> pmatch prod pat repl) (NTMap.find nt !g.map)) ) !g.order -(* edit a production: rename nonterminals, drop nonterminals, substitute nonterminals *) -let rec edit_prod g top edit_map prod = - let edit_nt edit_map sym0 nt = - try - let binding = StringMap.find nt edit_map in - match binding with - | "DELETE" -> [] - | "SPLICE" -> - begin - try let splice_prods = NTMap.find nt !g.map in - match splice_prods with - | [] -> error "Empty splice for '%s'\n" nt; [] - | [p] -> List.rev (remove_Sedit2 p) - | _ -> [Sprod (List.map remove_Sedit2 splice_prods)] - with Not_found -> error "Missing nt '%s' for splice\n" nt; [Snterm nt] - end - | _ -> [Snterm binding] - with Not_found -> [sym0] - in - let maybe_wrap syms = - match syms with - | s :: [] -> List.hd syms - | s -> Sparen (List.rev syms) - in - - let rec edit_symbol sym0 = - match sym0 with - | Sterm s -> [sym0] - | Snterm s -> edit_nt edit_map sym0 s - | Slist1 sym -> [Slist1 (maybe_wrap (edit_symbol sym))] - (* you'll get a run-time failure deleting a SEP symbol *) - | Slist1sep (sym, sep) -> [Slist1sep (maybe_wrap (edit_symbol sym), (List.hd (edit_symbol sep)))] - | Slist0 sym -> [Slist0 (maybe_wrap (edit_symbol sym))] - | Slist0sep (sym, sep) -> [Slist0sep (maybe_wrap (edit_symbol sym), (List.hd (edit_symbol sep)))] - | Sopt sym -> [Sopt (maybe_wrap (edit_symbol sym))] - | Sparen slist -> [Sparen (List.hd (edit_prod g false edit_map slist))] - | Sprod slistlist -> let (_, prods) = edit_rule g edit_map "" slistlist in - [Sprod prods] - | Sedit _ - | Sedit2 _ -> [sym0] (* these constructors not used here *) - in - let is_splice nt = - try - StringMap.find nt edit_map = "SPLICE" - with Not_found -> false - in - let get_splice_prods nt = - try NTMap.find nt !g.map - with Not_found -> (error "Missing nt '%s' for splice\n" nt; []) - in - - (* special case splice creating multiple new productions *) - let splice_prods = match prod with - | Snterm nt :: [] when is_splice nt -> - get_splice_prods nt - | _ -> [] - in - if top && splice_prods <> [] then - splice_prods - else - [List.rev (List.concat (List.rev (List.map (fun sym -> edit_symbol sym) prod)))] - -and edit_rule g edit_map nt rule = - let nt = - try let new_name = StringMap.find nt edit_map in - match new_name with - | "SPLICE" -> nt - | "DELETE" -> "" - | _ -> new_name - with Not_found -> nt - in - (nt, (List.concat (List.map (edit_prod g true edit_map) rule))) - (*** splice: replace a reference to a nonterminal with its definition ***) (* todo: create a better splice routine *) -let apply_splice g splice_map = +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 splice_map nt prods 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 @@ -867,19 +928,8 @@ let apply_splice g splice_map = | "SPLICE" -> g_remove g nt; | _ -> ()) - (StringMap.bindings splice_map) + (StringMap.bindings edit_map) -let find_first edit prods nt = - let rec find_first_r edit prods nt i = - match prods with - | [] -> - error "Can't find '%s' in edit for '%s'\n" (prod_to_str edit) nt; - raise Not_found - | prod :: tl -> - if ematch prod edit then i - else find_first_r edit tl nt (i+1) - in - find_first_r edit prods nt 0 let remove_prod edit prods nt = let res, got_first = List.fold_left (fun args prod -> @@ -1087,6 +1137,29 @@ let expand_lists g = with | Queue.Empty -> () +let apply_merge g edit_map = + List.iter (fun b -> + let (from_nt, to_nt) = b in + let from_prods = NTMap.find from_nt !g.map in + List.iter (fun prod -> + try + ignore( get_first prod (NTMap.find to_nt !g.map)); + with Not_found -> g_add_prod_after g None to_nt prod) + from_prods) + (NTMap.bindings edit_map) + +let apply_rename_delete g edit_map = + List.iter (fun b -> let (nt, _) = b in + let prods = try NTMap.find nt !g.map with Not_found -> [] in + let (nt', prods') = edit_rule g edit_map nt prods in + if nt' = "" then + g_remove g nt + else if nt <> nt' then + g_rename_merge g nt nt' prods' + else + g_update_prods g nt prods') + (NTMap.bindings !g.map) + let edit_all_prods g op eprods = let do_it op eprods num = let rec aux eprods res = @@ -1101,25 +1174,20 @@ let edit_all_prods g op eprods = op (prod_to_str eprod) num; aux tl res in - let map = create_edit_map g op (aux eprods []) in - if op = "SPLICE" then - apply_splice g map - else (* RENAME/DELETE *) - List.iter (fun b -> let (nt, _) = b in - let prods = try NTMap.find nt !g.map with Not_found -> [] in - let (nt', prods') = edit_rule g map nt prods in - if nt' = "" then - g_remove g nt - else if nt <> nt' then - g_rename_merge g nt nt' prods' - else - g_update_prods g nt prods') - (NTMap.bindings !g.map); + let edit_map = create_edit_map g op (aux eprods []) in + match op with + | "SPLICE" -> apply_splice g edit_map + | "MERGE" -> apply_merge g edit_map; apply_rename_delete g edit_map + | "RENAME" + | "DELETE" -> apply_rename_delete g edit_map + | _ -> () + in match op with | "RENAME" -> do_it op eprods 2; true | "DELETE" -> do_it op eprods 1; true | "SPLICE" -> do_it op eprods 1; true + | "MERGE" -> do_it op eprods 2; true | "EXPAND" -> if List.length eprods > 1 || List.length (List.hd eprods) <> 0 then error "'EXPAND:' expects a single empty production\n"; @@ -1559,7 +1627,7 @@ let rec dump prod = [@@@ocaml.warning "+32"] let reorder_grammar eg reordered_rules file = - let og = ref { map = NTMap.empty; order = [] } in + let og = g_empty () in List.iter (fun rule -> let nt, prods = rule in try @@ -1761,11 +1829,12 @@ let process_rst g file args seen tac_prods cmd_prods = let prods = NTMap.find nt !g.map in List.iteri (fun i prod -> let rhs = String.trim (prod_to_prodn prod) in + let tag = get_tag file prod in let sep = if i = 0 then " ::=" else "|" in if has_empty_prod prod then error "%s line %d: Empty (sub-)production for %s, edit to remove: '%s %s'\n" file !linenum nt sep rhs; - fprintf new_rst "%s %s%s %s\n" indent (if i = 0 then nt else "") sep rhs) + fprintf new_rst "%s %s%s %s%s\n" indent (if i = 0 then nt else "") sep rhs tag) prods; if nt <> end_ then copy_prods tl in @@ -1832,8 +1901,10 @@ let process_rst g file args seen tac_prods cmd_prods = "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/user-extensions/syntax-extensions.rst"; + "doc/sphinx/proof-engine/vernacular-commands.rst" ] in @@ -1941,12 +2012,16 @@ let report_omitted_prods g seen label split = (if first = "" then nt else first), nt, n + 1, total + 1) ("", "", 0, 0) !g.order in maybe_warn first last n; +(* List.iter (fun nt -> + if not (NTMap.mem nt seen || (List.mem nt included)) then + warn "%s %s not included in .rst files\n" "Nonterminal" nt) + !g.order;*) if total <> 0 then Printf.eprintf "TOTAL %ss not included = %d\n" label total let process_grammar args = let symdef_map = ref StringMap.empty in - let g = ref { map = NTMap.empty; order = [] } in + let g = g_empty () in let level_renames = read_mlg_files g args symdef_map in if args.verbose then begin diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index c5edb538b7..7f4e92fc37 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -59,7 +59,6 @@ universe: [ lconstr: [ | operconstr200 -| l_constr ] constr: [ @@ -118,8 +117,12 @@ operconstr0: [ | "{|" record_declaration bar_cbrace | "{" binder_constr "}" | "`{" operconstr200 "}" +| test_array_opening "[" "|" array_elems "|" lconstr type_cstr test_array_closing "|" "]" univ_instance | "`(" operconstr200 ")" -| "ltac" ":" "(" Pltac.tactic_expr ")" +] + +array_elems: [ +| LIST0 lconstr SEP ";" ] record_declaration: [ @@ -305,7 +308,6 @@ open_binders: [ binders: [ | LIST0 binder -| Pcoq.Constr.binders ] binder: [ @@ -435,7 +437,6 @@ integer: [ natural: [ | bignat -| _natural ] bigint: [ @@ -456,7 +457,6 @@ strategy_level: [ | "opaque" | integer | "transparent" -| strategy_level0 ] vernac_toplevel: [ @@ -635,26 +635,37 @@ command: [ | "Add" "Relation" constr constr "reflexivity" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident | "Add" "Relation" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident | "Add" "Relation" constr constr "transitivity" "proved" "by" constr "as" ident -| "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "as" ident -| "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "as" ident -| "Add" "Parametric" "Relation" binders ":" constr constr "as" ident -| "Add" "Parametric" "Relation" binders ":" constr constr "symmetry" "proved" "by" constr "as" ident -| "Add" "Parametric" "Relation" binders ":" constr constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident -| "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident -| "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident -| "Add" "Parametric" "Relation" binders ":" constr constr "transitivity" "proved" "by" constr "as" ident +| "Add" "Parametric" "Relation" G_REWRITE_binders ":" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "as" ident +| "Add" "Parametric" "Relation" G_REWRITE_binders ":" constr constr "reflexivity" "proved" "by" constr "as" ident +| "Add" "Parametric" "Relation" G_REWRITE_binders ":" constr constr "as" ident +| "Add" "Parametric" "Relation" G_REWRITE_binders ":" constr constr "symmetry" "proved" "by" constr "as" ident +| "Add" "Parametric" "Relation" G_REWRITE_binders ":" constr constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident +| "Add" "Parametric" "Relation" G_REWRITE_binders ":" constr constr "reflexivity" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident +| "Add" "Parametric" "Relation" G_REWRITE_binders ":" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident +| "Add" "Parametric" "Relation" G_REWRITE_binders ":" constr constr "transitivity" "proved" "by" constr "as" ident | "Add" "Setoid" constr constr constr "as" ident -| "Add" "Parametric" "Setoid" binders ":" constr constr constr "as" ident +| "Add" "Parametric" "Setoid" G_REWRITE_binders ":" constr constr constr "as" ident | "Add" "Morphism" constr ":" ident | "Declare" "Morphism" constr ":" ident | "Add" "Morphism" constr "with" "signature" lconstr "as" ident -| "Add" "Parametric" "Morphism" binders ":" constr "with" "signature" lconstr "as" ident +| "Add" "Parametric" "Morphism" G_REWRITE_binders ":" constr "with" "signature" lconstr "as" ident | "Print" "Rewrite" "HintDb" preident | "Reset" "Ltac" "Profile" | "Show" "Ltac" "Profile" | "Show" "Ltac" "Profile" "CutOff" int | "Show" "Ltac" "Profile" string | "Show" "Lia" "Profile" (* micromega plugin *) +| "Add" "Zify" "InjTyp" constr (* micromega plugin *) +| "Add" "Zify" "BinOp" constr (* micromega plugin *) +| "Add" "Zify" "UnOp" constr (* micromega plugin *) +| "Add" "Zify" "CstOp" constr (* micromega plugin *) +| "Add" "Zify" "BinRel" constr (* micromega plugin *) +| "Add" "Zify" "PropOp" constr (* micromega plugin *) +| "Add" "Zify" "PropBinOp" constr (* micromega plugin *) +| "Add" "Zify" "PropUOp" constr (* micromega plugin *) +| "Add" "Zify" "BinOpSpec" constr (* micromega plugin *) +| "Add" "Zify" "UnOpSpec" constr (* micromega plugin *) +| "Add" "Zify" "Saturate" constr (* micromega plugin *) | "Add" "InjTyp" constr (* micromega plugin *) | "Add" "BinOp" constr (* micromega plugin *) | "Add" "UnOp" constr (* micromega plugin *) @@ -663,7 +674,6 @@ command: [ | "Add" "PropOp" constr (* micromega plugin *) | "Add" "PropBinOp" constr (* micromega plugin *) | "Add" "PropUOp" constr (* micromega plugin *) -| "Add" "Spec" constr (* micromega plugin *) | "Add" "BinOpSpec" constr (* micromega plugin *) | "Add" "UnOpSpec" constr (* micromega plugin *) | "Add" "Saturate" constr (* micromega plugin *) @@ -672,6 +682,8 @@ command: [ | "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 ":" constr OPT ring_mods (* setoid_ring plugin *) | "Print" "Rings" (* setoid_ring plugin *) @@ -679,6 +691,9 @@ command: [ | "Print" "Fields" (* setoid_ring plugin *) | "Numeral" "Notation" reference reference reference ":" ident numnotoption | "String" "Notation" reference reference reference ":" ident +| "Ltac2" ltac2_entry (* Ltac2 plugin *) +| "Ltac2" "Eval" ltac2_expr (* Ltac2 plugin *) +| "Print" "Ltac2" reference (* Ltac2 plugin *) ] reference_or_constr: [ @@ -700,7 +715,6 @@ hint: [ | "Mode" global mode | "Unfold" LIST1 global | "Constructors" LIST1 global -| "Extern" natural OPT Constr.constr_pattern "=>" Pltac.tactic ] constr_body: [ @@ -791,7 +805,7 @@ gallina: [ | "Combined" "Scheme" identref "from" LIST1 identref SEP "," | "Register" global "as" qualid | "Register" "Inline" global -| "Primitive" identref OPT [ ":" lconstr ] ":=" register_token +| "Primitive" ident_decl OPT [ ":" lconstr ] ":=" register_token | "Universe" LIST1 identref | "Universes" LIST1 identref | "Constraint" LIST1 univ_constraint SEP "," @@ -872,7 +886,7 @@ reduce: [ ] decl_notation: [ -| ne_lstring ":=" constr only_parsing OPT [ ":" IDENT ] +| ne_lstring ":=" constr syntax_modifiers OPT [ ":" IDENT ] ] decl_sep: [ @@ -1353,12 +1367,12 @@ syntax: [ | "Delimit" "Scope" IDENT; "with" IDENT | "Undelimit" "Scope" IDENT | "Bind" "Scope" IDENT; "with" LIST1 class_rawexpr -| "Infix" ne_lstring ":=" constr [ "(" LIST1 syntax_modifier SEP "," ")" | ] OPT [ ":" IDENT ] +| "Infix" ne_lstring ":=" constr syntax_modifiers OPT [ ":" IDENT ] | "Notation" identref LIST0 ident ":=" constr only_parsing -| "Notation" lstring ":=" constr [ "(" LIST1 syntax_modifier SEP "," ")" | ] OPT [ ":" IDENT ] +| "Notation" lstring ":=" constr syntax_modifiers OPT [ ":" IDENT ] | "Format" "Notation" STRING STRING STRING -| "Reserved" "Infix" ne_lstring [ "(" LIST1 syntax_modifier SEP "," ")" | ] -| "Reserved" "Notation" ne_lstring [ "(" LIST1 syntax_modifier SEP "," ")" | ] +| "Reserved" "Infix" ne_lstring syntax_modifiers +| "Reserved" "Notation" ne_lstring syntax_modifiers ] only_parsing: [ @@ -1387,6 +1401,11 @@ syntax_modifier: [ | IDENT syntax_extension_type ] +syntax_modifiers: [ +| "(" LIST1 syntax_modifier SEP "," ")" +| +] + syntax_extension_type: [ | "ident" | "global" @@ -1791,6 +1810,10 @@ orient: [ | ] +EXTRAARGS_natural: [ +| _natural +] + occurrences: [ | LIST1 integer | var @@ -1800,8 +1823,12 @@ glob: [ | constr ] +EXTRAARGS_lconstr: [ +| l_constr +] + lglob: [ -| lconstr +| EXTRAARGS_lconstr ] casted_constr: [ @@ -1829,18 +1856,18 @@ by_arg_tac: [ in_clause: [ | in_clause' -| "*" occs -| "*" "|-" concl_occ -| LIST0 hypident_occ SEP "," "|-" concl_occ -| LIST0 hypident_occ SEP "," ] test_lpar_id_colon: [ | local_test_lpar_id_colon ] +EXTRAARGS_strategy_level: [ +| strategy_level0 +] + strategy_level_or_var: [ -| strategy_level +| EXTRAARGS_strategy_level | identref ] @@ -1985,7 +2012,6 @@ failkw: [ binder_tactic: [ | "fun" LIST1 input_fun "=>" tactic_expr5 | "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" tactic_expr5 -| "info" tactic_expr5 ] tactic_arg_compat: [ @@ -2124,6 +2150,14 @@ tactic_mode: [ | "par" ":" OPT ltac_info tactic ltac_use_default ] +G_LTAC_hint: [ +| "Extern" natural OPT Constr.constr_pattern "=>" Pltac.tactic +] + +G_LTAC_operconstr0: [ +| "ltac" ":" "(" Pltac.tactic_expr ")" +] + ltac_selector: [ | toplevel_selector ] @@ -2194,6 +2228,10 @@ rewstrategy: [ | "fold" constr ] +G_REWRITE_binders: [ +| Pcoq.Constr.binders +] + int_or_var: [ | integer | identref @@ -2372,19 +2410,26 @@ hypident_occ: [ | hypident occs ] +G_TACTIC_in_clause: [ +| "*" occs +| "*" "|-" concl_occ +| LIST0 hypident_occ SEP "," "|-" concl_occ +| LIST0 hypident_occ SEP "," +] + clause_dft_concl: [ -| "in" in_clause +| "in" G_TACTIC_in_clause | occs | ] clause_dft_all: [ -| "in" in_clause +| "in" G_TACTIC_in_clause | ] opt_clause: [ -| "in" in_clause +| "in" G_TACTIC_in_clause | "at" occs_nums | ] @@ -2521,3 +2566,642 @@ numnotoption: [ | "(" "abstract" "after" bignat ")" ] +tac2pat1: [ +| Prim.qualid LIST1 tac2pat0 (* Ltac2 plugin *) +| Prim.qualid (* Ltac2 plugin *) +| "[" "]" (* Ltac2 plugin *) +| tac2pat0 "::" tac2pat0 (* Ltac2 plugin *) +| tac2pat0 (* Ltac2 plugin *) +] + +tac2pat0: [ +| "_" (* Ltac2 plugin *) +| "()" (* Ltac2 plugin *) +| Prim.qualid (* Ltac2 plugin *) +| "(" atomic_tac2pat ")" (* Ltac2 plugin *) +] + +atomic_tac2pat: [ +| (* Ltac2 plugin *) +| tac2pat1 ":" tac2type5 (* Ltac2 plugin *) +| tac2pat1 "," LIST0 tac2pat1 SEP "," (* Ltac2 plugin *) +| tac2pat1 (* Ltac2 plugin *) +] + +tac2expr6: [ +| tac2expr5 ";" tac2expr6 (* Ltac2 plugin *) +| tac2expr5 (* 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 *) +] + +tac2expr4: [ +| tac2expr3 (* Ltac2 plugin *) +] + +tac2expr3: [ +| tac2expr2 "," LIST1 tac2expr2 SEP "," (* Ltac2 plugin *) +| tac2expr2 (* Ltac2 plugin *) +] + +tac2expr2: [ +| tac2expr1 "::" tac2expr2 (* Ltac2 plugin *) +| tac2expr1 (* Ltac2 plugin *) +] + +tac2expr1: [ +| tac2expr0 LIST1 tac2expr0 (* Ltac2 plugin *) +| tac2expr0 ".(" Prim.qualid ")" (* Ltac2 plugin *) +| tac2expr0 ".(" Prim.qualid ")" ":=" tac2expr5 (* Ltac2 plugin *) +| tac2expr0 (* Ltac2 plugin *) +] + +tac2expr0: [ +| "(" tac2expr6 ")" (* Ltac2 plugin *) +| "(" tac2expr6 ":" tac2type5 ")" (* Ltac2 plugin *) +| "()" (* Ltac2 plugin *) +| "(" ")" (* Ltac2 plugin *) +| "[" LIST0 tac2expr5 SEP ";" "]" (* Ltac2 plugin *) +| "{" tac2rec_fieldexprs "}" (* Ltac2 plugin *) +| G_LTAC2_tactic_atom (* Ltac2 plugin *) +] + +G_LTAC2_branches: [ +| (* Ltac2 plugin *) +| "|" LIST1 branch SEP "|" (* Ltac2 plugin *) +| LIST1 branch SEP "|" (* Ltac2 plugin *) +] + +branch: [ +| tac2pat1 "=>" tac2expr6 (* Ltac2 plugin *) +] + +rec_flag: [ +| "rec" (* Ltac2 plugin *) +| (* Ltac2 plugin *) +] + +mut_flag: [ +| "mutable" (* Ltac2 plugin *) +| (* Ltac2 plugin *) +] + +typ_param: [ +| "'" Prim.ident (* Ltac2 plugin *) +] + +G_LTAC2_tactic_atom: [ +| Prim.integer (* Ltac2 plugin *) +| Prim.string (* Ltac2 plugin *) +| Prim.qualid (* Ltac2 plugin *) +| "@" Prim.ident (* Ltac2 plugin *) +| "&" lident (* Ltac2 plugin *) +| "'" Constr.constr (* Ltac2 plugin *) +| "constr" ":" "(" Constr.lconstr ")" (* Ltac2 plugin *) +| "open_constr" ":" "(" Constr.lconstr ")" (* Ltac2 plugin *) +| "ident" ":" "(" lident ")" (* Ltac2 plugin *) +| "pattern" ":" "(" Constr.lconstr_pattern ")" (* 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 *) +] + +tac2expr_in_env: [ +| test_ltac1_env LIST0 locident "|-" tac2expr6 (* Ltac2 plugin *) +| tac2expr6 (* Ltac2 plugin *) +] + +G_LTAC2_let_clause: [ +| let_binder ":=" tac2expr6 (* Ltac2 plugin *) +] + +let_binder: [ +| LIST1 G_LTAC2_input_fun (* Ltac2 plugin *) +] + +tac2type5: [ +| tac2type2 "->" tac2type5 (* Ltac2 plugin *) +| tac2type2 (* Ltac2 plugin *) +] + +tac2type2: [ +| tac2type1 "*" LIST1 tac2type1 SEP "*" (* Ltac2 plugin *) +| tac2type1 (* Ltac2 plugin *) +] + +tac2type1: [ +| tac2type0 Prim.qualid (* Ltac2 plugin *) +| tac2type0 (* Ltac2 plugin *) +] + +tac2type0: [ +| "(" LIST1 tac2type5 SEP "," ")" OPT Prim.qualid (* Ltac2 plugin *) +| typ_param (* Ltac2 plugin *) +| "_" (* Ltac2 plugin *) +| Prim.qualid (* Ltac2 plugin *) +] + +locident: [ +| Prim.ident (* Ltac2 plugin *) +] + +G_LTAC2_binder: [ +| "_" (* Ltac2 plugin *) +| Prim.ident (* Ltac2 plugin *) +] + +G_LTAC2_input_fun: [ +| tac2pat0 (* Ltac2 plugin *) +] + +tac2def_body: [ +| G_LTAC2_binder LIST0 G_LTAC2_input_fun ":=" tac2expr6 (* Ltac2 plugin *) +] + +tac2def_val: [ +| mut_flag rec_flag LIST1 tac2def_body SEP "with" (* Ltac2 plugin *) +] + +tac2def_mut: [ +| "Set" Prim.qualid OPT [ "as" locident ] ":=" tac2expr6 (* Ltac2 plugin *) +] + +tac2typ_knd: [ +| tac2type5 (* Ltac2 plugin *) +| "[" ".." "]" (* Ltac2 plugin *) +| "[" tac2alg_constructors "]" (* Ltac2 plugin *) +| "{" tac2rec_fields "}" (* Ltac2 plugin *) +] + +tac2alg_constructors: [ +| "|" LIST1 tac2alg_constructor SEP "|" (* Ltac2 plugin *) +| LIST0 tac2alg_constructor SEP "|" (* Ltac2 plugin *) +] + +tac2alg_constructor: [ +| Prim.ident (* Ltac2 plugin *) +| Prim.ident "(" LIST0 tac2type5 SEP "," ")" (* Ltac2 plugin *) +] + +tac2rec_fields: [ +| tac2rec_field ";" tac2rec_fields (* Ltac2 plugin *) +| tac2rec_field ";" (* Ltac2 plugin *) +| tac2rec_field (* Ltac2 plugin *) +| (* Ltac2 plugin *) +] + +tac2rec_field: [ +| mut_flag Prim.ident ":" tac2type5 (* Ltac2 plugin *) +] + +tac2rec_fieldexprs: [ +| tac2rec_fieldexpr ";" tac2rec_fieldexprs (* Ltac2 plugin *) +| tac2rec_fieldexpr ";" (* Ltac2 plugin *) +| tac2rec_fieldexpr (* Ltac2 plugin *) +| (* Ltac2 plugin *) +] + +tac2rec_fieldexpr: [ +| Prim.qualid ":=" tac2expr1 (* Ltac2 plugin *) +] + +tac2typ_prm: [ +| (* Ltac2 plugin *) +| typ_param (* Ltac2 plugin *) +| "(" LIST1 typ_param SEP "," ")" (* Ltac2 plugin *) +] + +tac2typ_def: [ +| tac2typ_prm Prim.qualid tac2type_body (* Ltac2 plugin *) +] + +tac2type_body: [ +| (* Ltac2 plugin *) +| ":=" tac2typ_knd (* Ltac2 plugin *) +| "::=" tac2typ_knd (* Ltac2 plugin *) +] + +tac2def_typ: [ +| "Type" rec_flag LIST1 tac2typ_def SEP "with" (* Ltac2 plugin *) +] + +tac2def_ext: [ +| "@" "external" locident ":" tac2type5 ":=" Prim.string Prim.string (* Ltac2 plugin *) +] + +syn_node: [ +| "_" (* Ltac2 plugin *) +| Prim.ident (* Ltac2 plugin *) +] + +sexpr: [ +| Prim.string (* Ltac2 plugin *) +| Prim.integer (* Ltac2 plugin *) +| syn_node (* Ltac2 plugin *) +| syn_node "(" LIST1 sexpr SEP "," ")" (* Ltac2 plugin *) +] + +syn_level: [ +| (* Ltac2 plugin *) +| ":" Prim.integer (* Ltac2 plugin *) +] + +tac2def_syn: [ +| "Notation" LIST1 sexpr syn_level ":=" tac2expr6 (* Ltac2 plugin *) +] + +lident: [ +| Prim.ident (* Ltac2 plugin *) +] + +globref: [ +| "&" Prim.ident (* Ltac2 plugin *) +| Prim.qualid (* Ltac2 plugin *) +] + +anti: [ +| "$" Prim.ident (* Ltac2 plugin *) +] + +ident_or_anti: [ +| lident (* Ltac2 plugin *) +| "$" Prim.ident (* Ltac2 plugin *) +] + +lnatural: [ +| Prim.natural (* Ltac2 plugin *) +] + +q_ident: [ +| ident_or_anti (* Ltac2 plugin *) +] + +qhyp: [ +| anti (* Ltac2 plugin *) +| lnatural (* Ltac2 plugin *) +| lident (* Ltac2 plugin *) +] + +G_LTAC2_simple_binding: [ +| "(" qhyp ":=" Constr.lconstr ")" (* Ltac2 plugin *) +] + +G_LTAC2_bindings: [ +| test_lpar_idnum_coloneq LIST1 G_LTAC2_simple_binding (* Ltac2 plugin *) +| LIST1 Constr.constr (* Ltac2 plugin *) +] + +q_bindings: [ +| G_LTAC2_bindings (* Ltac2 plugin *) +] + +q_with_bindings: [ +| G_LTAC2_with_bindings (* Ltac2 plugin *) +] + +G_LTAC2_intropatterns: [ +| LIST0 nonsimple_intropattern (* Ltac2 plugin *) +] + +G_LTAC2_or_and_intropattern: [ +| "[" LIST1 G_LTAC2_intropatterns SEP "|" "]" (* Ltac2 plugin *) +| "()" (* Ltac2 plugin *) +| "(" G_LTAC2_simple_intropattern ")" (* Ltac2 plugin *) +| "(" G_LTAC2_simple_intropattern "," LIST1 G_LTAC2_simple_intropattern SEP "," ")" (* Ltac2 plugin *) +| "(" G_LTAC2_simple_intropattern "&" LIST1 G_LTAC2_simple_intropattern SEP "&" ")" (* Ltac2 plugin *) +] + +G_LTAC2_equality_intropattern: [ +| "->" (* Ltac2 plugin *) +| "<-" (* Ltac2 plugin *) +| "[=" G_LTAC2_intropatterns "]" (* Ltac2 plugin *) +] + +G_LTAC2_naming_intropattern: [ +| LEFTQMARK lident (* Ltac2 plugin *) +| "?$" lident (* Ltac2 plugin *) +| "?" (* Ltac2 plugin *) +| ident_or_anti (* Ltac2 plugin *) +] + +nonsimple_intropattern: [ +| G_LTAC2_simple_intropattern (* Ltac2 plugin *) +| "*" (* Ltac2 plugin *) +| "**" (* Ltac2 plugin *) +] + +G_LTAC2_simple_intropattern: [ +| G_LTAC2_simple_intropattern_closed (* Ltac2 plugin *) +] + +G_LTAC2_simple_intropattern_closed: [ +| G_LTAC2_or_and_intropattern (* Ltac2 plugin *) +| G_LTAC2_equality_intropattern (* Ltac2 plugin *) +| "_" (* Ltac2 plugin *) +| G_LTAC2_naming_intropattern (* Ltac2 plugin *) +] + +q_intropatterns: [ +| G_LTAC2_intropatterns (* Ltac2 plugin *) +] + +q_intropattern: [ +| G_LTAC2_simple_intropattern (* Ltac2 plugin *) +] + +nat_or_anti: [ +| lnatural (* Ltac2 plugin *) +| "$" Prim.ident (* Ltac2 plugin *) +] + +G_LTAC2_eqn_ipat: [ +| "eqn" ":" G_LTAC2_naming_intropattern (* Ltac2 plugin *) +| (* Ltac2 plugin *) +] + +G_LTAC2_with_bindings: [ +| "with" G_LTAC2_bindings (* Ltac2 plugin *) +| (* Ltac2 plugin *) +] + +G_LTAC2_constr_with_bindings: [ +| Constr.constr G_LTAC2_with_bindings (* Ltac2 plugin *) +] + +G_LTAC2_destruction_arg: [ +| lnatural (* Ltac2 plugin *) +| lident (* Ltac2 plugin *) +| G_LTAC2_constr_with_bindings (* Ltac2 plugin *) +] + +q_destruction_arg: [ +| G_LTAC2_destruction_arg (* Ltac2 plugin *) +] + +G_LTAC2_as_or_and_ipat: [ +| "as" G_LTAC2_or_and_intropattern (* Ltac2 plugin *) +| (* Ltac2 plugin *) +] + +G_LTAC2_occs_nums: [ +| LIST1 nat_or_anti (* Ltac2 plugin *) +| "-" nat_or_anti LIST0 nat_or_anti (* Ltac2 plugin *) +] + +G_LTAC2_occs: [ +| "at" G_LTAC2_occs_nums (* Ltac2 plugin *) +| (* Ltac2 plugin *) +] + +G_LTAC2_hypident: [ +| ident_or_anti (* Ltac2 plugin *) +| "(" "type" "of" ident_or_anti ")" (* Ltac2 plugin *) +| "(" "value" "of" ident_or_anti ")" (* Ltac2 plugin *) +] + +G_LTAC2_hypident_occ: [ +| G_LTAC2_hypident G_LTAC2_occs (* Ltac2 plugin *) +] + +G_LTAC2_in_clause: [ +| "*" G_LTAC2_occs (* Ltac2 plugin *) +| "*" "|-" G_LTAC2_concl_occ (* Ltac2 plugin *) +| LIST0 G_LTAC2_hypident_occ SEP "," "|-" G_LTAC2_concl_occ (* Ltac2 plugin *) +| LIST0 G_LTAC2_hypident_occ SEP "," (* Ltac2 plugin *) +] + +clause: [ +| "in" G_LTAC2_in_clause (* Ltac2 plugin *) +| "at" G_LTAC2_occs_nums (* Ltac2 plugin *) +] + +q_clause: [ +| clause (* Ltac2 plugin *) +] + +G_LTAC2_concl_occ: [ +| "*" G_LTAC2_occs (* Ltac2 plugin *) +| (* Ltac2 plugin *) +] + +G_LTAC2_induction_clause: [ +| G_LTAC2_destruction_arg G_LTAC2_as_or_and_ipat G_LTAC2_eqn_ipat OPT clause (* Ltac2 plugin *) +] + +q_induction_clause: [ +| G_LTAC2_induction_clause (* Ltac2 plugin *) +] + +G_LTAC2_conversion: [ +| Constr.constr (* Ltac2 plugin *) +| Constr.constr "with" Constr.constr (* Ltac2 plugin *) +] + +q_conversion: [ +| G_LTAC2_conversion (* Ltac2 plugin *) +] + +ltac2_orient: [ +| "->" (* Ltac2 plugin *) +| "<-" (* Ltac2 plugin *) +| (* Ltac2 plugin *) +] + +G_LTAC2_rewriter: [ +| "!" G_LTAC2_constr_with_bindings (* Ltac2 plugin *) +| [ "?" | LEFTQMARK ] G_LTAC2_constr_with_bindings (* Ltac2 plugin *) +| lnatural "!" G_LTAC2_constr_with_bindings (* Ltac2 plugin *) +| lnatural [ "?" | LEFTQMARK ] G_LTAC2_constr_with_bindings (* Ltac2 plugin *) +| lnatural G_LTAC2_constr_with_bindings (* Ltac2 plugin *) +| G_LTAC2_constr_with_bindings (* Ltac2 plugin *) +] + +G_LTAC2_oriented_rewriter: [ +| ltac2_orient G_LTAC2_rewriter (* Ltac2 plugin *) +] + +q_rewriting: [ +| G_LTAC2_oriented_rewriter (* Ltac2 plugin *) +] + +G_LTAC2_tactic_then_last: [ +| "|" LIST0 ( OPT tac2expr6 ) 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_tactic_then_last (* Ltac2 plugin *) +| tac2expr6 (* Ltac2 plugin *) +| "|" G_LTAC2_tactic_then_gen (* Ltac2 plugin *) +| (* Ltac2 plugin *) +] + +q_dispatch: [ +| G_LTAC2_tactic_then_gen (* Ltac2 plugin *) +] + +q_occurrences: [ +| G_LTAC2_occs (* Ltac2 plugin *) +] + +red_flag: [ +| "beta" (* Ltac2 plugin *) +| "iota" (* Ltac2 plugin *) +| "match" (* Ltac2 plugin *) +| "fix" (* Ltac2 plugin *) +| "cofix" (* Ltac2 plugin *) +| "zeta" (* Ltac2 plugin *) +| "delta" G_LTAC2_delta_flag (* Ltac2 plugin *) +] + +refglobal: [ +| "&" Prim.ident (* Ltac2 plugin *) +| Prim.qualid (* Ltac2 plugin *) +| "$" Prim.ident (* Ltac2 plugin *) +] + +q_reference: [ +| refglobal (* Ltac2 plugin *) +] + +refglobals: [ +| LIST1 refglobal (* Ltac2 plugin *) +] + +G_LTAC2_delta_flag: [ +| "-" "[" refglobals "]" (* Ltac2 plugin *) +| "[" refglobals "]" (* Ltac2 plugin *) +| (* Ltac2 plugin *) +] + +G_LTAC2_strategy_flag: [ +| LIST1 red_flag (* Ltac2 plugin *) +| G_LTAC2_delta_flag (* Ltac2 plugin *) +] + +q_strategy_flag: [ +| G_LTAC2_strategy_flag (* Ltac2 plugin *) +] + +hintdb: [ +| "*" (* Ltac2 plugin *) +| LIST1 ident_or_anti (* Ltac2 plugin *) +] + +q_hintdb: [ +| hintdb (* Ltac2 plugin *) +] + +G_LTAC2_match_pattern: [ +| "context" OPT Prim.ident "[" Constr.lconstr_pattern "]" (* Ltac2 plugin *) +| Constr.lconstr_pattern (* Ltac2 plugin *) +] + +G_LTAC2_match_rule: [ +| G_LTAC2_match_pattern "=>" tac2expr6 (* Ltac2 plugin *) +] + +G_LTAC2_match_list: [ +| LIST1 G_LTAC2_match_rule SEP "|" (* Ltac2 plugin *) +| "|" LIST1 G_LTAC2_match_rule SEP "|" (* Ltac2 plugin *) +] + +q_constr_matching: [ +| G_LTAC2_match_list (* Ltac2 plugin *) +] + +gmatch_hyp_pattern: [ +| Prim.name ":" G_LTAC2_match_pattern (* Ltac2 plugin *) +] + +gmatch_pattern: [ +| "[" LIST0 gmatch_hyp_pattern SEP "," "|-" G_LTAC2_match_pattern "]" (* Ltac2 plugin *) +] + +gmatch_rule: [ +| gmatch_pattern "=>" tac2expr6 (* Ltac2 plugin *) +] + +gmatch_list: [ +| LIST1 gmatch_rule SEP "|" (* Ltac2 plugin *) +| "|" LIST1 gmatch_rule SEP "|" (* Ltac2 plugin *) +] + +q_goal_matching: [ +| gmatch_list (* Ltac2 plugin *) +] + +move_location: [ +| "at" "top" (* Ltac2 plugin *) +| "at" "bottom" (* Ltac2 plugin *) +| "after" ident_or_anti (* Ltac2 plugin *) +| "before" ident_or_anti (* Ltac2 plugin *) +] + +q_move_location: [ +| move_location (* Ltac2 plugin *) +] + +G_LTAC2_as_name: [ +| (* Ltac2 plugin *) +| "as" ident_or_anti (* Ltac2 plugin *) +] + +pose: [ +| test_lpar_id_coloneq "(" ident_or_anti ":=" Constr.lconstr ")" (* Ltac2 plugin *) +| Constr.constr G_LTAC2_as_name (* Ltac2 plugin *) +] + +q_pose: [ +| pose (* Ltac2 plugin *) +] + +G_LTAC2_as_ipat: [ +| "as" G_LTAC2_simple_intropattern (* Ltac2 plugin *) +| (* Ltac2 plugin *) +] + +G_LTAC2_by_tactic: [ +| "by" tac2expr6 (* Ltac2 plugin *) +| (* Ltac2 plugin *) +] + +assertion: [ +| test_lpar_id_coloneq "(" ident_or_anti ":=" Constr.lconstr ")" (* Ltac2 plugin *) +| test_lpar_id_colon "(" ident_or_anti ":" Constr.lconstr ")" G_LTAC2_by_tactic (* Ltac2 plugin *) +| Constr.constr G_LTAC2_as_ipat G_LTAC2_by_tactic (* Ltac2 plugin *) +] + +q_assert: [ +| assertion (* Ltac2 plugin *) +] + +ltac2_entry: [ +| tac2def_val (* Ltac2 plugin *) +| tac2def_typ (* Ltac2 plugin *) +| tac2def_ext (* Ltac2 plugin *) +| tac2def_syn (* Ltac2 plugin *) +| tac2def_mut (* Ltac2 plugin *) +] + +ltac2_expr: [ +| tac2expr6 (* Ltac2 plugin *) +] + +tac2mode: [ +| ltac2_expr ltac_use_default (* Ltac2 plugin *) +| G_vernac.query_command (* Ltac2 plugin *) +] + diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index f4bf51b6ba..84efc1e36c 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -45,6 +45,7 @@ term0: [ | term_match | term_record | term_generalizing +| "[|" LIST0 term SEP ";" "|" term OPT ( ":" type ) "|]" OPT univ_annot | term_ltac | "(" term ")" ] @@ -192,6 +193,32 @@ NOTINRSTS: [ | simple_tactic | REACHABLE | NOTINRSTS +| l1_tactic +| l3_tactic +| l2_tactic +| binder_tactic +| value_tactic +| ltac2_entry +| q_intropatterns +| q_intropattern +| q_ident +| q_destruction_arg +| q_with_bindings +| q_bindings +| q_strategy_flag +| q_reference +| q_clause +| q_occurrences +| q_induction_clause +| q_conversion +| q_rewriting +| q_dispatch +| q_hintdb +| q_move_location +| q_pose +| q_assert +| q_constr_matching +| q_goal_matching ] document: [ @@ -462,11 +489,11 @@ delta_flag: [ ] strategy_flag: [ -| LIST1 red_flags +| LIST1 red_flag | delta_flag ] -red_flags: [ +red_flag: [ | "beta" | "iota" | "match" @@ -751,6 +778,26 @@ command: [ | "Declare" "Reduction" ident ":=" red_expr | "Declare" "Custom" "Entry" ident | "Derive" ident "SuchThat" one_term "As" ident (* derive plugin *) +| "Extraction" qualid (* extraction plugin *) +| "Recursive" "Extraction" LIST1 qualid (* extraction plugin *) +| "Extraction" string LIST1 qualid (* extraction plugin *) +| "Extraction" "TestCompile" LIST1 qualid (* extraction plugin *) +| "Separate" "Extraction" LIST1 qualid (* extraction plugin *) +| "Extraction" "Library" ident (* extraction plugin *) +| "Recursive" "Extraction" "Library" ident (* extraction plugin *) +| "Extraction" "Language" language (* extraction plugin *) +| "Extraction" "Inline" LIST1 qualid (* extraction plugin *) +| "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" "Blacklist" LIST1 ident (* extraction plugin *) +| "Print" "Extraction" "Blacklist" (* extraction plugin *) +| "Reset" "Extraction" "Blacklist" (* extraction plugin *) +| "Extract" "Constant" qualid LIST0 string "=>" [ ident | string ] (* extraction plugin *) +| "Extract" "Inlined" "Constant" qualid "=>" [ ident | string ] (* extraction plugin *) +| "Extract" "Inductive" qualid "=>" [ ident | string ] "[" LIST0 [ ident | string ] "]" OPT string (* extraction plugin *) +| "Show" "Extraction" (* extraction plugin *) | "Proof" | "Proof" "Mode" string | "Proof" term @@ -807,6 +854,17 @@ command: [ | "Reset" "Ltac" "Profile" | "Show" "Ltac" "Profile" OPT [ "CutOff" int | 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 *) @@ -815,7 +873,6 @@ command: [ | "Add" "PropOp" one_term (* micromega plugin *) | "Add" "PropBinOp" one_term (* micromega plugin *) | "Add" "PropUOp" one_term (* micromega plugin *) -| "Add" "Spec" one_term (* micromega plugin *) | "Add" "BinOpSpec" one_term (* micromega plugin *) | "Add" "UnOpSpec" one_term (* micromega plugin *) | "Add" "Saturate" one_term (* micromega plugin *) @@ -824,8 +881,13 @@ command: [ | "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 "," ")" ) (* setoid_ring plugin *) +| "Print" "Rings" (* setoid_ring plugin *) +| "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" ) (* setoid_ring plugin *) +| "Print" "Fields" (* setoid_ring plugin *) | "Hint" "Cut" "[" hints_path "]" OPT ( ":" LIST1 ident ) | "Typeclasses" "Transparent" LIST0 qualid | "Typeclasses" "Opaque" LIST0 qualid @@ -841,26 +903,6 @@ command: [ | "Print" "Firstorder" "Solver" | "Function" fix_definition LIST0 ( "with" fix_definition ) | "Functional" "Scheme" fun_scheme_arg LIST0 ( "with" fun_scheme_arg ) -| "Extraction" qualid (* extraction plugin *) -| "Recursive" "Extraction" LIST1 qualid (* extraction plugin *) -| "Extraction" string LIST1 qualid (* extraction plugin *) -| "Extraction" "TestCompile" LIST1 qualid (* extraction plugin *) -| "Separate" "Extraction" LIST1 qualid (* extraction plugin *) -| "Extraction" "Library" ident (* extraction plugin *) -| "Recursive" "Extraction" "Library" ident (* extraction plugin *) -| "Extraction" "Language" language (* extraction plugin *) -| "Extraction" "Inline" LIST1 qualid (* extraction plugin *) -| "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" "Blacklist" LIST1 ident (* extraction plugin *) -| "Print" "Extraction" "Blacklist" (* extraction plugin *) -| "Reset" "Extraction" "Blacklist" (* extraction plugin *) -| "Extract" "Constant" qualid LIST0 string "=>" [ ident | string ] (* extraction plugin *) -| "Extract" "Inlined" "Constant" qualid "=>" [ ident | string ] (* extraction plugin *) -| "Extract" "Inductive" qualid "=>" [ ident | string ] "[" LIST0 [ ident | string ] "]" OPT string (* extraction plugin *) -| "Show" "Extraction" (* extraction plugin *) | "Functional" "Case" fun_scheme_arg (* funind plugin *) | "Generate" "graph" "for" qualid (* funind plugin *) | "Hint" "Rewrite" OPT [ "->" | "<-" ] LIST1 one_term OPT ( "using" ltac_expr ) OPT ( ":" LIST0 ident ) @@ -870,9 +912,6 @@ command: [ | "Derive" "Dependent" "Inversion_clear" ident "with" one_term "Sort" sort_family | "Declare" "Left" "Step" one_term | "Declare" "Right" "Step" one_term -| "Print" "Rings" (* setoid_ring plugin *) -| "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" ) (* setoid_ring plugin *) -| "Print" "Fields" (* setoid_ring plugin *) | "Numeral" "Notation" qualid qualid qualid ":" scope_name OPT numeral_modifier | "String" "Notation" qualid qualid qualid ":" scope_name | "SubClass" ident_decl def_body @@ -889,7 +928,7 @@ command: [ | "Combined" "Scheme" ident "from" LIST1 ident SEP "," | "Register" qualid "as" qualid | "Register" "Inline" qualid -| "Primitive" ident OPT [ ":" term ] ":=" "#" ident +| "Primitive" ident_decl OPT [ ":" term ] ":=" "#" ident | "Universe" LIST1 ident | "Universes" LIST1 ident | "Constraint" LIST1 univ_constraint SEP "," @@ -932,12 +971,12 @@ command: [ | "Delimit" "Scope" scope_name "with" scope_key | "Undelimit" "Scope" scope_name | "Bind" "Scope" scope_name "with" LIST1 class -| "Infix" string ":=" one_term OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" scope_name ] +| "Infix" string ":=" one_term OPT ( "(" LIST1 syntax_modifier SEP "," ")" ) OPT [ ":" scope_name ] | "Notation" ident LIST0 ident ":=" one_term OPT ( "(" "only" "parsing" ")" ) -| "Notation" string ":=" one_term OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" scope_name ] +| "Notation" string ":=" one_term OPT ( "(" LIST1 syntax_modifier SEP "," ")" ) OPT [ ":" scope_name ] | "Format" "Notation" string string string -| "Reserved" "Infix" string OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] -| "Reserved" "Notation" string OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] +| "Reserved" "Infix" string OPT ( "(" LIST1 syntax_modifier SEP "," ")" ) +| "Reserved" "Notation" string OPT ( "(" LIST1 syntax_modifier SEP "," ")" ) | "Eval" red_expr "in" term | "Compute" term | "Check" term @@ -946,6 +985,14 @@ command: [ | "SearchPattern" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid ) | "SearchRewrite" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid ) | "Search" LIST1 ( search_query ) OPT ( [ "inside" | "outside" ] LIST1 qualid ) +| "Ltac2" OPT "mutable" OPT "rec" tac2def_body LIST0 ( "with" tac2def_body ) +| "Ltac2" "Type" OPT "rec" tac2typ_def LIST0 ( "with" tac2typ_def ) +| "Ltac2" "@" "external" ident ":" ltac2_type ":=" string string +| "Ltac2" "Notation" LIST1 ltac2_scope OPT ( ":" int ) ":=" ltac2_expr +| "Ltac2" "Set" qualid OPT [ "as" ident ] ":=" ltac2_expr +| "Ltac2" "Notation" [ string | lident ] ":=" ltac2_expr (* Ltac2 plugin *) +| "Ltac2" "Eval" ltac2_expr (* Ltac2 plugin *) +| "Print" "Ltac2" qualid (* Ltac2 plugin *) | "Time" sentence | "Redirect" string sentence | "Timeout" num sentence @@ -1044,8 +1091,170 @@ ltac_production_item: [ | ident OPT ( "(" ident OPT ( "," string ) ")" ) ] +tac2expr_in_env: [ +| LIST0 ident "|-" ltac2_expr (* Ltac2 plugin *) +| ltac2_expr (* Ltac2 plugin *) +] + +ltac2_type: [ +| ltac2_type2 "->" ltac2_type (* Ltac2 plugin *) +| ltac2_type2 (* Ltac2 plugin *) +] + +ltac2_type2: [ +| ltac2_type1 "*" LIST1 ltac2_type1 SEP "*" (* Ltac2 plugin *) +| ltac2_type1 (* Ltac2 plugin *) +] + +ltac2_type1: [ +| ltac2_type0 qualid (* Ltac2 plugin *) +| ltac2_type0 (* Ltac2 plugin *) +] + +ltac2_type0: [ +| "(" LIST1 ltac2_type SEP "," ")" OPT qualid (* Ltac2 plugin *) +| ltac2_typevar (* Ltac2 plugin *) +| "_" (* Ltac2 plugin *) +| qualid (* Ltac2 plugin *) +] + +ltac2_typevar: [ +| "'" ident (* Ltac2 plugin *) +] + +lident: [ +| ident (* Ltac2 plugin *) +] + +destruction_arg: [ +| num +| constr_with_bindings +| constr_with_bindings_arg +] + +constr_with_bindings_arg: [ +| ">" constr_with_bindings +| constr_with_bindings +] + +clause_dft_concl: [ +| "in" in_clause +| OPT ( "at" occs_nums ) +] + +in_clause: [ +| "*" OPT ( "at" occs_nums ) +| "*" "|-" OPT concl_occ +| LIST0 hypident_occ SEP "," OPT ( "|-" OPT concl_occ ) +] + +hypident_occ: [ +| hypident OPT ( "at" occs_nums ) +] + +hypident: [ +| ident +| "(" "type" "of" ident ")" +| "(" "value" "of" ident ")" +] + +concl_occ: [ +| "*" OPT ( "at" occs_nums ) +] + +q_intropatterns: [ +| ltac2_intropatterns (* Ltac2 plugin *) +] + +ltac2_intropatterns: [ +| LIST0 nonsimple_intropattern (* Ltac2 plugin *) +] + +nonsimple_intropattern: [ +| "*" (* Ltac2 plugin *) +| "**" (* Ltac2 plugin *) +| ltac2_simple_intropattern (* Ltac2 plugin *) +] + +q_intropattern: [ +| ltac2_simple_intropattern (* Ltac2 plugin *) +] + +ltac2_simple_intropattern: [ +| ltac2_naming_intropattern (* Ltac2 plugin *) +| "_" (* Ltac2 plugin *) +| ltac2_or_and_intropattern (* Ltac2 plugin *) +| ltac2_equality_intropattern (* Ltac2 plugin *) +] + +ltac2_or_and_intropattern: [ +| "[" LIST1 ltac2_intropatterns SEP "|" "]" (* Ltac2 plugin *) +| "()" (* Ltac2 plugin *) +| "(" LIST1 ltac2_simple_intropattern SEP "," ")" (* Ltac2 plugin *) +| "(" LIST1 ltac2_simple_intropattern SEP "&" ")" (* Ltac2 plugin *) +] + +ltac2_equality_intropattern: [ +| "->" (* Ltac2 plugin *) +| "<-" (* Ltac2 plugin *) +| "[=" ltac2_intropatterns "]" (* Ltac2 plugin *) +] + +ltac2_naming_intropattern: [ +| "?" lident (* Ltac2 plugin *) +| "?$" lident (* Ltac2 plugin *) +| "?" (* Ltac2 plugin *) +| ident_or_anti (* Ltac2 plugin *) +] + +q_ident: [ +| ident_or_anti (* Ltac2 plugin *) +] + +ident_or_anti: [ +| lident (* Ltac2 plugin *) +| "$" ident (* Ltac2 plugin *) +] + +q_destruction_arg: [ +| ltac2_destruction_arg (* Ltac2 plugin *) +] + +ltac2_destruction_arg: [ +| num (* Ltac2 plugin *) +| lident (* Ltac2 plugin *) +| ltac2_constr_with_bindings (* Ltac2 plugin *) +] + +ltac2_constr_with_bindings: [ +| term OPT ( "with" ltac2_bindings ) (* Ltac2 plugin *) +] + +q_bindings: [ +| ltac2_bindings (* Ltac2 plugin *) +] + +q_with_bindings: [ +| OPT ( "with" ltac2_bindings ) (* Ltac2 plugin *) +] + +ltac2_bindings: [ +| LIST1 ltac2_simple_binding (* Ltac2 plugin *) +| LIST1 term (* Ltac2 plugin *) +] + +ltac2_simple_binding: [ +| "(" qhyp ":=" term ")" (* Ltac2 plugin *) +] + +qhyp: [ +| "$" ident (* Ltac2 plugin *) +| num (* Ltac2 plugin *) +| lident (* Ltac2 plugin *) +] + int_or_id: [ -| ident (* extraction plugin *) +| ident | int (* extraction plugin *) ] @@ -1151,7 +1360,7 @@ decl_notations: [ ] decl_notation: [ -| string ":=" one_term OPT ( "(" "only" "parsing" ")" ) OPT [ ":" scope_name ] +| string ":=" one_term OPT ( "(" LIST1 syntax_modifier SEP "," ")" ) OPT [ ":" scope_name ] ] simple_tactic: [ @@ -1210,6 +1419,7 @@ simple_tactic: [ | "solve" "[" LIST0 ltac_expr SEP "|" "]" | "idtac" LIST0 [ ident | string | int ] | [ "fail" | "gfail" ] OPT int_or_var LIST0 [ ident | string | int ] +| "fun" LIST1 name "=>" ltac_expr | "eval" red_expr "in" term | "context" ident "[" term "]" | "type" "of" term @@ -1219,13 +1429,14 @@ simple_tactic: [ | "uconstr" ":" "(" term ")" | "fun" LIST1 name "=>" ltac_expr | "let" OPT "rec" let_clause LIST0 ( "with" let_clause ) "in" ltac_expr -| "info" ltac_expr | ltac_expr3 ";" [ ltac_expr3 | binder_tactic ] | ltac_expr3 ";" "[" for_each_goal "]" | ltac_expr1 "+" [ ltac_expr2 | binder_tactic ] | ltac_expr1 "||" [ ltac_expr2 | binder_tactic ] | "[>" for_each_goal "]" | toplevel_selector ":" ltac_expr +| ltac2_match_key ltac2_expr "with" ltac2_match_list "end" +| ltac2_match_key OPT "reverse" "goal" "with" goal_match_list "end" | "simplify_eq" OPT destruction_arg | "esimplify_eq" OPT destruction_arg | "discriminate" OPT destruction_arg @@ -1329,10 +1540,10 @@ simple_tactic: [ | "setoid_reflexivity" | "setoid_transitivity" one_term | "setoid_etransitivity" -| "decide" "equality" -| "compare" one_term one_term | "intros" LIST0 intropattern | "eintros" LIST0 intropattern +| "decide" "equality" +| "compare" one_term one_term | "apply" LIST1 constr_with_bindings_arg SEP "," OPT in_hyp_as | "eapply" LIST1 constr_with_bindings_arg SEP "," OPT in_hyp_as | "simple" "apply" LIST1 constr_with_bindings_arg SEP "," OPT in_hyp_as @@ -1453,6 +1664,7 @@ simple_tactic: [ | "psatz" term OPT int_or_var | "ring" OPT ( "[" LIST1 term "]" ) | "ring_simplify" OPT ( "[" LIST1 term "]" ) LIST1 term OPT ( "in" ident ) +| "match" ltac2_expr5 "with" OPT ltac2_branches "end" | qualid LIST1 tactic_arg ] @@ -1465,26 +1677,6 @@ hloc: [ | "in" "(" "value" "of" ident ")" ] -in_clause: [ -| LIST0 hypident_occ SEP "," OPT ( "|-" OPT concl_occ ) -| "*" "|-" OPT concl_occ -| "*" OPT ( "at" occs_nums ) -] - -concl_occ: [ -| "*" OPT ( "at" occs_nums ) -] - -hypident_occ: [ -| hypident OPT ( "at" occs_nums ) -] - -hypident: [ -| ident -| "(" "type" "of" ident ")" -| "(" "value" "of" ident ")" -] - as_ipat: [ | "as" simple_intropattern ] @@ -1507,12 +1699,7 @@ as_name: [ ] rewriter: [ -| "!" constr_with_bindings_arg -| "?" constr_with_bindings_arg -| num "!" constr_with_bindings_arg -| num [ "?" | "?" ] constr_with_bindings_arg -| num constr_with_bindings_arg -| constr_with_bindings_arg +| OPT num OPT [ "?" | "!" ] constr_with_bindings_arg ] oriented_rewriter: [ @@ -1554,9 +1741,9 @@ naming_intropattern: [ ] intropattern: [ -| simple_intropattern | "*" | "**" +| simple_intropattern ] simple_intropattern: [ @@ -1597,9 +1784,367 @@ bindings_with_parameters: [ | "(" ident LIST0 simple_binder ":=" term ")" ] -clause_dft_concl: [ -| "in" in_clause -| OPT ( "at" occs_nums ) +q_clause: [ +| ltac2_clause (* Ltac2 plugin *) +] + +ltac2_clause: [ +| "in" ltac2_in_clause (* Ltac2 plugin *) +| "at" ltac2_occs_nums (* Ltac2 plugin *) +] + +ltac2_in_clause: [ +| "*" OPT ltac2_occs (* Ltac2 plugin *) +| "*" "|-" OPT ltac2_concl_occ (* Ltac2 plugin *) +| LIST0 ltac2_hypident_occ SEP "," OPT ( "|-" OPT ltac2_concl_occ ) (* Ltac2 plugin *) +] + +q_occurrences: [ +| OPT ltac2_occs (* Ltac2 plugin *) +] + +ltac2_occs: [ +| "at" ltac2_occs_nums (* Ltac2 plugin *) +] + +ltac2_occs_nums: [ +| OPT "-" LIST1 [ num (* Ltac2 plugin *) | "$" ident ] (* Ltac2 plugin *) +] + +ltac2_concl_occ: [ +| "*" OPT ltac2_occs (* Ltac2 plugin *) +] + +ltac2_hypident_occ: [ +| ltac2_hypident OPT ltac2_occs (* Ltac2 plugin *) +] + +ltac2_hypident: [ +| ident_or_anti (* Ltac2 plugin *) +| "(" "type" "of" ident_or_anti ")" (* Ltac2 plugin *) +| "(" "value" "of" ident_or_anti ")" (* Ltac2 plugin *) +] + +q_induction_clause: [ +| ltac2_induction_clause (* Ltac2 plugin *) +] + +ltac2_induction_clause: [ +| ltac2_destruction_arg OPT ltac2_as_or_and_ipat OPT ltac2_eqn_ipat OPT ltac2_clause (* Ltac2 plugin *) +] + +ltac2_as_or_and_ipat: [ +| "as" ltac2_or_and_intropattern (* Ltac2 plugin *) +] + +ltac2_eqn_ipat: [ +| "eqn" ":" ltac2_naming_intropattern (* Ltac2 plugin *) +] + +q_conversion: [ +| ltac2_conversion (* Ltac2 plugin *) +] + +ltac2_conversion: [ +| term (* Ltac2 plugin *) +| term "with" term (* Ltac2 plugin *) +] + +q_rewriting: [ +| ltac2_oriented_rewriter (* Ltac2 plugin *) +] + +ltac2_oriented_rewriter: [ +| [ "->" | "<-" ] ltac2_rewriter (* Ltac2 plugin *) +] + +ltac2_rewriter: [ +| OPT num OPT [ "?" | "!" ] ltac2_constr_with_bindings +] + +q_dispatch: [ +| ltac2_for_each_goal (* Ltac2 plugin *) +] + +ltac2_for_each_goal: [ +| ltac2_goal_tactics (* Ltac2 plugin *) +| OPT ( ltac2_goal_tactics "|" ) OPT ltac2_expr ".." OPT ( "|" ltac2_goal_tactics ) (* Ltac2 plugin *) +] + +ltac2_goal_tactics: [ +| LIST0 ( OPT ltac2_expr ) SEP "|" (* Ltac2 plugin *) +] + +q_strategy_flag: [ +| ltac2_strategy_flag (* Ltac2 plugin *) +] + +ltac2_strategy_flag: [ +| LIST1 ltac2_red_flag (* Ltac2 plugin *) +| OPT ltac2_delta_flag (* Ltac2 plugin *) +] + +ltac2_red_flag: [ +| "beta" (* Ltac2 plugin *) +| "iota" (* Ltac2 plugin *) +| "match" (* Ltac2 plugin *) +| "fix" (* Ltac2 plugin *) +| "cofix" (* Ltac2 plugin *) +| "zeta" (* Ltac2 plugin *) +| "delta" OPT ltac2_delta_flag (* Ltac2 plugin *) +] + +ltac2_delta_flag: [ +| OPT "-" "[" LIST1 refglobal "]" +] + +q_reference: [ +| refglobal (* Ltac2 plugin *) +] + +refglobal: [ +| "&" ident (* Ltac2 plugin *) +| qualid (* Ltac2 plugin *) +| "$" ident (* Ltac2 plugin *) +] + +q_hintdb: [ +| hintdb (* Ltac2 plugin *) +] + +hintdb: [ +| "*" (* Ltac2 plugin *) +| LIST1 ident_or_anti (* Ltac2 plugin *) +] + +q_constr_matching: [ +| ltac2_match_list (* Ltac2 plugin *) +] + +ltac2_match_key: [ +| "lazy_match!" +| "match!" +| "multi_match!" +] + +ltac2_match_list: [ +| OPT "|" LIST1 ltac2_match_rule SEP "|" +] + +ltac2_match_rule: [ +| ltac2_match_pattern "=>" ltac2_expr (* Ltac2 plugin *) +] + +ltac2_match_pattern: [ +| cpattern (* Ltac2 plugin *) +| "context" OPT ident "[" cpattern "]" (* Ltac2 plugin *) +] + +q_goal_matching: [ +| goal_match_list (* Ltac2 plugin *) +] + +goal_match_list: [ +| OPT "|" LIST1 gmatch_rule SEP "|" +] + +gmatch_rule: [ +| gmatch_pattern "=>" ltac2_expr (* Ltac2 plugin *) +] + +gmatch_pattern: [ +| "[" LIST0 gmatch_hyp_pattern SEP "," "|-" ltac2_match_pattern "]" (* Ltac2 plugin *) +] + +gmatch_hyp_pattern: [ +| name ":" ltac2_match_pattern (* Ltac2 plugin *) +] + +q_move_location: [ +| move_location (* Ltac2 plugin *) +] + +move_location: [ +| "at" "top" (* Ltac2 plugin *) +| "at" "bottom" (* Ltac2 plugin *) +| "after" ident_or_anti (* Ltac2 plugin *) +| "before" ident_or_anti (* Ltac2 plugin *) +] + +q_pose: [ +| pose (* Ltac2 plugin *) +] + +pose: [ +| "(" ident_or_anti ":=" term ")" (* Ltac2 plugin *) +| term OPT ltac2_as_name (* Ltac2 plugin *) +] + +ltac2_as_name: [ +| "as" ident_or_anti (* Ltac2 plugin *) +] + +q_assert: [ +| assertion (* Ltac2 plugin *) +] + +assertion: [ +| "(" ident_or_anti ":=" term ")" (* Ltac2 plugin *) +| "(" ident_or_anti ":" term ")" OPT ltac2_by_tactic (* Ltac2 plugin *) +| term OPT ltac2_as_ipat OPT ltac2_by_tactic (* Ltac2 plugin *) +] + +ltac2_as_ipat: [ +| "as" ltac2_simple_intropattern (* Ltac2 plugin *) +] + +ltac2_by_tactic: [ +| "by" ltac2_expr (* Ltac2 plugin *) +] + +ltac2_entry: [ +] + +tac2def_body: [ +| [ "_" | ident ] LIST0 tac2pat0 ":=" ltac2_expr (* Ltac2 plugin *) +] + +tac2typ_def: [ +| OPT tac2typ_prm qualid OPT ( [ ":=" | "::=" ] tac2typ_knd ) (* Ltac2 plugin *) +] + +tac2typ_prm: [ +| ltac2_typevar (* Ltac2 plugin *) +| "(" LIST1 ltac2_typevar SEP "," ")" (* Ltac2 plugin *) +] + +tac2typ_knd: [ +| ltac2_type (* Ltac2 plugin *) +| "[" OPT ( OPT "|" LIST1 tac2alg_constructor SEP "|" ) "]" (* Ltac2 plugin *) +| "[" ".." "]" (* Ltac2 plugin *) +| "{" OPT ( LIST1 tac2rec_field SEP ";" OPT ";" ) "}" (* Ltac2 plugin *) +] + +tac2alg_constructor: [ +| ident (* Ltac2 plugin *) +| ident "(" LIST0 ltac2_type SEP "," ")" (* Ltac2 plugin *) +] + +tac2rec_field: [ +| OPT "mutable" ident ":" ltac2_type (* Ltac2 plugin *) +] + +ltac2_scope: [ +| string (* Ltac2 plugin *) +| int (* Ltac2 plugin *) +| name (* Ltac2 plugin *) +| name "(" LIST1 ltac2_scope SEP "," ")" (* Ltac2 plugin *) +] + +ltac2_expr: [ +| ltac2_expr5 ";" ltac2_expr (* Ltac2 plugin *) +| ltac2_expr5 (* Ltac2 plugin *) +] + +ltac2_expr5: [ +| "fun" LIST1 tac2pat0 "=>" ltac2_expr (* Ltac2 plugin *) +| "let" OPT "rec" ltac2_let_clause LIST0 ( "with" ltac2_let_clause ) "in" ltac2_expr (* Ltac2 plugin *) +| ltac2_expr3 (* Ltac2 plugin *) +] + +ltac2_let_clause: [ +| LIST1 tac2pat0 ":=" ltac2_expr (* Ltac2 plugin *) +] + +ltac2_expr3: [ +| LIST1 ltac2_expr2 SEP "," (* Ltac2 plugin *) +] + +ltac2_expr2: [ +| ltac2_expr1 "::" ltac2_expr2 (* Ltac2 plugin *) +| ltac2_expr1 (* Ltac2 plugin *) +] + +ltac2_expr1: [ +| ltac2_expr0 LIST1 ltac2_expr0 (* Ltac2 plugin *) +| ltac2_expr0 ".(" qualid ")" (* Ltac2 plugin *) +| ltac2_expr0 ".(" qualid ")" ":=" ltac2_expr5 (* Ltac2 plugin *) +| ltac2_expr0 (* Ltac2 plugin *) +] + +tac2rec_fieldexpr: [ +| qualid ":=" ltac2_expr1 (* Ltac2 plugin *) +] + +ltac2_expr0: [ +| "(" ltac2_expr ")" (* Ltac2 plugin *) +| "(" ltac2_expr ":" ltac2_type ")" (* Ltac2 plugin *) +| "()" (* Ltac2 plugin *) +| "[" LIST0 ltac2_expr5 SEP ";" "]" (* Ltac2 plugin *) +| "{" OPT ( LIST1 tac2rec_fieldexpr OPT ";" ) "}" (* Ltac2 plugin *) +| ltac2_tactic_atom (* Ltac2 plugin *) +] + +ltac2_tactic_atom: [ +| int (* Ltac2 plugin *) +| string (* Ltac2 plugin *) +| qualid (* Ltac2 plugin *) +| "@" ident (* Ltac2 plugin *) +| "&" lident (* Ltac2 plugin *) +| "'" term (* Ltac2 plugin *) +| ltac2_quotations +] + +ltac2_quotations: [ +| "ident" ":" "(" lident ")" +| "constr" ":" "(" term ")" +| "open_constr" ":" "(" term ")" +| "pattern" ":" "(" cpattern ")" +| "reference" ":" "(" [ "&" ident | qualid ] ")" +| "ltac1" ":" "(" ltac1_expr_in_env ")" +| "ltac1val" ":" "(" ltac1_expr_in_env ")" +] + +ltac1_expr_in_env: [ +| ltac_expr (* Ltac2 plugin *) +| LIST0 ident "|-" ltac_expr (* Ltac2 plugin *) +] + +ltac2_branches: [ +| OPT "|" LIST1 ( tac2pat1 "=>" ltac2_expr ) SEP "|" +] + +tac2pat1: [ +| qualid LIST1 tac2pat0 (* Ltac2 plugin *) +| qualid (* Ltac2 plugin *) +| "[" "]" (* Ltac2 plugin *) +| tac2pat0 "::" tac2pat0 (* Ltac2 plugin *) +| tac2pat0 (* Ltac2 plugin *) +] + +tac2pat0: [ +| "_" (* Ltac2 plugin *) +| "()" (* Ltac2 plugin *) +| qualid (* Ltac2 plugin *) +| "(" OPT atomic_tac2pat ")" (* Ltac2 plugin *) +] + +atomic_tac2pat: [ +| tac2pat1 ":" ltac2_type (* Ltac2 plugin *) +| tac2pat1 "," LIST0 tac2pat1 SEP "," (* Ltac2 plugin *) +| tac2pat1 (* Ltac2 plugin *) +] + +tac2mode: [ +| ltac2_expr [ "." | "..." ] (* Ltac2 plugin *) +| "Eval" red_expr "in" term +| "Compute" term +| "Check" term +| "About" reference OPT univ_name_list +| "SearchHead" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid ) +| "SearchPattern" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid ) +| "SearchRewrite" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid ) +| "Search" LIST1 ( search_query ) OPT ( [ "inside" | "outside" ] LIST1 qualid ) ] clause_dft_all: [ @@ -1636,17 +2181,6 @@ constr_with_bindings: [ | one_term OPT ( "with" bindings ) ] -destruction_arg: [ -| num -| constr_with_bindings -| constr_with_bindings_arg -] - -constr_with_bindings_arg: [ -| ">" constr_with_bindings -| constr_with_bindings -] - conversion: [ | one_term | one_term "with" one_term |