Merge PR#253: Sort Search results by relevance

6 files changed, 198 insertions, 124 deletions

diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
index c17b285bc..81fda176e 100644
--- a/test-suite/output/Search.out
+++ b/test-suite/output/Search.out
@@ -1,108 +1,108 @@
 le_n: forall n : nat, n <= n
+le_0_n: forall n : nat, 0 <= n
 le_S: forall n m : nat, n <= m -> n <= S m
+le_n_S: forall n m : nat, n <= m -> S n <= S m
+le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m
+le_S_n: forall n m : nat, S n <= S m -> n <= m
+min_l: forall n m : nat, n <= m -> Nat.min n m = n
+max_r: forall n m : nat, n <= m -> Nat.max n m = m
+min_r: forall n m : nat, m <= n -> Nat.min n m = m
+max_l: forall n m : nat, m <= n -> Nat.max n m = n
 le_ind:
   forall (n : nat) (P : nat -> Prop),
   P n ->
   (forall m : nat, n <= m -> P m -> P (S m)) ->
   forall n0 : nat, n <= n0 -> P n0
-le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m
-le_S_n: forall n m : nat, S n <= S m -> n <= m
-le_0_n: forall n : nat, 0 <= n
-le_n_S: forall n m : nat, n <= m -> S n <= S m
-max_l: forall n m : nat, m <= n -> Nat.max n m = n
-max_r: forall n m : nat, n <= m -> Nat.max n m = m
-min_l: forall n m : nat, n <= m -> Nat.min n m = n
-min_r: forall n m : nat, m <= n -> Nat.min n m = m
-true: bool
 false: bool
-bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b
-bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b
-bool_rec: forall P : bool -> Set, P true -> P false -> forall b : bool, P b
-andb: bool -> bool -> bool
-orb: bool -> bool -> bool
-implb: bool -> bool -> bool
-xorb: bool -> bool -> bool
+true: bool
+is_true: bool -> Prop
 negb: bool -> bool
-andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
-andb_true_intro:
-  forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true
 eq_true: bool -> Prop
-eq_true_rect:
-  forall P : bool -> Type, P true -> forall b : bool, eq_true b -> P b
-eq_true_ind:
-  forall P : bool -> Prop, P true -> forall b : bool, eq_true b -> P b
+implb: bool -> bool -> bool
+orb: bool -> bool -> bool
+andb: bool -> bool -> bool
+xorb: bool -> bool -> bool
+Nat.even: nat -> bool
+Nat.odd: nat -> bool
+BoolSpec: Prop -> Prop -> bool -> Prop
+Nat.eqb: nat -> nat -> bool
+Nat.testbit: nat -> nat -> bool
+Nat.ltb: nat -> nat -> bool
+Nat.leb: nat -> nat -> bool
+Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
+bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b
+bool_rec: forall P : bool -> Set, P true -> P false -> forall b : bool, P b
 eq_true_rec:
   forall P : bool -> Set, P true -> forall b : bool, eq_true b -> P b
-is_true: bool -> Prop
-eq_true_ind_r:
-  forall (P : bool -> Prop) (b : bool), P b -> eq_true b -> P true
-eq_true_rec_r:
-  forall (P : bool -> Set) (b : bool), P b -> eq_true b -> P true
+eq_true_ind:
+  forall P : bool -> Prop, P true -> forall b : bool, eq_true b -> P b
 eq_true_rect_r:
   forall (P : bool -> Type) (b : bool), P b -> eq_true b -> P true
-BoolSpec: Prop -> Prop -> bool -> Prop
+eq_true_rec_r:
+  forall (P : bool -> Set) (b : bool), P b -> eq_true b -> P true
+eq_true_rect:
+  forall P : bool -> Type, P true -> forall b : bool, eq_true b -> P b
+bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b
+eq_true_ind_r:
+  forall (P : bool -> Prop) (b : bool), P b -> eq_true b -> P true
+andb_true_intro:
+  forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true
+andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
 BoolSpec_ind:
   forall (P Q : Prop) (P0 : bool -> Prop),
   (P -> P0 true) ->
   (Q -> P0 false) -> forall b : bool, BoolSpec P Q b -> P0 b
