Be cleverer and do not hopelessly rezip a term when not needed.

A quick analysis showed that most of the calls to whd do not lead to a
term which further triggers reduction, so there is no point in refolding
a potentiall huge term for no reason.

3 files changed, 33 insertions, 13 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 84f284c2df..01f3537a7f 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1746,29 +1746,43 @@ 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 all = CClosure.RedFlags.red_add_transparent CClosure.all ts 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 c =
-    let r = clos_whd_flags all env' sigma (Stack.zip sigma c) in
-    let (r, args) = Termops.decompose_app_vect sigma r in
-    r, Stack.append_app args []
+  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) = whd (t, args) in
-        if reducible_mind_case sigma t_o then whrec (t_o, stack_o@stack') else s
+        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) = whd (t, args) in
-        if isConstruct sigma t_o then whrec (t_o, stack_o@stack') else s
+        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) = whd (t, args) in
-        if isConstruct sigma t_o then
-          whrec (Stack.nth stack_o (Projection.npars p + Projection.arg p), stack'')
-        else s
+        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
   whrec s