From c20139f870430d856d6b891a7129ee72d7b54ff4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 28 Mar 2020 07:50:23 +0100
Subject: 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.
---
 pretyping/reductionops.ml | 34 ++++++++++++++++++++--------------
 1 file 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 =
-- 
cgit v1.2.3


From b5f2b861a3d391716e976469a1a100536550bef8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 28 Mar 2020 09:28:00 +0100
Subject: 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.
---
 kernel/cClosure.ml        |  2 ++
 kernel/cClosure.mli       |  4 ++++
 pretyping/reductionops.ml | 40 +++++++++++++++++++++++++++-------------
 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
-- 
cgit v1.2.3


From 5a961410854f01a4445b6605483d0b227279a1fd Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 29 Mar 2020 15:29:50 +0200
Subject: Fix the test for bug #4544.

It seems that this PR is making the rewrite much, much faster.
---
 test-suite/bugs/closed/bug_4544.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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.
-- 
cgit v1.2.3