Add head reduction flags (lazy head beta etc)

doc/changelog/04-tactics/17503-redexpr.rst

@@ -0,0 +1,6 @@
+- **Added:**
+  :tacn:`lazy`, :tacn:`simpl` and :tacn:`cbn` and the associated :cmd:`Eval` and :tacn:`eval` reductions
+  learnt to do head reduction when given flag `head`
+  (eg `Eval lazy head in (fun x => Some ((fun y => y) x)) 0` produces `Some ((fun y => y) 0)`)
+  (`#17503 <https://github.com/coq/coq/pull/17503>`_,
+  by Gaëtan Gilbert).

doc/sphinx/proofs/writing-proofs/equality.rst

@@ -492,9 +492,10 @@ which reduction engine to use.  See :ref:`type-cast`.)  For example:
 
    .. prodn::
       reductions ::= {+ @reduction }
-      | @delta_reductions
+      | {? head } @delta_reductions
       reduction ::= beta
       | delta {? @delta_reductions }
+      | head
       | match
       | fix
       | cofix
@@ -506,6 +507,11 @@ which reduction engine to use.  See :ref:`type-cast`.)  For example:
    specified by name, all reductions are applied.  If any reductions are specified by name,
    then only the named reductions are applied.  The reductions include:
 
+   `head`
+     Do only head reduction, without going under binders.  Only
+     supported by :tacn:`simpl`, :tacn:`cbn` and :tacn:`lazy`.
+     If this is the only specified reduction, all other reductions are applied.
+
    `beta`
      :term:`beta-reduction` of functional application
 
@@ -577,7 +583,7 @@ which reduction engine to use.  See :ref:`type-cast`.)  For example:
    information about the constants it encounters and the unfolding decisions it
    makes.
 
-.. tacn:: simpl {? @delta_reductions } {? {| @reference_occs | @pattern_occs } } @simple_occurrences
+.. tacn:: simpl {? head } {? @delta_reductions } {? {| @reference_occs | @pattern_occs } } @simple_occurrences
 
    .. insertprodn reference_occs pattern_occs
 
@@ -891,7 +897,7 @@ Evaluation of a term can be performed with:
       | native_compute {? {| @reference_occs | @pattern_occs } }
       | red
       | hnf
-      | simpl {? @delta_reductions } {? {| @reference_occs | @pattern_occs } }
+      | simpl {? head } {? @delta_reductions } {? {| @reference_occs | @pattern_occs } }
       | cbn {? @reductions }
       | unfold {+, @reference_occs }
       | fold {+ @one_term }

doc/tools/docgram/common.edit_mlg

