Merge PR#253: Sort Search results by relevance

3 files changed, 78 insertions, 4 deletions

diff --git a/toplevel/search.ml b/toplevel/search.ml
index d319b2419..e1b56b131 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -107,6 +107,72 @@ 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
+
+  (* 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)
+
+  (** A measure of the size of a term *)
+  let rec size t =
+    Constr.fold (fun s t -> 1 + s + size t) 0 t
+
+  (** Set of the "symbols" (definitions, inductives, constructors)
+      which appear in a term. *)
+  let rec symbols acc t =
+    let open Constr in
+    match kind t with
+    | Const _ | Ind _ | Construct _ -> ConstrSet.add t acc
+    | _ -> Constr.fold symbols acc t
+
+  (** The number of distinct "symbols" (see {!symbols}) which appear
+      in a term. *)
+  let num_symbols t =
+    ConstrSet.(cardinal (symbols empty t))
+
+  let priority t : priority =
+    -(3*(num_symbols t) + size t)
+
+  let compare (_,_,_,p1) (_,_,_,p2) =
+    compare p1 p2
+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 =
+    let p = ConstrPriority.priority t in
+    acc := PriorityQueue.add (gref,env,t,p) !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 ba3d48efc..c9167c485 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 a2f2ded32..862a761b2 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1787,13 +1787,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)