From 6c416d50c71d113afbfdb477d8486975459ee1db Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Thu, 22 Feb 2024 16:37:14 +0100 Subject: [PATCH] Make focus command and goal selection for query commands independent of ltac1 Fix #18351 --- .../18707-vernac-focus.rst | 6 ++ doc/tools/docgram/common.edit_mlg | 34 +++----- doc/tools/docgram/fullGrammar | 61 ++++++------- plugins/ltac/g_ltac.mlg | 5 -- test-suite/bugs/bug_18351.v | 10 +++ vernac/g_vernac.mlg | 87 +++++++++---------- 6 files changed, 99 insertions(+), 104 deletions(-) create mode 100644 doc/changelog/08-vernac-commands-and-options/18707-vernac-focus.rst create mode 100644 test-suite/bugs/bug_18351.v diff --git a/doc/changelog/08-vernac-commands-and-options/18707-vernac-focus.rst b/doc/changelog/08-vernac-commands-and-options/18707-vernac-focus.rst new file mode 100644 index 0000000000000..592690c00cddf --- /dev/null +++ b/doc/changelog/08-vernac-commands-and-options/18707-vernac-focus.rst @@ -0,0 +1,6 @@ +- **Changed:** + focus commands such as `1:{` and goal selection for query commands such as `1: Check` + do not need `Classic` (Ltac1) proof mode to function. In particular they function in Ltac2 mode + (`#18707 `_, + fixes `#18351 `_, + by Gaëtan Gilbert). diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 1eff25b8ffc82..6babe77a66e0b 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -836,10 +836,6 @@ STRING: [ (* added productions *) -command_entry: [ -| noedit_mode -] - DELETE: [ | tactic_then_locality ] @@ -1738,18 +1734,12 @@ let_clause: [ tactic_mode: [ (* todo: make sure to document this production! *) (* deleting to allow splicing query_command into command *) -| DELETE OPT toplevel_selector query_command | DELETE OPT ltac_selector OPT ltac_info tactic ltac_use_default | DELETE "par" ":" OPT ltac_info tactic ltac_use_default (* Ignore attributes (none apply) and "...". *) | ltac_info tactic | MOVETO command ltac_info tactic | DELETE command -| REPLACE OPT toplevel_selector "{" -(* semantically restricted *) -| WITH OPT ( [ natural | "[" ident "]" ] ":" ) "{" -| MOVETO simple_tactic OPT ( [ natural | "[" ident "]" ] ":" ) "{" -| DELETE simple_tactic | DELETENT ] @@ -1808,6 +1798,18 @@ vernac_aux: [ | DELETENT ] +subprf: [ +| REPLACE OPT toplevel_selector_temp "{" +(* semantically restricted *) +| WITH OPT ( [ natural | "[" ident "]" ] ":" ) "{" +| MOVEALLBUT simple_tactic +| OPT toplevel_selector_temp; query_command +] + +subprf: [ +| DELETENT +] + command: [ | gallina | gallina_ext @@ -2148,16 +2150,6 @@ simple_binding: [ | DELETE "(" natural ":=" lconstr ")" ] - -subprf: [ -| MOVEALLBUT simple_tactic -| "{" (* should be removed. See https://github.com/coq/coq/issues/12004 *) -] - -subprf: [ -| DELETENT -] - ltac2_expr: [ | DELETE _ltac2_expr ] @@ -2263,7 +2255,6 @@ ne_rewstrategy1_list_sep_semicolon: [ SPLICE: [ | ne_rewstrategy1_list_sep_semicolon | clause -| noedit_mode | match_list | match_context_list | IDENT @@ -2515,7 +2506,6 @@ SPLICE: [ | syntax | vernac_control | vernac_toplevel -| command_entry | ltac_builtins | ltac_constructs | ltac2_constructs diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 317dbd030eca0..072fd47cd9d20 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -791,14 +791,11 @@ vernac_aux: [ | command_entry ] -noedit_mode: [ -| query_command -] - subprf: [ | BULLET -| "{" +| OPT toplevel_selector "{" | "}" +| OPT toplevel_selector query_command ] gallina: [ @@ -1282,6 +1279,27 @@ simple_reserv: [ | LIST1 identref ":" lconstr ] +range_selector: [ +| natural "-" natural +| natural +] + +range_selector_or_nth: [ +| natural "-" natural OPT [ "," LIST1 range_selector SEP "," ] +| natural OPT [ "," LIST1 range_selector SEP "," ] +] + +goal_selector: [ +| range_selector_or_nth +| test_bracket_ident "[" ident "]" +] + +toplevel_selector: [ +| goal_selector ":" +| "!" ":" +| "all" ":" +] + query_command: [ | "Eval" red_expr "in" lconstr "." | "Compute" lconstr "." @@ -1543,27 +1561,6 @@ binder_interp: [ | "as" "strict" "pattern" ] -range_selector: [ -| natural "-" natural -| natural -] - -range_selector_or_nth: [ -| natural "-" natural OPT [ "," LIST1 range_selector SEP "," ] -| natural OPT [ "," LIST1 range_selector SEP "," ] -] - -goal_selector: [ -| range_selector_or_nth -| test_bracket_ident "[" ident "]" -] - -toplevel_selector: [ -| goal_selector ":" -| "!" ":" -| "all" ":" -] - simple_tactic: [ | "btauto" | "congruence" OPT natural @@ -2235,13 +2232,6 @@ tactic: [ | ltac_expr5 ] -tactic_mode: [ -| OPT toplevel_selector G_vernac.query_command -| OPT toplevel_selector "{" -| OPT ltac_selector OPT ltac_info tactic ltac_use_default -| "par" ":" OPT ltac_info tactic ltac_use_default -] - ltac_selector: [ | toplevel_selector ] @@ -2255,6 +2245,11 @@ ltac_use_default: [ | "..." ] +tactic_mode: [ +| OPT ltac_selector OPT ltac_info tactic ltac_use_default +| "par" ":" OPT ltac_info tactic ltac_use_default +] + ltac_tactic_level: [ | "(" "at" "level" natural ")" ] diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index c840ab3547e25..e4eaff54fe290 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -282,11 +282,6 @@ GRAMMAR EXTEND Gram tactic: [ [ tac = ltac_expr -> { tac } ] ] ; - - tactic_mode: - [ [ g = OPT toplevel_selector; tac = G_vernac.query_command -> { Vernacexpr.VernacSynPure (tac g) } - | g = OPT toplevel_selector; "{" -> { Vernacexpr.VernacSynPure (Vernacexpr.VernacSubproof g) } ] ] - ; command: TOP [ [ IDENT "Proof"; "with"; ta = Pltac.tactic; l = OPT [ IDENT "using"; l = G_vernac.section_subset_expr -> { l } ] -> diff --git a/test-suite/bugs/bug_18351.v b/test-suite/bugs/bug_18351.v new file mode 100644 index 0000000000000..6e19705d7b6bd --- /dev/null +++ b/test-suite/bugs/bug_18351.v @@ -0,0 +1,10 @@ +Require Import Ltac2.Ltac2. + +Set Default Goal Selector "!". + +Goal True /\ True. + split. + Fail exact I. (* not focused *) + 1:{ exact I. } + exact I. +Qed. diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index f14577f4ee257..d023ce57aa0e7 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -170,14 +170,13 @@ GRAMMAR EXTEND Gram vernac_aux: LAST [ [ prfcom = command_entry -> { prfcom } ] ] ; - noedit_mode: - [ [ c = query_command -> { VernacSynPure (c None) } ] ] - ; subprf: [ [ s = BULLET -> { VernacBullet (make_bullet s) } - | "{" -> { VernacSubproof None } + | g = OPT toplevel_selector; "{" -> { VernacSubproof g } | "}" -> { VernacEndSubproof } + (* query_command needs to be here to factor with VernacSubproof *) + | g = OPT toplevel_selector; c = query_command -> { c g } ] ] ; @@ -970,6 +969,45 @@ GRAMMAR EXTEND Gram END +{ + +(* Hack to parse "[ id" without dropping [ *) +let test_bracket_ident = + let open Pcoq.Lookahead in + to_entry "test_bracket_ident" begin + lk_kw "[" >> lk_ident + end + +} + +GRAMMAR EXTEND Gram + GLOBAL: toplevel_selector goal_selector; + range_selector: + [ [ n = natural ; "-" ; m = natural -> { (n, m) } + | n = natural -> { (n, n) } ] ] + ; + (* We unfold a range selectors list once so that we can make a special case + * for a unique SelectNth selector. *) + range_selector_or_nth: + [ [ n = natural ; "-" ; m = natural; + l = OPT [","; l = LIST1 range_selector SEP "," -> { l } ] -> + { Goal_select.SelectList ((n, m) :: Option.default [] l) } + | n = natural; + l = OPT [","; l = LIST1 range_selector SEP "," -> { l } ] -> + { let open Goal_select in + Option.cata (fun l -> SelectList ((n, n) :: l)) (SelectNth n) l } ] ] + ; + goal_selector: + [ [ l = range_selector_or_nth -> { l } + | test_bracket_ident; "["; id = ident; "]" -> { Goal_select.SelectId id } ] ] + ; + toplevel_selector: + [ [ sel = goal_selector; ":" -> { sel } + | "!"; ":" -> { Goal_select.SelectAlreadyFocused } + | IDENT "all"; ":" -> { Goal_select.SelectAll } ] ] + ; +END + GRAMMAR EXTEND Gram GLOBAL: command query_command coercion_class gallina_ext search_query search_queries; @@ -1051,7 +1089,7 @@ GRAMMAR EXTEND Gram | IDENT "Remove"; table = IDENT; v = LIST1 table_value -> { VernacSynPure (VernacRemoveOption ([table], v)) } ]] ; - query_command: (* TODO: rapprocher Eval et Check *) + query_command: [ [ IDENT "Eval"; r = red_expr; "in"; c = lconstr; "." -> { fun g -> VernacCheckMayEval (Some r, g, c) } | IDENT "Compute"; c = lconstr; "." -> @@ -1383,42 +1421,3 @@ GRAMMAR EXTEND Gram | "as"; IDENT "strict"; IDENT "pattern" -> { Notation_term.AsStrictPattern } ] ] ; END - -{ - -(* Hack to parse "[ id" without dropping [ *) -let test_bracket_ident = - let open Pcoq.Lookahead in - to_entry "test_bracket_ident" begin - lk_kw "[" >> lk_ident - end - -} - -GRAMMAR EXTEND Gram - GLOBAL: toplevel_selector goal_selector; - range_selector: - [ [ n = natural ; "-" ; m = natural -> { (n, m) } - | n = natural -> { (n, n) } ] ] - ; - (* We unfold a range selectors list once so that we can make a special case - * for a unique SelectNth selector. *) - range_selector_or_nth: - [ [ n = natural ; "-" ; m = natural; - l = OPT [","; l = LIST1 range_selector SEP "," -> { l } ] -> - { Goal_select.SelectList ((n, m) :: Option.default [] l) } - | n = natural; - l = OPT [","; l = LIST1 range_selector SEP "," -> { l } ] -> - { let open Goal_select in - Option.cata (fun l -> SelectList ((n, n) :: l)) (SelectNth n) l } ] ] - ; - goal_selector: - [ [ l = range_selector_or_nth -> { l } - | test_bracket_ident; "["; id = ident; "]" -> { Goal_select.SelectId id } ] ] - ; - toplevel_selector: - [ [ sel = goal_selector; ":" -> { sel } - | "!"; ":" -> { Goal_select.SelectAlreadyFocused } - | IDENT "all"; ":" -> { Goal_select.SelectAll } ] ] - ; -END