From c7026ec14f94875fc4b58951fa8bec628fcfac42 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 30 Jan 2018 14:20:48 +0100
Subject: Use whd-all on rigid-flex conversion.

This heuristic is justified by the fact that during a conversion check
between a flexible and a rigid term, the flexible one is eventually going
to be fully weak-head normalized. So in this case instead of performing
many small reduction steps on the flexible term, we perform full weak-head
reduction, including delta.

It is slightly more efficient in actual developments, and it fixes a corner
case encountered by Jason Gross.

Fixes #6667: Kernel conversion is much, much slower than `Eval lazy`.
---
 kernel/reduction.ml | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index c07ac973b8..a152a5c5f2 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -479,7 +479,12 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
     | (FFlex fl1, c2)      ->
        (match unfold_reference infos fl1 with
 	| Some def1 ->
-           eqappr cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv
+          (** By virtue of the previous case analyses, we know [c2] is rigid.
+              Conversion check to rigid terms eventually implies full weak-head
+              reduction, so instead of repeatedly performing small-step
+              unfoldings, we perform reduction with all flags on. *)
+            let r1 = whd_stack (infos_with_reds infos all) def1 v1 in
+            eqappr cv_pb l2r infos (lft1, r1) appr2 cuniv
 	| None -> 
 	   match c2 with
 	   | FConstruct ((ind2,j2),u2) ->
@@ -493,7 +498,9 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
     | (c1, FFlex fl2)      ->
        (match unfold_reference infos fl2 with
         | Some def2 ->
-           eqappr cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv
+          (** Symmetrical case of above. *)
+          let r2 = whd_stack (infos_with_reds infos all) def2 v2 in
+          eqappr cv_pb l2r infos appr1 (lft2, r2) cuniv
         | None -> 
 	   match c1 with
 	   | FConstruct ((ind1,j1),u1) ->
-- 
cgit v1.2.3


From e849572cd2b242b34fbec6c3eaa42e7d2e7cc550 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 5 Feb 2018 13:56:22 +0100
Subject: Respect the transparent state of the current conversion on strong
 weak-head.

This fixes the previous patch in rare corner-cases where unification code was
relying on both kernel conversion and specific transparent state.
---
 kernel/cClosure.ml  | 3 +++
 kernel/cClosure.mli | 3 +++
 kernel/reduction.ml | 2 ++
 3 files changed, 8 insertions(+)

diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index b1181157e1..4fd274ae13 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -91,6 +91,7 @@ module type RedFlagsSig = sig
   val red_add : reds -> red_kind -> reds
   val red_sub : reds -> red_kind -> reds
   val red_add_transparent : reds -> transparent_state -> reds
+  val red_transparent : reds -> transparent_state
   val mkflags : red_kind list -> reds
   val red_set : reds -> red_kind -> bool
   val red_projection : reds -> projection -> bool
@@ -164,6 +165,8 @@ module RedFlags = (struct
 	let (l1,l2) = red.r_const in
 	{ red with r_const = Id.Pred.remove id l1, l2 }
 
+  let red_transparent red = red.r_const
+
   let red_add_transparent red tr =
     { red with r_const = tr }
 
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index 119b70e301..41db0af753 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -61,6 +61,9 @@ module type RedFlagsSig = sig
   (** Adds a reduction kind to a set *)
   val red_add_transparent : reds -> transparent_state -> reds
 
+  (** Retrieve the transparent state of the reduction flags *)
+  val red_transparent : reds -> transparent_state
+
   (** Build a reduction set from scratch = iter [red_add] on [no_red] *)
   val mkflags : red_kind list -> reds
 
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index a152a5c5f2..6104f56c63 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -483,6 +483,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
               Conversion check to rigid terms eventually implies full weak-head
               reduction, so instead of repeatedly performing small-step
               unfoldings, we perform reduction with all flags on. *)
+            let all = RedFlags.red_add_transparent all (RedFlags.red_transparent (info_flags infos)) in
             let r1 = whd_stack (infos_with_reds infos all) def1 v1 in
             eqappr cv_pb l2r infos (lft1, r1) appr2 cuniv
 	| None -> 
@@ -499,6 +500,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
        (match unfold_reference infos fl2 with
         | Some def2 ->
           (** Symmetrical case of above. *)
+          let all = RedFlags.red_add_transparent all (RedFlags.red_transparent (info_flags infos)) in
           let r2 = whd_stack (infos_with_reds infos all) def2 v2 in
           eqappr cv_pb l2r infos appr1 (lft2, r2) cuniv
         | None -> 
-- 
cgit v1.2.3