From e0e52953a7b06b52603eb6f592dbf40cb325a4de Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Sat, 30 Jul 2016 17:51:19 +0200
Subject: Refine the relevance measure

Having more disctinc symbols incurs a penalty.
---
 toplevel/search.ml | 23 +++++++++++++++++++++--
 1 file changed, 21 insertions(+), 2 deletions(-)

diff --git a/toplevel/search.ml b/toplevel/search.ml
index d207ba7e0e..e4db764759 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -118,12 +118,29 @@ module ConstrPriority = struct
 
   type t = Globnames.global_reference * Environ.env * Constr.t
 
+  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))
+
+    -(3*(num_symbols t) + size t)
+
   let compare (_,_,t1) (_,_,t2) =
-    -compare (size t1) (size t2)
+    compare (priority t1) (priority t2)
 end
 
 module PriorityQueue = Heap.Functional(ConstrPriority)
@@ -137,7 +154,9 @@ let rec iter_priority_queue q fn =
       with Heap.EmptyHeap -> None
   end in
   match next with
-  | Some (gref,env,t) -> fn gref env t; iter_priority_queue (PriorityQueue.remove q) fn
+  | Some (gref,env,t) ->
+    fn gref env t;
+    iter_priority_queue (PriorityQueue.remove q) fn
   | None -> ()
 
 let prioritize_search seq fn =
-- 
cgit v1.2.3