-Nat.eqb: nat -> nat -> bool
-Nat.leb: nat -> nat -> bool
-Nat.ltb: nat -> nat -> bool
-Nat.even: nat -> bool
-Nat.odd: nat -> bool
-Nat.testbit: nat -> nat -> bool
-Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
 bool_choice:
   forall (S : Set) (R1 R2 : S -> Prop),
   (forall x : S, {R1 x} + {R2 x}) ->
   {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x}
-eq_S: forall x y : nat, x = y -> S x = S y
-f_equal_nat: forall (B : Type) (f : nat -> B) (x y : nat), x = y -> f x = f y
-f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y
+mult_n_O: forall n : nat, 0 = n * 0
+plus_O_n: forall n : nat, 0 + n = n
+plus_n_O: forall n : nat, n = n + 0
+n_Sn: forall n : nat, n <> S n
 pred_Sn: forall n : nat, n = Nat.pred (S n)
+O_S: forall n : nat, 0 <> S n
+f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y
+eq_S: forall x y : nat, x = y -> S x = S y
 eq_add_S: forall n m : nat, S n = S m -> n = m
+min_r: forall n m : nat, m <= n -> Nat.min n m = m
+min_l: forall n m : nat, n <= m -> Nat.min n m = n
+max_r: forall n m : nat, n <= m -> Nat.max n m = m
+max_l: forall n m : nat, m <= n -> Nat.max n m = n
+plus_Sn_m: forall n m : nat, S n + m = S (n + m)
+plus_n_Sm: forall n m : nat, S (n + m) = n + S m
+f_equal_nat: forall (B : Type) (f : nat -> B) (x y : nat), x = y -> f x = f y
 not_eq_S: forall n m : nat, n <> m -> S n <> S m
-O_S: forall n : nat, 0 <> S n
-n_Sn: forall n : nat, n <> S n
+mult_n_Sm: forall n m : nat, n * m + n = n * S m
 f_equal2_plus:
   forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2
+f_equal2_mult:
+  forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2
 f_equal2_nat:
   forall (B : Type) (f : nat -> nat -> B) (x1 y1 x2 y2 : nat),
   x1 = y1 -> x2 = y2 -> f x1 x2 = f y1 y2
-plus_n_O: forall n : nat, n = n + 0
-plus_O_n: forall n : nat, 0 + n = n
-plus_n_Sm: forall n m : nat, S (n + m) = n + S m
-plus_Sn_m: forall n m : nat, S n + m = S (n + m)
-f_equal2_mult:
-  forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2
-mult_n_O: forall n : nat, 0 = n * 0
-mult_n_Sm: forall n m : nat, n * m + n = n * S m
-max_l: forall n m : nat, m <= n -> Nat.max n m = n
-max_r: forall n m : nat, n <= m -> Nat.max n m = m
-min_l: forall n m : nat, n <= m -> Nat.min n m = n
-min_r: forall n m : nat, m <= n -> Nat.min n m = m
-andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
 andb_true_intro:
   forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true
+andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
 bool_choice:
   forall (S : Set) (R1 R2 : S -> Prop),
   (forall x : S, {R1 x} + {R2 x}) ->
   {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x}
-andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
 andb_true_intro:
   forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true
 andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
-h': newdef n <> n
+andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
 h: n <> newdef n
 h': newdef n <> n
 h: n <> newdef n
+h': newdef n <> n
 h: n <> newdef n
 h: n <> newdef n
-h': ~ P n
 h: P n
 h': ~ P n
 h: P n
 h': ~ P n
 h: P n
+h': ~ P n
 h: P n
 h: P n
diff --git a/test-suite/output/SearchHead.out b/test-suite/output/SearchHead.out
index 0d5924ec6..7038eac22 100644
--- a/test-suite/output/SearchHead.out
+++ b/test-suite/output/SearchHead.out
@@ -1,39 +1,39 @@
 le_n: forall n : nat, n <= n
