cList: a few alternative to hashtbl-based uniquize, distinct, subset

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16924 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 32 insertions, 0 deletions

diff --git a/lib/cList.ml b/lib/cList.ml
index 8fa8c392ff..db2aa2bcfa 100644
--- a/lib/cList.ml
+++ b/lib/cList.ml
@@ -73,6 +73,7 @@ sig
   val make : int -> 'a -> 'a list
   val assign : 'a list -> int -> 'a -> 'a list
   val distinct : 'a list -> bool
+  val distinct_f : 'a cmp -> 'a list -> bool
   val duplicates : 'a eq -> 'a list -> 'a list
   val filter2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list
   val map_filter : ('a -> 'b option) -> 'a list -> 'b list
@@ -107,6 +108,7 @@ sig
   val sep_last : 'a list -> 'a * 'a list
   val find_map : ('a -> 'b option) -> 'a list -> 'b
   val uniquize : 'a list -> 'a list
+  val sort_uniquize : 'a cmp -> 'a list -> 'a list
   val merge_uniq : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list
   val subset : 'a list -> 'a list -> bool
   val chop : int -> 'a list -> 'a list * 'a list
@@ -507,6 +509,9 @@ let rec find_map f = function
   | None -> find_map f l
   | Some y -> y
 
+(* FIXME: we should avoid relying on the generic hash function,
+   just as we'd better avoid Pervasives.compare *)
+
 let uniquize l =
   let visited = Hashtbl.create 23 in
   let rec aux acc = function
@@ -518,6 +523,18 @@ let uniquize l =
     | [] -> List.rev acc
   in aux [] l
 
+(** [sort_uniquize] might be an alternative to the hashtbl-based
+    [uniquize], when the order of the elements is irrelevant *)
+
+let rec uniquize_sorted cmp = function
+  | a::b::l when Int.equal (cmp a b) 0 -> uniquize_sorted cmp (a::l)
+  | a::l -> a::uniquize_sorted cmp l
+  | [] -> []
+
+let sort_uniquize cmp l = uniquize_sorted cmp (List.sort cmp l)
+
+(* FIXME: again, generic hash function *)
+
 let distinct l =
   let visited = Hashtbl.create 23 in
   let rec loop = function
@@ -531,6 +548,13 @@ let distinct l =
     | [] -> true
   in loop l
 
+let distinct_f cmp l =
+  let rec loop = function
+    | a::b::_ when Int.equal (cmp a b) 0 -> false
+    | a::l -> loop l
+    | [] -> true
+  in loop (List.sort cmp l)
+
 let rec merge_uniq cmp l1 l2 =
   match l1, l2 with
   | [], l2 -> l2
@@ -588,6 +612,8 @@ let rec filter_with filter l = match filter, l with
 | false :: filter, _ :: l -> filter_with filter l
 | _ -> invalid_arg "List.filter_with"
 
+(* FIXME: again, generic hash function *)
+
 let subset l1 l2 =
   let t2 = Hashtbl.create 151 in
   List.iter (fun x -> Hashtbl.add t2 x ()) l2;
diff --git a/lib/cList.mli b/lib/cList.mli
index 99d6aab156..60110228a2 100644
--- a/lib/cList.mli
+++ b/lib/cList.mli
@@ -103,6 +103,8 @@ sig
   val distinct : 'a list -> bool
   (** Return [true] if all elements of the list are distinct. *)
 
+  val distinct_f : 'a cmp -> 'a list -> bool
+
   val duplicates : 'a eq -> 'a list -> 'a list
   (** Return the list of unique elements which appear at least twice. Elements
       are kept in the order of their first appearance. *)
@@ -169,6 +171,10 @@ sig
   val uniquize : 'a list -> 'a list
   (** Return the list of elements without duplicates. *)
 
+  val sort_uniquize : 'a cmp -> 'a list -> 'a list
+  (** Return a sorted and de-duplicated version of a list,
+      according to some comparison function. *)
+
   val merge_uniq : 'a cmp -> 'a list -> 'a list -> 'a list
   (** Merge two sorted lists and preserves the uniqueness property. *)