@@ -673,8 +673,8 @@ ltac2_branches: [
 ]
 
 strategy_flag: [
-| REPLACE OPT delta_flag
-| WITH delta_flag
+| REPLACE OPT "head" OPT delta_flag
+| WITH OPT "head" delta_flag
 (*| REPLACE LIST1 red_flags
 | WITH LIST1 red_flag*)
 | (* empty *)
@@ -980,8 +980,8 @@ simple_tactic: [
 | WITH "autounfold" hintbases OPT simple_occurrences
 | REPLACE "red" clause_dft_concl
 | WITH "red" simple_occurrences
-| REPLACE "simpl" OPT delta_flag OPT ref_or_pattern_occ clause_dft_concl
-| WITH "simpl" OPT delta_flag OPT ref_or_pattern_occ simple_occurrences
+| REPLACE "simpl" OPT "head" OPT delta_flag OPT ref_or_pattern_occ clause_dft_concl
+| WITH "simpl" OPT "head" OPT delta_flag OPT ref_or_pattern_occ simple_occurrences
 | REPLACE "hnf" clause_dft_concl
 | WITH "hnf" simple_occurrences
 | REPLACE "cbv" strategy_flag clause_dft_concl

doc/tools/docgram/fullGrammar

@@ -1779,7 +1779,7 @@ simple_tactic: [
 | "inversion" quantified_hypothesis "using" constr in_hyp_list
 | "red" clause_dft_concl
 | "hnf" clause_dft_concl
-| "simpl" delta_flag OPT ref_or_pattern_occ clause_dft_concl
+| "simpl" OPT "head" delta_flag OPT ref_or_pattern_occ clause_dft_concl
 | "cbv" strategy_flag clause_dft_concl
 | "cbn" strategy_flag clause_dft_concl
 | "lazy" strategy_flag clause_dft_concl
@@ -2432,6 +2432,7 @@ red_flag: [
 | "cofix"
 | "zeta"
 | "delta" delta_flag
+| "head"
 ]
 
 delta_flag: [
@@ -2442,13 +2443,13 @@ delta_flag: [
 
 strategy_flag: [
 | LIST1 red_flag
-| delta_flag
+| OPT "head" delta_flag
 ]
 
 red_expr: [
 | "red"
 | "hnf"
-| "simpl" delta_flag OPT ref_or_pattern_occ
+| "simpl" OPT "head" delta_flag OPT ref_or_pattern_occ
 | "cbv" strategy_flag
 | "cbn" strategy_flag
 | "lazy" strategy_flag

doc/tools/docgram/orderedGrammar

@@ -485,7 +485,7 @@ red_expr: [
 | "native_compute" OPT [ reference_occs | pattern_occs ]
 | "red"
 | "hnf"
-| "simpl" OPT delta_reductions OPT [ reference_occs | pattern_occs ]
+| "simpl" OPT "head" OPT delta_reductions OPT [ reference_occs | pattern_occs ]
 | "cbn" OPT reductions
 | "unfold" LIST1 reference_occs SEP ","
 | "fold" LIST1 one_term
@@ -495,12 +495,13 @@ red_expr: [
 
 reductions: [
 | LIST1 reduction
-| delta_reductions
+| OPT "head" delta_reductions
 ]
 
 reduction: [
 | "beta"
 | "delta" OPT delta_reductions
+| "head"
 | "match"
 | "fix"
 | "cofix"
@@ -1527,7 +1528,7 @@ simple_tactic: [
 | "inversion" [ ident | natural ] "using" one_term OPT ( "in" LIST1 ident )
 | "red" simple_occurrences
 | "hnf" simple_occurrences
-| "simpl" OPT delta_reductions OPT [ reference_occs | pattern_occs ] simple_occurrences
+| "simpl" OPT "head" OPT delta_reductions OPT [ reference_occs | pattern_occs ] simple_occurrences
 | "cbv" OPT reductions simple_occurrences
 | "cbn" OPT reductions simple_occurrences
 | "lazy" OPT reductions simple_occurrences

plugins/funind/recdef.ml

@@ -161,7 +161,8 @@ let simpl_iter clause =
        ; rCofix = true
        ; rZeta = true
        ; rDelta = false
-       ; rConst = [EvalConstRef (const_of_ref (delayed_force iter_ref))] })
+       ; rConst = [EvalConstRef (const_of_ref (delayed_force iter_ref))]
+       ; rStrength = Norm })
     clause
 
 (* Others ugly things ... *)

plugins/ltac/g_tactic.mlg

@@ -30,7 +30,9 @@ open Locus
 open Pcoq
 
 
-let all_with delta = Redops.make_red_flag [FBeta;FMatch;FFix;FCofix;FZeta;delta]
+let all_with ~head delta =
+  let all = [FBeta;FMatch;FFix;FCofix;FZeta;delta] in
+  Redops.make_red_flag (if head then FHead :: all else all)
 
 let err () = raise Gramlib.Stream.Failure
 
@@ -348,6 +350,7 @@ GRAMMAR EXTEND Gram
       | IDENT "cofix" -> { [FCofix] }
       | IDENT "zeta" -> { [FZeta] }
       | IDENT "delta"; d = delta_flag -> { [d] }
+      | IDENT "head" -> { [FHead] }
     ] ]
   ;
   delta_flag:
@@ -358,17 +361,18 @@ GRAMMAR EXTEND Gram
   ;
   strategy_flag:
     [ [ s = LIST1 red_flag -> { Redops.make_red_flag (List.flatten s) }
-      | d = delta_flag -> { all_with d }
+      | h = OPT [ IDENT "head" -> { () } ]; d = delta_flag -> { all_with ~head:(Option.has_some h) d }
     ] ]
   ;
   red_expr:
     [ [ IDENT "red" -> { Red false }
       | IDENT "hnf" -> { Hnf }
-      | IDENT "simpl"; d = delta_flag; po = OPT ref_or_pattern_occ -> { Simpl (all_with d,po) }
+      | IDENT "simpl"; h = OPT [ IDENT "head" -> { () } ];
+        d = delta_flag; po = OPT ref_or_pattern_occ -> { Simpl (all_with ~head:(Option.has_some h) d,po) }
       | IDENT "cbv"; s = strategy_flag -> { Cbv s }
       | IDENT "cbn"; s = strategy_flag -> { Cbn s }
       | IDENT "lazy"; s = strategy_flag -> { Lazy s }
-      | IDENT "compute"; delta = delta_flag -> { Cbv (all_with delta) }
+      | IDENT "compute"; delta = delta_flag -> { Cbv (all_with ~head:false delta) }
       | IDENT "vm_compute"; po = OPT ref_or_pattern_occ -> { CbvVm po }
       | IDENT "native_compute"; po = OPT ref_or_pattern_occ -> { CbvNative po }
       | IDENT "unfold"; ul = LIST1 unfold_occ SEP "," -> { Unfold ul }
@@ -677,16 +681,17 @@ GRAMMAR EXTEND Gram
           { CAst.make ~loc @@ TacAtom (TacReduce (Red false, cl)) }
       | IDENT "hnf"; cl = clause_dft_concl ->
           { CAst.make ~loc @@ TacAtom (TacReduce (Hnf, cl)) }
-      | IDENT "simpl"; d = delta_flag; po = OPT ref_or_pattern_occ; cl = clause_dft_concl ->
-          { CAst.make ~loc @@ TacAtom (TacReduce (Simpl (all_with d, po), cl)) }
+      | IDENT "simpl"; h = OPT [ IDENT "head" -> { () } ]; d = delta_flag;
+        po = OPT ref_or_pattern_occ; cl = clause_dft_concl ->
+          { CAst.make ~loc @@ TacAtom (TacReduce (Simpl (all_with ~head:(Option.has_some h) d, po), cl)) }
       | IDENT "cbv"; s = strategy_flag; cl = clause_dft_concl ->
           { CAst.make ~loc @@ TacAtom (TacReduce (Cbv s, cl)) }
       | IDENT "cbn"; s = strategy_flag; cl = clause_dft_concl ->
           { CAst.make ~loc @@ TacAtom (TacReduce (Cbn s, cl)) }
       | IDENT "lazy"; s = strategy_flag; cl = clause_dft_concl ->
           { CAst.make ~loc @@ TacAtom (TacReduce (Lazy s, cl)) }
       | IDENT "compute"; delta = delta_flag; cl = clause_dft_concl ->
-          { CAst.make ~loc @@ TacAtom (TacReduce (Cbv (all_with delta), cl)) }
+          { CAst.make ~loc @@ TacAtom (TacReduce (Cbv (all_with ~head:false delta), cl)) }
       | IDENT "vm_compute"; po = OPT ref_or_pattern_occ; cl = clause_dft_concl ->
           { CAst.make ~loc @@ TacAtom (TacReduce (CbvVm po, cl)) }
       | IDENT "native_compute"; po = OPT ref_or_pattern_occ; cl = clause_dft_concl ->

plugins/ltac2/tac2quote.ml

@@ -379,7 +379,7 @@ let make_red_flag l =
   in
   add_flag
     {rBeta = false; rMatch = false; rFix = false; rCofix = false;
-     rZeta = false; rDelta = false; rConst = []}
+     rZeta = false; rDelta = false; rConst = []; rStrength = Norm; }
     l
 
 let of_reference r =

plugins/ltac2/tac2stdlib.ml

@@ -63,6 +63,7 @@ let clause = make_to_repr to_clause
 let to_red_flag v = match Value.to_tuple v with
 | [| beta; iota; fix; cofix; zeta; delta; const |] ->
   {
+    rStrength = Norm; (* specifying rStrength is not yet supported *)
     rBeta = Value.to_bool beta;
     rMatch = Value.to_bool iota;
     rFix = Value.to_bool fix;

plugins/ssr/ssrcommon.ml

@@ -1194,7 +1194,7 @@ let tclFULL_BETAIOTA = Goal.enter begin fun gl ->
   let r, _ = Redexpr.reduction_of_red_expr (Goal.env gl)
     Genredexpr.(Lazy {
       rBeta=true; rMatch=true; rFix=true; rCofix=true;
-      rZeta=false; rDelta=false; rConst=[]}) in
+      rZeta=false; rDelta=false; rConst=[]; rStrength=Norm}) in
   Tactics.e_reduct_in_concl ~cast:false ~check:false (r,Constr.DEFAULTcast)
 end
 

tactics/genredexpr.mli

@@ -20,10 +20,15 @@ type 'a red_atom =
   | FZeta
   | FConst of 'a list
   | FDeltaBut of 'a list
+  | FHead
 
 (** This list of atoms is immediately converted to a [glob_red_flag] *)
 
+type strength = Norm | Head
+(* someday we may add NotUnderBinders *)
+
 type 'a glob_red_flag = {
+  rStrength : strength;
   rBeta : bool;
   rMatch : bool;
   rFix : bool;

tactics/redexpr.ml

@@ -131,7 +131,7 @@ type red_expr =
     (constr, evaluable_global_reference, constr_pattern) red_expr_gen
 
 type red_expr_val =
-  (constr, evaluable_global_reference, constr_pattern, RedFlags.reds) red_expr_gen0
+  (constr, evaluable_global_reference, constr_pattern, strength * RedFlags.reds) red_expr_gen0
 
 let make_flag_constant = function
   | EvalVarRef id -> fVAR id
@@ -157,7 +157,8 @@ let make_flag env f =
         List.fold_right
           (fun v red -> red_add red (make_flag_constant v))
           f.rConst red
-  in red
+  in
+  f.rStrength, red
 
 (* table of custom reductino fonctions, not synchronized,
    filled via ML calls to [declare_reduction] *)
@@ -226,7 +227,7 @@ let rec eval_red_expr env = function
   let () =
     if not (simplIsCbn () || List.is_empty f.rConst) then
       warn_simpl_unfolding_modifiers () in
-  let f = if simplIsCbn () then make_flag env f else RedFlags.all (* dummy *) in
+  let f = if simplIsCbn () then make_flag env f else f.rStrength, RedFlags.all (* dummy *) in
   Simpl (f, o)
 | Cbv f -> Cbv (make_flag env f)
 | Cbn f -> Cbn (make_flag env f)
@@ -243,13 +244,22 @@ let reduction_of_red_expr_val = function
       if internal then (e_red try_red_product,DEFAULTcast)
       else (e_red red_product,DEFAULTcast)
   | Hnf -> (e_red hnf_constr,DEFAULTcast)
-  | Simpl (f,o) ->
-     let am = if simplIsCbn () then Cbn.norm_cbn f else simpl in
+  | Simpl ((w,f),o) ->
+    let am = match w, simplIsCbn () with
+      | Norm, true -> Cbn.norm_cbn f
+      | Norm, false -> simpl
+      | Head, true -> Cbn.whd_cbn f
+      | Head, false -> whd_simpl
+    in
      (contextuallize am o,DEFAULTcast)
-  | Cbv f -> (e_red (cbv_norm_flags f),DEFAULTcast)
-  | Cbn f ->
-     (e_red (Cbn.norm_cbn f), DEFAULTcast)
-  | Lazy f -> (e_red (clos_norm_flags f),DEFAULTcast)
+  | Cbv (Norm, f) -> (e_red (cbv_norm_flags f),DEFAULTcast)
+  | Cbv (Head, _) -> CErrors.user_err Pp.(str "cbv does not support head-only reduction.")
+  | Cbn (w,f) ->
+    let cbn = match w with Norm -> Cbn.norm_cbn | Head -> Cbn.whd_cbn in
+     (e_red (cbn f), DEFAULTcast)
+  | Lazy (w,f) ->
+    let redf = match w with Norm -> clos_norm_flags | Head -> clos_whd_flags in
+    (e_red (redf f),DEFAULTcast)
   | Unfold ubinds -> (e_red (unfoldn (List.map out_with_occurrences ubinds)),DEFAULTcast)
   | Fold cl -> (e_red (fold_commands cl),DEFAULTcast)
   | Pattern lp -> (pattern_occs (List.map out_with_occurrences lp),DEFAULTcast)

tactics/redops.ml

@@ -12,9 +12,15 @@ open Genredexpr
 
 let union_consts l1 l2 = Util.List.union (=) l1 l2 (* FIXME *)
 
+
+let all_flags =
+  {rBeta = true; rMatch = true; rFix = true; rCofix = true;
+   rZeta = true; rDelta = true; rConst = []; rStrength = Norm; }
+
 let make_red_flag l =
   let rec add_flag red = function
     | [] -> red
+    | FHead :: lf -> add_flag { red with rStrength = Head } lf
     | FBeta :: lf -> add_flag { red with rBeta = true } lf
     | FMatch :: lf -> add_flag { red with rMatch = true } lf
     | FFix :: lf -> add_flag { red with rFix = true } lf
@@ -35,13 +41,12 @@ let make_red_flag l =
   in
   add_flag
     {rBeta = false; rMatch = false; rFix = false; rCofix = false;
-     rZeta = false; rDelta = false; rConst = []}
+     rZeta = false; rDelta = false; rConst = []; rStrength = Norm; }
     l
 
-
-let all_flags =
-  {rBeta = true; rMatch = true; rFix = true; rCofix = true;
-   rZeta = true; rDelta = true; rConst = []}
+let make_red_flag = function
+  | [FHead] -> { all_flags with rStrength = Head }
+  | l -> make_red_flag l
 
 (** Mapping [red_expr_gen] *)
 

test-suite/output/reduction.out

@@ -2,3 +2,30 @@
      : nat
      = n + 0
      : nat
+     = S (1 + 2)
+     : nat
+     = S (1 + 2)
+     : nat
+     = S
+         ((fix add (n m : nat) {struct n} : nat :=
+             match n with
+             | 0 => m
+             | S p => S (add p m)
+             end) 1 2)
+     : nat
+     = (fix add (n m : nat) {struct n} : nat :=
+          match n with
+          | 0 => m
+          | S p => S (add p m)
+          end) 2 2
+     : nat
+     = S (1 + (2 + 2))
+     : nat
+     = S (1 + 2 + 2)
+     : nat
+     = ignore (fun x : nat => 1 + x)
+     : unit
+     = ignore (fun x : nat => 1 + x)
+     : unit
+     = ignore (fun x : nat => 1 + x)
+     : unit

test-suite/output/reduction.v

@@ -11,3 +11,17 @@ Eval simpl in (fix plus (n m : nat) {struct n} : nat :=
 
 Eval hnf in match (plus (S n) O) with S n => n | _ => O end.
 
+Eval simpl head in 2 + 2.
+Eval cbn head in 2 + 2.
+Eval lazy head in 2 + 2.
+
+Eval lazy head delta in 2 + 2.
+
+Eval simpl head in 2 + (2 + 2).
+
+Eval simpl head in (2 + 2) + 2.
+
+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).