diff --git a/doc/changelog/06-Ltac2-language/18273-ltac2-head-red.rst b/doc/changelog/06-Ltac2-language/18273-ltac2-head-red.rst new file mode 100644 index 000000000000..7c504d58b3b0 --- /dev/null +++ b/doc/changelog/06-Ltac2-language/18273-ltac2-head-red.rst @@ -0,0 +1,5 @@ +- **Changed:** + `Ltac2.Std.red_flags` added field `rStrength` to support head-only reduction + (`#18273 `_, + fixes `#18209 `_, + by Gaëtan Gilbert). diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 2a3c2c617deb..97c1d404c4f4 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -1643,6 +1643,7 @@ Here is the syntax for the :n:`q_*` nonterminals: | cofix | zeta | delta {? @ltac2_delta_reductions } + | head ltac2_delta_reductions ::= {? - } [ {+ @refglobal } ] .. insertprodn refglobal refglobal diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 877f96778708..06bd1cb77212 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -3190,6 +3190,7 @@ ltac2_red_flag: [ | "cofix" (* ltac2 plugin *) | "zeta" (* ltac2 plugin *) | "delta" G_LTAC2_delta_flag (* ltac2 plugin *) +| "head" (* ltac2 plugin *) ] refglobal: [ diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index efc77699a4b4..97eb87e34cab 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -1858,6 +1858,7 @@ ltac2_red_flag: [ | "cofix" (* ltac2 plugin *) | "zeta" (* ltac2 plugin *) | "delta" OPT ltac2_delta_reductions (* ltac2 plugin *) +| "head" (* ltac2 plugin *) ] ltac2_delta_reductions: [ diff --git a/plugins/ltac2/g_ltac2.mlg b/plugins/ltac2/g_ltac2.mlg index 32424e9a8ba4..5dbce598423c 100644 --- a/plugins/ltac2/g_ltac2.mlg +++ b/plugins/ltac2/g_ltac2.mlg @@ -773,6 +773,7 @@ GRAMMAR EXTEND Gram | IDENT "cofix" -> { CAst.make ~loc @@ QCofix } | IDENT "zeta" -> { CAst.make ~loc @@ QZeta } | IDENT "delta"; d = delta_flag -> { d } + | IDENT "head" -> { CAst.make ~loc @@ QHead } ] ] ; refglobal: diff --git a/plugins/ltac2/tac2qexpr.mli b/plugins/ltac2/tac2qexpr.mli index aac32cfb95d4..5e072237ddab 100644 --- a/plugins/ltac2/tac2qexpr.mli +++ b/plugins/ltac2/tac2qexpr.mli @@ -128,6 +128,7 @@ type red_flag_r = | QZeta | QConst of reference or_anti list CAst.t | QDeltaBut of reference or_anti list CAst.t +| QHead type red_flag = red_flag_r CAst.t diff --git a/plugins/ltac2/tac2quote.ml b/plugins/ltac2/tac2quote.ml index 2fb529456e93..3295942ae7ac 100644 --- a/plugins/ltac2/tac2quote.ml +++ b/plugins/ltac2/tac2quote.ml @@ -357,6 +357,7 @@ let make_red_flag l = | [] -> red | {v=flag} :: lf -> let red = match flag with + | QHead -> { red with rStrength = Head } | QBeta -> { red with rBeta = true } | QMatch -> { red with rMatch = true } | QFix -> { red with rFix = true } @@ -388,10 +389,18 @@ let of_reference r = in of_anti of_ref r +let of_strength ?loc s = + let s = let open Genredexpr in match s with + | Norm -> std_core "Norm" + | Head -> std_core "Head" + in + constructor ?loc s [] + let of_strategy_flag {loc;v=flag} = let open Genredexpr in let flag = make_red_flag flag in CAst.make ?loc @@ CTacRec (None, [ + std_proj "rStrength", of_strength ?loc flag.rStrength; std_proj "rBeta", of_bool ?loc flag.rBeta; std_proj "rMatch", of_bool ?loc flag.rMatch; std_proj "rFix", of_bool ?loc flag.rFix; diff --git a/plugins/ltac2/tac2stdlib.ml b/plugins/ltac2/tac2stdlib.ml index 775923e9c3c3..324f873fe62a 100644 --- a/plugins/ltac2/tac2stdlib.ml +++ b/plugins/ltac2/tac2stdlib.ml @@ -60,10 +60,15 @@ let to_clause v = match Value.to_tuple v with let clause = make_to_repr to_clause +let to_red_strength = function + | ValInt 0 -> Norm + | ValInt 1 -> Head + | _ -> assert false + let to_red_flag v = match Value.to_tuple v with -| [| beta; iota; fix; cofix; zeta; delta; const |] -> +| [| strength; beta; iota; fix; cofix; zeta; delta; const |] -> { - rStrength = Norm; (* specifying rStrength is not yet supported *) + rStrength = to_red_strength strength; rBeta = Value.to_bool beta; rMatch = Value.to_bool iota; rFix = Value.to_bool fix; diff --git a/test-suite/output/reduction.out b/test-suite/output/reduction.out index 19f7dcaaffc5..909221eb47b0 100644 --- a/test-suite/output/reduction.out +++ b/test-suite/output/reduction.out @@ -29,3 +29,5 @@ : unit = ignore (fun x : nat => 1 + x) : unit +- : constr = constr:(4) +- : constr = constr:(2 + 2) diff --git a/test-suite/output/reduction.v b/test-suite/output/reduction.v index 5263ed40d493..c94a01ad7b2c 100644 --- a/test-suite/output/reduction.v +++ b/test-suite/output/reduction.v @@ -25,3 +25,8 @@ Axiom ignore : forall {T}, T -> unit. Eval simpl head in ignore (fun x => 1 + x). Eval cbn head in ignore (fun x => 1 + x). Eval lazy head in ignore (fun x => 1 + x). + +Require Import Ltac2.Ltac2. + +Ltac2 Eval eval lazy in (2 + 2). +Ltac2 Eval eval lazy head in (2 + 2). diff --git a/user-contrib/Ltac2/RedFlags.v b/user-contrib/Ltac2/RedFlags.v index 999fb1f9cc1a..9e26b977a349 100644 --- a/user-contrib/Ltac2/RedFlags.v +++ b/user-contrib/Ltac2/RedFlags.v @@ -19,12 +19,12 @@ End Notations. Ltac2 none := { rBeta := false; rMatch := false; rFix := false; rCofix := false; - rZeta := false; rDelta := false; rConst := []; + rZeta := false; rDelta := false; rConst := []; rStrength := Norm; }. Ltac2 all : t := { rBeta := true; rMatch := true; rFix := true; rCofix := true; - rZeta := true; rDelta := true; rConst := []; + rZeta := true; rDelta := true; rConst := []; rStrength := Norm; }. Ltac2 beta : t := red_flags:(beta). diff --git a/user-contrib/Ltac2/Std.v b/user-contrib/Ltac2/Std.v index 3ea8a6c44ca7..bc2d00db72d7 100644 --- a/user-contrib/Ltac2/Std.v +++ b/user-contrib/Ltac2/Std.v @@ -43,7 +43,10 @@ Ltac2 Type reference := [ | ConstructRef (constructor) ]. +Ltac2 Type strength := [ Norm | Head ]. + Ltac2 Type red_flags := { + rStrength : strength; rBeta : bool; rMatch : bool; rFix : bool;