aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/closure.ml17
-rw-r--r--kernel/mod_subst.ml2
-rw-r--r--kernel/names.ml108
-rw-r--r--kernel/names.mli4
-rw-r--r--kernel/univ.ml16
-rw-r--r--lib/flags.ml8
-rw-r--r--lib/hashcons.ml3
-rw-r--r--lib/hashset.ml2
-rw-r--r--lib/util.ml18
-rw-r--r--library/libnames.ml4
-rw-r--r--pretyping/evd.ml2
-rw-r--r--pretyping/recordops.ml2
-rw-r--r--pretyping/unification.ml6
-rw-r--r--tactics/autorewrite.ml4
-rw-r--r--toplevel/obligations.ml2
15 files changed, 132 insertions, 66 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml
index 251c32ac5..51e264106 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -199,6 +199,15 @@ let unfold_red kn =
type table_key = id_key
+module IdKeyHash =
+struct
+ type t = id_key
+ let equal = Names.eq_id_key
+ let hash = Hashtbl.hash
+end
+
+module KeyTable = Hashtbl.Make(IdKeyHash)
+
let eq_table_key = Names.eq_id_key
type 'a infos = {
@@ -208,13 +217,13 @@ type 'a infos = {
i_sigma : existential -> constr option;
i_rels : int * (int * constr) list;
i_vars : (identifier * constr) list;
- i_tab : (table_key, 'a) Hashtbl.t }
+ i_tab : 'a KeyTable.t }
let info_flags info = info.i_flags
let ref_value_cache info ref =
try
- Some (Hashtbl.find info.i_tab ref)
+ Some (KeyTable.find info.i_tab ref)
with Not_found ->
try
let body =
@@ -225,7 +234,7 @@ let ref_value_cache info ref =
| ConstKey cst -> constant_value info.i_env cst
in
let v = info.i_repr info body in
- Hashtbl.add info.i_tab ref v;
+ KeyTable.add info.i_tab ref v;
Some v
with
| Not_found (* List.assoc *)
@@ -262,7 +271,7 @@ let create mk_cl flgs env evars =
i_sigma = evars;
i_rels = defined_rels flgs env;
i_vars = defined_vars flgs env;
- i_tab = Hashtbl.create 17 }
+ i_tab = KeyTable.create 17 }
(**********************************************************************)
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 8bd0a653c..f2511dbde 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -50,7 +50,7 @@ let empty_delta_resolver = Deltamap.empty
module MBImap = Map.Make
(struct
type t = mod_bound_id
- let compare = Pervasives.compare
+ let compare = mod_bound_id_ord
end)
module Umap = struct
diff --git a/kernel/names.ml b/kernel/names.ml
index 520a9aa64..cbd66e03d 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -42,10 +42,9 @@ let id_of_string s =
let string_of_id id = String.copy id
-let id_ord (x:string) (y:string) =
- if x == y
- then 0
- else Pervasives.compare x y
+let id_ord (x : string) (y : string) =
+ (* String.compare already checks for pointer equality *)
+ String.compare x y
module IdOrdered =
struct
@@ -81,6 +80,17 @@ type dir_path = module_ident list
module ModIdmap = Idmap
+let rec dir_path_ord (p1 : dir_path) (p2 : dir_path) =
+ if p1 == p2 then 0
+ else begin match p1, p2 with
+ | [], [] -> 0
+ | [], _ -> -1
+ | _, [] -> 1
+ | id1 :: p1, id2 :: p2 ->
+ let c = id_ord id1 id2 in
+ if c <> 0 then c else dir_path_ord p1 p2
+ end
+
let make_dirpath x = x
let repr_dirpath x = x
@@ -102,15 +112,28 @@ let make_uid dir s = incr u_number;(!u_number,s,dir)
let string_of_uid (i,s,p) =
string_of_dirpath p ^"."^s
-module Umap = Map.Make(struct
- type t = uniq_ident
- let compare x y =
- if x == y
- then 0
- else Pervasives.compare x y
- end)
+let uniq_ident_ord (x : uniq_ident) (y : uniq_ident) =
+ if x == y then 0
+ else match (x, y) with
+ | (nl, idl, dpl), (nr, idr, dpr) ->
+ let ans = nl - nr in
+ if ans <> 0 then ans
+ else
+ let ans = id_ord idl idr in
+ if ans <> 0 then ans
+ else
+ dir_path_ord dpl dpr
+
+module UOrdered =
+struct
+ type t = uniq_ident
+ let compare = uniq_ident_ord
+end
+
+module Umap = Map.Make(UOrdered)
type mod_bound_id = uniq_ident
+let mod_bound_id_ord = uniq_ident_ord
let make_mbid = make_uid
let repr_mbid (n, id, dp) = (n, id, dp)
let debug_string_of_mbid = debug_string_of_uid
@@ -150,14 +173,19 @@ let rec string_of_mp = function
(** we compare labels first if both are MPdots *)
let rec mp_ord mp1 mp2 =
if mp1 == mp2 then 0
- else match (mp1,mp2) with
- MPdot(mp1,l1), MPdot(mp2,l2) ->
- let c = Pervasives.compare l1 l2 in
- if c<>0 then
- c
- else
- mp_ord mp1 mp2
- | _,_ -> Pervasives.compare mp1 mp2
+ else match (mp1, mp2) with
+ | MPfile p1, MPfile p2 ->
+ dir_path_ord p1 p2
+ | MPbound id1, MPbound id2 ->
+ uniq_ident_ord id1 id2
+ | MPdot (mp1, l1), MPdot (mp2, l2) ->
+ let c = String.compare l1 l2 in
+ if c <> 0 then c
+ else mp_ord mp1 mp2
+ | MPfile _, _ -> -1
+ | MPbound _, MPfile _ -> 1
+ | MPbound _, MPdot _ -> -1
+ | MPdot _, _ -> 1
module MPord = struct
type t = module_path
@@ -192,21 +220,17 @@ let string_of_kn (mp,dir,l) =
let pr_kn kn = str (string_of_kn kn)
-let kn_ord kn1 kn2 =
- if kn1 == kn2 then
- 0
+let kn_ord (kn1 : kernel_name) (kn2 : kernel_name) =
+ if kn1 == kn2 then 0
else
- let mp1,dir1,l1 = kn1 in
- let mp2,dir2,l2 = kn2 in
- let c = Pervasives.compare l1 l2 in
- if c <> 0 then
- c
+ let mp1, dir1, l1 = kn1 in
+ let mp2, dir2, l2 = kn2 in
+ let c = String.compare l1 l2 in
+ if c <> 0 then c
else
- let c = Pervasives.compare dir1 dir2 in
- if c<>0 then
- c
- else
- MPord.compare mp1 mp2
+ let c = dir_path_ord dir1 dir2 in
+ if c <> 0 then c
+ else MPord.compare mp1 mp2
module KNord = struct
type t = kernel_name
@@ -392,7 +416,7 @@ module Huniqid = Hashcons.Make(
let hashcons (hid,hdir) (n,s,dir) = (n,hid s,hdir dir)
let equal ((n1,s1,dir1) as x) ((n2,s2,dir2) as y) =
(x == y) ||
- (n1 = n2 && s1 == s2 && dir1 == dir2)
+ (n1 - n2 = 0 && s1 == s2 && dir1 == dir2)
let hash = Hashtbl.hash
end)
@@ -454,7 +478,7 @@ module Hconstruct = Hashcons.Make(
type t = constructor
type u = inductive -> inductive
let hashcons hind (ind, j) = (hind ind, j)
- let equal (ind1,j1) (ind2,j2) = ind1 == ind2 && j1 = j2
+ let equal (ind1,j1) (ind2,j2) = ind1 == ind2 && (j1 - j2 = 0)
let hash = Hashtbl.hash
end)
@@ -493,11 +517,17 @@ type inv_rel_key = int (* index in the [rel_context] part of environment
type id_key = inv_rel_key tableKey
let eq_id_key ik1 ik2 =
- (ik1 == ik2) ||
- (match ik1,ik2 with
- ConstKey (_,kn1),
- ConstKey (_,kn2) -> kn1=kn2
- | a,b -> a=b)
+ if ik1 == ik2 then true
+ else match ik1,ik2 with
+ | ConstKey (u1, kn1), ConstKey (u2, kn2) ->
+ let ans = (kn_ord u1 u2 = 0) in
+ if ans then kn_ord kn1 kn2 = 0
+ else ans
+ | VarKey id1, VarKey id2 ->
+ id_ord id1 id2 = 0
+ | RelKey k1, RelKey k2 ->
+ k1 - k2 = 0
+ | _ -> false
let eq_con_chk (kn1,_) (kn2,_) = kn1=kn2
let eq_mind_chk (kn1,_) (kn2,_) = kn1=kn2
diff --git a/kernel/names.mli b/kernel/names.mli
index bb6696389..5c2bd5b0a 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -40,6 +40,8 @@ module ModIdmap : Map.S with type key = module_ident
type dir_path
+val dir_path_ord : dir_path -> dir_path -> int
+
(** Inner modules idents on top of list (to improve sharing).
For instance: A.B.C is ["C";"B";"A"] *)
val make_dirpath : module_ident list -> dir_path
@@ -68,6 +70,8 @@ module Labmap : Map.S with type key = label
type mod_bound_id
+val mod_bound_id_ord : mod_bound_id -> mod_bound_id -> int
+
(** The first argument is a file name - to prevent conflict between
different files *)
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 39cb6bc10..635991494 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -53,11 +53,12 @@ module UniverseLevel = struct
| Level (i1, dp1), Level (i2, dp2) ->
if i1 < i2 then -1
else if i1 > i2 then 1
- else compare dp1 dp2)
+ else Names.dir_path_ord dp1 dp2)
let equal u v = match u,v with
| Set, Set -> true
- | Level (i1, dp1), Level (i2, dp2) -> i1 = i2 && dp1 = dp2
+ | Level (i1, dp1), Level (i2, dp2) ->
+ i1 = i2 && (Names.dir_path_ord dp1 dp2 = 0)
| _ -> false
let to_string = function
@@ -272,6 +273,15 @@ let between g arcu arcv =
type constraint_type = Lt | Le | Eq
type explanation = (constraint_type * universe) list
+let constraint_type_ord c1 c2 = match c1, c2 with
+| Lt, Lt -> 0
+| Lt, _ -> -1
+| Le, Lt -> 1
+| Le, Le -> 0
+| Le, Eq -> -1
+| Eq, Eq -> 0
+| Eq, _ -> 1
+
(* Assuming the current universe has been reached by [p] and [l]
correspond to the universes in (direct) relation [rel] with it,
make a list of canonical universe, updating the relation with
@@ -527,7 +537,7 @@ module Constraint = Set.Make(
struct
type t = univ_constraint
let compare (u,c,v) (u',c',v') =
- let i = Pervasives.compare c c' in
+ let i = constraint_type_ord c c' in
if i <> 0 then i
else
let i' = UniverseLevel.compare u u' in
diff --git a/lib/flags.ml b/lib/flags.ml
index 2b10125a0..4ec378793 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -101,7 +101,13 @@ let print_hyps_limit () = !print_hyps_limit
(* A list of the areas of the system where "unsafe" operation
* has been requested *)
-module Stringset = Set.Make(struct type t = string let compare = compare end)
+module StringOrd =
+struct
+ type t = string
+ let compare (x : t) (y : t) = String.compare x y
+end
+
+module Stringset = Set.Make(StringOrd)
let unsafe_set = ref Stringset.empty
let add_unsafe s = unsafe_set := Stringset.add s !unsafe_set
diff --git a/lib/hashcons.ml b/lib/hashcons.ml
index 8daeec944..745169dc0 100644
--- a/lib/hashcons.ml
+++ b/lib/hashcons.ml
@@ -132,8 +132,7 @@ module Hstring = Make(
type t = string
type u = unit
let hashcons () s =(* incr accesstr;*) s
- let equal s1 s2 =(* incr comparaisonstr;
- if*) s1=s2(* then (incr successtr; true) else false*)
+ let equal (s1 : t) (s2 : t) = s1 = s2
let hash = Hashtbl.hash
end)
diff --git a/lib/hashset.ml b/lib/hashset.ml
index fd3d1a554..6f62e1a90 100644
--- a/lib/hashset.ml
+++ b/lib/hashset.ml
@@ -79,6 +79,8 @@ module Make (E : EqType) =
if i >= Weak.length b then accu else
count_bucket (i+1) b (accu + (if Weak.check b i then 1 else 0))
+ let min x y = if x - y < 0 then x else y
+
let next_sz n = min (3 * n / 2 + 3) Sys.max_array_length
let prev_sz n = ((n - 3) * 2 + 2) / 3
diff --git a/lib/util.ml b/lib/util.ml
index af3b13fa7..6a0ba470a 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -137,9 +137,14 @@ let subst_command_placeholder s t =
done;
Buffer.contents buff
-module Stringset = Set.Make(struct type t = string let compare (x:t) (y:t) = compare x y end)
+module StringOrd =
+struct
+ type t = string
+ external compare : string -> string -> int = "caml_string_compare"
+end
-module Stringmap = Map.Make(struct type t = string let compare (x:t) (y:t) = compare x y end)
+module Stringset = Set.Make(StringOrd)
+module Stringmap = Map.Make(StringOrd)
(* Lists *)
@@ -202,9 +207,14 @@ let delayed_force f = f ()
type ('a,'b) union = Inl of 'a | Inr of 'b
-module Intset = Set.Make(struct type t = int let compare (x:t) (y:t) = compare x y end)
+module IntOrd =
+struct
+ type t = int
+ external compare : int -> int -> int = "caml_int_compare"
+end
-module Intmap = Map.Make(struct type t = int let compare (x:t) (y:t) = compare x y end)
+module Intset = Set.Make(IntOrd)
+module Intmap = Map.Make(IntOrd)
(*s interruption *)
diff --git a/library/libnames.ml b/library/libnames.ml
index 3555766f8..197588f53 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -69,8 +69,8 @@ let dirpath_of_string s =
let string_of_dirpath = Names.string_of_dirpath
-module Dirset = Set.Make(struct type t = dir_path let compare = compare end)
-module Dirmap = Map.Make(struct type t = dir_path let compare = compare end)
+module Dirset = Set.Make(struct type t = dir_path let compare = dir_path_ord end)
+module Dirmap = Map.Make(struct type t = dir_path let compare = dir_path_ord end)
(*s Section paths are absolute names *)
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index dab4ee9c7..d696db3e7 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -568,7 +568,7 @@ let undefined_metas evd =
| (n,Cltyp (_,typ)) -> Some n
in
let m = List.map_filter filter (meta_list evd) in
- List.sort Pervasives.compare m
+ List.sort (-) m
let metas_of evd =
List.map (function
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index f32eb0879..fdc7875d7 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -114,6 +114,8 @@ module MethodsDnet : Term_dnet.S
= Term_dnet.Make
(struct
type t = global_reference * Evd.evar * Evd.evar_map
+ (** ppedrot: FIXME: this is surely wrong, generic equality has nothing to
+ do w.r.t. evar maps. *)
let compare = Pervasives.compare
let subst = subst_id
let constr_of (_,ev,evm) = Evd.evar_concl (Evd.find evm ev)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index e25a880f8..447ee8e3b 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -103,13 +103,9 @@ let extract_instance_status = function
| CUMUL -> add_type_status (IsSubType, IsSuperType)
| CONV -> add_type_status (Conv, Conv)
-let rec assoc_pair x = function
- [] -> raise Not_found
- | (a,b,_)::l -> if compare a x = 0 then b else assoc_pair x l
-
let rec subst_meta_instances bl c =
match kind_of_term c with
- | Meta i -> (try assoc_pair i bl with Not_found -> c)
+ | Meta i -> (try List.assoc_snd_in_triple i bl with Not_found -> c)
| _ -> map_constr (subst_meta_instances bl) c
let pose_all_metas_as_evars env evd t =
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 6a96d5bb7..e1a4d4f36 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -41,9 +41,7 @@ module HintIdent =
struct
type t = int * rew_rule
- let compare (i,t) (i',t') =
- Pervasives.compare i i'
-(* Pervasives.compare t.rew_lemma t'.rew_lemma *)
+ let compare (i, t) (j, t') = i - j
let subst s (i,t) = (i,subst_hint s t)
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 775212eda..6277faf27 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -428,7 +428,7 @@ let subst_deps_obl obls obl =
let t' = subst_deps true obls obl.obl_deps obl.obl_type in
{ obl with obl_type = t' }
-module ProgMap = Map.Make(struct type t = identifier let compare = compare end)
+module ProgMap = Map.Make(struct type t = identifier let compare = id_ord end)
let map_replace k v m = ProgMap.add k v (ProgMap.remove k m)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 17:12:11 +0000