diff options
Diffstat (limited to 'kernel/names.ml')
| -rw-r--r-- | kernel/names.ml | 64 |
1 files changed, 34 insertions, 30 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index 96055ca16..250b4a6b5 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -88,7 +88,7 @@ let rec dir_path_ord (p1 : dir_path) (p2 : dir_path) = | _, [] -> 1 | id1 :: p1, id2 :: p2 -> let c = id_ord id1 id2 in - if c <> 0 then c else dir_path_ord p1 p2 + if Int.equal c 0 then dir_path_ord p1 p2 else c end let make_dirpath x = x @@ -116,11 +116,11 @@ 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 + let ans = Int.compare nl nr in + if not (Int.equal ans 0) then ans else let ans = id_ord idl idr in - if ans <> 0 then ans + if not (Int.equal ans 0) then ans else dir_path_ord dpl dpr @@ -180,7 +180,7 @@ let rec mp_ord mp1 mp2 = uniq_ident_ord id1 id2 | MPdot (mp1, l1), MPdot (mp2, l2) -> let c = String.compare l1 l2 in - if c <> 0 then c + if not (Int.equal c 0) then c else mp_ord mp1 mp2 | MPfile _, _ -> -1 | MPbound _, MPfile _ -> 1 @@ -226,10 +226,10 @@ let kn_ord (kn1 : kernel_name) (kn2 : kernel_name) = let mp1, dir1, l1 = kn1 in let mp2, dir2, l2 = kn2 in let c = String.compare l1 l2 in - if c <> 0 then c + if not (Int.equal c 0) then c else let c = dir_path_ord dir1 dir2 in - if c <> 0 then c + if not (Int.equal c 0) then c else MPord.compare mp1 mp2 module KNord = struct @@ -259,7 +259,7 @@ let canonical_con con = snd con let user_con con = fst con let repr_con con = fst con -let eq_constant (_,kn1) (_,kn2) = kn1=kn2 +let eq_constant (_, kn1) (_, kn2) = Int.equal (kn_ord kn1 kn2) 0 let con_label con = label (fst con) let con_modpath con = modpath (fst con) @@ -271,8 +271,9 @@ let debug_string_of_con con = let debug_pr_con con = str (debug_string_of_con con) let con_with_label ((mp1,dp1,l1),(mp2,dp2,l2) as con) lbl = - if lbl = l1 && lbl = l2 then con - else ((mp1,dp1,lbl),(mp2,dp2,lbl)) + if Int.equal (String.compare lbl l1) 0 && Int.equal (String.compare lbl l2) 0 + then con + else ((mp1, dp1, lbl), (mp2, dp2, lbl)) (** For the environment we distinguish constants by their user part*) module User_ord = struct @@ -319,7 +320,7 @@ let user_mind mind = fst mind let repr_mind mind = fst mind let mind_label mind = label (fst mind) -let eq_mind (_, kn1) (_, kn2) = kn_ord kn1 kn2 = 0 +let eq_mind (_, kn1) (_, kn2) = Int.equal (kn_ord kn1 kn2) 0 let string_of_mind mind = string_of_kn (fst mind) let pr_mind mind = str (string_of_mind mind) @@ -331,10 +332,10 @@ let ith_mutual_inductive (kn, _) i = (kn, i) let ith_constructor_of_inductive ind i = (ind, i) let inductive_of_constructor (ind, i) = ind let index_of_constructor (ind, i) = i -let eq_ind (kn1, i1) (kn2, i2) = - i1 - i2 = 0 && eq_mind kn1 kn2 -let eq_constructor (kn1, i1) (kn2, i2) = - i1 - i2 = 0 && eq_ind kn1 kn2 + +let eq_ind (kn1, i1) (kn2, i2) = Int.equal i1 i2 && eq_mind kn1 kn2 + +let eq_constructor (kn1, i1) (kn2, i2) = Int.equal i1 i2 && eq_ind kn1 kn2 module Mindmap = Map.Make(Canonical_ord) module Mindset = Set.Make(Canonical_ord) @@ -343,13 +344,15 @@ module Mindmap_env = Map.Make(User_ord) module InductiveOrdered = struct type t = inductive let compare (spx,ix) (spy,iy) = - let c = ix - iy in if c = 0 then Canonical_ord.compare spx spy else c + let c = Int.compare ix iy in + if Int.equal c 0 then Canonical_ord.compare spx spy else c end module InductiveOrdered_env = struct type t = inductive let compare (spx,ix) (spy,iy) = - let c = ix - iy in if c = 0 then User_ord.compare spx spy else c + let c = Int.compare ix iy in + if Int.equal c 0 then User_ord.compare spx spy else c end module Indmap = Map.Make(InductiveOrdered) @@ -358,13 +361,15 @@ module Indmap_env = Map.Make(InductiveOrdered_env) module ConstructorOrdered = struct type t = constructor let compare (indx,ix) (indy,iy) = - let c = ix - iy in if c = 0 then InductiveOrdered.compare indx indy else c + let c = Int.compare ix iy in + if Int.equal c 0 then InductiveOrdered.compare indx indy else c end module ConstructorOrdered_env = struct type t = constructor let compare (indx,ix) (indy,iy) = - let c = ix - iy in if c = 0 then InductiveOrdered_env.compare indx indy else c + let c = Int.compare ix iy in + if Int.equal c 0 then InductiveOrdered_env.compare indx indy else c end module Constrmap = Map.Make(ConstructorOrdered) @@ -418,7 +423,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 = 0 && s1 == s2 && dir1 == dir2) + (Int.equal n1 n2 && s1 == s2 && dir1 == dir2) let hash = Hashtbl.hash end) @@ -471,7 +476,7 @@ module Hind = Hashcons.Make( type t = inductive type u = mutual_inductive -> mutual_inductive let hashcons hmind (mind, i) = (hmind mind, i) - let equal (mind1,i1) (mind2,i2) = mind1 == mind2 && i1 = i2 + let equal (mind1,i1) (mind2,i2) = mind1 == mind2 && Int.equal i1 i2 let hash = Hashtbl.hash end) @@ -480,7 +485,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 = 0) + let equal (ind1, j1) (ind2, j2) = ind1 == ind2 && Int.equal j1 j2 let hash = Hashtbl.hash end) @@ -522,15 +527,14 @@ let eq_id_key ik1 ik2 = 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 + let ans = Int.equal (kn_ord u1 u2) 0 in + if ans then Int.equal (kn_ord kn1 kn2) 0 else ans | VarKey id1, VarKey id2 -> - id_ord id1 id2 = 0 - | RelKey k1, RelKey k2 -> - k1 - k2 = 0 + Int.equal (id_ord id1 id2) 0 + | RelKey k1, RelKey k2 -> Int.equal k1 k2 | _ -> false -let eq_con_chk (kn1,_) (kn2,_) = kn1=kn2 -let eq_mind_chk (kn1,_) (kn2,_) = kn1=kn2 -let eq_ind_chk (kn1,i1) (kn2,i2) = i1=i2&&eq_mind_chk kn1 kn2 +let eq_con_chk (kn1,_) (kn2,_) = Int.equal (kn_ord kn1 kn2) 0 +let eq_mind_chk (kn1,_) (kn2,_) = Int.equal (kn_ord kn1 kn2) 0 +let eq_ind_chk (kn1,i1) (kn2,i2) = Int.equal i1 i2 && eq_mind_chk kn1 kn2 |