Ltac2: support "head" reduction flag

Close #18209
coq · Nov 8, 2023 · 33b30c9 · 33b30c9
1 parent aaa8c94
commit 33b30c9
Show file tree

Hide file tree

Showing 12 changed files with 38 additions and 4 deletions.
diff --git a/doc/changelog/06-Ltac2-language/18273-ltac2-head-red.rst 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 <https://github.com/coq/coq/pull/18273>`_,
+  fixes `#18209 <https://github.com/coq/coq/issues/18209>`_,
+  by Gaëtan Gilbert).
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
@@ -1634,6 +1634,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
@@ -3179,6 +3179,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
@@ -1856,6 +1856,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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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;