From 9eaeb462425728ee2df225619a632d3a6c25cad9 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 21 Nov 2017 07:23:59 +0100
Subject: 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.
---
 engine/proofview.ml | 29 +++++++++++++++++++----------
 1 file changed, 19 insertions(+), 10 deletions(-)

(limited to 'engine')

diff --git a/engine/proofview.ml b/engine/proofview.ml
index 598358c472..af65bc3207 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
-- 
cgit v1.2.3


From 8eea5a5ecdd33d85e4e7d42408360fff68e04f5d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 21 Nov 2017 11:24:04 +0100
Subject: Experimenting with a fine-grained cache for undefined evars in
 evinfos.

---
 engine/evarutil.ml  | 49 +++++++++++++++++++++++++++++++++++++++++++++++++
 engine/evarutil.mli |  6 ++++++
 engine/proofview.ml |  3 ++-
 3 files changed, 57 insertions(+), 1 deletion(-)

(limited to 'engine')

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index df4ef2ce71..8202cc05ca 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 62288ced46..63aa4cf5e4 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 af65bc3207..613fb1d207 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
-- 
cgit v1.2.3