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

15 files changed, 73 insertions, 21 deletions

diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index ab4a6a25c..bf5b7db41 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -48,7 +48,8 @@ let gen_constant_in_modules locstr dirs s =
   let dirs = List.map make_dir dirs in
   let qualid = qualid_of_string s in
   let all = Nametab.locate_extended_all qualid in
-  let all = List.uniquize (List.map_filter global_of_extended all) in
+  let all = List.map_filter global_of_extended all in
+  let all = List.sort_uniquize RefOrdered_env.compare all in
   let these = List.filter (has_suffix_in_dirs dirs) all in
   match these with
     | [x] -> constr_of_global x
diff --git a/kernel/names.ml b/kernel/names.ml
index 2a04ff3c5..00b8df486 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -71,10 +71,16 @@ module Name =
 struct
   type t = Name of Id.t | Anonymous
 
+  let compare n1 n2 = match n1, n2 with
+    | Anonymous, Anonymous -> 0
+    | Name id1, Name id2 -> Id.compare id1 id2
+    | Anonymous, Name _ -> -1
+    | Name _, Anonymous -> 1
+
   let equal n1 n2 = match n1, n2 with
-  | Anonymous, Anonymous -> true
-  | Name id1, Name id2 -> String.equal id1 id2
-  | _ -> false
+    | Anonymous, Anonymous -> true
+    | Name id1, Name id2 -> String.equal id1 id2
+    | _ -> false
 
   module Self_Hashcons =
     struct
diff --git a/kernel/names.mli b/kernel/names.mli
index 82df07562..6f4ac9a53 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -53,6 +53,9 @@ sig
   type t = Name of Id.t | Anonymous
   (** A name is either undefined, either an identifier. *)
 
+  val compare : t -> t -> int
+  (** Comparison over names. *)
+
   val equal : t -> t -> bool
   (** Equality over names. *)
 
diff --git a/lib/cList.ml b/lib/cList.ml
index 8fa8c392f..db2aa2bcf 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 99d6aab15..60110228a 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. *)
 
diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4
index d94a7136a..082eac422 100644
--- a/plugins/omega/g_omega.ml4
+++ b/plugins/omega/g_omega.ml4
@@ -26,7 +26,7 @@ let omega_tactic l =
        | "N" -> Tacinterp.interp <:tactic<zify_N>>
        | "Z" -> Tacinterp.interp <:tactic<zify_op>>
        | s -> Errors.error ("No Omega knowledge base for type "^s))
-    (Util.List.uniquize (List.sort compare l))
+    (Util.List.sort_uniquize String.compare l)
   in
   tclTHEN
     (tclREPEAT (tclPROGRESS (tclTHENLIST tacs)))
diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4
index a68196e8c..055546c8b 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
@@ -19,7 +19,7 @@ let romega_tactic l =
        | "N" -> Tacinterp.interp <:tactic<zify_N>>
        | "Z" -> Tacinterp.interp <:tactic<zify_op>>
        | s -> Errors.error ("No ROmega knowledge base for type "^s))
-    (Util.List.uniquize (List.sort compare l))
+    (Util.List.sort_uniquize String.compare l)
   in
   tclTHEN
     (tclREPEAT (tclPROGRESS (tclTHENLIST tacs)))
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index fc5fc0d2c..aa8f2d08e 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -781,17 +781,20 @@ let invert_invertible_arg fullenv evd aliases k (evk,argsv) args' =
  * such that "hyps' |- ?e : T"
  *)
 
+let set_of_evctx l =
+  List.fold_left (fun s (id,_,_) -> Id.Set.add id s) Id.Set.empty l
+
 let filter_candidates evd evk filter candidates =
   let evi = Evd.find_undefined evd evk in
   let candidates = match candidates with
   | None -> evi.evar_candidates
-  | Some _ -> candidates in
+  | Some _ -> candidates
+  in
   match candidates,filter with
   | None,_ | _, None -> candidates
   | Some l, Some filter ->
-      let ids = List.map pi1 (List.filter_with filter (evar_context evi)) in
-      Some (List.filter (fun a ->
-        List.subset (Id.Set.elements (collect_vars a)) ids) l)
+      let ids = set_of_evctx (List.filter_with filter (evar_context evi)) in
+      Some (List.filter (fun a -> Id.Set.subset (collect_vars a) ids) l)
 
 let eq_filter f1 f2 =
   let eq_bool b1 b2 = if b1 then b2 else not b2 in
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 1db40e8db..13eb91393 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -180,7 +180,7 @@ let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) =
 	     raise Elimconst) args
   in
   let reversible_rels = List.map fst li in
