Use the kernel machine in whd_betaiota_deltazeta_for_iota_state.

There is no point in using the exaggerately inefficient Reductionops machine.
We need to be call-by-name to preserve the shape of the reduced terms, as
call-by-need would introduce sharing and thus at-distance effects in term
refolding. Yet, the Reductionops machine is worse than that, since it performs
substitutions eagerly, leading to a catastrophical performance profile.

Instead, we use the kernel reduction in by-name mode to replace the Reductionops
machine in whd_betaiota_deltazeta_for_iota_state with all flags on. Since the
kernel is using explicit substitutions, this is algorithmically more efficient.
Apart from minor differences, this should produce the same normal form.

As showed by the benchmarks, this is a critical change for the odd-order proofs.
Ideally, we should use delayed substitutions in the Reductionops machine as well
for great profit, but due to code entanglement this is a much less self-contained
change.

1 files changed, 20 insertions, 14 deletions

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 8bb268a92e..84f284c2df 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1746,26 +1746,32 @@ 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 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 []
+  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'
+        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
       |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'
+        let (t_o, stack_o) = whd (t, args) in
+        if isConstruct sigma t_o then whrec (t_o, stack_o@stack') else s
       |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
+        let (t_o, stack_o) = whd (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'
+          whrec (Stack.nth stack_o (Projection.npars p + Projection.arg p), stack'')
+        else s
+      |_, ((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 =