diff options
-rw-r--r-- | engine/evarutil.ml | 49 | ||||
-rw-r--r-- | engine/evarutil.mli | 6 | ||||
-rw-r--r-- | engine/proofview.ml | 3 |
3 files changed, 57 insertions, 1 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index df4ef2ce7..8202cc05c 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -691,6 +691,55 @@ let undefined_evars_of_evar_info evd evi = (undefined_evars_of_named_context evd (named_context_of_val evi.evar_hyps))) +type undefined_evars_cache = { + mutable cache : (EConstr.named_declaration * Evar.Set.t) ref Id.Map.t; +} + +let create_undefined_evars_cache () = { cache = Id.Map.empty; } + +let cached_evar_of_hyp cache sigma decl accu = match cache with +| None -> + let fold c acc = + let evs = undefined_evars_of_term sigma c in + Evar.Set.union evs acc + in + NamedDecl.fold_constr fold decl accu +| Some cache -> + let id = NamedDecl.get_id decl in + let r = + try Id.Map.find id cache.cache + with Not_found -> + (** Dummy value *) + let r = ref (NamedDecl.LocalAssum (id, EConstr.mkProp), Evar.Set.empty) in + let () = cache.cache <- Id.Map.add id r cache.cache in + r + in + let (decl', evs) = !r in + let evs = + if NamedDecl.equal (==) decl decl' then snd !r + else + let fold c acc = + let evs = undefined_evars_of_term sigma c in + Evar.Set.union evs acc + in + let evs = NamedDecl.fold_constr fold decl Evar.Set.empty in + let () = r := (decl, evs) in + evs + in + Evar.Set.fold Evar.Set.add evs accu + +let filtered_undefined_evars_of_evar_info ?cache sigma evi = + let evars_of_named_context cache accu nc = + let fold decl accu = cached_evar_of_hyp cache sigma (EConstr.of_named_decl decl) accu in + Context.Named.fold_outside fold nc ~init:accu + in + let accu = match evi.evar_body with + | Evar_empty -> Evar.Set.empty + | Evar_defined b -> evars_of_term b + in + let accu = Evar.Set.union (undefined_evars_of_term sigma (EConstr.of_constr evi.evar_concl)) accu in + evars_of_named_context cache accu (evar_filtered_context evi) + (* spiwack: this is a more complete version of {!Termops.occur_evar}. The latter does not look recursively into an [evar_map]. If unification only need to check superficially, tactics diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 62288ced4..63aa4cf5e 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -133,6 +133,12 @@ val undefined_evars_of_term : evar_map -> constr -> Evar.Set.t val undefined_evars_of_named_context : evar_map -> Context.Named.t -> Evar.Set.t val undefined_evars_of_evar_info : evar_map -> evar_info -> Evar.Set.t +type undefined_evars_cache + +val create_undefined_evars_cache : unit -> undefined_evars_cache + +val filtered_undefined_evars_of_evar_info : ?cache:undefined_evars_cache -> evar_map -> evar_info -> Evar.Set.t + (** [occur_evar_upto sigma k c] returns [true] if [k] appears in [c]. It looks up recursively in [sigma] for the value of existential variables. *) diff --git a/engine/proofview.ml b/engine/proofview.ml index af65bc320..613fb1d20 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -645,12 +645,13 @@ let unifiable_delayed g l = CList.exists (fun (tgt, lazy evs) -> not (Evar.equal g tgt) && Evar.Set.mem g evs) l let free_evars sigma l = + let cache = Evarutil.create_undefined_evars_cache () in let map ev = (** Computes the set of evars appearing in the hypotheses, the conclusion or the body of the evar_info [evi]. Note: since we want to use it on goals, the body is actually supposed to be empty. *) let evi = Evd.find sigma ev in - let fevs = lazy (Evd.evars_of_filtered_evar_info (Evarutil.nf_evar_info sigma evi)) in + let fevs = lazy (Evarutil.filtered_undefined_evars_of_evar_info ~cache sigma evi) in (ev, fevs) in List.map map l |