From a9658f29280dd7c00f5b50942da5f8225f28c754 Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Sun, 6 Sep 2020 19:09:05 -0700 Subject: Add global version of OPTINREF --- doc/sphinx/proof-engine/ltac2.rst | 2 +- doc/tools/docgram/README.md | 2 + doc/tools/docgram/common.edit_mlg | 243 ++------------------------------------ doc/tools/docgram/doc_grammar.ml | 20 +++- doc/tools/docgram/orderedGrammar | 2 +- 5 files changed, 27 insertions(+), 242 deletions(-) diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index b912bcbdf8..81c497d60a 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -1633,7 +1633,7 @@ Here is the syntax for the :n:`q_*` nonterminals: .. insertprodn ltac2_oriented_rewriter ltac2_rewriter .. prodn:: - ltac2_oriented_rewriter ::= {| -> | <- } @ltac2_rewriter + ltac2_oriented_rewriter ::= {? {| -> | <- } } @ltac2_rewriter ltac2_rewriter ::= {? @natural } {? {| ? | ! } } @ltac2_constr_with_bindings .. insertprodn ltac2_for_each_goal ltac2_goal_tactics diff --git a/doc/tools/docgram/README.md b/doc/tools/docgram/README.md index dbb04bb6a6..6c507e1d57 100644 --- a/doc/tools/docgram/README.md +++ b/doc/tools/docgram/README.md @@ -179,6 +179,8 @@ grammar with its productions and removing the non-terminal. Each should appear as a separate production. (Doesn't work recursively; splicing for both `A: [ | B ]` and `B: [ | C ]` must be done in separate SPLICE operations.) +`OPTINREF` - applies the local `OPTINREF` edit to every nonterminal + `EXPAND` - expands LIST0, LIST1, LIST* ... SEP and OPT constructs into new non-terminals diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 97d479b238..76a41828f7 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -202,10 +202,6 @@ for_each_goal: [ | OPT ( goal_tactics "|" ) OPT ltac_expr5 ".." OPT ( "|" goal_tactics ) ] -tactic_then_last: [ -| OPTINREF -] - ltac2_tactic_then_last: [ | REPLACE "|" LIST0 ( OPT ltac2_expr6 ) SEP "|" (* Ltac2 plugin *) | WITH LIST0 ( "|" OPT ltac2_expr6 ) TAG Ltac2 @@ -222,10 +218,6 @@ ltac2_for_each_goal: [ | OPT ( ltac2_goal_tactics "|" ) OPT ltac2_expr6 ".." OPT ( "|" ltac2_goal_tactics ) TAG Ltac2 ] -ltac2_tactic_then_last: [ -| OPTINREF -] - reference: [ | DELETENT ] reference: [ @@ -530,14 +522,6 @@ eqn: [ | WITH LIST1 [ LIST1 pattern100 SEP "," ] SEP "|" "=>" lconstr ] -universe_increment: [ -| OPTINREF -] - -evar_instance: [ -| OPTINREF -] - (* No constructor syntax, OPT [ "|" binders ] is not supported for Record *) record_definition: [ | opt_coercion ident_decl binders OPT [ ":" sort ] OPT ( ":=" OPT [ identref ] "{" record_fields "}" ) @@ -632,14 +616,6 @@ def_body: [ | WITH LIST0 binder ":" type ] -reduce: [ -| OPTINREF -] - -occs: [ -| OPTINREF -] - delta_flag: [ | REPLACE "-" "[" LIST1 smart_global "]" | WITH OPT "-" "[" LIST1 smart_global "]" @@ -653,7 +629,6 @@ ltac2_delta_flag: [ ltac2_branches: [ | EDIT ADD_OPT "|" LIST1 branch SEP "|" (* Ltac2 plugin *) -| OPTINREF ] strategy_flag: [ @@ -662,7 +637,6 @@ strategy_flag: [ (*| REPLACE LIST1 red_flags | WITH LIST1 red_flag*) | (* empty *) -| OPTINREF ] filtered_import: [ @@ -671,20 +645,14 @@ filtered_import: [ | DELETE global ] -functor_app_annot: [ -| OPTINREF -] - is_module_expr: [ | REPLACE ":=" module_expr_inl LIST0 ext_module_expr | WITH ":=" LIST1 module_expr_inl SEP "<+" -| OPTINREF ] is_module_type: [ | REPLACE ":=" module_type_inl LIST0 ext_module_type | WITH ":=" LIST1 module_type_inl SEP "<+" -| OPTINREF ] gallina_ext: [ @@ -729,10 +697,6 @@ gallina_ext: [ | WITH "From" dirpath "Require" export_token LIST1 global ] -export_token: [ -| OPTINREF -] - (* lexer stuff *) LEFTQMARK: [ | "?" @@ -1319,10 +1283,6 @@ command: [ | WITH "Goal" type ] -option_setting: [ -| OPTINREF -] - syntax: [ | REPLACE "Open" "Scope" IDENT | WITH "Open" "Scope" scope @@ -1435,7 +1395,6 @@ cofix_definition: [ type_cstr: [ | REPLACE ":" lconstr | WITH ":" type -| OPTINREF ] inductive_definition: [ @@ -1460,10 +1419,6 @@ record_binder: [ | DELETE name ] -at_level_opt: [ -| OPTINREF -] - query_command: [ | REPLACE "Eval" red_expr "in" lconstr "." | WITH "Eval" red_expr "in" lconstr @@ -1498,10 +1453,6 @@ vernac_toplevel: [ | DELETE vernac_control ] -in_or_out_modules: [ -| OPTINREF -] - vernac_control: [ (* replacing vernac_control with command is cheating a little; they can't refer to the vernac_toplevel commands. @@ -1517,90 +1468,8 @@ vernac_control: [ | DELETE decorated_vernac ] -orient: [ -| OPTINREF -] - -in_hyp_as: [ -| OPTINREF -] - -as_name: [ -| OPTINREF -] - -hloc: [ -| OPTINREF -] - -as_or_and_ipat: [ -| OPTINREF -] - -hintbases: [ -| OPTINREF -] - -as_ipat: [ -| OPTINREF -] - -auto_using: [ -| OPTINREF -] - -with_bindings: [ -| OPTINREF -] - -eqn_ipat: [ -| OPTINREF -] - -withtac: [ -| OPTINREF -] - of_module_type: [ | (* empty *) -| OPTINREF -] - - -clause_dft_all: [ -| OPTINREF -] - -opt_clause: [ -| OPTINREF -] - -with_names: [ -| OPTINREF -] - -in_hyp_list: [ -| OPTINREF -] - -struct_annot: [ -| OPTINREF -] - -firstorder_using: [ -| OPTINREF -] - -fun_ind_using: [ -| OPTINREF -] - -by_arg_tac: [ -| OPTINREF -] - -by_tactic: [ -| OPTINREF ] rewriter: [ @@ -1647,43 +1516,18 @@ record_declaration: [ fields_def: [ | DELETENT ] -hint_info: [ -| OPTINREF -] - -debug: [ -| OPTINREF -] - -eauto_search_strategy: [ -| OPTINREF -] - - constr_body: [ | DELETE ":=" lconstr | REPLACE ":" lconstr ":=" lconstr | WITH OPT ( ":" type ) ":=" lconstr ] -opt_hintbases: [ -| OPTINREF -] - -opthints: [ -| OPTINREF -] - scheme: [ | DELETE scheme_kind | REPLACE identref ":=" scheme_kind | WITH OPT ( identref ":=" ) scheme_kind ] -instance_name: [ -| OPTINREF -] - simple_reserv: [ | REPLACE LIST1 identref ":" lconstr | WITH LIST1 identref ":" type @@ -1702,22 +1546,9 @@ ltac2_in_clause: [ | DELETE LIST0 ltac2_hypident_occ SEP "," (* Ltac2 plugin *) ] -concl_occ: [ -| OPTINREF -] - -opt_coercion: [ -| OPTINREF -] - -opt_constructors_or_fields: [ -| OPTINREF -] - decl_notations: [ | REPLACE "where" LIST1 decl_notation SEP decl_sep | WITH "where" decl_notation LIST0 (decl_sep decl_notation ) -| OPTINREF ] module_expr: [ @@ -1778,15 +1609,6 @@ decl_notation: [ | WITH ne_lstring ":=" constr syntax_modifiers OPT [ ":" scope_name ] ] -syntax_modifiers: [ -| OPTINREF -] - - -only_parsing: [ -| OPTINREF -] - ltac_production_item: [ | REPLACE ident "(" ident OPT ltac_production_sep ")" | WITH ident OPT ( "(" ident OPT ltac_production_sep ")" ) @@ -2024,10 +1846,6 @@ DELETE: [ | test_ltac1_env ] -mut_flag: [ -| OPTINREF -] - rec_flag: [ | OPTINREF ] @@ -2081,7 +1899,6 @@ tac2rec_fieldexprs: [ | DELETE tac2rec_fieldexpr ";" | DELETE tac2rec_fieldexpr | LIST1 tac2rec_fieldexpr OPT ";" -| OPTINREF ] tac2rec_fields: [ @@ -2089,7 +1906,6 @@ tac2rec_fields: [ | DELETE tac2rec_field ";" | DELETE tac2rec_field | LIST1 tac2rec_field SEP ";" OPT ";" TAG Ltac2 -| OPTINREF ] (* todo: weird productions, ints only after an initial "-"??: @@ -2103,46 +1919,6 @@ ltac2_occs_nums: [ | 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 @@ -2177,14 +1953,9 @@ SPLICE: [ | 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 @@ -2233,8 +2004,8 @@ q_clause: [ ] 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 +| REPLACE ltac2_destruction_arg ltac2_as_or_and_ipat ltac2_eqn_ipat OPT clause (* Ltac2 plugin *) +| WITH ltac2_destruction_arg ltac2_as_or_and_ipat ltac2_eqn_ipat OPT ltac2_clause TAG Ltac2 ] starredidentref: [ @@ -2464,6 +2235,11 @@ SPLICE: [ | number_string_mapping | number_options | string_option +| tac2type_body +| tac2rec_fields +| mut_flag +| tac2rec_fieldexprs +| syn_level ] (* end SPLICE *) RENAME: [ @@ -2500,11 +2276,6 @@ simple_tactic: [ | qualid LIST1 tactic_arg ] -(* todo: doesn't work if up above... maybe because 'clause' doesn't exist? *) -clause_dft_concl: [ -| OPTINREF -] - SPLICE: [ | gallina | gallina_ext diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml index 92bcd51528..96eaff2895 100644 --- a/doc/tools/docgram/doc_grammar.ml +++ b/doc/tools/docgram/doc_grammar.ml @@ -1190,6 +1190,15 @@ let edit_all_prods g op eprods = | "DELETE" -> do_it op eprods 1; true | "SPLICE" -> do_it op eprods 1; true | "MERGE" -> do_it op eprods 2; true + | "OPTINREF" -> + List.iter (fun nt -> + let prods = NTMap.find nt !g.map in + if has_match [] prods then begin + let prods' = remove_prod [] prods nt in + g_update_prods g nt prods'; + global_repl g [(Snterm nt)] [(Sopt (Snterm nt))] + end) + !g.order; true | "EXPAND" -> if List.length eprods > 1 || List.length (List.hd eprods) <> 0 then error "'EXPAND:' expects a single empty production\n"; @@ -2007,10 +2016,13 @@ 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;*) + (* + Printf.printf "\n"; + NTMap.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.map; + *) if total <> 0 then Printf.eprintf "TOTAL %ss not included = %d\n" label total diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 75c0ca1453..94a6fa730b 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -1837,7 +1837,7 @@ q_rewriting: [ ] ltac2_oriented_rewriter: [ -| [ "->" | "<-" ] ltac2_rewriter (* Ltac2 plugin *) +| OPT [ "->" | "<-" ] ltac2_rewriter (* Ltac2 plugin *) ] ltac2_rewriter: [ -- cgit v1.2.3 From 7d8389d012aa8dbdeb7b82217087f1b7dfb2b24e Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Wed, 9 Sep 2020 02:07:44 -0700 Subject: Add additional escape sequences for notations --- doc/tools/coqrst/notations/TacticNotations.g | 3 +- doc/tools/coqrst/notations/TacticNotationsLexer.py | 59 ++++++++++++---------- doc/tools/docgram/doc_grammar.ml | 5 ++ 3 files changed, 39 insertions(+), 28 deletions(-) diff --git a/doc/tools/coqrst/notations/TacticNotations.g b/doc/tools/coqrst/notations/TacticNotations.g index f29c69eeaf..70107eba46 100644 --- a/doc/tools/coqrst/notations/TacticNotations.g +++ b/doc/tools/coqrst/notations/TacticNotations.g @@ -43,7 +43,8 @@ LGROUP: '{+' | '{*' | '{?'; LBRACE: '{'; RBRACE: '}'; // todo: need a cleaner way to escape the 3-character strings here -ESCAPED: '%{' | '%}' | '%|' | '`%{' | '@%{'; +ESCAPED: '%{' | '%}' | '%|' | '`%{' | '@%{' | + '%|-' | '%|->' | '%||' | '%|||' | '%||||'; // for SSR PIPE: '|'; ATOM: '@' | '_' | ~[@_{}| ]+; ID: '@' ('_'? [a-zA-Z0-9])+; diff --git a/doc/tools/coqrst/notations/TacticNotationsLexer.py b/doc/tools/coqrst/notations/TacticNotationsLexer.py index 7bda849010..a7ad55ad34 100644 --- a/doc/tools/coqrst/notations/TacticNotationsLexer.py +++ b/doc/tools/coqrst/notations/TacticNotationsLexer.py @@ -8,35 +8,40 @@ import sys def serializedATN(): with StringIO() as buf: buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\2\f") - buf.write("S\b\1\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7") + buf.write("f\b\1\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7") buf.write("\4\b\t\b\4\t\t\t\4\n\t\n\4\13\t\13\3\2\3\2\3\2\3\3\3\3") buf.write("\3\3\3\3\3\3\3\3\5\3!\n\3\3\4\3\4\3\5\3\5\3\6\3\6\3\6") - buf.write("\3\6\3\6\3\6\3\6\3\6\3\6\3\6\3\6\3\6\5\6\63\n\6\3\7\3") - buf.write("\7\3\b\3\b\6\b9\n\b\r\b\16\b:\5\b=\n\b\3\t\3\t\5\tA\n") - buf.write("\t\3\t\6\tD\n\t\r\t\16\tE\3\n\3\n\3\n\6\nK\n\n\r\n\16") - buf.write("\nL\3\13\6\13P\n\13\r\13\16\13Q\2\2\f\3\3\5\4\7\5\t\6") - buf.write("\13\7\r\b\17\t\21\n\23\13\25\f\3\2\5\4\2BBaa\6\2\"\"B") - buf.write("Baa}\177\5\2\62;C\\c|\2^\2\3\3\2\2\2\2\5\3\2\2\2\2\7\3") - buf.write("\2\2\2\2\t\3\2\2\2\2\13\3\2\2\2\2\r\3\2\2\2\2\17\3\2\2") - buf.write("\2\2\21\3\2\2\2\2\23\3\2\2\2\2\25\3\2\2\2\3\27\3\2\2\2") - buf.write("\5 \3\2\2\2\7\"\3\2\2\2\t$\3\2\2\2\13\62\3\2\2\2\r\64") - buf.write("\3\2\2\2\17<\3\2\2\2\21>\3\2\2\2\23G\3\2\2\2\25O\3\2\2") - buf.write("\2\27\30\7}\2\2\30\31\7~\2\2\31\4\3\2\2\2\32\33\7}\2\2") - buf.write("\33!\7-\2\2\34\35\7}\2\2\35!\7,\2\2\36\37\7}\2\2\37!\7") - buf.write("A\2\2 \32\3\2\2\2 \34\3\2\2\2 \36\3\2\2\2!\6\3\2\2\2\"") - buf.write("#\7}\2\2#\b\3\2\2\2$%\7\177\2\2%\n\3\2\2\2&\'\7\'\2\2") - buf.write("\'\63\7}\2\2()\7\'\2\2)\63\7\177\2\2*+\7\'\2\2+\63\7~") - buf.write("\2\2,-\7b\2\2-.\7\'\2\2.\63\7}\2\2/\60\7B\2\2\60\61\7") - buf.write("\'\2\2\61\63\7}\2\2\62&\3\2\2\2\62(\3\2\2\2\62*\3\2\2") - buf.write("\2\62,\3\2\2\2\62/\3\2\2\2\63\f\3\2\2\2\64\65\7~\2\2\65") - buf.write("\16\3\2\2\2\66=\t\2\2\2\679\n\3\2\28\67\3\2\2\29:\3\2") - buf.write("\2\2:8\3\2\2\2:;\3\2\2\2;=\3\2\2\2<\66\3\2\2\2<8\3\2\2") - buf.write("\2=\20\3\2\2\2>C\7B\2\2?A\7a\2\2@?\3\2\2\2@A\3\2\2\2A") - buf.write("B\3\2\2\2BD\t\4\2\2C@\3\2\2\2DE\3\2\2\2EC\3\2\2\2EF\3") - buf.write("\2\2\2F\22\3\2\2\2GH\7a\2\2HJ\7a\2\2IK\t\4\2\2JI\3\2\2") - buf.write("\2KL\3\2\2\2LJ\3\2\2\2LM\3\2\2\2M\24\3\2\2\2NP\7\"\2\2") - buf.write("ON\3\2\2\2PQ\3\2\2\2QO\3\2\2\2QR\3\2\2\2R\26\3\2\2\2\13") - buf.write("\2 \62:<@ELQ\2") + buf.write("\3\6\3\6\3\6\3\6\3\6\3\6\3\6\3\6\3\6\3\6\3\6\3\6\3\6\3") + buf.write("\6\3\6\3\6\3\6\3\6\3\6\3\6\3\6\3\6\3\6\3\6\3\6\3\6\3\6") + buf.write("\3\6\5\6F\n\6\3\7\3\7\3\b\3\b\6\bL\n\b\r\b\16\bM\5\bP") + buf.write("\n\b\3\t\3\t\5\tT\n\t\3\t\6\tW\n\t\r\t\16\tX\3\n\3\n\3") + buf.write("\n\6\n^\n\n\r\n\16\n_\3\13\6\13c\n\13\r\13\16\13d\2\2") + buf.write("\f\3\3\5\4\7\5\t\6\13\7\r\b\17\t\21\n\23\13\25\f\3\2\5") + buf.write("\4\2BBaa\6\2\"\"BBaa}\177\5\2\62;C\\c|\2v\2\3\3\2\2\2") + buf.write("\2\5\3\2\2\2\2\7\3\2\2\2\2\t\3\2\2\2\2\13\3\2\2\2\2\r") + buf.write("\3\2\2\2\2\17\3\2\2\2\2\21\3\2\2\2\2\23\3\2\2\2\2\25\3") + buf.write("\2\2\2\3\27\3\2\2\2\5 \3\2\2\2\7\"\3\2\2\2\t$\3\2\2\2") + buf.write("\13E\3\2\2\2\rG\3\2\2\2\17O\3\2\2\2\21Q\3\2\2\2\23Z\3") + buf.write("\2\2\2\25b\3\2\2\2\27\30\7}\2\2\30\31\7~\2\2\31\4\3\2") + buf.write("\2\2\32\33\7}\2\2\33!\7-\2\2\34\35\7}\2\2\35!\7,\2\2\36") + buf.write("\37\7}\2\2\37!\7A\2\2 \32\3\2\2\2 \34\3\2\2\2 \36\3\2") + buf.write("\2\2!\6\3\2\2\2\"#\7}\2\2#\b\3\2\2\2$%\7\177\2\2%\n\3") + buf.write("\2\2\2&\'\7\'\2\2\'F\7}\2\2()\7\'\2\2)F\7\177\2\2*+\7") + buf.write("\'\2\2+F\7~\2\2,-\7b\2\2-.\7\'\2\2.F\7}\2\2/\60\7B\2\2") + buf.write("\60\61\7\'\2\2\61F\7}\2\2\62\63\7\'\2\2\63\64\7~\2\2\64") + buf.write("F\7/\2\2\65\66\7\'\2\2\66\67\7~\2\2\678\7/\2\28F\7@\2") + buf.write("\29:\7\'\2\2:;\7~\2\2;F\7~\2\2<=\7\'\2\2=>\7~\2\2>?\7") + buf.write("~\2\2?F\7~\2\2@A\7\'\2\2AB\7~\2\2BC\7~\2\2CD\7~\2\2DF") + buf.write("\7~\2\2E&\3\2\2\2E(\3\2\2\2E*\3\2\2\2E,\3\2\2\2E/\3\2") + buf.write("\2\2E\62\3\2\2\2E\65\3\2\2\2E9\3\2\2\2E<\3\2\2\2E@\3\2") + buf.write("\2\2F\f\3\2\2\2GH\7~\2\2H\16\3\2\2\2IP\t\2\2\2JL\n\3\2") + buf.write("\2KJ\3\2\2\2LM\3\2\2\2MK\3\2\2\2MN\3\2\2\2NP\3\2\2\2O") + buf.write("I\3\2\2\2OK\3\2\2\2P\20\3\2\2\2QV\7B\2\2RT\7a\2\2SR\3") + buf.write("\2\2\2ST\3\2\2\2TU\3\2\2\2UW\t\4\2\2VS\3\2\2\2WX\3\2\2") + buf.write("\2XV\3\2\2\2XY\3\2\2\2Y\22\3\2\2\2Z[\7a\2\2[]\7a\2\2\\") + buf.write("^\t\4\2\2]\\\3\2\2\2^_\3\2\2\2_]\3\2\2\2_`\3\2\2\2`\24") + buf.write("\3\2\2\2ac\7\"\2\2ba\3\2\2\2cd\3\2\2\2db\3\2\2\2de\3\2") + buf.write("\2\2e\26\3\2\2\2\13\2 EMOSX_d\2") return buf.getvalue() diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml index 96eaff2895..548ca7364c 100644 --- a/doc/tools/docgram/doc_grammar.ml +++ b/doc/tools/docgram/doc_grammar.ml @@ -309,6 +309,11 @@ let rec output_prodn = function | "{|" -> "%{%|" | "`{" -> "`%{" | "@{" -> "@%{" + | "|-" -> "%|-" + | "|->" -> "%|->" + | "||" -> "%||" + | "|||" -> "%|||" + | "||||" -> "%||||" | "{" | "}" | "|" -> "%" ^ s -- cgit v1.2.3 From da9fd81c887024e991467d4dd586661c4ca01022 Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Sat, 12 Sep 2020 20:54:22 -0700 Subject: Convert logic.rst to prodn --- Makefile.doc | 3 +- doc/sphinx/addendum/ring.rst | 15 +- doc/sphinx/proof-engine/ltac.rst | 8 +- doc/sphinx/proof-engine/ltac2.rst | 8 +- doc/sphinx/proofs/automatic-tactics/logic.rst | 278 ++++------ doc/tools/docgram/common.edit_mlg | 491 ++++++++++++++++-- doc/tools/docgram/doc_grammar.ml | 50 +- doc/tools/docgram/fullGrammar | 719 ++++++++++++++++++++++++-- doc/tools/docgram/orderedGrammar | 352 ++++++++++++- plugins/firstorder/g_ground.mlg | 11 +- 10 files changed, 1607 insertions(+), 328 deletions(-) diff --git a/Makefile.doc b/Makefile.doc index 473a70fb72..a5ff8e0123 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -248,8 +248,7 @@ $(DOC_GRAM): $(DOC_GRAMCMO) coqpp/coqpp_parser.mli coqpp/coqpp_parser.ml doc/too # user-contrib/*/*.mlg omitted for now (e.g. ltac2) PLUGIN_MLGS := $(wildcard plugins/*/*.mlg) -OMITTED_PLUGIN_MLGS := plugins/ssr/ssrparser.mlg plugins/ssr/ssrvernac.mlg plugins/ssrmatching/g_ssrmatching.mlg \ - plugins/ssrsearch/g_search.mlg +OMITTED_PLUGIN_MLGS := DOC_MLGS := $(wildcard */*.mlg) $(sort $(filter-out $(OMITTED_PLUGIN_MLGS), $(PLUGIN_MLGS))) \ user-contrib/Ltac2/g_ltac2.mlg DOC_EDIT_MLGS := $(wildcard doc/tools/docgram/*.edit_mlg) diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index d46dea1f5d..c93d621048 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -567,6 +567,19 @@ Dealing with fields intros x y H H1; field [H1]; auto. Abort. + +.. example:: :tacn:`field` that generates side goals + + .. coqtop:: reset all + + Require Import Reals. + Goal forall x y:R, + (x * y > 0)%R -> + (x * (1 / x + x / (x + y)))%R = + ((- 1 / y) * y * (- x * (x / (x + y)) - 1))%R. + + intros; field. + .. tacn:: field_simplify {? [ {+ @one_term__eq } ] } {+ @one_term } {? in @ident } Performs the simplification in the conclusion of the @@ -679,7 +692,7 @@ First Samuel Boutin designed the tactic ``ACDSimpl``. This tactic did lot of rewriting. But the proofs terms generated by rewriting were too big for Coq’s type checker. Let us see why: -.. coqtop:: all +.. coqtop:: reset all Require Import ZArith. Open Scope Z_scope. diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index e1f57c9bea..6464f085b8 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -60,7 +60,7 @@ The constructs in :token:`ltac_expr` are :term:`left associative`. ltac_expr3 ::= @l3_tactic | @ltac_expr2 ltac_expr2 ::= @ltac_expr1 + {| @ltac_expr2 | @binder_tactic } - | @ltac_expr1 || {| @ltac_expr2 | @binder_tactic } + | @ltac_expr1 %|| {| @ltac_expr2 | @binder_tactic } | @l2_tactic | @ltac_expr1 ltac_expr1 ::= @tactic_value @@ -729,7 +729,7 @@ First tactic to make progress: || Yet another way of branching without backtracking is the following structure: -.. tacn:: @ltac_expr1 || {| @ltac_expr2 | @binder_tactic } +.. tacn:: @ltac_expr1 %|| {| @ltac_expr2 | @binder_tactic } :name: || (first tactic making progress) :n:`@ltac_expr1 || @ltac_expr2` is @@ -1353,8 +1353,8 @@ Pattern matching on goals and hypotheses: match goal .. insertprodn goal_pattern match_hyp .. prodn:: - goal_pattern ::= {*, @match_hyp } |- @match_pattern - | [ {*, @match_hyp } |- @match_pattern ] + goal_pattern ::= {*, @match_hyp } %|- @match_pattern + | [ {*, @match_hyp } %|- @match_pattern ] | _ match_hyp ::= @name : @match_pattern | @name := @match_pattern diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 81c497d60a..a46f4fb894 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -562,7 +562,7 @@ Built-in quotations | ltac1 : ( @ltac1_expr_in_env ) | ltac1val : ( @ltac1_expr_in_env ) ltac1_expr_in_env ::= @ltac_expr - | {* @ident } |- @ltac_expr + | {* @ident } %|- @ltac_expr The current implementation recognizes the following built-in quotations: @@ -978,7 +978,7 @@ Match over goals .. prodn:: goal_match_list ::= {? %| } {+| @gmatch_rule } gmatch_rule ::= @gmatch_pattern => @ltac2_expr - gmatch_pattern ::= [ {*, @gmatch_hyp_pattern } |- @ltac2_match_pattern ] + gmatch_pattern ::= [ {*, @gmatch_hyp_pattern } %|- @ltac2_match_pattern ] gmatch_hyp_pattern ::= @name : @ltac2_match_pattern Matches over goals, similar to Ltac1 :tacn:`match goal`. @@ -1602,8 +1602,8 @@ Here is the syntax for the :n:`q_*` nonterminals: ltac2_clause ::= in @ltac2_in_clause | at @ltac2_occs_nums ltac2_in_clause ::= * {? @ltac2_occs } - | * |- {? @ltac2_concl_occ } - | {*, @ltac2_hypident_occ } {? |- {? @ltac2_concl_occ } } + | * %|- {? @ltac2_concl_occ } + | {*, @ltac2_hypident_occ } {? %|- {? @ltac2_concl_occ } } .. insertprodn q_occurrences ltac2_hypident diff --git a/doc/sphinx/proofs/automatic-tactics/logic.rst b/doc/sphinx/proofs/automatic-tactics/logic.rst index c4faa7284f..5aaded2726 100644 --- a/doc/sphinx/proofs/automatic-tactics/logic.rst +++ b/doc/sphinx/proofs/automatic-tactics/logic.rst @@ -5,7 +5,6 @@ Solvers for logic and equality ============================== .. tacn:: tauto - :name: tauto This tactic implements a decision procedure for intuitionistic propositional calculus based on the contraction-free sequent calculi LJT* of Roy Dyckhoff @@ -13,53 +12,58 @@ Solvers for logic and equality intuitionistic tautological proposition. :tacn:`tauto` unfolds negations and logical equivalence but does not unfold any other definition. -.. example:: + .. example:: + + The following goal can be proved by :tacn:`tauto` whereas :tacn:`auto` would + fail: - The following goal can be proved by :tacn:`tauto` whereas :tacn:`auto` would - fail: + .. coqtop:: reset all - .. coqtop:: reset all + Goal forall (x:nat) (P:nat -> Prop), x = 0 \/ P x -> x <> 0 -> P x. + intros. + tauto. - Goal forall (x:nat) (P:nat -> Prop), x = 0 \/ P x -> x <> 0 -> P x. - intros. - tauto. + Moreover, if it has nothing else to do, :tacn:`tauto` performs introductions. + Therefore, the use of :tacn:`intros` in the previous proof is unnecessary. + :tacn:`tauto` can for instance for: -Moreover, if it has nothing else to do, :tacn:`tauto` performs introductions. -Therefore, the use of :tacn:`intros` in the previous proof is unnecessary. -:tacn:`tauto` can for instance for: + .. example:: -.. example:: + .. coqtop:: reset all - .. coqtop:: reset all + Goal forall (A:Prop) (P:nat -> Prop), A \/ (forall x:nat, ~ A -> P x) -> forall x:nat, ~ A -> P x. + tauto. - Goal forall (A:Prop) (P:nat -> Prop), A \/ (forall x:nat, ~ A -> P x) -> forall x:nat, ~ A -> P x. - tauto. + .. note:: + In contrast, :tacn:`tauto` cannot solve the following goal + :g:`Goal forall (A:Prop) (P:nat -> Prop), A \/ (forall x:nat, ~ A -> P x) ->` + :g:`forall x:nat, ~ ~ (A \/ P x).` + because :g:`(forall x:nat, ~ A -> P x)` cannot be treated as atomic and + an instantiation of `x` is necessary. -.. note:: - In contrast, :tacn:`tauto` cannot solve the following goal - :g:`Goal forall (A:Prop) (P:nat -> Prop), A \/ (forall x:nat, ~ A -> P x) ->` - :g:`forall x:nat, ~ ~ (A \/ P x).` - because :g:`(forall x:nat, ~ A -> P x)` cannot be treated as atomic and - an instantiation of `x` is necessary. + .. tacn:: dtauto -.. tacv:: dtauto - :name: dtauto + While :tacn:`tauto` recognizes inductively defined connectives isomorphic to + the standard connectives ``and``, ``prod``, ``or``, ``sum``, ``False``, + ``Empty_set``, ``unit`` and ``True``, :tacn:`dtauto` also recognizes all inductive + types with one constructor and no indices, i.e. record-style connectives. - While :tacn:`tauto` recognizes inductively defined connectives isomorphic to - the standard connectives ``and``, ``prod``, ``or``, ``sum``, ``False``, - ``Empty_set``, ``unit``, ``True``, :tacn:`dtauto` also recognizes all inductive - types with one constructor and no indices, i.e. record-style connectives. +.. todo would be nice to explain/discuss the various types of flags + that define the differences between these tactics. See Tauto.v/tauto.ml. -.. tacn:: intuition @tactic - :name: intuition +.. tacn:: intuition {? @ltac_expr } - The tactic :tacn:`intuition` takes advantage of the search-tree built by the - decision procedure involved in the tactic :tacn:`tauto`. It uses this - information to generate a set of subgoals equivalent to the original one (but - simpler than it) and applies the tactic :n:`@tactic` to them :cite:`Mun94`. If - this tactic fails on some goals then :tacn:`intuition` fails. In fact, + Uses the search tree built by the decision procedure for :tacn:`tauto` + to generate a set of subgoals equivalent to the original one (but + simpler than it) and applies :n:`@ltac_expr` to them :cite:`Mun94`. If + :n:`@ltac_expr` is not specified, it defaults to :n:`auto with *` + If :n:`@ltac_expr` fails on some goals then :tacn:`intuition` fails. In fact, :tacn:`tauto` is simply :g:`intuition fail`. + :tacn:`intuition` recognizes inductively defined connectives + isomorphic to the standard connectives ``and``, ``prod``, ``or``, ``sum``, ``False``, + ``Empty_set``, ``unit`` and ``True``. + .. example:: For instance, the tactic :g:`intuition auto` applied to the goal:: @@ -72,98 +76,76 @@ Therefore, the use of :tacn:`intros` in the previous proof is unnecessary. and then uses :tacn:`auto` which completes the proof. -Originally due to César Muñoz, these tactics (:tacn:`tauto` and -:tacn:`intuition`) have been completely re-engineered by David Delahaye using -mainly the tactic language (see :ref:`ltac`). The code is -now much shorter and a significant increase in performance has been noticed. -The general behavior with respect to dependent types, unfolding and -introductions has slightly changed to get clearer semantics. This may lead to -some incompatibilities. + .. tacn:: dintuition {? @ltac_expr } -.. tacv:: intuition - - Is equivalent to :g:`intuition auto with *`. - -.. tacv:: dintuition - :name: dintuition - - While :tacn:`intuition` recognizes inductively defined connectives - isomorphic to the standard connectives ``and``, ``prod``, ``or``, ``sum``, ``False``, - ``Empty_set``, ``unit``, ``True``, :tacn:`dintuition` also recognizes all inductive - types with one constructor and no indices, i.e. record-style connectives. + In addition to the inductively defined connectives recognized by :tacn:`intuition`, + :tacn:`dintuition` also recognizes all inductive + types with one constructor and no indices, i.e. record-style connectives. -.. flag:: Intuition Negation Unfolding + .. flag:: Intuition Negation Unfolding - Controls whether :tacn:`intuition` unfolds inner negations which do not need - to be unfolded. This flag is on by default. + Controls whether :tacn:`intuition` unfolds inner negations which do not need + to be unfolded. The flag is on by default. .. tacn:: rtauto - :name: rtauto - The :tacn:`rtauto` tactic solves propositional tautologies similarly to what - :tacn:`tauto` does. The main difference is that the proof term is built using a + Solves propositional tautologies similarly to + :tacn:`tauto`, but the proof term is built using a reflection scheme applied to a sequent calculus proof of the goal. The search procedure is also implemented using a different technique. - Users should be aware that this difference may result in faster proof-search - but slower proof-checking, and :tacn:`rtauto` might not solve goals that + Users should be aware that this difference may result in faster proof search + but slower proof checking, and :tacn:`rtauto` might not solve goals that :tacn:`tauto` would be able to solve (e.g. goals involving universal quantifiers). Note that this tactic is only available after a ``Require Import Rtauto``. -.. tacn:: firstorder - :name: firstorder +.. tacn:: firstorder {? @ltac_expr } {? using {+, @qualid } } {? with {+ @ident } } - The tactic :tacn:`firstorder` is an experimental extension of :tacn:`tauto` to - first- order reasoning, written by Pierre Corbineau. It is not restricted to - usual logical connectives but instead may reason about any first-order class + An experimental extension of :tacn:`tauto` to + first-order reasoning. It is not restricted to + usual logical connectives but instead can reason about any first-order class inductive definition. -.. opt:: Firstorder Solver @tactic - :name: Firstorder Solver - - The default tactic used by :tacn:`firstorder` when no rule applies is - :g:`auto with core`, it can be reset locally or globally using this option. - - .. cmd:: Print Firstorder Solver - - Prints the default tactic used by :tacn:`firstorder` when no rule applies. - -.. tacv:: firstorder @tactic - - Tries to solve the goal with :n:`@tactic` when no logical rule may apply. - -.. tacv:: firstorder using {+ @qualid} + :token:`ltac_expr` + Tries to solve the goal with :token:`ltac_expr` when no logical rule applies. + If unspecified, the tactic uses the default from the :opt:`Firstorder Solver` + option. - .. deprecated:: 8.3 + :n:`using {+, @qualid }` + Adds the lemmas :n:`{+, @qualid }` to the proof search environment. If :n:`@qualid` + refers to an inductive type, its constructors are + added to the proof search environment. - Use the syntax below instead (with commas). + :n:`with {+ @ident }` + Adds lemmas from :tacn:`auto` hint bases :n:`{+ @ident }` to the proof search + environment. -.. tacv:: firstorder using {+, @qualid} + .. opt:: Firstorder Solver @ltac_expr - Adds lemmas :n:`{+, @qualid}` to the proof-search environment. If :n:`@qualid` - refers to an inductive type, it is the collection of its constructors which are - added to the proof-search environment. + The default tactic used by :tacn:`firstorder` when no rule applies in + :g:`auto with core`. It can be set locally or globally using this option. -.. tacv:: firstorder with {+ @ident} + .. cmd:: Print Firstorder Solver - Adds lemmas from :tacn:`auto` hint bases :n:`{+ @ident}` to the proof-search - environment. + Prints the default tactic used by :tacn:`firstorder` when no rule applies. -.. tacv:: firstorder @tactic using {+, @qualid} with {+ @ident} + .. opt:: Firstorder Depth @natural - This combines the effects of the different variants of :tacn:`firstorder`. + Controls the proof search depth bound. -.. opt:: Firstorder Depth @natural - :name: Firstorder Depth +.. tacn:: congruence {? @natural } {? with {+ @one_term } } - This option controls the proof-search depth bound. + :token:`natural` + Specifies the maximum number of hypotheses stating quantified equalities that may be added + to the problem in order to solve it. The default is 1000. -.. tacn:: congruence - :name: congruence + :n:`{? with {+ @one_term } }` + Adds :n:`{+ @one_term }` to the pool of terms used by :tacn:`congruence`. This helps + in case you have partially applied constructors in your goal. - The tactic :tacn:`congruence`, by Pierre Corbineau, implements the standard + Implements the standard Nelson and Oppen congruence closure algorithm, which is a decision procedure for ground equalities with uninterpreted symbols. It also includes constructor theory (see :tacn:`injection` and :tacn:`discriminate`). If the goal @@ -178,53 +160,45 @@ some incompatibilities. equality must contain all the quantified variables in order for congruence to match against it. -.. example:: - - .. coqtop:: reset all - - Theorem T (A:Type) (f:A -> A) (g: A -> A -> A) a b: a=(f a) -> (g b (f a))=(f (f a)) -> (g a b)=(f (g b a)) -> (g a b)=a. - intros. - congruence. - Qed. - - Theorem inj (A:Type) (f:A -> A * A) (a c d: A) : f = pair a -> Some (f c) = Some (f d) -> c=d. - intros. - congruence. - Qed. + Increasing the maximum number of hypotheses may solve + problems that would have failed with a smaller value. It will make failures slower but it + won't make successes found with the smaller value any slower. + You may want to use :tacn:`assert` to add some lemmas as + hypotheses so that :tacn:`congruence` can use them. -.. tacv:: congruence @natural + .. example:: - Tries to add at most :token:`natural` instances of hypotheses stating quantified equalities - to the problem in order to solve it. A bigger value of :token:`natural` does not make - success slower, only failure. You might consider adding some lemmas as - hypotheses using assert in order for :tacn:`congruence` to use them. + .. coqtop:: reset all -.. tacv:: congruence with {+ @term} - :name: congruence with + Theorem T (A:Type) (f:A -> A) (g: A -> A -> A) a b: a=(f a) -> (g b (f a))=(f (f a)) -> (g a b)=(f (g b a)) -> (g a b)=a. + intros. + congruence. + Qed. - Adds :n:`{+ @term}` to the pool of terms used by :tacn:`congruence`. This helps - in case you have partially applied constructors in your goal. + Theorem inj (A:Type) (f:A -> A * A) (a c d: A) : f = pair a -> Some (f c) = Some (f d) -> c=d. + intros. + congruence. + Qed. -.. exn:: I don’t know how to handle dependent equality. + .. exn:: I don’t know how to handle dependent equality. - The decision procedure managed to find a proof of the goal or of a - discriminable equality but this proof could not be built in Coq because of - dependently-typed functions. + The decision procedure managed to find a proof of the goal or of a + discriminable equality but this proof could not be built in Coq because of + dependently-typed functions. -.. exn:: Goal is solvable by congruence but some arguments are missing. Try congruence with {+ @term}, replacing metavariables by arbitrary terms. + .. exn:: Goal is solvable by congruence but some arguments are missing. Try congruence with {+ @term}, replacing metavariables by arbitrary terms. - The decision procedure could solve the goal with the provision that additional - arguments are supplied for some partially applied constructors. Any term of an - appropriate type will allow the tactic to successfully solve the goal. Those - additional arguments can be given to congruence by filling in the holes in the - terms given in the error message, using the :tacn:`congruence with` variant described above. + The decision procedure could solve the goal with the provision that additional + arguments are supplied for some partially applied constructors. Any term of an + appropriate type will allow the tactic to successfully solve the goal. Those + additional arguments can be given to congruence by filling in the holes in the + terms given in the error message, using the `with` clause. -.. flag:: Congruence Verbose + .. flag:: Congruence Verbose - This flag makes :tacn:`congruence` print debug information. + Makes :tacn:`congruence` print debug information. .. tacn:: btauto - :name: btauto The tactic :tacn:`btauto` implements a reflexive solver for boolean tautologies. It solves goals of the form :g:`t = u` where `t` and `u` are @@ -252,43 +226,3 @@ some incompatibilities. The goal is not of the form :g:`t = u`. Especially note that :tacn:`btauto` doesn't introduce variables into the context on its own. - -.. tacv:: field - field_simplify {* @term} - field_simplify_eq - - The field tactic is built on the same ideas as ring: this is a - reflexive tactic that solves or simplifies equations in a field - structure. The main idea is to reduce a field expression (which is an - extension of ring expressions with the inverse and division - operations) to a fraction made of two polynomial expressions. - - Tactic :n:`field` is used to solve subgoals, whereas :n:`field_simplify {+ @term}` - replaces the provided terms by their reduced fraction. - :n:`field_simplify_eq` applies when the conclusion is an equation: it - simplifies both hand sides and multiplies so as to cancel - denominators. So it produces an equation without division nor inverse. - - All of these 3 tactics may generate a subgoal in order to prove that - denominators are different from zero. - - See :ref:`Theringandfieldtacticfamilies` for more information on the tactic and how to - declare new field structures. All declared field structures can be - printed with the Print Fields command. - -.. example:: - - .. coqtop:: reset all - - Require Import Reals. - Goal forall x y:R, - (x * y > 0)%R -> - (x * (1 / x + x / (x + y)))%R = - ((- 1 / y) * y * (- x * (x / (x + y)) - 1))%R. - - intros; field. - -.. seealso:: - - File plugins/ring/RealField.v for an example of instantiation, - theory theories/Reals for many examples of use of field. diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 76a41828f7..4ad32e15eb 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -19,7 +19,8 @@ lglob: [ ] hint: [ -| "Extern" natural OPT constr_pattern "=>" tactic +| REPLACE "Extern" natural OPT Constr.constr_pattern "=>" Pltac.tactic +| WITH "Extern" natural OPT constr_pattern "=>" tactic ] (* todo: does ARGUMENT EXTEND make the symbol global? It is in both extraargs and extratactics *) @@ -28,19 +29,12 @@ strategy_level_or_var: [ | strategy_level ] -term0: [ -| "ltac" ":" "(" ltac_expr5 ")" -] - EXTRAARGS_natural: [ | DELETENT ] EXTRAARGS_lconstr: [ | DELETENT ] EXTRAARGS_strategy_level: [ | DELETENT ] -G_LTAC_hint: [ | DELETENT ] -G_LTAC_term0: [ | DELETENT ] -G_REWRITE_binders: [ +binders: [ | DELETE Pcoq.Constr.binders -| binders ] G_TACTIC_in_clause: [ @@ -50,7 +44,6 @@ G_TACTIC_in_clause: [ ] SPLICE: [ -| G_REWRITE_binders | G_TACTIC_in_clause ] @@ -92,6 +85,7 @@ RENAME: [ | G_LTAC2_as_ipat ltac2_as_ipat | G_LTAC2_by_tactic ltac2_by_tactic | G_LTAC2_match_list ltac2_match_list +| G_SSRMATCHING_cpattern ssr_one_term_pattern ] (* Renames to eliminate qualified names. @@ -112,13 +106,14 @@ RENAME: [ | Prim.natural natural | Pvernac.Vernac_.main_entry vernac_control | Tactic.tactic tactic +| Pltac.ltac_expr ltac_expr5 (* SSR *) +| Pcoq.Constr.constr term +| Prim.identref ident (* | G_vernac.def_body def_body -| Pcoq.Constr.constr term | Prim.by_notation by_notation -| Prim.identref ident | Prim.natural natural *) | Vernac.fix_definition fix_definition @@ -156,11 +151,16 @@ DELETE: [ | test_array_closing (* SSR *) -(* | ssr_null_entry *) -(* +| ssr_null_entry | ssrtermkind (* todo: rename as "test..." *) -| term_annotation (* todo: rename as "test..." *) +| ssrdoarg (* todo: this and the next one should be removed from the grammar? *) +| ssrseqdir +| ssrindex +| ssrintrosarg +| ssrtclarg +| term_annotation (* todo: what is this? *) | test_idcomma +| test_ident_no_do | test_nohidden | test_not_ssrslashnum | test_ssr_rw_syntax @@ -171,10 +171,6 @@ DELETE: [ | test_ssrslashnum01 | test_ssrslashnum10 | test_ssrslashnum11 -| test_ident_no_do -| ssrdoarg (* todo: this and the next one should be removed from the grammar? *) -| ssrseqdir -*) (* unused *) | constr_comma_sequence' @@ -182,8 +178,6 @@ DELETE: [ | constr_may_eval ] -(* ssrintrosarg: [ | DELETENT ] *) - (* additional nts to be spliced *) tactic_then_last: [ @@ -262,7 +256,18 @@ binder_constr: [ | MOVETO term_forall_or_fun "forall" open_binders "," term200 | MOVETO term_forall_or_fun "fun" open_binders "=>" term200 | MOVETO term_let "let" name binders let_type_cstr ":=" term200 "in" term200 +(*| MOVETO term_let "let" ":" ssr_mpat ":=" lconstr "in" lconstr TAG SSR *) +| DELETE "let" ":" ssr_mpat ":=" lconstr "in" lconstr TAG SSR (* todo: restore for ssr *) +| REPLACE "let" ":" ssr_mpat "in" pattern200 ":=" lconstr ssr_rtype "in" lconstr (* ssr plugin *) +| WITH "let" ":" ssr_mpat OPT ( "in" pattern200 ) ":=" lconstr ssr_rtype "in" lconstr TAG SSR +| DELETE "let" ":" ssr_mpat ":=" lconstr ssr_rtype "in" lconstr (* SSR plugin *) +| DELETE "let" ":" ssr_mpat OPT ( "in" pattern200 ) ":=" lconstr ssr_rtype "in" lconstr TAG SSR (* todo: restore for SSR *) +(*| MOVETO term_let "let" ":" ssr_mpat OPT ( "in" pattern200 ) ":=" lconstr ssr_rtype "in" lconstr TAG SSR*) | MOVETO term_if "if" term200 as_return_type "then" term200 "else" term200 +| REPLACE "if" term200 "is" ssr_dthen ssr_else +| WITH "if" term200 [ "is" | "isn't" ] ssr_dthen ssr_else TAG SSR +| DELETE "if" term200 "isn't" ssr_dthen ssr_else +| DELETE "if" term200 [ "is" | "isn't" ] ssr_dthen ssr_else TAG SSR (* todo: restore for SSR *) | MOVETO term_fix "let" "fix" fix_decl "in" term200 | MOVETO term_cofix "let" "cofix" cofix_body "in" term200 | MOVETO term_let "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" term200 "in" term200 @@ -302,6 +307,7 @@ atomic_constr: [ ltac_expr0: [ | REPLACE "[" ">" for_each_goal "]" | WITH "[>" for_each_goal "]" +| DELETE ssrparentacarg ] (* lexer token *) @@ -465,6 +471,7 @@ closed_binder: [ | MOVETO generalizing_binder "`(" LIST1 typeclass_constraint SEP "," ")" | MOVETO generalizing_binder "`{" LIST1 typeclass_constraint SEP "," "}" | MOVETO generalizing_binder "`[" LIST1 typeclass_constraint SEP "," "]" +| DELETE [ "of" | "&" ] term99 (* todo: remove for SSR *) ] name_colon: [ @@ -565,10 +572,6 @@ finite_token: [ | DELETENT ] -constructors_or_record: [ -| OPTINREF -] - record_fields: [ | REPLACE record_field ";" record_fields | WITH LIST0 record_field SEP ";" OPT ";" @@ -584,11 +587,6 @@ inline: [ | REPLACE "Inline" "(" natural ")" | WITH "Inline" OPT ( "(" natural ")" ) | DELETE "Inline" -| OPTINREF -] - -univ_annot: [ -| OPTINREF ] univ_decl: [ @@ -604,10 +602,6 @@ of_type: [ | [ ":" | ":>" ] type ] -attr_value: [ -| OPTINREF -] - def_body: [ | DELETE binders ":=" reduce lconstr | REPLACE binders ":" lconstr ":=" reduce lconstr @@ -749,6 +743,7 @@ subsequent_letter: [ ident: [ | DELETE IDENT +| DELETE IDENT (* 2nd copy from SSR *) | first_letter LIST0 subsequent_letter ] @@ -804,6 +799,10 @@ ltac_expr4: [ | REPLACE ltac_expr3 ";" binder_tactic | WITH ltac_expr3 ";" [ ltac_expr3 | binder_tactic ] | DELETE ltac_expr3 ";" ltac_expr3 +| MOVETO simple_tactic ltac_expr5 ";" "first" ssr_first_else TAG SSR +| MOVETO simple_tactic ltac_expr5 ";" "first" ssrseqarg TAG SSR +| MOVETO simple_tactic ltac_expr5 ";" "last" ssrseqarg TAG SSR +| DELETE simple_tactic ] l3_tactic: [ ] @@ -813,6 +812,7 @@ ltac_expr3: [ | REPLACE "abstract" ltac_expr2 "using" ident | WITH "abstract" ltac_expr2 OPT ( "using" ident ) | l3_tactic +| EDIT "do" ADD_OPT int_or_var ssrmmod ssrdotac ssrclauses TAG SSR | MOVEALLBUT ltac_builtins | l3_tactic | ltac_expr2 @@ -1069,6 +1069,43 @@ simple_tactic: [ (* in Tactic Notation: *) | "setoid_replace" constr "with" constr OPT ( "using" "relation" constr ) OPT ( "in" hyp ) OPT ( "at" LIST1 int_or_var ) OPT ( "by" ltac_expr3 ) +| REPLACE "apply" ssrapplyarg (* SSR plugin *) +| WITH "apply" OPT ssrapplyarg TAG SSR +| DELETE "apply" +| REPLACE "elim" ssrarg ssrclauses (* SSR plugin *) +| WITH "elim" OPT ( ssrarg ssrclauses ) TAG SSR +| DELETE "elim" (* SSR plugin *) +| REPLACE "case" ssrcasearg ssrclauses (* SSR plugin *) +| WITH "case" OPT ( ssrcasearg ssrclauses ) TAG SSR +| DELETE "case" (* SSR plugin *) +| REPLACE "under" ssrrwarg ssrintros_ne "do" ssrhint3arg (* SSR plugin *) +| WITH "under" ssrrwarg OPT ssrintros_ne OPT ( "do" ssrhint3arg ) TAG SSR +| DELETE "under" ssrrwarg (* SSR plugin *) +| DELETE "under" ssrrwarg ssrintros_ne (* SSR plugin *) +| DELETE "under" ssrrwarg "do" ssrhint3arg (* SSR plugin *) +| REPLACE "move" ssrmovearg ssrrpat (* SSR plugin *) +| WITH "move" OPT ( OPT ssrmovearg ssrrpat ) TAG SSR +| DELETE "move" ssrrpat (* SSR plugin *) +| DELETE "move" (* SSR plugin *) +| REPLACE "suff" "have" ssrhpats_nobs ssrhavefwd (* SSR plugin *) +| WITH [ "suff" | "suffices" ] OPT ( "have" ssrhpats_nobs ) ssrhavefwd TAG SSR +| DELETE "suffices" "have" ssrhpats_nobs ssrhavefwd (* SSR plugin *) +| REPLACE "suff" ssrsufffwd (* SSR plugin *) +| WITH [ "suff" | "suffices" ] ssrsufffwd TAG SSR +| DELETE "suffices" ssrsufffwd (* SSR plugin *) +| REPLACE "have" "suff" ssrhpats_nobs ssrhavefwd (* SSR plugin *) +| WITH "have" [ "suff" | "suffices" ] ssrhpats_nobs ssrhavefwd TAG SSR +| DELETE "have" "suffices" ssrhpats_nobs ssrhavefwd (* SSR plugin *) +| REPLACE "gen" "have" ssrclear ssr_idcomma ssrhpats_nobs ssrwlogfwd ssrhint (* SSR plugin *) +| WITH [ "gen" | "generally" ] "have" ssrclear ssr_idcomma ssrhpats_nobs ssrwlogfwd ssrhint TAG SSR +| DELETE "generally" "have" ssrclear ssr_idcomma ssrhpats_nobs ssrwlogfwd ssrhint (* SSR plugin *) +| REPLACE "wlog" "suff" ssrhpats_nobs ssrwlogfwd ssrhint (* SSR plugin *) +| WITH [ "wlog" | "without loss" ] OPT [ "suff" | "suffices" ] ssrhpats_nobs ssrwlogfwd ssrhint TAG SSR +| DELETE "wlog" "suffices" ssrhpats_nobs ssrwlogfwd ssrhint (* SSR plugin *) +| DELETE "wlog" ssrhpats_nobs ssrwlogfwd ssrhint (* SSR plugin *) +| DELETE "without" "loss" ssrhpats_nobs ssrwlogfwd ssrhint (* SSR plugin *) +| DELETE "without" "loss" "suff" ssrhpats_nobs ssrwlogfwd ssrhint (* SSR plugin *) +| DELETE "without" "loss" "suffices" ssrhpats_nobs ssrwlogfwd ssrhint (* SSR plugin *) ] (* todo: don't use DELETENT for this *) @@ -1730,6 +1767,7 @@ ltac_defined_tactics: [ | "lra" | "nia" | "nra" +| "over" TAG SSR | "split_Rabs" | "split_Rmult" | "tauto" @@ -1741,10 +1779,12 @@ ltac_defined_tactics: [ tactic_notation_tactics: [ | "assert_fails" ltac_expr3 | "assert_succeeds" ltac_expr3 +| "dintuition" OPT ltac_expr5 +| "dtauto" | "field" OPT ( "[" LIST1 constr "]" ) | "field_simplify" OPT ( "[" LIST1 constr "]" ) LIST1 constr OPT ( "in" ident ) | "field_simplify_eq" OPT ( "[" LIST1 constr "]" ) OPT ( "in" ident ) -| "intuition" OPT ltac_expr5 +| "intuition" OPT ltac_expr5 (* todo: Not too keen on things like "with_power_flags" in tauto.ml, not easy to follow *) | "nsatz" OPT ( "with" "radicalmax" ":=" constr "strategy" ":=" constr "parameters" ":=" constr "variables" ":=" constr ) | "psatz" constr OPT int_or_var | "ring" OPT ( "[" LIST1 constr "]" ) @@ -1860,18 +1900,6 @@ SPLICE: [ | ltac2_orient ] -tac2typ_prm: [ -| OPTINREF -] - -tac2type_body: [ -| OPTINREF -] - -atomic_tac2pat: [ -| OPTINREF -] - ltac2_expr0: [ (* | DELETE "(" ")" (* covered by "()" prodn *) @@ -1964,7 +1992,7 @@ SPLICE: [ ltac2_expr5: [ | REPLACE "let" OPT "rec" LIST1 ltac2_let_clause SEP "with" "in" ltac2_expr6 (* Ltac2 plugin *) | WITH "let" OPT "rec" ltac2_let_clause LIST0 ( "with" ltac2_let_clause ) "in" ltac2_expr6 TAG Ltac2 -| MOVETO simple_tactic "match" ltac2_expr5 "with" OPT ltac2_branches "end" (* Ltac2 plugin *) +| MOVETO simple_tactic "match" ltac2_expr5 "with" ltac2_branches "end" (* Ltac2 plugin *) | MOVETO simple_tactic "if" ltac2_expr5 "then" ltac2_expr5 "else" ltac2_expr5 (* Ltac2 plugin *) | DELETE simple_tactic ] @@ -2042,6 +2070,322 @@ ltac2_expr: [ | DELETE _ltac2_expr ] +ssrfwdview: [ +| REPLACE "/" ast_closure_term ssrfwdview (* SSR plugin *) +| WITH LIST1 ( "/" ast_closure_term ) TAG SSR +| DELETE "/" ast_closure_term (* SSR plugin *) +] + +ssrfwd: [ +| REPLACE ":" ast_closure_lterm ":=" ast_closure_lterm (* SSR plugin *) +| WITH OPT ( ":" ast_closure_lterm ) ":=" ast_closure_lterm TAG SSR +| DELETE ":=" ast_closure_lterm (* SSR plugin *) +] + +ssrsetfwd: [ +| REPLACE ":" ast_closure_lterm ":=" "{" ssrocc "}" cpattern (* SSR plugin *) +| WITH OPT ( ":" ast_closure_lterm ) ":=" [ "{" ssrocc "}" cpattern | lcpattern ] TAG SSR +| DELETE ":" ast_closure_lterm ":=" lcpattern (* SSR plugin *) +| DELETE ":=" "{" ssrocc "}" cpattern (* SSR plugin *) +| DELETE ":=" lcpattern (* SSR plugin *) +] + + +(* per @gares *) +ssrdgens: [ +| REPLACE ":" ssrgen ssrdgens_tl (* SSR plugin *) +| WITH ":" ssrgen OPT ( "/" ssrgen ) TAG SSR +] + +ssrdgens_tl: [ | DELETENT ] + +ssrgen: [ +| REPLACE ssrdocc cpattern (* SSR plugin *) +| WITH cpattern LIST0 [ LIST1 ident | cpattern ] TAG SSR +| DELETE cpattern (* SSR plugin *) +] + +OPTINREF: [ ] + +ssrortacs: [ +| EDIT ssrtacarg "|" ADD_OPT ssrortacs (* ssr plugin *) +| EDIT "|" ADD_OPT ssrortacs (* ssr plugin *) +| EDIT ADD_OPT ssrtacarg "|" OPT ssrortacs +] + +ssrocc: [ +| REPLACE natural LIST0 natural (* SSR plugin *) +| WITH [ natural | "+" | "-" ] LIST0 natural TAG SSR +| DELETE "-" LIST0 natural (* SSR plugin *) +| DELETE "+" LIST0 natural (* SSR plugin *) +] + +ssripat: [ +| DELETE ssrdocc "->" (* SSR plugin *) +| DELETE ssrdocc "<-" (* SSR plugin *) +| REPLACE ssrdocc (* SSR plugin *) +| WITH ssrdocc OPT [ "->" | "<-" ] TAG SSR +| DELETE "->" (* SSR plugin *) +| DELETE "<-" (* SSR plugin *) +| DELETE "-/" "=" (* SSR plugin *) +| DELETE "-/" "/" (* SSR plugin *) +| DELETE "-/" integer "/" (* SSR plugin *) +| DELETE "-/" integer "/=" (* SSR plugin *) +| REPLACE "-/" integer "/" integer "=" (* SSR plugin *) +| WITH "-/" integer [ "/=" | "/" | "/" integer "=" ] TAG SSR +| DELETE "-/" "/=" (* SSR plugin *) +| DELETE "-//" "=" (* SSR plugin *) +| DELETE "[" ":" LIST0 ident "]" (* SSR plugin *) +] + +ssrsimpl_ne: [ +| DELETE "/" natural "/" "=" (* SSR plugin *) +(* parsed but not supported per @gares *) +| DELETE "/" natural "/" (* SSR plugin *) +| DELETE "/" natural "=" (* SSR plugin *) +| DELETE "//" natural "=" (* SSR plugin *) +] + +hat: [ +| DELETE "^" "~" ident (* SSR plugin *) +| DELETE "^" "~" natural (* SSR plugin *) +] + +ssriorpat: [ +| ssripats OPT ( [ "|" | "|-" ] ssriorpat ) TAG SSR +| DELETE OPT ssripats "|" ssriorpat (* SSR plugin *) +| DELETE OPT ssripats "|-" ">" ssriorpat (* SSR plugin *) +| DELETE OPT ssripats "|-" ssriorpat (* SSR plugin *) +(* "|->" | "||" | "|||" | "||||" are parsing hacks *) +| DELETE OPT ssripats "|->" ssriorpat (* SSR plugin *) +| DELETE OPT ssripats "||" ssriorpat (* SSR plugin *) +| DELETE OPT ssripats "|||" ssriorpat (* SSR plugin *) +| DELETE OPT ssripats "||||" ssriorpat (* SSR plugin *) +| DELETE OPT ssripats (* SSR plugin *) +] + +ssrbinder: [ +| REPLACE "(" ssrbvar LIST1 ssrbvar ":" lconstr ")" (* SSR plugin *) +| WITH "(" LIST1 ssrbvar ":" lconstr ")" TAG SSR +| REPLACE "(" ssrbvar ":" lconstr ":=" lconstr ")" (* SSR plugin *) +| WITH "(" ssrbvar OPT ( ":" lconstr ) OPT ( ":=" lconstr ) ")" TAG SSR +| DELETE "(" ssrbvar ")" (* SSR plugin *) +| DELETE "(" ssrbvar ":" lconstr ")" (* SSR plugin *) +| DELETE "(" ssrbvar ":=" lconstr ")" (* SSR plugin *) +] + +ssrhavefwd: [ +| REPLACE ":" ast_closure_lterm ":=" ast_closure_lterm (* SSR plugin *) +| WITH ":" ast_closure_lterm ":=" OPT ast_closure_lterm TAG SSR +| DELETE ":" ast_closure_lterm ":=" (* SSR plugin *) +| DELETE ":=" ast_closure_lterm (* SSR plugin *) +] + +ssrmult_ne: [ +| EDIT ADD_OPT natural ssrmmod TAG SSR +] + +rpattern: [ +| REPLACE lconstr "in" lconstr "in" lconstr (* SSR plugin *) +| WITH OPT ( OPT ( OPT ( OPT lconstr "in" ) lconstr ) "in" ) lconstr TAG SSR +| DELETE lconstr (* SSR plugin *) +| DELETE "in" lconstr (* SSR plugin *) +| DELETE lconstr "in" lconstr (* SSR plugin *) +| DELETE "in" lconstr "in" lconstr (* SSR plugin *) +] + +ssrrule_ne: [ +| DELETE ssrsimpl_ne (* SSR plugin *) +| REPLACE [ "/" ssrterm | ssrterm | ssrsimpl_ne ] (* SSR plugin *) +| WITH [ OPT "/" ssrterm | ssrsimpl_ne ] TAG SSR +] + +ssrunlockarg: [ +| REPLACE "{" ssrocc "}" ssrterm (* SSR plugin *) +| WITH OPT ( "{" ssrocc "}" ) ssrterm TAG SSR +| DELETE ssrterm (* SSR plugin *) +] + +ssrclauses: [ +| REPLACE "in" ssrclausehyps "|-" "*" (* SSR plugin *) +| WITH "in" ssrclausehyps OPT "|-" OPT "*" TAG SSR +| DELETE "in" ssrclausehyps "|-" (* SSR plugin *) +| DELETE "in" ssrclausehyps "*" (* SSR plugin *) +| DELETE "in" ssrclausehyps (* SSR plugin *) +| REPLACE "in" "|-" "*" (* SSR plugin *) +| WITH "in" [ "*" | "*" "|-" | "|-" "*" ] TAG SSR +| DELETE "in" "*" (* SSR plugin *) +| DELETE "in" "*" "|-" (* SSR plugin *) +] + +ssrclausehyps: [ +| REPLACE ssrwgen "," ssrclausehyps (* SSR plugin *) +| WITH ssrwgen LIST0 ( OPT "," ssrwgen ) TAG SSR +| DELETE ssrwgen ssrclausehyps (* SSR plugin *) +| DELETE ssrwgen (* SSR plugin *) +] + +ssrwgen: [ +| DELETE ssrhoi_hyp (* SSR plugin *) +| REPLACE "@" ssrhoi_hyp (* SSR plugin *) +| WITH OPT "@" ssrhoi_hyp TAG SSR +| REPLACE "(" ssrhoi_id ":=" lcpattern ")" (* SSR plugin *) +| WITH "(" ssrhoi_id OPT ( ":=" lcpattern ) ")" TAG SSR +| DELETE "(" ssrhoi_id ")" (* SSR plugin *) +| DELETE "(" "@" ssrhoi_id ":=" lcpattern ")" (* SSR plugin *) +] + +ssrcongrarg: [ +| REPLACE natural constr ssrdgens (* SSR plugin *) +| WITH OPT natural constr OPT ssrdgens TAG SSR +| DELETE natural constr (* SSR plugin *) +| DELETE constr ssrdgens (* SSR plugin *) +| DELETE constr (* SSR plugin *) +] + +ssrviewpos: [ +| DELETE "for" "apply" "/" "/" (* SSR plugin *) +] + +ssrhintref: [ +| REPLACE constr "|" natural (* SSR plugin *) +| WITH constr OPT ( "|" natural ) TAG SSR +| DELETE constr (* SSR plugin *) +] + +ssr_search_arg: [ +| REPLACE "-" ssr_search_item OPT ssr_search_arg (* SSR plugin *) +| WITH LIST1 ( "-" ssr_search_item ) TAG SSR +| DELETE ssr_search_item OPT ssr_search_arg (* SSR plugin *) +] + +ssr_search_item: [ +| DELETE string (* SSR plugin *) +| REPLACE string "%" preident (* SSR plugin *) +| WITH string OPT ( "%" preident ) TAG SSR +] + +modloc: [ +| REPLACE "-" global (* SSR plugin *) +| WITH OPT "-" global TAG SSR +| DELETE global +] + +ssrmmod: [ +| DELETE LEFTQMARK (* SSR plugin *) (* duplicate *) +] + +clear_switch: [ +| "{" LIST0 ident "}" +] + +ssrrwocc: [ +| REPLACE "{" LIST0 ssrhyp "}" (* SSR plugin *) +| WITH clear_switch +] + +ssrrwarg: [ +| EDIT "{" ADD_OPT ssrocc "}" OPT ssrpattern_squarep ssrrule_ne TAG SSR +| REPLACE "{" LIST1 ssrhyp "}" ssrpattern_ne_squarep ssrrule_ne (* SSR plugin *) +| WITH OPT ( OPT ( "{" LIST1 ssrhyp "}" ) ssrpattern_ne_squarep ) ssrrule_ne TAG SSR +| DELETE ssrpattern_ne_squarep ssrrule_ne (* SSR plugin *) +| DELETE ssrrule_ne (* SSR plugin *) +] + +ssrpattern_squarep: [ (* fix inconsistency *) +| REPLACE "[" rpattern "]" (* SSR plugin *) +| WITH ssrpattern_ne_squarep TAG SSR +] + +ssripats_ne: [ +| REPLACE ssripat OPT ssripats (* SSR plugin *) +| WITH LIST1 ssripat TAG SSR +] + +ssripats: [ (* fix inconsistency *) +| REPLACE ssripat OPT ssripats (* SSR plugin *) +| WITH ssripats_ne TAG SSR +] + +lcpattern: [ +(* per @gares *) +| DELETE "Qed" lconstr +] + +ssrapplyarg: [ +| EDIT ADD_OPT ssrbwdview ":" ssragen OPT ssragens OPT ssrintros TAG SSR +] + +constr_with_bindings_arg: [ +| EDIT ADD_OPT ">" constr_with_bindings TAG SSR +] + +destruction_arg: [ +| DELETE constr_with_bindings +] + +ssrhintarg: [ +| EDIT "[" ADD_OPT ssrortacs "]" TAG SSR +] + + +ssrhint3arg: [ +| EDIT "[" ADD_OPT ssrortacs "]" TAG SSR +] + + +ssr_first: [ +| DELETE ssr_first ssrintros_ne (* SSR plugin *) +| REPLACE "[" LIST0 ltac_expr5 SEP "|" "]" (* SSR plugin *) +| WITH "[" LIST0 ltac_expr5 SEP "|" "]" LIST0 ssrintros_ne TAG SSR +] + +ssr_first_else: [ +| EDIT ssr_first ADD_OPT ssrorelse TAG SSR +] + +ssrseqarg: [ +| EDIT ADD_OPT ssrseqidx ssrswap TAG SSR +] + +ssr_dpat: [ +| REPLACE ssr_mpat "in" pattern200 ssr_rtype (* SSR plugin *) +| WITH ssr_mpat OPT ( OPT ( "in" pattern200 ) ssr_rtype ) TAG SSR +| DELETE ssr_mpat ssr_rtype (* SSR plugin *) +| DELETE ssr_mpat (* SSR plugin *) +] + +ssr_one_term_pattern: [ +| DELETE "Qed" constr +] + +ssrarg: [ +| EDIT ADD_OPT ssrfwdview OPT ssreqid ssrdgens OPT ssrintros (* SSR plugin *) +] + +ssragen: [ +| REPLACE "{" LIST1 ssrhyp "}" ssrterm (* SSR plugin *) +| WITH OPT ( "{" LIST1 ssrhyp "}" ) ssrterm TAG SSR +| DELETE ssrterm (* SSR plugin *) +] + +ssrbinder: [ +| REPLACE [ "of" | "&" ] term99 (* SSR plugin *) +| WITH "of" term99 TAG SSR +| "&" term99 TAG SSR +] + +firstorder_rhs: [ +| DELETE OPT firstorder_using +| DELETE "with" LIST1 preident +| REPLACE OPT firstorder_using "with" LIST1 preident +| WITH OPT firstorder_using OPT ( "with" LIST1 preident ) +] + +attribute: [ +| DELETE "using" OPT attr_value +] + SPLICE: [ | clause | noedit_mode @@ -2077,18 +2421,16 @@ SPLICE: [ | bar_cbrace | lconstr -(* +(* SSR *) | ast_closure_term | ast_closure_lterm | ident_no_do | ssrterm | ssrtacarg | ssrtac3arg -| ssrtclarg | ssrhyp | ssrhoi_hyp | ssrhoi_id -| ssrindex | ssrhpats | ssrhpats_nobs | ssrfwdid @@ -2103,11 +2445,34 @@ SPLICE: [ | ssrcofixfwd | ssrfixfwd | ssrhavefwdwbinders -| ssripats_ne | ssrparentacarg | ssrposefwd -*) - +| ssrstruct +| ssrrpat +| ssrhint +| ssrpattern_squarep +| ssrhintref +| ssr_search_item +| ssr_modlocs +| modloc +| ssrexactarg +| ssrclear +| ssrmult +| ssripats +| ssrintros +| ssrrule +| ssrpattern_squarep +| ssrcongrarg +| ssrdotac +| ssrunlockarg +| ssr_search_arg +| ssrortacarg +| ssrsetfwd +| ssr_idcomma +| ssr_dthen +| ssr_else +| ssr_rtype +| ssreqid | preident | lpar_id_coloneq | binders @@ -2240,6 +2605,8 @@ SPLICE: [ | mut_flag | tac2rec_fieldexprs | syn_level +| firstorder_rhs +| firstorder_using ] (* end SPLICE *) RENAME: [ @@ -2269,6 +2636,22 @@ RENAME: [ | ltac2_type5 ltac2_type | ltac2_expr6 ltac2_expr | starredidentref starred_ident_ref +| ssrocc ssr_occurrences +| ssrsimpl_ne s_item +| ssrclear_ne ssrclear +| ssrmult_ne mult +| ssripats_ne ssripats +| ssrrule_ne r_item +| ssrintros_ne ssrintros +| ssrpattern_ne_squarep ssrpattern_squarep +| ssrrwarg rewrite_item +| ssrrwocc occ_or_clear +| rpattern rewrite_pattern +| ssripat i_item +| ssrwgen gen_item +| ssrfwd ssrdefbody +| ssrclauses ssr_in +| ssrcpat ssrblockpat ] simple_tactic: [ diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml index 548ca7364c..92a745c863 100644 --- a/doc/tools/docgram/doc_grammar.ml +++ b/doc/tools/docgram/doc_grammar.ml @@ -12,12 +12,14 @@ open Coqpp_parser open Coqpp_ast let exit_code = ref 0 +let error_count = ref 0 let show_warn = ref true let fprintf = Printf.fprintf let error s = exit_code := 1; + incr error_count; Printf.eprintf "Error: "; Printf.eprintf s @@ -359,10 +361,9 @@ 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 + (* todo: only Ltac2 and SSR for now, outside of their main chapters *) + | Sedit2 ("TAG", "Ltac2") when file <> "doc/sphinx/proof-engine/ltac2.rst" -> " Ltac2" + | Sedit2 ("TAG", "SSR") when file <> "doc/sphinx/proof-engine/ssreflect-proof-language.rst" -> " SSR" | _ -> rv ) "" prod @@ -559,6 +560,10 @@ let level_regex = Str.regexp "[a-zA-Z0-9_]*$" let get_plugin_name file = if file = "user-contrib/Ltac2/g_ltac2.mlg" then "Ltac2" + (* todo: would be better if g_search.mlg has an "ssr" prefix *) + else if List.mem file ["plugins/ssr/ssrparser.mlg"; "plugins/ssr/ssrvernac.mlg"; + "plugins/ssrmatching/g_ssrmatching.mlg"; "plugins/ssrsearch/g_search.mlg"] then + "SSR" else if Str.string_match plugin_regex file 0 then Str.matched_group 1 file else @@ -568,12 +573,12 @@ 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 = + let add_prods nt prods gramext_globals = if not is_edit then - if NTMap.mem nt !g.map && nt <> "command" && nt <> "simple_tactic" then begin + if NTMap.mem nt !g.map && not (List.mem nt gramext_globals) && 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 + if false then Printf.printf "** dup local sym %s -> %s in %s\n" nt new_name file end; add_symdef nt file symdef_map; let plugin = get_plugin_name file in @@ -594,11 +599,12 @@ let read_mlg g is_edit ast file level_renames symdef_map = | Some s -> s | None -> "" in + let gramext_globals = ref grammar_ext.gramext_globals in List.iter (fun ent -> let len = List.length ent.gentry_rules in List.iteri (fun i rule -> let nt = ent.gentry_name in - if not (List.mem nt grammar_ext.gramext_globals) then + if not (List.mem nt !gramext_globals) then locals := StringSet.add nt !locals; let level = (get_label rule.grule_label) in let level = if level <> "" then level else @@ -629,8 +635,11 @@ let read_mlg g is_edit ast file level_renames symdef_map = if cur_level <> nt && i+1 < len then edited @ [[Snterm next_level]] else - edited in - add_prods cur_level prods_to_add) + edited + in + if cur_level <> nt && List.mem nt !gramext_globals then + gramext_globals := cur_level :: !gramext_globals; + add_prods cur_level prods_to_add !gramext_globals) ent.gentry_rules ) grammar_ext.gramext_entries @@ -640,16 +649,16 @@ let read_mlg g is_edit ast file level_renames symdef_map = | Some c -> String.trim c.code in add_prods node - (List.map (fun r -> cvt_ext r.vernac_toks) vernac_ext.vernacext_rules) + (List.map (fun r -> cvt_ext r.vernac_toks) vernac_ext.vernacext_rules) [] | VernacArgumentExt vernac_argument_ext -> add_prods vernac_argument_ext.vernacargext_name - (List.map (fun r -> cvt_ext r.tac_toks) vernac_argument_ext.vernacargext_rules) + (List.map (fun r -> cvt_ext r.tac_toks) vernac_argument_ext.vernacargext_rules) [] | TacticExt tactic_ext -> add_prods "simple_tactic" - (List.map (fun r -> cvt_ext r.tac_toks) tactic_ext.tacext_rules) + (List.map (fun r -> cvt_ext r.tac_toks) tactic_ext.tacext_rules) [] | ArgumentExt argument_ext -> add_prods argument_ext.argext_name - (List.map (fun r -> cvt_ext r.tac_toks) argument_ext.argext_rules) + (List.map (fun r -> cvt_ext r.tac_toks) argument_ext.argext_rules) [] | _ -> () in @@ -1910,7 +1919,10 @@ let process_rst g file args seen tac_prods cmd_prods = let cmd_exclude_files = [ "doc/sphinx/proof-engine/ssreflect-proof-language.rst"; - "doc/sphinx/proof-engine/tactics.rst" + "doc/sphinx/proofs/automatic-tactics/auto.rst"; + "doc/sphinx/proofs/writing-proofs/rewriting.rst"; + "doc/sphinx/proofs/writing-proofs/proof-mode.rst"; + "doc/sphinx/proof-engine/tactics.rst"; ] in @@ -2021,13 +2033,11 @@ 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; - (* - Printf.printf "\n"; + Printf.printf "\n\n"; NTMap.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.map; - *) if total <> 0 then Printf.eprintf "TOTAL %ss not included = %d\n" label total @@ -2090,7 +2100,7 @@ let process_grammar args = print_in_order out g `MLG !g.order StringSet.empty; close_out out; finish_with_file (dir "orderedGrammar") args; - check_singletons g; +(* check_singletons g*) (* print_dominated g*) let seen = ref { nts=NTMap.empty; tacs=NTMap.empty; tacvs=NTMap.empty; cmds=NTMap.empty; cmdvs=NTMap.empty } in @@ -2185,5 +2195,7 @@ let () = if !exit_code = 0 then begin process_grammar args end; + if !error_count > 0 then + Printf.eprintf "%d error(s)\n" !error_count; exit !exit_code (*with _ -> Printexc.print_backtrace stdout; exit 1*) diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 20ac8f8bf3..a787d769fb 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -119,6 +119,7 @@ term0: [ | "`{" term200 "}" | test_array_opening "[" "|" array_elems "|" lconstr type_cstr test_array_closing "|" "]" univ_annot | "`(" term200 ")" +| "ltac" ":" "(" Pltac.ltac_expr ")" ] array_elems: [ @@ -152,6 +153,11 @@ binder_constr: [ | "if" term200 as_return_type "then" term200 "else" term200 | "fix" fix_decls | "cofix" cofix_decls +| "if" term200 "is" ssr_dthen ssr_else (* SSR plugin *) +| "if" term200 "isn't" ssr_dthen ssr_else (* SSR plugin *) +| "let" ":" ssr_mpat ":=" lconstr "in" lconstr (* SSR plugin *) +| "let" ":" ssr_mpat ":=" lconstr ssr_rtype "in" lconstr (* SSR plugin *) +| "let" ":" ssr_mpat "in" pattern200 ":=" lconstr ssr_rtype "in" lconstr (* SSR plugin *) ] arg: [ @@ -308,6 +314,7 @@ open_binders: [ binders: [ | LIST0 binder +| Pcoq.Constr.binders ] binder: [ @@ -332,6 +339,7 @@ closed_binder: [ | "`{" LIST1 typeclass_constraint SEP "," "}" | "`[" LIST1 typeclass_constraint SEP "," "]" | "'" pattern0 +| [ "of" | "&" ] term99 (* SSR plugin *) ] typeclass_constraint: [ @@ -632,20 +640,20 @@ 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" 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" "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" "Setoid" constr constr constr "as" ident -| "Add" "Parametric" "Setoid" G_REWRITE_binders ":" constr constr constr "as" ident +| "Add" "Parametric" "Setoid" 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" G_REWRITE_binders ":" constr "with" "signature" lconstr "as" ident +| "Add" "Parametric" "Morphism" binders ":" constr "with" "signature" lconstr "as" ident | "Print" "Rewrite" "HintDb" preident | "Reset" "Ltac" "Profile" | "Show" "Ltac" "Profile" @@ -686,6 +694,10 @@ command: [ | "Print" "Rings" (* ring plugin *) | "Add" "Field" ident ":" constr OPT field_mods (* ring plugin *) | "Print" "Fields" (* ring plugin *) +| "Prenex" "Implicits" LIST1 global (* SSR plugin *) +| "Print" "Hint" "View" ssrviewpos (* SSR plugin *) +| "Hint" "View" ssrviewposspc LIST1 ssrhintref (* SSR plugin *) +| "Search" ssr_search_arg ssr_modlocs (* SSR plugin *) | "Number" "Notation" reference reference reference OPT number_options ":" ident | "Numeral" "Notation" reference reference reference ":" ident deprecated_number_modifier | "String" "Notation" reference reference reference OPT string_option ":" ident @@ -713,6 +725,7 @@ hint: [ | "Mode" global mode | "Unfold" LIST1 global | "Constructors" LIST1 global +| "Extern" natural OPT Constr.constr_pattern "=>" Pltac.tactic ] constr_body: [ @@ -746,6 +759,7 @@ attribute_list: [ attribute: [ | ident attr_value +| "using" attr_value ] attr_value: [ @@ -1021,6 +1035,7 @@ gallina_ext: [ | "Generalizable" [ "All" "Variables" | "No" "Variables" | [ "Variable" | "Variables" ] LIST1 identref ] | "Export" "Set" setting_name option_setting | "Export" "Unset" setting_name +| "Import" "Prenex" "Implicits" (* SSR plugin *) ] filtered_import: [ @@ -1743,6 +1758,51 @@ simple_tactic: [ | "ring_lookup" tactic0 "[" LIST0 constr "]" LIST1 constr (* ring plugin *) | "field_lookup" tactic "[" LIST0 constr "]" LIST1 constr (* ring plugin *) | "rtauto" +| "by" ssrhintarg (* SSR plugin *) +| "clear" natural (* SSR plugin *) +| "move" ssrmovearg ssrrpat (* SSR plugin *) +| "move" ssrmovearg ssrclauses (* SSR plugin *) +| "move" ssrrpat (* SSR plugin *) +| "move" (* SSR plugin *) +| "case" ssrcasearg ssrclauses (* SSR plugin *) +| "case" (* SSR plugin *) +| "elim" ssrarg ssrclauses (* SSR plugin *) +| "elim" (* SSR plugin *) +| "apply" ssrapplyarg (* SSR plugin *) +| "apply" (* SSR plugin *) +| "exact" ssrexactarg (* SSR plugin *) +| "exact" (* SSR plugin *) +| "exact" "<:" lconstr (* SSR plugin *) +| "congr" ssrcongrarg (* SSR plugin *) +| "ssrinstancesofruleL2R" ssrterm (* SSR plugin *) +| "ssrinstancesofruleR2L" ssrterm (* SSR plugin *) +| "rewrite" ssrrwargs ssrclauses (* SSR plugin *) +| "unlock" ssrunlockargs ssrclauses (* SSR plugin *) +| "pose" ssrfixfwd (* SSR plugin *) +| "pose" ssrcofixfwd (* SSR plugin *) +| "pose" ssrfwdid ssrposefwd (* SSR plugin *) +| "set" ssrfwdid ssrsetfwd ssrclauses (* SSR plugin *) +| "abstract" ssrdgens (* SSR plugin *) +| "have" ssrhavefwdwbinders (* SSR plugin *) +| "have" "suff" ssrhpats_nobs ssrhavefwd (* SSR plugin *) +| "have" "suffices" ssrhpats_nobs ssrhavefwd (* SSR plugin *) +| "suff" "have" ssrhpats_nobs ssrhavefwd (* SSR plugin *) +| "suffices" "have" ssrhpats_nobs ssrhavefwd (* SSR plugin *) +| "suff" ssrsufffwd (* SSR plugin *) +| "suffices" ssrsufffwd (* SSR plugin *) +| "wlog" ssrhpats_nobs ssrwlogfwd ssrhint (* SSR plugin *) +| "wlog" "suff" ssrhpats_nobs ssrwlogfwd ssrhint (* SSR plugin *) +| "wlog" "suffices" ssrhpats_nobs ssrwlogfwd ssrhint (* SSR plugin *) +| "without" "loss" ssrhpats_nobs ssrwlogfwd ssrhint (* SSR plugin *) +| "without" "loss" "suff" ssrhpats_nobs ssrwlogfwd ssrhint (* SSR plugin *) +| "without" "loss" "suffices" ssrhpats_nobs ssrwlogfwd ssrhint (* SSR plugin *) +| "gen" "have" ssrclear ssr_idcomma ssrhpats_nobs ssrwlogfwd ssrhint (* SSR plugin *) +| "generally" "have" ssrclear ssr_idcomma ssrhpats_nobs ssrwlogfwd ssrhint (* SSR plugin *) +| "under" ssrrwarg (* SSR plugin *) +| "under" ssrrwarg ssrintros_ne (* SSR plugin *) +| "under" ssrrwarg ssrintros_ne "do" ssrhint3arg (* SSR plugin *) +| "under" ssrrwarg "do" ssrhint3arg (* SSR plugin *) +| "ssrinstancesoftpat" G_SSRMATCHING_cpattern (* SSR plugin *) ] mlname: [ @@ -1763,9 +1823,7 @@ language: [ ] firstorder_using: [ -| "using" reference -| "using" reference "," LIST1 reference SEP "," -| "using" reference reference LIST0 reference +| "using" LIST1 reference SEP "," | ] @@ -1849,6 +1907,10 @@ by_arg_tac: [ in_clause: [ | in_clause' +| "*" occs +| "*" "|-" concl_occ +| LIST0 hypident_occ SEP "," "|-" concl_occ +| LIST0 hypident_occ SEP "," ] test_lpar_id_colon: [ @@ -1950,6 +2012,9 @@ ltac_expr4: [ | ltac_expr3 ";" ltac_expr3 | ltac_expr3 ";" tactic_then_locality for_each_goal "]" | ltac_expr3 +| ltac_expr5 ";" "first" ssr_first_else (* SSR plugin *) +| ltac_expr5 ";" "first" ssrseqarg (* SSR plugin *) +| ltac_expr5 ";" "last" ssrseqarg (* SSR plugin *) ] ltac_expr3: [ @@ -1966,6 +2031,10 @@ ltac_expr3: [ | "abstract" ltac_expr2 "using" ident | "only" selector ":" ltac_expr3 | ltac_expr2 +| "do" ssrmmod ssrdotac ssrclauses (* SSR plugin *) +| "do" ssrortacarg ssrclauses (* SSR plugin *) +| "do" int_or_var ssrmmod ssrdotac ssrclauses (* SSR plugin *) +| "abstract" ssrdgens (* SSR plugin *) ] ltac_expr2: [ @@ -1989,12 +2058,14 @@ ltac_expr1: [ | tactic_value | reference LIST0 tactic_arg | ltac_expr0 +| ltac_expr5 ssrintros_ne (* SSR plugin *) ] ltac_expr0: [ | "(" ltac_expr5 ")" | "[" ">" for_each_goal "]" | tactic_atom +| ssrparentacarg (* SSR plugin *) ] failkw: [ @@ -2139,14 +2210,6 @@ tactic_mode: [ | "par" ":" OPT ltac_info tactic ltac_use_default ] -G_LTAC_hint: [ -| "Extern" natural OPT Constr.constr_pattern "=>" Pltac.tactic -] - -G_LTAC_term0: [ -| "ltac" ":" "(" Pltac.ltac_expr ")" -] - ltac_selector: [ | toplevel_selector ] @@ -2217,10 +2280,6 @@ rewstrategy: [ | "fold" constr ] -G_REWRITE_binders: [ -| Pcoq.Constr.binders -] - int_or_var: [ | integer | identref @@ -2393,32 +2452,27 @@ hypident: [ | id_or_meta | "(" "type" "of" id_or_meta ")" | "(" "value" "of" id_or_meta ")" +| "(" "type" "of" Prim.identref ")" (* SSR plugin *) +| "(" "value" "of" Prim.identref ")" (* SSR plugin *) ] 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" G_TACTIC_in_clause +| "in" in_clause | occs | ] clause_dft_all: [ -| "in" G_TACTIC_in_clause +| "in" in_clause | ] opt_clause: [ -| "in" G_TACTIC_in_clause +| "in" in_clause | "at" occs_nums | ] @@ -2549,6 +2603,601 @@ field_mods: [ | "(" LIST1 field_mod SEP "," ")" (* ring plugin *) ] +ssrtacarg: [ +| ltac_expr5 (* SSR plugin *) +] + +ssrtac3arg: [ +| ltac_expr3 (* SSR plugin *) +] + +ssrtclarg: [ +| ssrtacarg (* SSR plugin *) +] + +ssrhyp: [ +| ident (* SSR plugin *) +] + +ssrhoi_hyp: [ +| ident (* SSR plugin *) +] + +ssrhoi_id: [ +| ident (* SSR plugin *) +] + +ssrsimpl_ne: [ +| "//=" (* SSR plugin *) +| "/=" (* SSR plugin *) +| test_ssrslashnum11 "/" natural "/" natural "=" (* SSR plugin *) +| test_ssrslashnum10 "/" natural "/" (* SSR plugin *) +| test_ssrslashnum10 "/" natural "=" (* SSR plugin *) +| test_ssrslashnum10 "/" natural "/=" (* SSR plugin *) +| test_ssrslashnum10 "/" natural "/" "=" (* SSR plugin *) +| test_ssrslashnum01 "//" natural "=" (* SSR plugin *) +| test_ssrslashnum00 "//" (* SSR plugin *) +] + +ssrclear_ne: [ +| "{" LIST1 ssrhyp "}" (* SSR plugin *) +] + +ssrclear: [ +| ssrclear_ne (* SSR plugin *) +| (* SSR plugin *) +] + +ssrindex: [ +] + +ssrocc: [ +| natural LIST0 natural (* SSR plugin *) +| "-" LIST0 natural (* SSR plugin *) +| "+" LIST0 natural (* SSR plugin *) +] + +ssrmmod: [ +| "!" (* SSR plugin *) +| LEFTQMARK (* SSR plugin *) +| "?" (* SSR plugin *) +] + +ssrmult_ne: [ +| natural ssrmmod (* SSR plugin *) +| ssrmmod (* SSR plugin *) +] + +ssrmult: [ +| ssrmult_ne (* SSR plugin *) +| (* SSR plugin *) +] + +ssrdocc: [ +| "{" ssrocc "}" (* SSR plugin *) +| "{" LIST0 ssrhyp "}" (* SSR plugin *) +] + +ssrterm: [ +| ssrtermkind Pcoq.Constr.constr (* SSR plugin *) +] + +ast_closure_term: [ +| term_annotation constr (* SSR plugin *) +] + +ast_closure_lterm: [ +| term_annotation lconstr (* SSR plugin *) +] + +ssrbwdview: [ +| test_not_ssrslashnum "/" Pcoq.Constr.constr (* SSR plugin *) +| test_not_ssrslashnum "/" Pcoq.Constr.constr ssrbwdview (* SSR plugin *) +] + +ssrfwdview: [ +| test_not_ssrslashnum "/" ast_closure_term (* SSR plugin *) +| test_not_ssrslashnum "/" ast_closure_term ssrfwdview (* SSR plugin *) +] + +ident_no_do: [ +| test_ident_no_do IDENT (* SSR plugin *) +] + +ssripat: [ +| "_" (* SSR plugin *) +| "*" (* SSR plugin *) +| ">" (* SSR plugin *) +| ident_no_do (* SSR plugin *) +| "?" (* SSR plugin *) +| "+" (* SSR plugin *) +| "++" (* SSR plugin *) +| ssrsimpl_ne (* SSR plugin *) +| ssrdocc "->" (* SSR plugin *) +| ssrdocc "<-" (* SSR plugin *) +| ssrdocc (* SSR plugin *) +| "->" (* SSR plugin *) +| "<-" (* SSR plugin *) +| "-" (* SSR plugin *) +| "-/" "=" (* SSR plugin *) +| "-/=" (* SSR plugin *) +| "-/" "/" (* SSR plugin *) +| "-//" (* SSR plugin *) +| "-/" integer "/" (* SSR plugin *) +| "-/" "/=" (* SSR plugin *) +| "-//" "=" (* SSR plugin *) +| "-//=" (* SSR plugin *) +| "-/" integer "/=" (* SSR plugin *) +| "-/" integer "/" integer "=" (* SSR plugin *) +| ssrfwdview (* SSR plugin *) +| "[" ":" LIST0 ident "]" (* SSR plugin *) +| "[:" LIST0 ident "]" (* SSR plugin *) +| ssrcpat (* SSR plugin *) +] + +ssripats: [ +| ssripat ssripats (* SSR plugin *) +| (* SSR plugin *) +] + +ssriorpat: [ +| ssripats "|" ssriorpat (* SSR plugin *) +| ssripats "|-" ">" ssriorpat (* SSR plugin *) +| ssripats "|-" ssriorpat (* SSR plugin *) +| ssripats "|->" ssriorpat (* SSR plugin *) +| ssripats "||" ssriorpat (* SSR plugin *) +| ssripats "|||" ssriorpat (* SSR plugin *) +| ssripats "||||" ssriorpat (* SSR plugin *) +| ssripats (* SSR plugin *) +] + +ssrcpat: [ +| test_nohidden "[" hat "]" (* SSR plugin *) +| test_nohidden "[" ssriorpat "]" (* SSR plugin *) +| test_nohidden "[=" ssriorpat "]" (* SSR plugin *) +] + +hat: [ +| "^" ident (* SSR plugin *) +| "^" "~" ident (* SSR plugin *) +| "^" "~" natural (* SSR plugin *) +| "^~" ident (* SSR plugin *) +| "^~" natural (* SSR plugin *) +] + +ssripats_ne: [ +| ssripat ssripats (* SSR plugin *) +] + +ssrhpats: [ +| ssripats (* SSR plugin *) +] + +ssrhpats_wtransp: [ +| ssripats (* SSR plugin *) +| ssripats "@" ssripats (* SSR plugin *) +] + +ssrhpats_nobs: [ +| ssripats (* SSR plugin *) +] + +ssrrpat: [ +| "->" (* SSR plugin *) +| "<-" (* SSR plugin *) +] + +ssrintros_ne: [ +| "=>" ssripats_ne (* SSR plugin *) +] + +ssrintros: [ +| ssrintros_ne (* SSR plugin *) +| (* SSR plugin *) +] + +ssrintrosarg: [ +] + +ssrfwdid: [ +| test_ssrfwdid Prim.ident (* SSR plugin *) +] + +ssrortacs: [ +| ssrtacarg "|" ssrortacs (* SSR plugin *) +| ssrtacarg "|" (* SSR plugin *) +| ssrtacarg (* SSR plugin *) +| "|" ssrortacs (* SSR plugin *) +| "|" (* SSR plugin *) +] + +ssrhintarg: [ +| "[" "]" (* SSR plugin *) +| "[" ssrortacs "]" (* SSR plugin *) +| ssrtacarg (* SSR plugin *) +] + +ssrhint3arg: [ +| "[" "]" (* SSR plugin *) +| "[" ssrortacs "]" (* SSR plugin *) +| ssrtac3arg (* SSR plugin *) +] + +ssrortacarg: [ +| "[" ssrortacs "]" (* SSR plugin *) +] + +ssrhint: [ +| (* SSR plugin *) +| "by" ssrhintarg (* SSR plugin *) +] + +ssrwgen: [ +| ssrclear_ne (* SSR plugin *) +| ssrhoi_hyp (* SSR plugin *) +| "@" ssrhoi_hyp (* SSR plugin *) +| "(" ssrhoi_id ":=" lcpattern ")" (* SSR plugin *) +| "(" ssrhoi_id ")" (* SSR plugin *) +| "(@" ssrhoi_id ":=" lcpattern ")" (* SSR plugin *) +| "(" "@" ssrhoi_id ":=" lcpattern ")" (* SSR plugin *) +] + +ssrclausehyps: [ +| ssrwgen "," ssrclausehyps (* SSR plugin *) +| ssrwgen ssrclausehyps (* SSR plugin *) +| ssrwgen (* SSR plugin *) +] + +ssrclauses: [ +| "in" ssrclausehyps "|-" "*" (* SSR plugin *) +| "in" ssrclausehyps "|-" (* SSR plugin *) +| "in" ssrclausehyps "*" (* SSR plugin *) +| "in" ssrclausehyps (* SSR plugin *) +| "in" "|-" "*" (* SSR plugin *) +| "in" "*" (* SSR plugin *) +| "in" "*" "|-" (* SSR plugin *) +| (* SSR plugin *) +] + +ssrfwd: [ +| ":=" ast_closure_lterm (* SSR plugin *) +| ":" ast_closure_lterm ":=" ast_closure_lterm (* SSR plugin *) +] + +ssrbvar: [ +| ident (* SSR plugin *) +| "_" (* SSR plugin *) +] + +ssrbinder: [ +| ssrbvar (* SSR plugin *) +| "(" ssrbvar ")" (* SSR plugin *) +| "(" ssrbvar ":" lconstr ")" (* SSR plugin *) +| "(" ssrbvar LIST1 ssrbvar ":" lconstr ")" (* SSR plugin *) +| "(" ssrbvar ":" lconstr ":=" lconstr ")" (* SSR plugin *) +| "(" ssrbvar ":=" lconstr ")" (* SSR plugin *) +| [ "of" | "&" ] term99 (* SSR plugin *) +] + +ssrstruct: [ +| "{" "struct" ident "}" (* SSR plugin *) +| (* SSR plugin *) +] + +ssrposefwd: [ +| LIST0 ssrbinder ssrfwd (* SSR plugin *) +] + +ssrfixfwd: [ +| "fix" ssrbvar LIST0 ssrbinder ssrstruct ssrfwd (* SSR plugin *) +] + +ssrcofixfwd: [ +| "cofix" ssrbvar LIST0 ssrbinder ssrfwd (* SSR plugin *) +] + +ssrsetfwd: [ +| ":" ast_closure_lterm ":=" "{" ssrocc "}" cpattern (* SSR plugin *) +| ":" ast_closure_lterm ":=" lcpattern (* SSR plugin *) +| ":=" "{" ssrocc "}" cpattern (* SSR plugin *) +| ":=" lcpattern (* SSR plugin *) +] + +ssrhavefwd: [ +| ":" ast_closure_lterm ssrhint (* SSR plugin *) +| ":" ast_closure_lterm ":=" ast_closure_lterm (* SSR plugin *) +| ":" ast_closure_lterm ":=" (* SSR plugin *) +| ":=" ast_closure_lterm (* SSR plugin *) +] + +ssrhavefwdwbinders: [ +| ssrhpats_wtransp LIST0 ssrbinder ssrhavefwd (* SSR plugin *) +] + +ssrdoarg: [ +] + +ssrseqarg: [ +| ssrswap (* SSR plugin *) +| ssrseqidx ssrortacarg OPT ssrorelse (* SSR plugin *) +| ssrseqidx ssrswap (* SSR plugin *) +| ltac_expr3 (* SSR plugin *) +] + +ssrseqidx: [ +| test_ssrseqvar Prim.ident (* SSR plugin *) +| Prim.natural (* SSR plugin *) +] + +ssrswap: [ +| "first" (* SSR plugin *) +| "last" (* SSR plugin *) +] + +ssrorelse: [ +| "||" ltac_expr2 (* SSR plugin *) +] + +Prim.ident: [ +| IDENT ssr_null_entry (* SSR plugin *) +] + +ssrparentacarg: [ +| "(" ltac_expr5 ")" (* SSR plugin *) +] + +ssrdotac: [ +| ltac_expr3 (* SSR plugin *) +| ssrortacarg (* SSR plugin *) +] + +ssrseqdir: [ +] + +ssr_first: [ +| ssr_first ssrintros_ne (* SSR plugin *) +| "[" LIST0 ltac_expr5 SEP "|" "]" (* SSR plugin *) +] + +ssr_first_else: [ +| ssr_first ssrorelse (* SSR plugin *) +| ssr_first (* SSR plugin *) +] + +ssrgen: [ +| ssrdocc cpattern (* SSR plugin *) +| cpattern (* SSR plugin *) +] + +ssrdgens_tl: [ +| "{" LIST1 ssrhyp "}" cpattern ssrdgens_tl (* SSR plugin *) +| "{" LIST1 ssrhyp "}" (* SSR plugin *) +| "{" ssrocc "}" cpattern ssrdgens_tl (* SSR plugin *) +| "/" ssrdgens_tl (* SSR plugin *) +| cpattern ssrdgens_tl (* SSR plugin *) +| (* SSR plugin *) +] + +ssrdgens: [ +| ":" ssrgen ssrdgens_tl (* SSR plugin *) +] + +ssreqid: [ +| test_ssreqid ssreqpat (* SSR plugin *) +| test_ssreqid (* SSR plugin *) +] + +ssreqpat: [ +| Prim.ident (* SSR plugin *) +| "_" (* SSR plugin *) +| "?" (* SSR plugin *) +| "+" (* SSR plugin *) +| ssrdocc "->" (* SSR plugin *) +| ssrdocc "<-" (* SSR plugin *) +| "->" (* SSR plugin *) +| "<-" (* SSR plugin *) +] + +ssrarg: [ +| ssrfwdview ssreqid ssrdgens ssrintros (* SSR plugin *) +| ssrfwdview ssrclear ssrintros (* SSR plugin *) +| ssreqid ssrdgens ssrintros (* SSR plugin *) +| ssrclear_ne ssrintros (* SSR plugin *) +| ssrintros_ne (* SSR plugin *) +] + +ssrmovearg: [ +| ssrarg (* SSR plugin *) +] + +ssrcasearg: [ +| ssrarg (* SSR plugin *) +] + +ssragen: [ +| "{" LIST1 ssrhyp "}" ssrterm (* SSR plugin *) +| ssrterm (* SSR plugin *) +] + +ssragens: [ +| "{" LIST1 ssrhyp "}" ssrterm ssragens (* SSR plugin *) +| "{" LIST1 ssrhyp "}" (* SSR plugin *) +| ssrterm ssragens (* SSR plugin *) +| (* SSR plugin *) +] + +ssrapplyarg: [ +| ":" ssragen ssragens ssrintros (* SSR plugin *) +| ssrclear_ne ssrintros (* SSR plugin *) +| ssrintros_ne (* SSR plugin *) +| ssrbwdview ":" ssragen ssragens ssrintros (* SSR plugin *) +| ssrbwdview ssrclear ssrintros (* SSR plugin *) +] + +ssrexactarg: [ +| ":" ssragen ssragens (* SSR plugin *) +| ssrbwdview ssrclear (* SSR plugin *) +| ssrclear_ne (* SSR plugin *) +] + +ssrcongrarg: [ +| natural constr ssrdgens (* SSR plugin *) +| natural constr (* SSR plugin *) +| constr ssrdgens (* SSR plugin *) +| constr (* SSR plugin *) +] + +ssrrwocc: [ +| "{" LIST0 ssrhyp "}" (* SSR plugin *) +| "{" ssrocc "}" (* SSR plugin *) +| (* SSR plugin *) +] + +ssrrule_ne: [ +| test_not_ssrslashnum [ "/" ssrterm | ssrterm | ssrsimpl_ne ] (* SSR plugin *) +| ssrsimpl_ne (* SSR plugin *) +] + +ssrrule: [ +| ssrrule_ne (* SSR plugin *) +| (* SSR plugin *) +] + +ssrpattern_squarep: [ +| "[" rpattern "]" (* SSR plugin *) +| (* SSR plugin *) +] + +ssrpattern_ne_squarep: [ +| "[" rpattern "]" (* SSR plugin *) +] + +ssrrwarg: [ +| "-" ssrmult ssrrwocc ssrpattern_squarep ssrrule_ne (* SSR plugin *) +| "-/" ssrterm (* SSR plugin *) +| ssrmult_ne ssrrwocc ssrpattern_squarep ssrrule_ne (* SSR plugin *) +| "{" LIST1 ssrhyp "}" ssrpattern_ne_squarep ssrrule_ne (* SSR plugin *) +| "{" LIST1 ssrhyp "}" ssrrule (* SSR plugin *) +| "{" ssrocc "}" ssrpattern_squarep ssrrule_ne (* SSR plugin *) +| "{" "}" ssrpattern_squarep ssrrule_ne (* SSR plugin *) +| ssrpattern_ne_squarep ssrrule_ne (* SSR plugin *) +| ssrrule_ne (* SSR plugin *) +] + +ssrrwargs: [ +| test_ssr_rw_syntax LIST1 ssrrwarg (* SSR plugin *) +] + +ssrunlockarg: [ +| "{" ssrocc "}" ssrterm (* SSR plugin *) +| ssrterm (* SSR plugin *) +] + +ssrunlockargs: [ +| LIST0 ssrunlockarg (* SSR plugin *) +] + +ssrsufffwd: [ +| ssrhpats LIST0 ssrbinder ":" ast_closure_lterm ssrhint (* SSR plugin *) +] + +ssrwlogfwd: [ +| ":" LIST0 ssrwgen "/" ast_closure_lterm (* SSR plugin *) +] + +ssr_idcomma: [ +| (* SSR plugin *) +| test_idcomma [ IDENT | "_" ] "," (* SSR plugin *) +] + +ssr_rtype: [ +| "return" term100 (* SSR plugin *) +] + +ssr_mpat: [ +| pattern200 (* SSR plugin *) +] + +ssr_dpat: [ +| ssr_mpat "in" pattern200 ssr_rtype (* SSR plugin *) +| ssr_mpat ssr_rtype (* SSR plugin *) +| ssr_mpat (* SSR plugin *) +] + +ssr_dthen: [ +| ssr_dpat "then" lconstr (* SSR plugin *) +] + +ssr_elsepat: [ +| "else" (* SSR plugin *) +] + +ssr_else: [ +| ssr_elsepat lconstr (* SSR plugin *) +] + +ssrhintref: [ +| constr (* SSR plugin *) +| constr "|" natural (* SSR plugin *) +] + +ssrviewpos: [ +| "for" "move" "/" (* SSR plugin *) +| "for" "apply" "/" (* SSR plugin *) +| "for" "apply" "/" "/" (* SSR plugin *) +| "for" "apply" "//" (* SSR plugin *) +| (* SSR plugin *) +] + +ssrviewposspc: [ +| ssrviewpos (* SSR plugin *) +] + +rpattern: [ +| lconstr (* SSR plugin *) +| "in" lconstr (* SSR plugin *) +| lconstr "in" lconstr (* SSR plugin *) +| "in" lconstr "in" lconstr (* SSR plugin *) +| lconstr "in" lconstr "in" lconstr (* SSR plugin *) +| lconstr "as" lconstr "in" lconstr (* SSR plugin *) +] + +G_SSRMATCHING_cpattern: [ +| "Qed" constr (* SSR plugin *) +| ssrtermkind constr (* SSR plugin *) +] + +lcpattern: [ +| "Qed" lconstr (* SSR plugin *) +| ssrtermkind lconstr (* SSR plugin *) +] + +ssrpatternarg: [ +| rpattern (* SSR plugin *) +] + +ssr_search_item: [ +| string (* SSR plugin *) +| string "%" preident (* SSR plugin *) +| constr_pattern (* SSR plugin *) +] + +ssr_search_arg: [ +| "-" ssr_search_item ssr_search_arg (* SSR plugin *) +| ssr_search_item ssr_search_arg (* SSR plugin *) +| (* SSR plugin *) +] + +ssr_modlocs: [ +| (* SSR plugin *) +| "in" LIST1 modloc (* SSR plugin *) +] + +modloc: [ +| "-" global (* SSR plugin *) +| global (* SSR plugin *) +] + deprecated_number_modifier: [ | | "(" "warning" "after" bignat ")" diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 94a6fa730b..c697043f27 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -174,10 +174,129 @@ subsequent_letter: [ | [ first_letter | digit | "'" | unicode_id_part ] ] -firstorder_rhs: [ -| OPT firstorder_using -| "with" LIST1 ident -| OPT firstorder_using "with" LIST1 ident +ssrarg: [ +| OPT ssrfwdview OPT ssreqpat ssrdgens OPT ssrintros +| ssrfwdview OPT ssrclear OPT ssrintros (* SSR plugin *) +| ssrclear OPT ssrintros (* SSR plugin *) +| ssrintros (* SSR plugin *) +] + +ssreqpat: [ +| ident (* SSR plugin *) +| "_" (* SSR plugin *) +| "?" (* SSR plugin *) +| "+" (* SSR plugin *) +| ssrdocc "->" (* SSR plugin *) +| ssrdocc "<-" (* SSR plugin *) +| "->" (* SSR plugin *) +| "<-" (* SSR plugin *) +] + +ssrapplyarg: [ +| ssrclear OPT ssrintros (* SSR plugin *) +| ssrintros (* SSR plugin *) +| OPT ssrbwdview ":" ssragen OPT ssragens OPT ssrintros (* SSR plugin *) +| ssrbwdview OPT ssrclear OPT ssrintros (* SSR plugin *) +] + +ssragen: [ +| OPT ( "{" LIST1 ident "}" ) term (* SSR plugin *) +] + +ssragens: [ +| "{" LIST1 ident "}" term OPT ssragens (* SSR plugin *) +| "{" LIST1 ident "}" (* SSR plugin *) +| term OPT ssragens (* SSR plugin *) +] + +ssrintros: [ +| "=>" ssripats (* SSR plugin *) +] + +ssrbwdview: [ +| "/" term (* SSR plugin *) +| "/" term ssrbwdview (* SSR plugin *) +] + +ssrdgens: [ +| ":" ssrgen OPT ( "/" ssrgen ) (* SSR plugin *) +] + +ssrgen: [ +| cpattern LIST0 [ LIST1 ident | cpattern ] (* SSR plugin *) +] + +rewrite_item: [ +| "-" OPT mult OPT occ_or_clear OPT ssrpattern_squarep r_item (* SSR plugin *) +| mult OPT occ_or_clear OPT ssrpattern_squarep r_item (* SSR plugin *) +| "-/" term (* SSR plugin *) +| OPT ( OPT ( "{" LIST1 ident "}" ) ssrpattern_squarep ) r_item (* SSR plugin *) +| "{" LIST1 ident "}" OPT r_item (* SSR plugin *) +| "{" OPT ssr_occurrences "}" OPT ssrpattern_squarep r_item (* SSR plugin *) +] + +occ_or_clear: [ +| clear_switch +| "{" ssr_occurrences "}" (* SSR plugin *) +] + +clear_switch: [ +| "{" LIST0 ident "}" +] + +ssr_occurrences: [ +| [ natural | "+" | "-" ] LIST0 natural (* SSR plugin *) +] + +r_item: [ +| [ OPT "/" term | s_item ] (* SSR plugin *) +] + +ssrpattern_squarep: [ +| "[" rewrite_pattern "]" (* SSR plugin *) +] + +rewrite_pattern: [ +| OPT ( OPT ( OPT ( OPT term "in" ) term ) "in" ) term (* SSR plugin *) +| term "as" term "in" term (* SSR plugin *) +] + +ssr_in: [ +| "in" ssrclausehyps OPT "|-" OPT "*" (* SSR plugin *) +| "in" [ "*" | "*" "|-" | "|-" "*" ] (* SSR plugin *) +] + +ssrclausehyps: [ +| gen_item LIST0 ( OPT "," gen_item ) (* SSR plugin *) +] + +gen_item: [ +| ssrclear (* SSR plugin *) +| OPT "@" ident (* SSR plugin *) +| "(" ident OPT ( ":=" lcpattern ) ")" (* SSR plugin *) +| "(@" ident ":=" lcpattern ")" (* SSR plugin *) +] + +ssrclear: [ +| "{" LIST1 ident "}" (* SSR plugin *) +] + +lcpattern: [ +| term +] + +ssrsufffwd: [ +| OPT ssripats LIST0 ssrbinder ":" term OPT ( "by" ssrhintarg ) (* SSR plugin *) +] + +ssrviewpos: [ +| "for" "move" "/" (* SSR plugin *) +| "for" "apply" "/" (* SSR plugin *) +| "for" "apply" "//" (* SSR plugin *) +] + +ssr_one_term_pattern: [ +| one_term (* SSR plugin *) ] where: [ @@ -347,6 +466,10 @@ term_if: [ | "if" term OPT [ OPT [ "as" name ] "return" term100 ] "then" term "else" term ] +ssr_dpat: [ +| pattern OPT ( OPT ( "in" pattern ) "return" term100 ) (* SSR plugin *) +] + term_let: [ | "let" name OPT ( ":" type ) ":=" term "in" term | "let" name LIST1 binder OPT ( ":" type ) ":=" term "in" term @@ -885,6 +1008,10 @@ command: [ | "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" ) (* ring plugin *) | "Print" "Fields" (* ring plugin *) | "Hint" "Cut" "[" hints_path "]" OPT ( ":" LIST1 ident ) +| "Prenex" "Implicits" LIST1 qualid (* SSR plugin *) +| "Print" "Hint" "View" OPT ssrviewpos (* SSR plugin *) +| "Hint" "View" OPT ssrviewpos LIST1 ( one_term OPT ( "|" natural ) ) (* SSR plugin *) +| "Search" OPT LIST1 ( "-" [ string OPT ( "%" ident ) | one_term ] ) OPT ( "in" LIST1 ( OPT "-" qualid ) ) (* SSR plugin *) | "Typeclasses" "Transparent" LIST1 qualid | "Typeclasses" "Opaque" LIST1 qualid | "Typeclasses" "eauto" ":=" OPT "debug" OPT ( "(" [ "bfs" | "dfs" ] ")" ) OPT natural @@ -909,7 +1036,7 @@ command: [ | "Declare" "Left" "Step" one_term | "Declare" "Right" "Step" one_term | "Number" "Notation" qualid qualid qualid OPT ( "(" LIST1 number_modifier SEP "," ")" ) ":" scope_name -| "Numeral" "Notation" qualid qualid qualid ":" scope_name deprecated_number_modifier +| "Numeral" "Notation" qualid qualid qualid ":" scope_name OPT deprecated_number_modifier | "String" "Notation" qualid qualid qualid OPT ( "(" number_string_via ")" ) ":" scope_name | "SubClass" ident_decl def_body | thm_token ident_decl LIST0 binder ":" type LIST0 [ "with" ident_decl LIST0 binder ":" type ] @@ -964,6 +1091,7 @@ command: [ | "Generalizable" [ [ "Variable" | "Variables" ] LIST1 ident | "All" "Variables" | "No" "Variables" ] | "Set" setting_name OPT [ integer | string ] | "Unset" setting_name +| "Import" "Prenex" "Implicits" (* SSR plugin *) | "Open" "Scope" scope | "Close" "Scope" scope | "Delimit" "Scope" scope_name "with" scope_key @@ -1117,13 +1245,11 @@ lident: [ destruction_arg: [ | natural -| one_term OPT ( "with" bindings ) | constr_with_bindings_arg ] constr_with_bindings_arg: [ -| ">" one_term OPT ( "with" bindings ) -| one_term OPT ( "with" bindings ) +| OPT ">" one_term OPT ( "with" bindings ) (* SSR plugin *) ] clause_dft_concl: [ @@ -1143,8 +1269,8 @@ hypident_occ: [ hypident: [ | ident -| "(" "type" "of" ident ")" -| "(" "value" "of" ident ")" +| "(" "type" "of" ident ")" (* SSR plugin *) +| "(" "value" "of" ident ")" (* SSR plugin *) ] concl_occ: [ @@ -1269,8 +1395,119 @@ field_mod: [ | "completeness" one_term (* ring plugin *) ] +ssrmmod: [ +| "!" (* SSR plugin *) +| "?" (* SSR plugin *) +] + +mult: [ +| OPT natural ssrmmod (* SSR plugin *) +] + +ssrwlogfwd: [ +| ":" LIST0 gen_item "/" term (* SSR plugin *) +] + +ssrhintarg: [ +| "[" OPT ssrortacs "]" (* SSR plugin *) +| ltac_expr (* SSR plugin *) +] + +ssrortacs: [ +| OPT ltac_expr "|" OPT ssrortacs +| ltac_expr (* SSR plugin *) +] + +ssrhint3arg: [ +| "[" OPT ssrortacs "]" (* SSR plugin *) +| ltac_expr3 (* SSR plugin *) +] + +ssrdefbody: [ +| OPT ( ":" term ) ":=" term (* SSR plugin *) +] + +i_item: [ +| "_" (* SSR plugin *) +| "*" (* SSR plugin *) +| ">" (* SSR plugin *) +| ident +| "?" (* SSR plugin *) +| "+" (* SSR plugin *) +| "++" (* SSR plugin *) +| s_item (* SSR plugin *) +| ssrdocc OPT [ "->" | "<-" ] (* SSR plugin *) +| "-" (* SSR plugin *) +| "-/=" (* SSR plugin *) +| "-//" (* SSR plugin *) +| "-//=" (* SSR plugin *) +| "-/" integer [ "/=" | "/" | "/" integer "=" ] (* SSR plugin *) +| ssrfwdview (* SSR plugin *) +| "[:" LIST0 ident "]" (* SSR plugin *) +| ssrblockpat (* SSR plugin *) +] + +ssrhpats_wtransp: [ +| OPT ssripats (* SSR plugin *) +| OPT ssripats "@" OPT ssripats (* SSR plugin *) +] + +ssripats: [ +| LIST1 i_item (* SSR plugin *) +] + +s_item: [ +| "//" (* SSR plugin *) +| "/=" (* SSR plugin *) +| "//=" (* SSR plugin *) +| "/" natural "/" natural "=" (* SSR plugin *) +| "/" natural "/=" (* SSR plugin *) +] + +ssrdocc: [ +| "{" ssr_occurrences "}" (* SSR plugin *) +| "{" LIST0 ident "}" (* SSR plugin *) +] + +ssrfwdview: [ +| LIST1 ( "/" one_term ) (* SSR plugin *) +] + +hat: [ +| "^" ident (* SSR plugin *) +| "^~" ident (* SSR plugin *) +| "^~" natural (* SSR plugin *) +] + +ssriorpat: [ +| ssripats OPT ( [ "|" | "|-" ] ssriorpat ) (* SSR plugin *) +] + +ssrblockpat: [ +| "[" hat "]" (* SSR plugin *) +| "[" ssriorpat "]" (* SSR plugin *) +| "[=" ssriorpat "]" (* SSR plugin *) +] + +ssrbinder: [ +| ssrbvar (* SSR plugin *) +| "(" LIST1 ssrbvar ":" term ")" (* SSR plugin *) +| "(" ssrbvar OPT ( ":" term ) OPT ( ":=" term ) ")" (* SSR plugin *) +| "of" term10 (* SSR plugin *) +| "&" term10 (* SSR plugin *) +] + +ssrbvar: [ +| ident (* SSR plugin *) +| "_" (* SSR plugin *) +] + +ssrhavefwd: [ +| ":" term OPT ( "by" ssrhintarg ) (* SSR plugin *) +| ":" term ":=" OPT term (* SSR plugin *) +] + deprecated_number_modifier: [ -| | "(" "warning" "after" bignat ")" | "(" "abstract" "after" bignat ")" ] @@ -1403,11 +1640,14 @@ simple_tactic: [ | "infoH" ltac_expr3 | "abstract" ltac_expr2 OPT ( "using" ident ) | "only" selector ":" ltac_expr3 +| "do" "[" ssrortacs "]" OPT ssr_in (* SSR plugin *) +| "do" OPT int_or_var ssrmmod [ ltac_expr3 | "[" ssrortacs "]" (* SSR plugin *) ] OPT ssr_in (* SSR plugin *) | "tryif" ltac_expr "then" ltac_expr "else" ltac_expr2 | "first" "[" LIST0 ltac_expr SEP "|" "]" | "solve" "[" LIST0 ltac_expr SEP "|" "]" | "idtac" LIST0 [ ident | string | natural ] | [ "fail" | "gfail" ] OPT int_or_var LIST0 [ ident | string | natural ] +| ltac_expr ssrintros (* SSR plugin *) | "fun" LIST1 name "=>" ltac_expr | "eval" red_expr "in" term | "context" ident "[" term "]" @@ -1595,7 +1835,7 @@ simple_tactic: [ | "rtauto" | "congruence" OPT natural OPT ( "with" LIST1 one_term ) | "f_equal" -| "firstorder" OPT ltac_expr firstorder_rhs +| "firstorder" OPT ltac_expr OPT ( "using" LIST1 qualid SEP "," ) OPT ( "with" LIST1 ident ) | "gintuition" OPT ltac_expr | "functional" "inversion" [ ident | natural ] OPT qualid (* funind plugin *) | "functional" "induction" term OPT ( "using" one_term OPT ( "with" bindings ) ) OPT ( "as" simple_intropattern ) (* funind plugin *) @@ -1622,12 +1862,47 @@ simple_tactic: [ | "protect_fv" string OPT ( "in" ident ) | "ring_lookup" ltac_expr0 "[" LIST0 one_term "]" LIST1 one_term (* ring plugin *) | "field_lookup" ltac_expr "[" LIST0 one_term "]" LIST1 one_term (* ring plugin *) +| "ring_lookup" ltac_expr0 "[" LIST0 one_term "]" LIST1 one_term (* ring plugin *) +| "field_lookup" ltac_expr "[" LIST0 one_term "]" LIST1 one_term (* ring plugin *) +| "by" ssrhintarg (* SSR plugin *) +| "clear" natural (* SSR plugin *) +| "move" OPT ( OPT ssrarg [ "->" | "<-" ] ) (* SSR plugin *) +| "move" ssrarg OPT ssr_in (* SSR plugin *) +| "case" OPT ( ssrarg OPT ssr_in ) (* SSR plugin *) +| "elim" OPT ( ssrarg OPT ssr_in ) (* SSR plugin *) +| "apply" OPT ssrapplyarg (* SSR plugin *) +| "exact" [ ":" ssragen OPT ssragens | ssrbwdview OPT ssrclear | ssrclear ] (* SSR plugin *) +| "exact" (* SSR plugin *) +| "exact" "<:" term (* SSR plugin *) +| "congr" OPT natural one_term OPT ssrdgens (* SSR plugin *) +| "ssrinstancesofruleL2R" term (* SSR plugin *) +| "ssrinstancesofruleR2L" term (* SSR plugin *) +| "rewrite" LIST1 rewrite_item OPT ssr_in (* SSR plugin *) +| "unlock" LIST0 ( OPT ( "{" ssr_occurrences "}" ) term ) OPT ssr_in (* SSR plugin *) +| "pose" "fix" ssrbvar LIST0 ssrbinder OPT ( "{" "struct" ident "}" ) ssrdefbody (* SSR plugin *) +| "pose" "cofix" ssrbvar LIST0 ssrbinder ssrdefbody (* SSR plugin *) +| "pose" ident LIST0 ssrbinder ssrdefbody (* SSR plugin *) +| "set" ident OPT ( ":" term ) ":=" [ "{" ssr_occurrences "}" cpattern | lcpattern ] OPT ssr_in (* SSR plugin *) +| "abstract" ssrdgens (* SSR plugin *) +| "have" ssrhpats_wtransp LIST0 ssrbinder ssrhavefwd (* SSR plugin *) +| "have" [ "suff" | "suffices" ] OPT ssripats ssrhavefwd (* SSR plugin *) +| [ "suff" | "suffices" ] OPT ( "have" OPT ssripats ) ssrhavefwd (* SSR plugin *) +| [ "suff" | "suffices" ] ssrsufffwd (* SSR plugin *) +| [ "wlog" | "without loss" ] OPT [ "suff" | "suffices" ] OPT ssripats ssrwlogfwd OPT ( "by" ssrhintarg ) (* SSR plugin *) +| [ "gen" | "generally" ] "have" OPT ssrclear OPT ( [ ident | "_" ] "," ) OPT ssripats ssrwlogfwd OPT ( "by" ssrhintarg ) (* SSR plugin *) +| "under" rewrite_item OPT ssrintros OPT ( "do" ssrhint3arg ) (* SSR plugin *) +| "ssrinstancesoftpat" ssr_one_term_pattern (* SSR plugin *) +| ltac_expr ";" "first" ssr_first_else (* SSR plugin *) +| ltac_expr ";" "first" ssrseqarg (* SSR plugin *) +| ltac_expr ";" "last" ssrseqarg (* SSR plugin *) | match_key OPT "reverse" "goal" "with" OPT "|" LIST1 ( goal_pattern "=>" ltac_expr ) SEP "|" "end" | match_key ltac_expr "with" OPT "|" LIST1 ( match_pattern "=>" ltac_expr ) SEP "|" "end" | "classical_left" | "classical_right" | "contradict" ident +| "dintuition" OPT ltac_expr | "discrR" +| "dtauto" | "easy" | "exfalso" | "inversion_sigma" @@ -1635,6 +1910,7 @@ simple_tactic: [ | "lra" | "nia" | "nra" +| "over" (* SSR plugin *) | "split_Rabs" | "split_Rmult" | "tauto" @@ -1685,20 +1961,25 @@ as_name: [ | "as" ident ] +oriented_rewriter: [ +| OPT [ "->" | "<-" ] rewriter +] + rewriter: [ | OPT natural OPT [ "?" | "!" ] constr_with_bindings_arg ] -oriented_rewriter: [ -| OPT [ "->" | "<-" ] rewriter +induction_clause_list: [ +| LIST1 induction_clause SEP "," OPT ( "using" one_term OPT ( "with" bindings ) ) OPT opt_clause ] induction_clause: [ | destruction_arg OPT as_or_and_ipat OPT eqn_ipat OPT opt_clause ] -induction_clause_list: [ -| LIST1 induction_clause SEP "," OPT ( "using" one_term OPT ( "with" bindings ) ) OPT opt_clause +opt_clause: [ +| "in" in_clause +| "at" occs_nums ] auto_using: [ @@ -2133,11 +2414,6 @@ clause_dft_all: [ | "in" in_clause ] -opt_clause: [ -| "in" in_clause -| "at" occs_nums -] - in_hyp_as: [ | "in" ident OPT as_ipat ] @@ -2165,12 +2441,6 @@ conversion: [ | one_term "at" occs_nums "with" one_term ] -firstorder_using: [ -| "using" qualid -| "using" qualid "," LIST1 qualid SEP "," -| "using" qualid qualid LIST0 qualid -] - func_scheme_def: [ | ident ":=" "Induction" "for" qualid "Sort" sort_family (* funind plugin *) ] @@ -2276,6 +2546,34 @@ tactic_atom: [ | "()" ] +ssrseqarg: [ +| ssrseqidx "[" ssrortacs "]" OPT ssrorelse (* SSR plugin *) +| OPT ssrseqidx ssrswap (* SSR plugin *) +| ltac_expr3 (* SSR plugin *) +] + +ssrseqidx: [ +| ident (* SSR plugin *) +| natural (* SSR plugin *) +] + +ssrorelse: [ +| "||" ltac_expr2 (* SSR plugin *) +] + +ssrswap: [ +| "first" (* SSR plugin *) +| "last" (* SSR plugin *) +] + +ssr_first_else: [ +| ssr_first OPT ssrorelse (* SSR plugin *) +] + +ssr_first: [ +| "[" LIST0 ltac_expr SEP "|" "]" LIST0 ssrintros (* SSR plugin *) +] + let_clause: [ | name ":=" ltac_expr | ident LIST1 name ":=" ltac_expr diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg index 6ddc6ba21e..d6790d008a 100644 --- a/plugins/firstorder/g_ground.mlg +++ b/plugins/firstorder/g_ground.mlg @@ -108,10 +108,6 @@ let pr_firstorder_using_raw _ _ _ = Pptactic.pr_auto_using pr_qualid let pr_firstorder_using_glob _ _ _ = Pptactic.pr_auto_using (Pputils.pr_or_var (fun x -> pr_global (snd x))) let pr_firstorder_using_typed _ _ _ = Pptactic.pr_auto_using pr_global -let warn_deprecated_syntax = - CWarnings.create ~name:"firstorder-deprecated-syntax" ~category:"deprecated" - (fun () -> Pp.strbrk "Deprecated syntax; use \",\" as separator") - } ARGUMENT EXTEND firstorder_using @@ -119,12 +115,7 @@ ARGUMENT EXTEND firstorder_using PRINTED BY { pr_firstorder_using_typed } RAW_PRINTED BY { pr_firstorder_using_raw } GLOB_PRINTED BY { pr_firstorder_using_glob } -| [ "using" reference(a) ] -> { [a] } -| [ "using" reference(a) "," ne_reference_list_sep(l,",") ] -> { a::l } -| [ "using" reference(a) reference(b) reference_list(l) ] -> { - warn_deprecated_syntax (); - a::b::l - } +| [ "using" ne_reference_list_sep(l,",") ] -> { l } | [ ] -> { [] } END -- cgit v1.2.3