+le_0_n: forall n : nat, 0 <= n
 le_S: forall n m : nat, n <= m -> n <= S m
 le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m
-le_S_n: forall n m : nat, S n <= S m -> n <= m
-le_0_n: forall n : nat, 0 <= n
 le_n_S: forall n m : nat, n <= m -> S n <= S m
-true: bool
+le_S_n: forall n m : nat, S n <= S m -> n <= m
 false: bool
-andb: bool -> bool -> bool
-orb: bool -> bool -> bool
+true: bool
+negb: bool -> bool
 implb: bool -> bool -> bool
+orb: bool -> bool -> bool
+andb: bool -> bool -> bool
 xorb: bool -> bool -> bool
-negb: bool -> bool
-Nat.eqb: nat -> nat -> bool
-Nat.leb: nat -> nat -> bool
-Nat.ltb: nat -> nat -> bool
 Nat.even: nat -> bool
 Nat.odd: nat -> bool
+Nat.leb: nat -> nat -> bool
+Nat.ltb: nat -> nat -> bool
 Nat.testbit: nat -> nat -> bool
-eq_S: forall x y : nat, x = y -> S x = S y
-f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y
+Nat.eqb: nat -> nat -> bool
+mult_n_O: forall n : nat, 0 = n * 0
+plus_O_n: forall n : nat, 0 + n = n
+plus_n_O: forall n : nat, n = n + 0
 pred_Sn: forall n : nat, n = Nat.pred (S n)
+f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y
 eq_add_S: forall n m : nat, S n = S m -> n = m
-f_equal2_plus:
-  forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2
-plus_n_O: forall n : nat, n = n + 0
-plus_O_n: forall n : nat, 0 + n = n
+eq_S: forall x y : nat, x = y -> S x = S y
+max_r: forall n m : nat, n <= m -> Nat.max n m = m
+max_l: forall n m : nat, m <= n -> Nat.max n m = n
+min_r: forall n m : nat, m <= n -> Nat.min n m = m
+min_l: forall n m : nat, n <= m -> Nat.min n m = n
 plus_n_Sm: forall n m : nat, S (n + m) = n + S m
 plus_Sn_m: forall n m : nat, S n + m = S (n + m)
+mult_n_Sm: forall n m : nat, n * m + n = n * S m
+f_equal2_plus:
+  forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2
 f_equal2_mult:
   forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2
-mult_n_O: forall n : nat, 0 = n * 0
-mult_n_Sm: forall n m : nat, n * m + n = n * S m
-max_l: forall n m : nat, m <= n -> Nat.max n m = n
-max_r: forall n m : nat, n <= m -> Nat.max n m = m
-min_l: forall n m : nat, n <= m -> Nat.min n m = n
-min_r: forall n m : nat, m <= n -> Nat.min n m = m
 h: newdef n
 h: P n
diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out
index f3c12effc..45ff5e73b 100644
--- a/test-suite/output/SearchPattern.out
+++ b/test-suite/output/SearchPattern.out
@@ -1,77 +1,77 @@
-true: bool
 false: bool
-andb: bool -> bool -> bool
-orb: bool -> bool -> bool
+true: bool
+negb: bool -> bool
 implb: bool -> bool -> bool
+orb: bool -> bool -> bool
+andb: bool -> bool -> bool
 xorb: bool -> bool -> bool
-negb: bool -> bool
-Nat.eqb: nat -> nat -> bool
-Nat.leb: nat -> nat -> bool
-Nat.ltb: nat -> nat -> bool
 Nat.even: nat -> bool
 Nat.odd: nat -> bool
+Nat.leb: nat -> nat -> bool
+Nat.ltb: nat -> nat -> bool
 Nat.testbit: nat -> nat -> bool
-O: nat
-S: nat -> nat
-length: forall A : Type, list A -> nat
+Nat.eqb: nat -> nat -> bool
+Nat.two: nat
 Nat.zero: nat
 Nat.one: nat
