diff options
Diffstat (limited to 'doc/tools/docgram/orderedGrammar')
| -rw-r--r-- | doc/tools/docgram/orderedGrammar | 369 |
1 files changed, 339 insertions, 30 deletions
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 7d773e3a5b..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 @@ -884,9 +1007,11 @@ command: [ | "Print" "Rings" (* ring plugin *) | "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" ) (* ring plugin *) | "Print" "Fields" (* ring plugin *) -| "Number" "Notation" qualid qualid qualid ":" scope_name OPT numeral_modifier -| "Numeral" "Notation" qualid qualid qualid ":" scope_name OPT numeral_modifier | "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 @@ -910,7 +1035,9 @@ command: [ | "Derive" "Dependent" "Inversion_clear" ident "with" one_term "Sort" sort_family | "Declare" "Left" "Step" one_term | "Declare" "Right" "Step" one_term -| "String" "Notation" qualid qualid qualid ":" scope_name +| "Number" "Notation" qualid qualid qualid OPT ( "(" LIST1 number_modifier SEP "," ")" ) ":" scope_name +| "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 ] | assumption_token OPT ( "Inline" OPT ( "(" natural ")" ) ) [ LIST1 ( "(" assumpt ")" ) | assumpt ] @@ -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,11 +1395,133 @@ field_mod: [ | "completeness" one_term (* ring plugin *) ] -numeral_modifier: [ +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 ")" ] +number_modifier: [ +| "warning" "after" bignat +| "abstract" "after" bignat +| number_string_via +] + +number_string_via: [ +| "via" qualid "mapping" "[" LIST1 [ qualid "=>" qualid | "[" qualid "]" "=>" qualid ] SEP "," "]" +] + hints_path: [ | "(" hints_path ")" | hints_path "*" @@ -1392,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 "]" @@ -1584,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 *) @@ -1611,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" @@ -1624,6 +1910,7 @@ simple_tactic: [ | "lra" | "nia" | "nra" +| "over" (* SSR plugin *) | "split_Rabs" | "split_Rmult" | "tauto" @@ -1674,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: [ @@ -1826,7 +2118,7 @@ q_rewriting: [ ] ltac2_oriented_rewriter: [ -| [ "->" | "<-" ] ltac2_rewriter (* Ltac2 plugin *) +| OPT [ "->" | "<-" ] ltac2_rewriter (* Ltac2 plugin *) ] ltac2_rewriter: [ @@ -2122,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 ] @@ -2154,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 *) ] @@ -2265,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 |