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

10 files changed, 56 insertions, 60 deletions

diff --git a/lib/bigint.ml b/lib/bigint.ml
index 9012d9322..be207f667 100644
--- a/lib/bigint.ml
+++ b/lib/bigint.ml
@@ -43,8 +43,8 @@ let size =
 
 let format_size =
   (* How to parametrize a printf format *)
-  if size = 4 then Printf.sprintf "%04d"
-  else if size = 9 then Printf.sprintf "%09d"
+  if Int.equal size 4 then Printf.sprintf "%04d"
+  else if Int.equal size 9 then Printf.sprintf "%09d"
   else fun n ->
     let rec aux j l n =
       if j=size then l else aux (j+1) (string_of_int (n mod 10) :: l) (n/10)
@@ -73,7 +73,7 @@ let neg_one = [|-1|]
 
 let canonical n =
   let ok x = (0 <= x && x < base) in
-  let rec ok_tail k = (k = 0) || (ok n.(k) && ok_tail (k-1)) in
+  let rec ok_tail k = (Int.equal k 0) || (ok n.(k) && ok_tail (k-1)) in
   let ok_init x = (-base <= x && x < base && x <> -1 && x <> 0)
   in
   (n = [||]) || (n = [|-1|]) ||
@@ -83,7 +83,7 @@ let canonical n =
 
 let normalize_pos n =
   let k = ref 0 in
