Sort search results by relevance

This orders the results of search commands (such as `Search`,
`SearchAbout`, …) according to a "relevance" metric to minimise.

In this minimal version, the metric is the size of the displayed term.

3 files changed, 53 insertions, 4 deletions

diff --git a/toplevel/search.ml b/toplevel/search.ml
index d319b24199..d207ba7e0e 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -107,6 +107,47 @@ let generic_search glnumopt fn =
   | Some glnum ->  iter_hypothesis glnum fn);
   iter_declarations fn
 
+(** This module defines a preference on constrs in the form of a
+    [compare] function (preferred constr must be big for this
+    functions, so preferences such as small constr must use a reversed
+    order). This priority will be used to order search results and
+    propose first results which are more likely to be relevant to the
+    query, this is why the type [t] contains the other elements
+    required of a search. *)
+module ConstrPriority = struct
+
+  type t = Globnames.global_reference * Environ.env * Constr.t
+
+  (** A measure of the size of a term *)
+  let rec size t =
+    Constr.fold (fun s t -> 1 + s + size t) 0 t
+
+  let compare (_,_,t1) (_,_,t2) =
+    -compare (size t1) (size t2)
+end
+
+module PriorityQueue = Heap.Functional(ConstrPriority)
+
+let rec iter_priority_queue q fn =
+  (* use an option to make the function tail recursive. Will be
+     obsoleted with Ocaml 4.02 with the [match … with | exception …]
+     syntax. *)
+  let next = begin
+      try Some (PriorityQueue.maximum q)
+      with Heap.EmptyHeap -> None
+  end in
+  match next with
+  | Some (gref,env,t) -> fn gref env t; iter_priority_queue (PriorityQueue.remove q) fn
+  | None -> ()
+
+let prioritize_search seq fn =
+  let acc = ref PriorityQueue.empty in
+  let iter gref env t =
+    acc := PriorityQueue.add (gref,env,t) !acc
+  in
+  let () = seq iter in
+  iter_priority_queue !acc fn
+
 (** Filters *)
 
 (** This function tries to see whether the conclusion matches a pattern. *)
diff --git a/toplevel/search.mli b/toplevel/search.mli
index ba3d48efcc..c9167c485d 100644
--- a/toplevel/search.mli
+++ b/toplevel/search.mli
@@ -74,3 +74,11 @@ val interface_search : ?glnum:int -> (search_constraint * bool) list ->
 val generic_search : int option -> display_function -> unit
 (** This function iterates over all hypothesis of the goal numbered
     [glnum] (if present) and all known declarations. *)
+
+(** {6 Search function modifiers} *)
+
+val prioritize_search : (display_function -> unit) -> display_function -> unit
+(** [prioritize_search iter] iterates over the values of [iter] (seen
+    as a sequence of declarations), in a relevance order. This requires to
+    perform the entire iteration of [iter] before starting streaming. So
+    [prioritize_search] should not be used for low-latency streaming. *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index ede88399ef..18410f9e97 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1784,13 +1784,13 @@ let vernac_search s gopt r =
   in
   match s with
   | SearchPattern c ->
-      Search.search_pattern gopt (get_pattern c) r pr_search
+      (Search.search_pattern gopt (get_pattern c) r |> Search.prioritize_search) pr_search
   | SearchRewrite c ->
-      Search.search_rewrite gopt (get_pattern c) r pr_search
+      (Search.search_rewrite gopt (get_pattern c) r |> Search.prioritize_search) pr_search
   | SearchHead c ->
-      Search.search_by_head gopt (get_pattern c) r pr_search
+      (Search.search_by_head gopt (get_pattern c) r |> Search.prioritize_search) pr_search
   | SearchAbout sl ->
-      Search.search_about gopt (List.map (on_snd (interp_search_about_item env)) sl) r pr_search
+      (Search.search_about gopt (List.map (on_snd (interp_search_about_item env)) sl) r |> Search.prioritize_search) pr_search
 
 let vernac_locate = let open Feedback in function
   | LocateAny (AN qid)  -> msg_notice (print_located_qualid qid)