memoized is_ground_env

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11893 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 35 insertions, 29 deletions

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 *)
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index fee8e29f5..37288d394 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -962,9 +962,19 @@ and evar_define env (evk,_ as ev) rhs evd =
 (* Auxiliary functions for the conversion algorithms modulo evars
  *)
 
-let has_undefined_evars evd t = 
-  try let _ = local_strong whd_ise (evars_of evd) t in false
-  with Uninstantiated_evar _ -> true
+let has_undefined_evars evd t =
+  let evm = evars_of evd in
+  let rec has_ev t =
+    match kind_of_term t with
+        Evar (ev,args) ->
+          (match evar_body (Evd.find evm ev) with
+            | Evar_defined c ->
+                has_ev c; Array.iter has_ev args
+            | Evar_empty ->
+	        raise NotInstantiatedEvar)
+      | _ -> iter_constr has_ev t in
+  try let _ = has_ev t in false
+  with (Not_found | NotInstantiatedEvar) -> true
 
 let is_ground_term evd t =
   not (has_undefined_evars evd t)
@@ -975,6 +985,9 @@ let is_ground_env evd env =
     | _ -> true in
   List.for_all is_ground_decl (rel_context env) &&
   List.for_all is_ground_decl (named_context env)
+(* Memoization is safe since evar_map and environ are applicative
+   structures *)
+let is_ground_env = memo1_2 is_ground_env
 
 let head_evar = 
   let rec hrec c = match kind_of_term c with
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 8a40361d3..38ac3485b 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -598,20 +598,6 @@ let pb_equal = function
 
 let sort_cmp = sort_cmp
 
-
-let nf_red_env sigma env =
-  let nf_decl = function
-      (x,Some t,ty) -> (x,Some (nf_evar sigma t),ty)
-    | d -> d in
-  let sign = named_context env in
-  let ctxt = rel_context env in
-  let env = reset_context env in
-  let env = Sign.fold_named_context
-    (fun d env -> push_named (nf_decl d) env) ~init:env sign in
-  Sign.fold_rel_context
-    (fun d env -> push_rel (nf_decl d) env) ~init:env ctxt
-
-
 let test_conversion (f:?evars:'a->'b) env sigma x y =
   try let _ =
     f ~evars:(safe_evar_value sigma) env x y in true