diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-26 21:14:52 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-27 00:48:28 +0100 |
| commit | 256ca51bafc7200c8c006981cad60e57014e0dbc (patch) | |
| tree | 292497aa4d7b03f7b3a22eaaee318dfe5fc44939 /kernel/reduction.ml | |
| parent | 27e8d8857ea5435ccec9eddd6c34324de82afd32 (diff) | |
Do not recompute twice the whnf of terms in conversion.
This performance bug was introduced 9 years ago in a8b0345, where the
responsibility of normalizing the term went from ccnv to eqappr in Reduction.
As a result, all recursive calls to eqappr that were preemptively reducing the
term ended up calling whd_stack twice, once by themselves, and once in the
subsequent call to eqappr.
This caused an important slowdown for conversion-intensive proofs, as the
whd_stack calls CClosure.zip to perfom in-place term sharing, leading to
useless huge re-allocations and repetitive write barriers.
Now that eqappr always head-normalizes the term beforehand, we simply don't
call whd_stack anymore when jumping to eqappr.
Diffstat (limited to 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 1ae89347a..fc379fb7d 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -322,17 +322,17 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = let (app1,app2) = if Conv_oracle.oracle_order Univ.out_punivs oracle l2r fl1 fl2 then match unfold_reference infos fl1 with - | Some def1 -> ((lft1, whd def1 v1), appr2) + | Some def1 -> ((lft1, (def1, v1)), appr2) | None -> (match unfold_reference infos fl2 with - | Some def2 -> (appr1, (lft2, whd def2 v2)) + | Some def2 -> (appr1, (lft2, (def2, v2))) | None -> raise NotConvertible) else match unfold_reference infos fl2 with - | Some def2 -> (appr1, (lft2, whd def2 v2)) + | Some def2 -> (appr1, (lft2, (def2, v2))) | None -> (match unfold_reference infos fl1 with - | Some def1 -> ((lft1, whd def1 v1), appr2) + | Some def1 -> ((lft1, (def1, v1)), appr2) | None -> raise NotConvertible) in eqappr cv_pb l2r infos app1 app2 cuniv) @@ -343,11 +343,11 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = form *) (match unfold_projection infos p1 c1 with | Some (def1,s1) -> - eqappr cv_pb l2r infos (lft1, whd def1 (s1 :: v1)) appr2 cuniv + eqappr cv_pb l2r infos (lft1, (def1, s1 :: v1)) appr2 cuniv | None -> match unfold_projection infos p2 c2 with | Some (def2,s2) -> - eqappr cv_pb l2r infos appr1 (lft2, whd def2 (s2 :: v2)) cuniv + eqappr cv_pb l2r infos appr1 (lft2, (def2, s2 :: v2)) cuniv | None -> if Constant.equal (Projection.constant p1) (Projection.constant p2) && compare_stack_shape v1 v2 then @@ -359,26 +359,26 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | (FProj (p1,c1), t2) -> (match unfold_projection infos p1 c1 with | Some (def1,s1) -> - eqappr cv_pb l2r infos (lft1, whd def1 (s1 :: v1)) appr2 cuniv + eqappr cv_pb l2r infos (lft1, (def1, s1 :: v1)) appr2 cuniv | None -> (match t2 with | FFlex fl2 -> (match unfold_reference infos fl2 with | Some def2 -> - eqappr cv_pb l2r infos appr1 (lft2, whd def2 v2) cuniv + eqappr cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv | None -> raise NotConvertible) | _ -> raise NotConvertible)) | (t1, FProj (p2,c2)) -> (match unfold_projection infos p2 c2 with | Some (def2,s2) -> - eqappr cv_pb l2r infos appr1 (lft2, whd def2 (s2 :: v2)) cuniv + eqappr cv_pb l2r infos appr1 (lft2, (def2, s2 :: v2)) cuniv | None -> (match t1 with | FFlex fl1 -> (match unfold_reference infos fl1 with | Some def1 -> - eqappr cv_pb l2r infos (lft1, whd def1 v1) appr2 cuniv + eqappr cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv | None -> raise NotConvertible) | _ -> raise NotConvertible)) @@ -424,7 +424,7 @@ 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, whd def1 v1) appr2 cuniv + eqappr cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv | None -> match c2 with | FConstruct ((ind2,j2),u2) -> @@ -438,7 +438,7 @@ 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, whd def2 v2) cuniv + eqappr cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv | None -> match c1 with | FConstruct ((ind1,j1),u1) -> |