From c580f69cc36cc4cc908febb900a55ae751039a0c Mon Sep 17 00:00:00 2001 From: barras Date: Mon, 9 Feb 2009 15:58:32 +0000 Subject: memoized is_ground_env git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11893 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/evarconv.ml | 31 +++++++++++++++++++------------ 1 file changed, 19 insertions(+), 12 deletions(-) (limited to 'pretyping/evarconv.ml') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index aba6e2e19..d7da100ab 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -164,18 +164,25 @@ let rec evar_conv_x env evd pbty term1 term2 = (* Maybe convertible but since reducing can erase evars which [evar_apprec] could have found, we do it only if the terms are free of evar. Note: incomplete heuristic... *) - if is_ground_term evd term1 && is_ground_term evd term2 - && is_ground_env evd env - then (evd, is_fconv pbty env (evars_of evd) term1 term2) - else - let term1 = apprec_nohdbeta env evd term1 in - let term2 = apprec_nohdbeta env evd term2 in - if is_undefined_evar evd term1 then - solve_simple_eqn evar_conv_x env evd (pbty,destEvar term1,term2) - else if is_undefined_evar evd term2 then - solve_simple_eqn evar_conv_x env evd (pbty,destEvar term2,term1) - else - evar_eqappr_x env evd pbty (decompose_app term1) (decompose_app term2) + let ground_test = + if is_ground_term evd term1 && is_ground_term evd term2 then + if is_fconv pbty env (evars_of evd) term1 term2 then + Some true + else if is_ground_env evd env then Some false + else None + else None in + match ground_test with + Some b -> (evd,b) + | None -> + let term1 = apprec_nohdbeta env evd term1 in + let term2 = apprec_nohdbeta env evd term2 in + if is_undefined_evar evd term1 then + solve_simple_eqn evar_conv_x env evd (pbty,destEvar term1,term2) + else if is_undefined_evar evd term2 then + solve_simple_eqn evar_conv_x env evd (pbty,destEvar term2,term1) + else + evar_eqappr_x env evd pbty + (decompose_app term1) (decompose_app term2) and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = (* Evar must be undefined since we have whd_ised *) -- cgit v1.2.3