Ordering search: memoise relevance metric

Recalculating the metric all the time was proving costly (it was obvious
even on small queries).

1 files changed, 11 insertions, 5 deletions

diff --git a/toplevel/search.ml b/toplevel/search.ml
index e4db764759..e1b56b1319 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -116,7 +116,11 @@ let generic_search glnumopt fn =
     required of a search. *)
 module ConstrPriority = struct
 
-  type t = Globnames.global_reference * Environ.env * Constr.t
+  (* The priority is memoised here. Because of the very localised use
+     of this module, it is not worth it making a convenient interface. *)
+  type t =
+    Globnames.global_reference * Environ.env * Constr.t * priority
+  and priority = int
 
   module ConstrSet = CSet.Make(Constr)
 
@@ -137,10 +141,11 @@ module ConstrPriority = struct
   let num_symbols t =
     ConstrSet.(cardinal (symbols empty t))
 
+  let priority t : priority =
     -(3*(num_symbols t) + size t)
 
-  let compare (_,_,t1) (_,_,t2) =
-    compare (priority t1) (priority t2)
+  let compare (_,_,_,p1) (_,_,_,p2) =
+    compare p1 p2
 end
 
 module PriorityQueue = Heap.Functional(ConstrPriority)
@@ -154,7 +159,7 @@ let rec iter_priority_queue q fn =
       with Heap.EmptyHeap -> None
   end in
   match next with
-  | Some (gref,env,t) ->
+  | Some (gref,env,t,_) ->
     fn gref env t;
     iter_priority_queue (PriorityQueue.remove q) fn
   | None -> ()
@@ -162,7 +167,8 @@ let rec iter_priority_queue q fn =
 let prioritize_search seq fn =
   let acc = ref PriorityQueue.empty in
   let iter gref env t =
-    acc := PriorityQueue.add (gref,env,t) !acc
+    let p = ConstrPriority.priority t in
+    acc := PriorityQueue.add (gref,env,t,p) !acc
   in
   let () = seq iter in
   iter_priority_queue !acc fn