aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/coqlib.ml3
-rw-r--r--kernel/names.ml12
-rw-r--r--kernel/names.mli3
-rw-r--r--lib/cList.ml26
-rw-r--r--lib/cList.mli6
-rw-r--r--plugins/omega/g_omega.ml42
-rw-r--r--plugins/romega/g_romega.ml42
-rw-r--r--pretyping/evarsolve.ml11
-rw-r--r--pretyping/tacred.ml2
-rw-r--r--pretyping/termops.ml2
-rw-r--r--proofs/logic.ml2
-rw-r--r--toplevel/indschemes.ml4
-rw-r--r--toplevel/lemmas.ml9
-rw-r--r--toplevel/record.ml3
-rw-r--r--toplevel/vernacentries.ml7
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 10:51:41 +0000