diff options
| -rw-r--r-- | kernel/names.ml | 34 | ||||
| -rw-r--r-- | kernel/names.mli | 2 | ||||
| -rw-r--r-- | library/globnames.ml | 19 | ||||
| -rw-r--r-- | library/globnames.mli | 1 | ||||
| -rw-r--r-- | library/libnames.ml | 2 | ||||
| -rw-r--r-- | library/nametab.ml | 8 |
6 files changed, 54 insertions, 12 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index 6b433c482..ef0e812ed 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -147,7 +147,10 @@ struct if Int.equal c 0 then compare p1 p2 else c end - let equal p1 p2 = Int.equal (compare p1 p2) 0 + let rec equal p1 p2 = p1 == p2 || match p1, p2 with + | [], [] -> true + | id1 :: p1, id2 :: p2 -> Id.equal id1 id2 && equal p1 p2 + | _ -> false let rec hash accu = function | [] -> accu @@ -210,7 +213,10 @@ struct else DirPath.compare dpl dpr - let equal x y = Int.equal (compare x y) 0 + let equal x y = x == y || + let (i1, id1, p1) = x in + let (i2, id2, p2) = y in + Int.equal i1 i2 && Id.equal id1 id2 && DirPath.equal p1 p2 let to_id (_, s, _) = s @@ -286,7 +292,12 @@ module ModPath = struct | MPbound _, MPdot _ -> -1 | MPdot _, _ -> 1 - let equal mp1 mp2 = Int.equal (compare mp1 mp2) 0 + let rec equal mp1 mp2 = mp1 == mp2 || + match mp1, mp2 with + | MPfile p1, MPfile p2 -> DirPath.equal p1 p2 + | MPbound id1, MPbound id2 -> MBId.equal id1 id2 + | MPdot (mp1, l1), MPdot (mp2, l2) -> String.equal l1 l2 && equal mp1 mp2 + | (MPfile _ | MPbound _ | MPdot _), _ -> false open Hashset.Combine @@ -373,7 +384,14 @@ module KerName = struct if not (Int.equal c 0) then c else ModPath.compare kn1.modpath kn2.modpath - let equal kn1 kn2 = Int.equal (compare kn1 kn2) 0 + let equal kn1 kn2 = + let h1 = kn1.refhash in + let h2 = kn2.refhash in + if 0 <= h1 && 0 <= h2 && not (Int.equal h1 h2) then false + else + Label.equal kn1.knlabel kn2.knlabel && + DirPath.equal kn1.dirpath kn2.dirpath && + ModPath.equal kn1.modpath kn2.modpath open Hashset.Combine @@ -553,24 +571,32 @@ let inductive_of_constructor (ind, i) = ind let index_of_constructor (ind, i) = i let eq_ind (m1, i1) (m2, i2) = Int.equal i1 i2 && MutInd.equal m1 m2 +let eq_user_ind (m1, i1) (m2, i2) = + Int.equal i1 i2 && MutInd.UserOrd.equal m1 m2 + let ind_ord (m1, i1) (m2, i2) = let c = Int.compare i1 i2 in if Int.equal c 0 then MutInd.CanOrd.compare m1 m2 else c let ind_user_ord (m1, i1) (m2, i2) = let c = Int.compare i1 i2 in if Int.equal c 0 then MutInd.UserOrd.compare m1 m2 else c + let ind_hash (m, i) = Hashset.Combine.combine (MutInd.hash m) (Int.hash i) let ind_user_hash (m, i) = Hashset.Combine.combine (MutInd.UserOrd.hash m) (Int.hash i) let eq_constructor (ind1, j1) (ind2, j2) = Int.equal j1 j2 && eq_ind ind1 ind2 +let eq_user_constructor (ind1, j1) (ind2, j2) = + Int.equal j1 j2 && eq_user_ind ind1 ind2 + let constructor_ord (ind1, j1) (ind2, j2) = let c = Int.compare j1 j2 in if Int.equal c 0 then ind_ord ind1 ind2 else c let constructor_user_ord (ind1, j1) (ind2, j2) = let c = Int.compare j1 j2 in if Int.equal c 0 then ind_user_ord ind1 ind2 else c + let constructor_hash (ind, i) = Hashset.Combine.combine (ind_hash ind) (Int.hash i) let constructor_user_hash (ind, i) = diff --git a/kernel/names.mli b/kernel/names.mli index b2a363174..db973ed3a 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -410,11 +410,13 @@ val ith_constructor_of_inductive : inductive -> int -> constructor val inductive_of_constructor : constructor -> inductive val index_of_constructor : constructor -> int val eq_ind : inductive -> inductive -> bool +val eq_user_ind : inductive -> inductive -> bool val ind_ord : inductive -> inductive -> int val ind_hash : inductive -> int val ind_user_ord : inductive -> inductive -> int val ind_user_hash : inductive -> int val eq_constructor : constructor -> constructor -> bool +val eq_user_constructor : constructor -> constructor -> bool val constructor_ord : constructor -> constructor -> int val constructor_user_ord : constructor -> constructor -> int val constructor_hash : constructor -> int diff --git a/library/globnames.ml b/library/globnames.ml index 7fce6b378..8a9e99621 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -77,6 +77,15 @@ let constr_of_global = function let constr_of_reference = constr_of_global let reference_of_constr = global_of_constr +let global_eq_gen eq_cst eq_ind eq_cons x y = + x == y || + match x, y with + | ConstRef cx, ConstRef cy -> eq_cst cx cy + | IndRef indx, IndRef indy -> eq_ind indx indy + | ConstructRef consx, ConstructRef consy -> eq_cons consx consy + | VarRef v1, VarRef v2 -> Id.equal v1 v2 + | (VarRef _ | ConstRef _ | IndRef _ | ConstructRef _), _ -> false + let global_ord_gen ord_cst ord_ind ord_cons x y = if x == y then 0 else match x, y with @@ -107,6 +116,7 @@ module RefOrdered = struct type t = global_reference let compare gr1 gr2 = global_ord_gen compare ind_ord constructor_ord gr1 gr2 + let equal gr1 gr2 = global_eq_gen equal eq_ind eq_constructor gr1 gr2 let hash gr = global_hash_gen hash ind_hash constructor_hash gr end @@ -115,6 +125,8 @@ module RefOrdered_env = struct type t = global_reference let compare gr1 gr2 = global_ord_gen compare ind_user_ord constructor_user_ord gr1 gr2 + let equal gr1 gr2 = + global_eq_gen equal eq_user_ind eq_user_constructor gr1 gr2 let hash gr = global_hash_gen hash ind_user_hash constructor_user_hash gr end @@ -140,6 +152,13 @@ type extended_global_reference = module ExtRefOrdered = struct type t = extended_global_reference + let equal x y = + x == y || + match x, y with + | TrueGlobal rx, TrueGlobal ry -> RefOrdered_env.equal rx ry + | SynDef knx, SynDef kny -> KerName.equal knx kny + | (TrueGlobal _ | SynDef _), _ -> false + let compare x y = if x == y then 0 else match x, y with diff --git a/library/globnames.mli b/library/globnames.mli index 4569d8e1f..0a7bf850c 100644 --- a/library/globnames.mli +++ b/library/globnames.mli @@ -77,6 +77,7 @@ type extended_global_reference = module ExtRefOrdered : sig type t = extended_global_reference val compare : t -> t -> int + val equal : t -> t -> bool val hash : t -> int end diff --git a/library/libnames.ml b/library/libnames.ml index cf6d4c8ad..97c352d61 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -105,7 +105,7 @@ let string_of_path sp = let sp_ord sp1 sp2 = let (p1,id1) = repr_path sp1 and (p2,id2) = repr_path sp2 in - let p_bit = compare p1 p2 in + let p_bit = DirPath.compare p1 p2 in if Int.equal p_bit 0 then Id.compare id1 id2 else p_bit module SpOrdered = diff --git a/library/nametab.ml b/library/nametab.ml index 08eb02c9d..03856736d 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -276,14 +276,8 @@ struct id, (DirPath.repr dir) end -module ExtRefEqual = -struct - type t = extended_global_reference - let equal e1 e2 = Int.equal (ExtRefOrdered.compare e1 e2) 0 -end - +module ExtRefEqual = ExtRefOrdered module KnEqual = Names.KerName - module MPEqual = Names.ModPath module ExtRefTab = Make(FullPath)(ExtRefEqual) |