Merge PR #8766: [nametab] [api] Provide basic support for efficient completion.

5 files changed, 59 insertions, 4 deletions

diff --git a/clib/cMap.ml b/clib/cMap.ml
index 040dede0a2..e4ce6c7c02 100644
--- a/clib/cMap.ml
+++ b/clib/cMap.ml
@@ -35,6 +35,7 @@ sig
   val fold_left : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
   val fold_right : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
   val height : 'a t -> int
+  val filter_range : (key -> int) -> 'a t -> 'a t
   module Smart :
   sig
     val map : ('a -> 'a) -> 'a t -> 'a t
@@ -62,6 +63,7 @@ sig
   val fold_left : (M.t -> 'a -> 'b -> 'b) -> 'a map -> 'b -> 'b
   val fold_right : (M.t -> 'a -> 'b -> 'b) -> 'a map -> 'b -> 'b
   val height : 'a map -> int
+  val filter_range : (M.t -> int) -> 'a map -> 'a map
   module Smart :
   sig
     val map : ('a -> 'a) -> 'a map -> 'a map
@@ -85,8 +87,11 @@ struct
       if this happens, we can still implement a less clever version of [domain].
   *)
 
-  type 'a map = 'a Map.Make(M).t
-  type set = Set.Make(M).t
+  module F = Map.Make(M)
+  type 'a map = 'a F.t
+
+  module S = Set.Make(M)
+  type set = S.t
 
   type 'a _map =
   | MEmpty
@@ -164,6 +169,23 @@ struct
   | MEmpty -> 0
   | MNode (_, _, _, _, h) -> h
 
+  (* Filter based on a range *)
+  let filter_range in_range m =
+    let rec aux m = function
+      | MEmpty -> m
+      | MNode (l, k, v, r, _) ->
+        let vr = in_range k in
+        (* the range is below the current value *)
+        if vr < 0 then aux m (map_prj l)
+        (* the range is above the current value *)
+        else if vr > 0 then aux m (map_prj r)
+        (* The current value is in the range *)
+        else
+          let m = aux m (map_prj l) in
+          let m = aux m (map_prj r) in
+          F.add k v m
+    in aux F.empty (map_prj m)
+
   module Smart =
   struct
 
diff --git a/clib/cMap.mli b/clib/cMap.mli
index f5496239f6..ca6ddb2f4e 100644
--- a/clib/cMap.mli
+++ b/clib/cMap.mli
@@ -60,6 +60,12 @@ sig
   val height : 'a t -> int
   (** An indication of the logarithmic size of a map *)
 
+  val filter_range : (key -> int) -> 'a t -> 'a t
+  (** [find_range in_range m] Given a comparison function [in_range x],
+      that tests if [x] is below, above, or inside a given range
+      [filter_range] returns the submap of [m] whose keys are in
+      range. Note that [in_range] has to define a continouous range. *)
+
   module Smart :
   sig
     val map : ('a -> 'a) -> 'a t -> 'a t
diff --git a/clib/hMap.ml b/clib/hMap.ml
index 33cb6d0131..9c80398e4d 100644
--- a/clib/hMap.ml
+++ b/clib/hMap.ml
@@ -398,6 +398,10 @@ struct
 
   let height s = Int.Map.height s
 
+  (* Not as efficient as the original version *)
+  let filter_range f s =
+    filter (fun x _ -> f x = 0) s
+
   module Unsafe =
   struct
     let map f s =
diff --git a/library/nametab.ml b/library/nametab.ml
index 06ace373c3..029d850504 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -74,6 +74,8 @@ module type NAMETREE = sig
   val user_name : qualid -> t -> user_name
   val shortest_qualid : ?loc:Loc.t -> Id.Set.t -> user_name -> t -> qualid
   val find_prefixes : qualid -> t -> elt list
+  (** Matches a prefix of [qualid], useful for completion *)
+  val match_prefixes : qualid -> t -> elt list
 end
 
 module Make (U : UserName) (E : EqualityType) : NAMETREE
@@ -259,9 +261,19 @@ let find_prefixes qid tab =
     search_prefixes (Id.Map.find id tab) (DirPath.repr dir)
   with Not_found -> []
 
-end
-
+let match_prefixes =
+  let cprefix x y = CString.(compare x (sub y 0 (min (length x) (length y)))) in
+  fun qid tab ->
+    try
+      let (dir,id) = repr_qualid qid in
+      let id_prefix = cprefix Id.(to_string id) in
+      let matches = Id.Map.filter_range (fun x -> id_prefix Id.(to_string x)) tab in
+      let matches = Id.Map.mapi (fun _key tab -> search_prefixes tab (DirPath.repr dir)) matches in
+      (* Coq's flatten is "magical", so this is not so bad perf-wise *)
+      CList.flatten @@ Id.Map.(fold (fun _ r l -> r :: l) matches [])
+    with Not_found -> []
 
+end
 
 (* Global name tables *************************************************)
 
@@ -447,6 +459,10 @@ let locate_extended_all_dir qid = DirTab.find_prefixes qid !the_dirtab
 
 let locate_extended_all_modtype qid = MPTab.find_prefixes qid !the_modtypetab
 
+(* Completion *)
+let completion_canditates qualid =
+  ExtRefTab.match_prefixes qualid !the_ccitab
+
 (* Derived functions *)
 
 let locate_constant qid =
diff --git a/library/nametab.mli b/library/nametab.mli
index 1c3322bfb1..1e479b200b 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -118,6 +118,12 @@ val locate_extended_all : qualid -> extended_global_reference list
 val locate_extended_all_dir : qualid -> global_dir_reference list
 val locate_extended_all_modtype : qualid -> ModPath.t list
 
+(** Experimental completion support, API is _unstable_ *)
+val completion_canditates : qualid -> extended_global_reference list
+(** [completion_canditates qualid] will return the list of global
+    references that have [qualid] as a prefix. UI usually will want to
+    compose this with [shortest_qualid_of_global] *)
+
 (** Mapping a full path to a global reference *)
 
 val global_of_path : full_path -> GlobRef.t
@@ -211,6 +217,7 @@ module type NAMETREE = sig
   val user_name : qualid -> t -> user_name
   val shortest_qualid : ?loc:Loc.t -> Id.Set.t -> user_name -> t -> qualid
   val find_prefixes : qualid -> t -> elt list
+  val match_prefixes : qualid -> t -> elt list
 end
 
 module Make (U : UserName) (E : EqualityType) :