-Nat.two: nat
-Nat.succ: nat -> nat
+O: nat
+Nat.double: nat -> nat
+Nat.sqrt: nat -> nat
+Nat.div2: nat -> nat
+Nat.log2: nat -> nat
 Nat.pred: nat -> nat
+Nat.square: nat -> nat
+S: nat -> nat
+Nat.succ: nat -> nat
+Nat.ldiff: nat -> nat -> nat
 Nat.add: nat -> nat -> nat
-Nat.double: nat -> nat
+Nat.lor: nat -> nat -> nat
+Nat.lxor: nat -> nat -> nat
+Nat.land: nat -> nat -> nat
 Nat.mul: nat -> nat -> nat
 Nat.sub: nat -> nat -> nat
 Nat.max: nat -> nat -> nat
-Nat.min: nat -> nat -> nat
-Nat.pow: nat -> nat -> nat
 Nat.div: nat -> nat -> nat
+Nat.pow: nat -> nat -> nat
+Nat.min: nat -> nat -> nat
 Nat.modulo: nat -> nat -> nat
 Nat.gcd: nat -> nat -> nat
-Nat.square: nat -> nat
 Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat
-Nat.sqrt: nat -> nat
 Nat.log2_iter: nat -> nat -> nat -> nat -> nat
-Nat.log2: nat -> nat
-Nat.div2: nat -> nat
+length: forall A : Type, list A -> nat
 Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
-Nat.land: nat -> nat -> nat
-Nat.lor: nat -> nat -> nat
+Nat.div2: nat -> nat
+Nat.sqrt: nat -> nat
+Nat.log2: nat -> nat
+Nat.double: nat -> nat
+Nat.pred: nat -> nat
+Nat.square: nat -> nat
+Nat.succ: nat -> nat
+S: nat -> nat
 Nat.ldiff: nat -> nat -> nat
+Nat.pow: nat -> nat -> nat
+Nat.land: nat -> nat -> nat
 Nat.lxor: nat -> nat -> nat
-S: nat -> nat
-Nat.succ: nat -> nat
-Nat.pred: nat -> nat
-Nat.add: nat -> nat -> nat
-Nat.double: nat -> nat
+Nat.div: nat -> nat -> nat
 Nat.mul: nat -> nat -> nat
-Nat.sub: nat -> nat -> nat
-Nat.max: nat -> nat -> nat
 Nat.min: nat -> nat -> nat
-Nat.pow: nat -> nat -> nat
-Nat.div: nat -> nat -> nat
 Nat.modulo: nat -> nat -> nat
+Nat.sub: nat -> nat -> nat
+Nat.lor: nat -> nat -> nat
 Nat.gcd: nat -> nat -> nat
-Nat.square: nat -> nat
-Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat
-Nat.sqrt: nat -> nat
+Nat.max: nat -> nat -> nat
+Nat.add: nat -> nat -> nat
 Nat.log2_iter: nat -> nat -> nat -> nat -> nat
-Nat.log2: nat -> nat
-Nat.div2: nat -> nat
+Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat
 Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
-Nat.land: nat -> nat -> nat
-Nat.lor: nat -> nat -> nat
-Nat.ldiff: nat -> nat -> nat
-Nat.lxor: nat -> nat -> nat
 mult_n_Sm: forall n m : nat, n * m + n = n * S m
-identity_refl: forall (A : Type) (a : A), identity a a
 iff_refl: forall A : Prop, A <-> A
+le_n: forall n : nat, n <= n
+identity_refl: forall (A : Type) (a : A), identity a a
 eq_refl: forall (A : Type) (x : A), x = x
 Nat.divmod: nat -> nat -> nat -> nat -> nat * nat
-le_n: forall n : nat, n <= n
-pair: forall A B : Type, A -> B -> A * B
 conj: forall A B : Prop, A -> B -> A /\ B
+pair: forall A B : Type, A -> B -> A * B
 Nat.divmod: nat -> nat -> nat -> nat -> nat * nat
 h: n <> newdef n
 h: n <> newdef n
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)