Merge PR #11955: Use the kernel machine in whd_betaiota_deltazeta_for_iota_state

Reviewed-by: SkySkimmer
Reviewed-by: mattam82

4 files changed, 43 insertions, 16 deletions

diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 1316dfe069..c31cdae6f5 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -678,6 +678,8 @@ let rec zip m stk =
 
 let fapp_stack (m,stk) = zip m stk
 
+let term_of_process c stk = term_of_fconstr (zip c stk)
+
 (*********************************************************************)
 
 (* The assertions in the functions below are granted because they are
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index 9e94248113..79092813bc 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -227,6 +227,10 @@ val kni: clos_infos -> clos_tab -> fconstr -> stack -> fconstr * stack
 val knr: clos_infos -> clos_tab -> fconstr -> stack -> fconstr * stack
 val kl : clos_infos -> clos_tab -> fconstr -> constr
 
+val zip : fconstr -> stack -> fconstr
+
+val term_of_process : fconstr -> stack -> constr
+
 val to_constr : lift -> fconstr -> constr
 
 (** End of cbn debug section i*)
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 8bb268a92e..01f3537a7f 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1746,26 +1746,46 @@ let is_sort env sigma t =
 let whd_betaiota_deltazeta_for_iota_state ts env sigma s =
   let refold = false in
   let tactic_mode = false in
-  let rec whrec csts s =
-    let (t, stack as s),csts' = whd_state_gen ~csts ~refold ~tactic_mode CClosure.betaiota env sigma s in
+  let all' = CClosure.RedFlags.red_add_transparent CClosure.all ts in
+  (* Unset the sharing flag to get a call-by-name reduction. This matters for
+     the shape of the generated term. *)
+  let env' = Environ.set_typing_flags { (Environ.typing_flags env) with Declarations.share_reduction = false } env in
+  let whd_opt c =
+    let open CClosure in
+    let evars ev = safe_evar_value sigma ev in
+    let infos = create_clos_infos ~evars all' env' in
+    let tab = create_tab () in
+    let c = inject (EConstr.Unsafe.to_constr (Stack.zip sigma c)) in
+    let (c, stk) = whd_stack infos tab c [] in
+    match fterm_of c with
+    | (FConstruct _ | FCoFix _) ->
+      (* Non-neutral normal, can trigger reduction below *)
+      let c = EConstr.of_constr (term_of_process c stk) in
+      Some (decompose_app_vect sigma c)
+    | _ -> None
+  in
+  let rec whrec s =
+    let (t, stack as s), _ = whd_state_gen ~refold ~tactic_mode CClosure.betaiota env sigma s in
     match Stack.strip_app stack with
       |args, (Stack.Case _ :: _ as stack') ->
-        let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' ~refold ~tactic_mode
-          (CClosure.RedFlags.red_add_transparent CClosure.all ts) env sigma (t,args) in
-        if reducible_mind_case sigma t_o then whrec csts_o (t_o, stack_o@stack') else s,csts'
+        begin match whd_opt (t, args) with
+        | Some (t_o, args) when reducible_mind_case sigma t_o -> whrec (t_o, Stack.append_app args stack')
+        | (Some _ | None) -> s
+        end
       |args, (Stack.Fix _ :: _ as stack') ->
-        let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' ~refold ~tactic_mode
-          (CClosure.RedFlags.red_add_transparent CClosure.all ts) env sigma (t,args) in
-        if isConstruct sigma t_o then whrec csts_o (t_o, stack_o@stack') else s,csts'
+        begin match whd_opt (t, args) with
+        | Some (t_o, args) when isConstruct sigma t_o -> whrec (t_o, Stack.append_app args stack')
+        | (Some _ | None) -> s
+        end
       |args, (Stack.Proj (p,_) :: stack'') ->
-        let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' ~refold ~tactic_mode
-          (CClosure.RedFlags.red_add_transparent CClosure.all ts) env sigma (t,args) in
-        if isConstruct sigma t_o then
-          whrec Cst_stack.empty (Stack.nth stack_o (Projection.npars p + Projection.arg p), stack'')
-        else s,csts'
-      |_, ((Stack.App _|Stack.Cst _|Stack.Primitive _) :: _|[]) -> s,csts'
+        begin match whd_opt (t, args) with
+        | Some (t_o, args) when isConstruct sigma t_o ->
+          whrec (args.(Projection.npars p + Projection.arg p), stack'')
+        | (Some _ | None) -> s
+        end
+      |_, ((Stack.App _|Stack.Cst _|Stack.Primitive _) :: _|[]) -> s
   in
-  fst (whrec Cst_stack.empty s)
+  whrec s
 
 let find_conclusion env sigma =
   let rec decrec env c =
diff --git a/test-suite/bugs/closed/bug_4544.v b/test-suite/bugs/closed/bug_4544.v
index 13c47edc8f..e9e9c552f6 100644
--- a/test-suite/bugs/closed/bug_4544.v
+++ b/test-suite/bugs/closed/bug_4544.v
@@ -1003,7 +1003,8 @@ Proof.
           = loops_functor (group_loops_functor
                                  (pmap_compose psi phi)) g).
   rewrite <- p.
-  Fail Timeout 1 Time rewrite !loops_functor_group.
+  Timeout 1 Time rewrite !loops_functor_group.
+  Undo.
   (* 0.004 s in 8.5rc1, 8.677 s in 8.5 *)
   Timeout 1 do 3 rewrite loops_functor_group.
 Abort.