-  while !k < Array.length n & n.(!k) = 0 do incr k done;
+  while !k < Array.length n && Int.equal n.(!k) 0 do incr k done;
   Array.sub n !k (Array.length n - !k)
 
 (* [normalize_neg] : avoid (-1) as first bloc.
@@ -94,16 +94,16 @@ let normalize_neg n =
   let k = ref 1 in
   while !k < Array.length n & n.(!k) = base - 1 do incr k done;
   let n' = Array.sub n !k (Array.length n - !k) in
-  if Array.length n' = 0 then [|-1|] else (n'.(0) <- n'.(0) - base; n')
+  if Int.equal (Array.length n') 0 then [|-1|] else (n'.(0) <- n'.(0) - base; n')
 
 (* [normalize] : avoid 0 and (-1) as first bloc.
    input: an array with first bloc in [-base;base[ and others in [0;base[
    output: a canonical array *)
 
 let normalize n =
-  if Array.length n = 0 then n
-  else if n.(0) = -1 then normalize_neg n
-  else if n.(0) = 0 then normalize_pos n
+  if Int.equal (Array.length n) 0 then n
+  else if Int.equal n.(0) (-1) then normalize_neg n
+  else if Int.equal n.(0) 0 then normalize_pos n
   else n
 
 (* Opposite (expects and returns canonical arrays) *)
@@ -112,8 +112,8 @@ let neg m =
   if m = zero then zero else
   let n = Array.copy m in
   let i = ref (Array.length m - 1) in
-  while !i > 0 & n.(!i) = 0 do decr i done;
-  if !i = 0 then begin
+  while !i > 0 && Int.equal n.(!i) 0 do decr i done;
+  if Int.equal !i 0 then begin
     n.(0) <- - n.(0);
     (* n.(0) cannot be 0 since m is canonical *)
     if n.(0) = -1 then normalize_neg n
@@ -261,7 +261,7 @@ let euclid m d =
     let q = Array.create (ql+1) 0 in
     let i = ref 0 in
     while not (less_than_shift_pos !i m d) do
-      if m.(!i)=0 then incr i else
+      if Int.equal m.(!i) 0 then incr i else
       if can_divide !i m d 0 then begin
         let v =
           if Array.length d > 1 && d.(0) <> m.(!i) then
@@ -297,14 +297,14 @@ let of_string s =
   let e = if h<>"" then 1 else 0 in
   let l = (len - !d) / size in
   let a = Array.create (l + e) 0 in
-  if e=1 then a.(0) <- int_of_string h;
-  for i=1 to l do
+  if Int.equal e 1 then a.(0) <- int_of_string h;
+  for i = 1 to l do
     a.(i+e-1) <- int_of_string (String.sub s ((i-1)*size + !d + r) size)
   done;
   if isneg then neg a else a
 
 let to_string_pos sgn n =
-   if Array.length n = 0 then "0" else
+   if Int.equal (Array.length n) 0 then "0" else
      sgn ^
      String.concat ""
       (string_of_int n.(0) :: List.map format_size (List.tl (Array.to_list n)))
@@ -342,7 +342,7 @@ let mkarray n =
   t
 
 let ints_of_int n =
-  if n = 0 then [| |]
+  if Int.equal n 0 then [| |]
   else if small n then [| n |]
   else mkarray n
 
@@ -352,7 +352,7 @@ let of_int n =
 let of_ints n =
   let n = normalize n in (* TODO: using normalize here seems redundant now *)
   if n = zero then Obj.repr 0 else
-  if Array.length n = 1 then Obj.repr n.(0) else
+  if Int.equal (Array.length n) 1 then Obj.repr n.(0) else
   Obj.repr n
 
 let coerce_to_int = (Obj.magic : Obj.t -> int)
@@ -366,7 +366,7 @@ let int_of_ints =
   let maxi = mkarray max_int and mini = mkarray min_int in
   fun t ->
     let l = Array.length t in
-    if (l > 3) || (l = 3 && (less_than maxi t || less_than t mini))
+    if (l > 3) || (Int.equal l 3 && (less_than maxi t || less_than t mini))
     then failwith "Bigint.to_int: too large";
     let sum = ref 0 in
     let pow = ref 1 in
diff --git a/lib/cArray.ml b/lib/cArray.ml
index bdc084f44..4615ad038 100644
--- a/lib/cArray.ml
+++ b/lib/cArray.ml
@@ -280,8 +280,9 @@ let smartmap f ar =
           Array.init ar_size copy
 
 let map2 f v1 v2 =
-  if Array.length v1 <> Array.length v2 then invalid_arg "Array.map2";
-  if Array.length v1 == 0 then
+  if not (Int.equal (Array.length v1) (Array.length v2)) then
+    invalid_arg "Array.map2";
+  if Int.equal (Array.length v1) 0 then
     [| |]
   else begin
     let res = Array.create (Array.length v1) (f v1.(0) v2.(0)) in
@@ -292,8 +293,9 @@ let map2 f v1 v2 =
   end
 
 let map2_i f v1 v2 =
-  if Array.length v1 <> Array.length v2 then invalid_arg "Array.map2";
-  if Array.length v1 == 0 then
+  if not (Int.equal (Array.length v1) (Array.length v2)) then
+    invalid_arg "Array.map2";
+  if Int.equal (Array.length v1) 0 then
     [| |]
   else begin
     let res = Array.create (Array.length v1) (f 0 v1.(0) v2.(0)) in
@@ -306,7 +308,7 @@ let map2_i f v1 v2 =
 let map3 f v1 v2 v3 =
   if Array.length v1 <> Array.length v2 ||
      Array.length v1 <> Array.length v3 then invalid_arg "Array.map3";
-  if Array.length v1 == 0 then
+  if Int.equal (Array.length v1) 0 then
     [| |]
   else begin
     let res = Array.create (Array.length v1) (f v1.(0) v2.(0) v3.(0)) in
@@ -318,7 +320,7 @@ let map3 f v1 v2 v3 =
 
 let map_left f a = (* Ocaml does not guarantee Array.map is LR *)
   let l = Array.length a in (* (even if so), then we rewrite it *)
-  if l = 0 then [||] else begin
+  if Int.equal l 0 then [||] else begin
     let r = Array.create l (f a.(0)) in
     for i = 1 to l - 1 do
       r.(i) <- f a.(i)
@@ -328,7 +330,7 @@ let map_left f a = (* Ocaml does not guarantee Array.map is LR *)
 
 let iter2 f v1 v2 =
   let n = Array.length v1 in
-  if Array.length v2 <> n then invalid_arg "Array.iter2"
+  if not (Int.equal (Array.length v2) n) then invalid_arg "Array.iter2"
   else for i = 0 to n - 1 do f v1.(i) v2.(i) done
 
 let pure_functional = false
diff --git a/lib/cList.ml b/lib/cList.ml
index 62d1ec3c1..ee6b073ea 100644
--- a/lib/cList.ml
+++ b/lib/cList.ml
@@ -377,7 +377,7 @@ let interval n m =
 
 let addn n v =
   let rec aux n l =
-    if n = 0 then l
+    if Int.equal n 0 then l
     else aux (pred n) (v :: l)
   in
   if n < 0 then invalid_arg "List.addn"
@@ -525,7 +525,7 @@ let rec remove_assoc_in_triple x = function
 
 let rec assoc_snd_in_triple x = function
     [] -> raise Not_found
-  | (a,b,_)::l -> if Pervasives.compare a x = 0 then b else assoc_snd_in_triple x l
+  | (a,b,_)::l -> if Int.equal (Pervasives.compare a x) 0 then b else assoc_snd_in_triple x l
 
 let add_set x l = if List.mem x l then l else x :: l
 
@@ -587,7 +587,7 @@ let rec merge_uniq cmp l1 l2 =
   | l1, [] -> l1
   | h1 :: t1, h2 :: t2 ->
       let c = cmp h1 h2 in
-      if c = 0
+      if Int.equal c 0
       then h1 :: merge_uniq cmp t1 t2
       else if c <= 0
       then h1 :: merge_uniq cmp t1 l2
diff --git a/lib/deque.ml b/lib/deque.ml
index 58049b094..335a1a267 100644
--- a/lib/deque.ml
+++ b/lib/deque.ml
@@ -17,9 +17,9 @@ type 'a t = {
 
 let rec split i accu l = match l with
 | [] ->
-  if i = 0 then (accu, []) else invalid_arg "split"
+  if Int.equal i 0 then (accu, []) else invalid_arg "split"
 | t :: q ->
-  if i = 0 then (accu, l)
+  if Int.equal i 0 then (accu, l)
   else split (pred i) (t :: accu) q
 
 let balance q =
@@ -88,7 +88,7 @@ let rev q = {
 
 let length q = q.lenf + q.lenr
 
-let is_empty q = length q = 0
+let is_empty q = Int.equal (length q) 0
 
 let filter f q =
   let fold (accu, len) x = if f x then (x :: accu, succ len) else (accu, len) in
diff --git a/lib/envars.ml b/lib/envars.ml
index b4c72b130..846391d83 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -51,7 +51,7 @@ let expand_path_macros ~warn s =
 	  let v = safe_getenv warn (String.sub s (i+1) (n-i-1)) in
 	  let s = (String.sub s 0 i)^v^(String.sub s n (l-n)) in
 	  expand_macros s (i + String.length v)
-	| '~' when i = 0 ->
+	| '~' when Int.equal i 0 ->
 	  let n = expand_atom s (i+1) in
 	  let v =
 	    if n=i+1 then home ~warn
diff --git a/lib/fmap.ml b/lib/fmap.ml
index 8ca56fe7a..21bd4b898 100644
--- a/lib/fmap.ml
+++ b/lib/fmap.ml
@@ -52,7 +52,7 @@ module Make = functor (X:Map.OrderedType) -> struct
           Node(Empty, x, data, Empty, 1)
       | Node(l, v, d, r, h) ->
           let c = X.compare x v in
-          if c = 0 then
+          if Int.equal c 0 then
             Node(l, x, data, r, h)
           else if c < 0 then
             bal (add x data l) v d r
@@ -64,7 +64,7 @@ module Make = functor (X:Map.OrderedType) -> struct
           raise Not_found
       | Node(l, v, d, r, _) ->
           let c = X.compare x v in
-          if c = 0 then d
+          if Int.equal c 0 then d
           else find x (if c < 0 then l else r)
 
     let rec mem x = function
@@ -72,7 +72,7 @@ module Make = functor (X:Map.OrderedType) -> struct
           false
       | Node(l, v, d, r, _) ->
           let c = X.compare x v in
-          c = 0 || mem x (if c < 0 then l else r)
+          Int.equal c 0 || mem x (if c < 0 then l else r)
 
     let rec min_binding = function
         Empty -> raise Not_found
@@ -97,7 +97,7 @@ module Make = functor (X:Map.OrderedType) -> struct
           Empty
       | Node(l, v, d, r, h) ->
           let c = X.compare x v in
-          if c = 0 then
+          if Int.equal c 0 then
             merge l r
           else if c < 0 then
             bal (remove x l) v d r
diff --git a/lib/fset.ml b/lib/fset.ml
index 567feaa75..c93ce535d 100644
--- a/lib/fset.ml
+++ b/lib/fset.ml
@@ -93,7 +93,7 @@ struct
           (Empty, None, Empty)
       | Node(l, v, r, _) ->
           let c = X.compare x v in
-          if c = 0 then (l, Some v, r)
+          if Int.equal c 0 then (l, Some v, r)
           else if c < 0 then
             let (ll, vl, rl) = split x l in (ll, vl, join rl v r)
           else
@@ -109,13 +109,13 @@ struct
         Empty -> false
       | Node(l, v, r, _) ->
           let c = X.compare x v in
-          c = 0 || mem x (if c < 0 then l else r)
+          Int.equal c 0 || mem x (if c < 0 then l else r)
 
     let rec add x = function
         Empty -> Node(Empty, x, Empty, 1)
       | Node(l, v, r, _) as t ->
           let c = X.compare x v in
-          if c = 0 then t else
+          if Int.equal c 0 then t else
           if c < 0 then bal (add x l) v r else bal l v (add x r)
 
     let singleton x = Node(Empty, x, Empty, 1)
@@ -124,7 +124,7 @@ struct
         Empty -> Empty
       | Node(l, v, r, _) ->
           let c = X.compare x v in
-          if c = 0 then merge l r else
+          if Int.equal c 0 then merge l r else
           if c < 0 then bal (remove x l) v r else bal l v (remove x r)
 
     let rec union s1 s2 =
@@ -133,12 +133,12 @@ struct
       | (t1, Empty) -> t1
       | (Node(l1, v1, r1, h1), Node(l2, v2, r2, h2)) ->
           if h1 >= h2 then
-            if h2 = 1 then add v2 s1 else begin
+            if Int.equal h2 1 then add v2 s1 else begin
               let (l2, _, r2) = split v1 s2 in
               join (union l1 l2) v1 (union r1 r2)
             end
           else
-            if h1 = 1 then add v1 s2 else begin
+            if Int.equal h1 1 then add v1 s2 else begin
               let (l1, _, r1) = split v2 s1 in
               join (union l1 l2) v2 (union r1 r2)
             end
@@ -184,7 +184,7 @@ struct
       compare_aux [s1] [s2]
 
     let equal s1 s2 =
-      compare s1 s2 = 0
+      Int.equal (compare s1 s2) 0
 
     let rec subset s1 s2 =
       match (s1, s2) with
@@ -194,7 +194,7 @@ struct
           false
       | Node (l1, v1, r1, _), (Node (l2, v2, r2, _) as t2) ->
           let c = X.compare v1 v2 in
-          if c = 0 then
+          if Int.equal c 0 then
             subset l1 l2 && subset r1 r2
           else if c < 0 then
             subset (Node (l1, v1, Empty, 0)) l2 && subset r1 t2
diff --git a/lib/gmap.ml b/lib/gmap.ml
index 08c99daff..65971b237 100644
--- a/lib/gmap.ml
+++ b/lib/gmap.ml
@@ -60,7 +60,7 @@
           Node(Empty, x, data, Empty, 1)
       | Node(l, v, d, r, h) ->
           let c = Pervasives.compare x v in
-          if c = 0 then
+          if Int.equal c 0 then
             Node(l, x, data, r, h)
           else if c < 0 then
             bal (add x data l) v d r
@@ -72,7 +72,7 @@
           raise Not_found
       | Node(l, v, d, r, _) ->
           let c = Pervasives.compare x v in
-          if c = 0 then d
+          if Int.equal c 0 then d
           else find x (if c < 0 then l else r)
 
     let rec mem x = function
@@ -80,7 +80,7 @@
           false
       | Node(l, v, d, r, _) ->
           let c = Pervasives.compare x v in
-          c = 0 || mem x (if c < 0 then l else r)
+          Int.equal c 0 || mem x (if c < 0 then l else r)
 
     let rec min_binding = function
         Empty -> raise Not_found
@@ -105,7 +105,7 @@
           Empty
       | Node(l, v, d, r, h) ->
           let c = Pervasives.compare x v in
-          if c = 0 then
+          if Int.equal c 0 then
             merge l r
           else if c < 0 then
             bal (remove x l) v d r
diff --git a/lib/pp.ml b/lib/pp.ml
index 5a38b08c3..71c72baa9 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -236,7 +236,7 @@ let rec pr_com ft s =
   Format.pp_print_as ft (utf8_length s1) s1;
   match os with
       Some s2 ->
-        if String.length s2 = 0 then (com_eol := true)
+        if Int.equal (String.length s2) 0 then (com_eol := true)
         else
           (Format.pp_force_newline ft (); pr_com ft s2)
     | None -> ()
@@ -441,14 +441,14 @@ let pr_vertical_list pr = function
 
 let prvecti_with_sep sep elem v =
   let rec pr i =
-    if i = 0 then
+    if Int.equal i 0 then
       elem 0 v.(0)
     else
       let r = pr (i-1) and s = sep () and e = elem i v.(i) in
       r ++ s ++ e
   in
   let n = Array.length v in
-  if n = 0 then mt () else pr (n - 1)
+  if Int.equal n 0 then mt () else pr (n - 1)
 
 (* [prvecti pr [|a0 ; ... ; an|]] outputs [pr 0 a0 ++ ... ++ pr n an] *)
 
diff --git a/lib/util.ml b/lib/util.ml
index 6a0ba470a..84249e6ae 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -65,7 +65,7 @@ let strip s =
 let string_map f s =
   let l = String.length s in
   let r = String.create l in
-  for i= 0 to (l - 1) do r.[i] <- f (s.[i]) done;
+  for i = 0 to (l - 1) do r.[i] <- f (s.[i]) done;
   r
 
 let drop_simple_quotes s =
@@ -118,7 +118,7 @@ let split_string_at c s =
     with
       | Not_found -> [String.sub s n (len-n)]
   in
-  if len = 0 then [] else split 0
+  if Int.equal len 0 then [] else split 0
 
 let parse_loadpath s =
   let l = split_string_at '/' s in
@@ -207,14 +207,8 @@ let delayed_force f = f ()
 
 type ('a,'b) union = Inl of 'a | Inr of 'b
 
-module IntOrd =
-struct
-  type t  = int
-  external compare : int -> int -> int = "caml_int_compare"
-end
-
-module Intset = Set.Make(IntOrd)
-module Intmap = Map.Make(IntOrd)
+module Intset = Set.Make(Int)
+module Intmap = Map.Make(Int)
 
 (*s interruption *)