-  if not (List.distinct reversible_rels) then
+  if not (List.distinct_f Int.compare reversible_rels) then
     raise Elimconst;
   List.iteri (fun i t_i ->
     if not (List.mem_assoc (i+1) li) then
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 2e2389f09..899def8c8 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -696,7 +696,7 @@ let replace_term = replace_term_gen eq_constr
    except the ones in l *)
 
 let error_invalid_occurrence l =
-  let l = List.uniquize (List.sort Pervasives.compare l) in
+  let l = List.sort_uniquize Int.compare l in
   errorlabstrm ""
     (str ("Invalid occurrence " ^ String.plural (List.length l) "number" ^": ") ++
      prlist_with_sep spc int l ++ str ".")
diff --git a/proofs/logic.ml b/proofs/logic.ml
index f88331750..5a29c3b0e 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -329,7 +329,7 @@ let collect_meta_variables c =
   List.rev (collrec false [] c)
 
 let check_meta_variables c =
-  if not (List.distinct (collect_meta_variables c)) then
+  if not (List.distinct_f Int.compare (collect_meta_variables c)) then
     raise (RefinerError (NonLinearProof c))
 
 let check_conv_leq_goal env sigma arg ty conclty =
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index bf07156f7..67c5ba92f 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -369,8 +369,8 @@ let get_common_underlying_mutual_inductive = function
       | (_,ind')::_ ->
 	  raise (RecursionSchemeError (NotMutualInScheme (ind,ind')))
       | [] ->
-	  if not (List.distinct (List.map snd (List.map snd all))) then
-	    error "A type occurs twice";
+	  if not (List.distinct_f Int.compare (List.map snd (List.map snd all)))
+          then error "A type occurs twice";
 	  mind,
 	  List.map_filter
 	    (function (Some id,(_,i)) -> Some (i,snd id) | (None,_) -> None) all
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index a25f96d46..519112dfd 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -135,8 +135,13 @@ let find_mutually_recursive_statements thms =
       | [], _::_ ->
           let () = match same_indccl with
           | ind :: _ ->
-            if List.distinct (List.map pi1 ind) then
-              if_verbose msg_info (strbrk "Coinductive statements do not follow the order of definition, assuming the proof to be by induction."); flush_all ()
+            if List.distinct_f ind_ord (List.map pi1 ind)
+            then
+              if_verbose msg_info
+                (strbrk
+                   ("Coinductive statements do not follow the order of "^
+                    "definition, assuming the proof to be by induction."));
+            flush_all ()
           | _ -> ()
           in
           let possible_guards = List.map (List.map pi3) inds_hyps in
diff --git a/toplevel/record.ml b/toplevel/record.ml
index e0dc6c3a3..cf5714546 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -376,7 +376,8 @@ let definition_structure (kind,finite,infer,(is_coe,(loc,idstruc)),ps,cfs,idbuil
     | Vernacexpr.DefExpr ((_,Name id),_,_) -> id::acc
     | _ -> acc in
   let allnames =  idstruc::(List.fold_left extract_name [] fs) in
-  if not (List.distinct allnames) then error "Two objects have the same name";
+  if not (List.distinct_f Id.compare allnames)
+  then error "Two objects have the same name";
   let isnot_class = match kind with Class false -> false | _ -> true in
   if isnot_class && List.exists (fun opt -> not (Option.is_empty opt)) priorities then
     error "Priorities only allowed for type class substructures";
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index fd4ac4890..3c104f543 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -802,7 +802,8 @@ let vernac_set_end_tac tac =
 
 let vernac_set_used_variables l =
   let l = List.map snd l in
-  if not (List.distinct l) then error "Used variables list contains duplicates";
+  if not (List.distinct_f Id.compare l)
+  then error "Used variables list contains duplicates";
   let vars = Environ.named_context (Global.env ()) in
   List.iter (fun id -> 
     if not (List.exists (fun (id',_,_) -> Id.equal id id') vars) then
@@ -898,8 +899,8 @@ let vernac_declare_arguments locality r l nargs flags =
   let scopes = List.map (List.map (fun (_,_, s, _,_) -> s)) l in
   if List.exists (fun na -> not (List.equal Name.equal na names)) rest then
     error "All arguments lists must declare the same names.";
-  if not (List.distinct (List.filter ((!=) Anonymous) names)) then
-    error "Arguments names must be distinct.";
+  if not (List.distinct_f Name.compare (List.filter ((!=) Anonymous) names))
+  then error "Arguments names must be distinct.";
   let sr = smart_global r in
   let inf_names =
     Impargs.compute_implicits_names (Global.env()) (Global.type_of_global sr) in