Merge PR #6222: Share computation of unifiable evars

3 files changed, 75 insertions, 10 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 3445b744a..374fdce72 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -692,6 +692,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 9d0b973a7..37f5968ad 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 3b945c87f..0a6435195 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -634,32 +634,42 @@ let shelve_goals l =
   InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve_goals")) >>
   Shelf.modify (fun gls -> gls @ l)
 
-(** [contained_in_info e evi] checks whether the evar [e] appears 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 contained_in_info sigma e evi =
-  Evar.Set.mem e (Evd.evars_of_filtered_evar_info (Evarutil.nf_evar_info sigma evi))
-
 (** [depends_on sigma src tgt] checks whether the goal [src] appears
     as an existential variable in the definition of the goal [tgt] in
     [sigma]. *)
 let depends_on sigma src tgt =
   let evi = Evd.find sigma tgt in
-  contained_in_info sigma src evi
+  Evar.Set.mem src (Evd.evars_of_filtered_evar_info (Evarutil.nf_evar_info sigma evi))
+
+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 (Evarutil.filtered_undefined_evars_of_evar_info ~cache sigma evi) in
+    (ev, fevs)
+  in
+  List.map map l
 
 (** [unifiable sigma g l] checks whether [g] appears in another
     subgoal of [l]. The list [l] may contain [g], but it does not
     affect the result. *)
 let unifiable sigma g l =
-  CList.exists (fun tgt -> not (Evar.equal g tgt) && depends_on sigma g tgt) l
+  let l = free_evars sigma l in
+  unifiable_delayed g l
 
 (** [partition_unifiable sigma l] partitions [l] into a pair [(u,n)]
     where [u] is composed of the unifiable goals, i.e. the goals on
     whose definition other goals of [l] depend, and [n] are the
     non-unifiable goals. *)
 let partition_unifiable sigma l =
-  CList.partition (fun g -> unifiable sigma g l) l
+  let fevs = free_evars sigma l in
+  CList.partition (fun g -> unifiable_delayed g fevs) l
 
 (** Shelves the unifiable goals under focus, i.e. the goals which
     appear in other goals under focus (the unfocused goals are not