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(-) (limited to 'kernel/reduction.ml') diff --git a/kernel/reduction.ml b/kernel/reduction.ml index c07ac973b..a152a5c5f 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