diff options
| author |  gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-11-08 15:23:52 +0000 |
|---|---|---|
| committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-11-08 15:23:52 +0000 |
| commit | 0cab74bb2906969e5ea72619be3a80dbc48b5675 (patch) | |
| tree | 8810b66531773a4b73654b2e5c2f625988207196 /pretyping/evarconv.ml | |
| parent | a0054d400f733bc1761cc1c07ff75b17f94c36f1 (diff) | |
optimization: memoization for is_open_canonical_projection
Assume a pile of constants on the left, and a stuck canonical projection
on the right. We are going to unfold the left constants step by step,
and at every step, we are going to recheck that the very same projection
on the right is stuck. The new check for stuck canonical projections is
more expensive, we thus memoize it for the whole sequence of delta steps
on the left.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14646 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 15 |
1 files changed, 11 insertions, 4 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 47822b22e..53c659062 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -195,7 +195,8 @@ let rec evar_conv_x ts env evd pbty term1 term2 = evar_eqappr_x ts env evd pbty (decompose_app term1) (decompose_app term2) -and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = +and evar_eqappr_x ?(rhs_is_stuck_proj = false) + ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = (* Evar must be undefined since we have flushed evars *) match (flex_kind_of_term term1 l1, flex_kind_of_term term2 l2) with | Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) -> @@ -324,11 +325,13 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = if the first argument is a beta-redex (expand a constant only if necessary) or the second argument is potentially usable as a canonical projection *) - if isLambda flex1 or is_open_canonical_projection env i appr2 - then + let rhs_is_stuck_proj = + rhs_is_stuck_proj || is_open_canonical_projection env i appr2 in + if isLambda flex1 || rhs_is_stuck_proj then match eval_flexible_term ts env flex1 with | Some v1 -> - evar_eqappr_x ts env i pbty (evar_apprec ts env i l1 v1) appr2 + evar_eqappr_x ~rhs_is_stuck_proj + ts env i pbty (evar_apprec ts env i l1 v1) appr2 | None -> match eval_flexible_term ts env flex2 with | Some v2 -> @@ -541,6 +544,10 @@ and conv_record trs env evd (c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) (fun i -> evar_conv_x trs env i CONV c1 (applist (c,(List.rev ks)))); (fun i -> ise_list2 i (fun i -> evar_conv_x trs env i CONV) ts ts1)] +(* getting rid of the optional argument rhs_is_stuck_proj *) +let evar_eqappr_x ts env evd pbty appr1 appr2 = + evar_eqappr_x ts env evd pbty appr1 appr2 + (* We assume here |l1| <= |l2| *) let first_order_unification ts env evd (ev1,l1) (term2,l2) = |