Fix #6204: `refine` is exponential in the number of fresh evars that it creates.

It is actually polynomial with a big exponent, probably quartic. This was due
to the Proofview.unifiable algorithm that kept recomputing the free evars of
an evar info. We share the computation instead.

This does not make the contrived example compile in a reasonable amount of time,
but it does make smaller instances compile way quicker than before. Indeed, the
example is essentially quadratic in size as all evars refer to the previously
defined ones in their signature.

1 files changed, 19 insertions, 10 deletions

diff --git a/engine/proofview.ml b/engine/proofview.ml
index 598358c47..af65bc320 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -634,32 +634,41 @@ 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 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
+    (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