Monomorphized a lot of equalities over OCaml integers, thanks to

the new Int module. Only the most obvious were removed, so there
are a lot more in the wild.

This may sound heavyweight, but it has two advantages:

1. Monomorphization is explicit, hence we do not miss particular
optimizations of equality when doing it carelessly with the generic
equality.

2. When we have removed all the generic equalities on integers, we
will be able to write something like "let (=) = ()" to retrieve all
its other uses (mostly faulty) spread throughout the code, statically.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15957 85f007b7-540e-0410-9357-904b9bb8a0f7

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