Do not precompute hint dnets eagerly.

Due to the way transparency is handled in hint databases, every time it is
changed, all dnets are recomputed from scratch. This is very expensive, and
a bench showed that it was sometimes contributing significantly to the whole
compilation time of hint-heavy libraries. This patch makes this computation
lazy, so that the dnet is computed only the first time a hint lookup is
performed.

The implementation is functionally equivalent to wrapping the sentry_bnet
field in a Lazy.t, but because dnets are stored in the summary and thus
marshalled, I had to manually perform a defunctionalization.

A (maybe cleaner?) alternative would be to track the set of constants a
hint depend on, in order to only refresh those touched by the change of
transparency. Yet, this would be a much more invasive change.

1 files changed, 36 insertions, 9 deletions

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 41b200bb83..0ab1adda4b 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -237,10 +237,38 @@ let pri_order t1 t2 = pri_order_int t1 t2 <= 0
 type stored_data = int * full_hint
     (* First component is the index of insertion in the table, to keep most recent first semantics. *)
 
-module Bounded_net = Btermdn.Make(struct
-                                    type t = stored_data
-                                    let compare = pri_order_int
-                                  end)
+module Bounded_net :
+sig
+  type t
+  val empty : t
+  val add : TransparentState.t option -> t -> Pattern.constr_pattern -> stored_data -> t
+  val lookup : Evd.evar_map -> TransparentState.t option -> t -> EConstr.constr -> stored_data list
+end =
+struct
+  module Data = struct type t = stored_data let compare = pri_order_int end
+  module Bnet = Btermdn.Make(Data)
+
+  type diff = TransparentState.t option * Pattern.constr_pattern * stored_data
+  type data = Bnet of Bnet.t | Diff of diff * data ref
+  type t = data ref
+
+  let empty = ref (Bnet Bnet.empty)
+
+  let add st net p v = ref (Diff ((st, p, v), net))
+
+  let rec force net = match !net with
+  | Bnet dn -> dn
+  | Diff ((st, p, v), rem) ->
+    let dn = force rem in
+    let p = Bnet.pattern st p in
+    let dn = Bnet.add dn p v in
+    let () = net := (Bnet dn) in
+    dn
+
+  let lookup sigma st net p =
+    let dn = force net in
+    Bnet.lookup sigma st dn p
+end
 
 type search_entry = {
   sentry_nopat : stored_data list;
@@ -263,18 +291,17 @@ let add_tac pat t se =
   | None ->
     if List.exists (eq_pri_auto_tactic t) se.sentry_nopat then se
     else { se with sentry_nopat = List.insert pri_order t se.sentry_nopat }
-  | Some pat ->
+  | Some (st, pat) ->
     if List.exists (eq_pri_auto_tactic t) se.sentry_pat then se
     else { se with
         sentry_pat = List.insert pri_order t se.sentry_pat;
-        sentry_bnet = Bounded_net.add se.sentry_bnet pat t; }
+        sentry_bnet = Bounded_net.add st se.sentry_bnet pat t; }
 
 let rebuild_dn st se =
   let dn' =
     List.fold_left
       (fun dn (id, t) ->
-        let pat = Bounded_net.pattern (Some st) (Option.get t.pat) in
-        Bounded_net.add dn pat (id, t))
+        Bounded_net.add (Some st) dn (Option.get t.pat) (id, t))
       Bounded_net.empty se.sentry_pat
   in
   { se with sentry_bnet = dn' }
@@ -650,7 +677,7 @@ struct
           if not db.use_dn && is_exact v.code.obj then None
           else
             let dnst = if db.use_dn then Some db.hintdb_state else None in
-            Option.map (fun p -> Bounded_net.pattern dnst p) v.pat
+            Option.map (fun p -> (dnst, p)) v.pat
         in
           let oval = find gr db in
             { db with hintdb_map = GlobRef.Map.add gr (add_tac pat idv oval) db.hintdb_map }