Removing a bunch of generic equalities.

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

1 files changed, 60 insertions, 51 deletions

diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 4ad681c053..1e6a1fffcc 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -29,7 +29,7 @@ let anonymous = Id anonymous_name
 
 let id_of_name = function
   | Anonymous -> anonymous_name
-  | Name id when id = dummy_name -> anonymous_name
+  | Name id when Id.equal id dummy_name -> anonymous_name
   | Name id -> id
 
 let id_of_mlid = function
@@ -85,7 +85,7 @@ let instantiation (nb,t) = type_subst_vect (Array.init nb new_meta) t
 
 let rec type_occurs alpha t =
   match t with
-  | Tmeta {id=beta; contents=None} -> alpha = beta
+  | Tmeta {id=beta; contents=None} -> Int.equal alpha beta
   | Tmeta {contents=Some u} -> type_occurs alpha u
   | Tarr (t1, t2) -> type_occurs alpha t1 || type_occurs alpha t2
   | Tglob (r,l) -> List.exists (type_occurs alpha) l
@@ -94,7 +94,7 @@ let rec type_occurs alpha t =
 (*s Most General Unificator *)
 
 let rec mgu = function
-  | Tmeta m, Tmeta m' when m.id = m'.id -> ()
+  | Tmeta m, Tmeta m' when Int.equal m.id m'.id -> ()
   | Tmeta m, t | t, Tmeta m ->
     (match m.contents with
       | Some u -> mgu (u, t)
@@ -102,21 +102,24 @@ let rec mgu = function
       | None -> m.contents <- Some t)
   | Tarr(a, b), Tarr(a', b') ->
       mgu (a, a'); mgu (b, b')
-  | Tglob (r,l), Tglob (r',l') when r = r' ->
+  | Tglob (r,l), Tglob (r',l') when Globnames.eq_gr r r' ->
        List.iter mgu (List.combine l l')
-  | (Tdummy _, _ | _, Tdummy _) when lang() = Haskell -> ()
+  | (Tdummy _, _ | _, Tdummy _) when lang() == Haskell -> ()
   | Tdummy _, Tdummy _ -> ()
-  | t, u when t = u -> () (* for Tvar, Tvar', Tunknown, Taxiom *)
+  | Tvar i, Tvar j when Int.equal i j -> ()
+  | Tvar' i, Tvar' j when  Int.equal i j -> ()
+  | Tunknown, Tunknown -> ()
+  | Taxiom, Taxiom -> ()
   | _ -> raise Impossible
 
 let needs_magic p = try mgu p; false with Impossible -> true
 
-let put_magic_if b a = if b && lang () <> Scheme then MLmagic a else a
+let put_magic_if b a = if b && lang () != Scheme then MLmagic a else a
 
-let put_magic p a = if needs_magic p && lang () <> Scheme then MLmagic a else a
+let put_magic p a = if needs_magic p && lang () != Scheme then MLmagic a else a
 
 let generalizable a =
-  lang () <> Ocaml ||
+  lang () != Ocaml ||
     match a with
       | MLapp _ -> false
       | _ -> true (* TODO, this is just an approximation for the moment *)
@@ -147,7 +150,7 @@ module Mlenv = struct
   (* [find_free] finds the free meta in a type. *)
 
   let rec find_free set = function
-    | Tmeta m when m.contents = None -> Metaset.add m set
+    | Tmeta m when Option.is_empty m.contents -> Metaset.add m set
     | Tmeta {contents = Some t} -> find_free set t
     | Tarr (a,b) -> find_free (find_free set a) b
     | Tglob (_,l) -> List.fold_left find_free set l
@@ -302,7 +305,7 @@ let rec sign_kind = function
 	| NonLogicalSig -> NonLogicalSig
 	| UnsafeLogicalSig -> UnsafeLogicalSig
 	| SafeLogicalSig | EmptySig ->
-	    if k = Kother then UnsafeLogicalSig else SafeLogicalSig
+	    if k == Kother then UnsafeLogicalSig else SafeLogicalSig
 
 (* Removing the final [Keep] in a signature *)
 
@@ -310,17 +313,17 @@ let rec sign_no_final_keeps = function
   | [] -> []
   | k :: s ->
       let s' = k :: sign_no_final_keeps s in
-      if s' = [Keep] then [] else s'
+      match s' with [Keep] -> [] | _ -> s'
 
 (*s Removing [Tdummy] from the top level of a ML type. *)
 
 let type_expunge_from_sign env s t =
   let rec expunge s t =
-    if s = [] then t else match t with
+    if List.is_empty s then t else match t with
       | Tmeta {contents = Some t} -> expunge s t
       | Tarr (a,b) ->
 	  let t = expunge (List.tl s) b in
-	  if List.hd s = Keep then Tarr (a, t) else t
+	  if List.hd s == Keep then Tarr (a, t) else t
       | Tglob (r,l) ->
 	  (match env r with
 	     | Some mlt -> expunge s (type_subst_list l mlt)
@@ -328,7 +331,7 @@ let type_expunge_from_sign env s t =
       | _ -> assert false
   in
   let t = expunge (sign_no_final_keeps s) t in
-  if lang () <> Haskell && sign_kind s = UnsafeLogicalSig then
+  if lang () != Haskell && sign_kind s == UnsafeLogicalSig then
     Tarr (Tdummy Kother, t)
   else t
 
@@ -337,7 +340,7 @@ let type_expunge env t =
 
 (*S Generic functions over ML ast terms. *)
 
-let mlapp f a = if a = [] then f else MLapp (f,a)
+let mlapp f a = if List.is_empty a then f else MLapp (f,a)
 
 (*s [ast_iter_rel f t] applies [f] on every [MLrel] in t. It takes care
    of the number of bingings crossed before reaching the [MLrel]. *)
@@ -412,7 +415,7 @@ let ast_iter f = function
 
 let ast_occurs k t =
   try
-    ast_iter_rel (fun i -> if i = k then raise Found) t; false
+    ast_iter_rel (fun i -> if Int.equal i k then raise Found) t; false
   with Found -> true
 
 (*s [occurs_itvl k k' t] returns [true] if there is a [(Rel i)]
@@ -428,7 +431,7 @@ let ast_occurs_itvl k k' t =
 
 let nb_occur_match =
   let rec nb k = function
-    | MLrel i -> if i = k then 1 else 0
+    | MLrel i -> if Int.equal i k then 1 else 0
     | MLcase(_,a,v) ->
         (nb k a) +
 	Array.fold_left
@@ -450,7 +453,7 @@ let ast_lift k t =
   let rec liftrec n = function
     | MLrel i as a -> if i-n < 1 then a else MLrel (i+k)
     | a -> ast_map_lift liftrec n a
-  in if k = 0 then t else liftrec 0 t
+  in if Int.equal k 0 then t else liftrec 0 t
 
 let ast_pop t = ast_lift (-1) t
 
@@ -474,7 +477,7 @@ let ast_subst e =
   let rec subst n = function
     | MLrel i as a ->
 	let i' = i-n in
-	if i'=1 then ast_lift n e
+	if Int.equal i' 1 then ast_lift n e
 	else if i'<1 then a
 	else MLrel (i-1)
     | a -> ast_map_lift subst n a
@@ -512,14 +515,15 @@ let has_deep_pattern br =
   Array.exists (function (_,pat,_) -> deep pat) br
 
 let is_regular_match br =
-  if Array.length br = 0 then false (* empty match becomes MLexn *)
+  if Array.is_empty br then false (* empty match becomes MLexn *)
   else
     try
       let get_r (ids,pat,c) =
 	match pat with
 	  | Pusual r -> r
 	  | Pcons (r,l) ->
-	    if not (List.for_all_i (fun i -> (=) (Prel i)) 1 (List.rev l))
+            let is_rel i = function Prel j -> Int.equal i j | _ -> false in
+	    if not (List.for_all_i is_rel 1 (List.rev l))
 	    then raise Impossible;
 	    r
 	  | _ -> raise Impossible
@@ -528,7 +532,11 @@ let is_regular_match br =
 	| ConstructRef (ind,_) -> ind
 	| _ -> raise Impossible
       in
-      Array.for_all_i (fun i tr -> get_r tr = ConstructRef (ind,i+1)) 0 br
+      let is_ref i tr = match get_r tr with
+      | ConstructRef (ind', j) -> eq_ind ind ind' && Int.equal j (i + 1)
+      | _ -> false
+      in
+      Array.for_all_i is_ref 0 br
     with Impossible -> false
 
 (*S Operations concerning lambdas. *)
@@ -546,7 +554,7 @@ let collect_lams =
 
 let collect_n_lams =
   let rec collect acc n t =
-    if n = 0 then acc,t
+    if Int.equal n 0 then acc,t
     else match t with
       | MLlam(id,t) -> collect (id::acc) (n-1) t
       | _ -> assert false
@@ -555,7 +563,7 @@ let collect_n_lams =
 (*s [remove_n_lams] just removes some [MLlam]. *)
 
 let rec remove_n_lams n t =
-  if n = 0 then t
+  if Int.equal n 0 then t
   else match t with
       | MLlam(_,t) -> remove_n_lams (n-1) t
       | _ -> assert false
@@ -593,7 +601,7 @@ let rec anonym_or_dummy_lams a = function
 (*s The following function creates [MLrel n;...;MLrel 1] *)
 
 let rec eta_args n =
-  if n = 0 then [] else (MLrel n)::(eta_args (pred n))
+  if Int.equal n 0 then [] else (MLrel n)::(eta_args (pred n))
 
 (*s Same, but filtered by a signature. *)
 
@@ -605,20 +613,21 @@ let rec eta_args_sign n = function
 (*s This one tests [MLrel (n+k); ... ;MLrel (1+k)] *)
 
 let rec test_eta_args_lift k n = function
-  | [] -> n=0
-  | a :: q -> (a = (MLrel (k+n))) && (test_eta_args_lift k (pred n) q)
+  | [] -> Int.equal n 0
+  | MLrel m :: q -> Int.equal (k+n) m && (test_eta_args_lift k (pred n) q)
+  | _ -> false
 
 (*s Computes an eta-reduction. *)
 
 let eta_red e =
   let ids,t = collect_lams e in
   let n = List.length ids in
-  if n = 0 then e
+  if Int.equal n 0 then e
   else match t with
     | MLapp (f,a) ->
 	let m = List.length a in
 	let ids,body,args =
-	  if m = n then
+	  if Int.equal m n then
 	    [], f, a
 	  else if m < n then
 	    List.skipn m ids, f, a
@@ -699,7 +708,7 @@ let branch_as_fun typ (l,p,c) =
 	if i'<1 then c
 	else if i'>nargs then MLrel (i-nargs+1)
 	else raise Impossible
-    | MLcons _ as cons' when cons' = ast_lift n cons -> MLrel (n+1)
+    | MLcons _ as cons' when Pervasives.(=) cons' (ast_lift n cons) -> MLrel (n+1) (*FIXME*)
     | a -> ast_map_lift genrec n a
   in genrec 0 c
 
@@ -767,7 +776,7 @@ let factor_branches o typ br =
     let br_factor, br_set = census_max MLdummy in
     census_clean ();
     let n = Int.Set.cardinal br_set in
-    if n = 0 then None
+    if Int.equal n 0 then None
     else if Array.length br >= 2 && n < 2 then None
     else Some (br_factor, br_set)
   end
@@ -778,7 +787,7 @@ let rec merge_ids ids ids' = match ids,ids' with
   | [],l -> l
   | l,[] -> l
   | i::ids, i'::ids' ->
-      (if i = Dummy then i' else i) :: (merge_ids ids ids')
+      (if i == Dummy then i' else i) :: (merge_ids ids ids')
 
 let is_exn = function MLexn _ -> true | _ -> false
 
@@ -788,7 +797,7 @@ let permut_case_fun br acc =
 		let ids, c = collect_lams t in
 		let n = List.length ids in
 		if (n < !nb) && (not (is_exn c)) then nb := n) br;
-  if !nb = max_int || !nb = 0 then ([],br)
+  if Int.equal !nb  max_int || Int.equal !nb 0 then ([],br)
   else begin
     let br = Array.copy br in
     let ids = ref [] in
@@ -821,16 +830,16 @@ let rec iota_red i lift br ((typ,r,a) as cons) =
   if i >= Array.length br then raise Impossible;
   let (ids,p,c) = br.(i) in
   match p with
-    | Pusual r' | Pcons (r',_) when r'<>r -> iota_red (i+1) lift br cons
+    | Pusual r' | Pcons (r',_) when not (Globnames.eq_gr r' r) -> iota_red (i+1) lift br cons
     | Pusual r' ->
       let c = named_lams (List.rev ids) c in
       let c = ast_lift lift c
       in MLapp (c,a)
-    | Prel 1 when List.length ids = 1 ->
+    | Prel 1 when Int.equal (List.length ids) 1 ->
       let c = MLlam (List.hd ids, c) in
       let c = ast_lift lift c
       in MLapp(c,[MLcons(typ,r,a)])
-    | Pwild when ids = [] -> ast_lift lift c
+    | Pwild when List.is_empty ids -> ast_lift lift c
     | _ -> raise Impossible (* TODO: handle some more cases *)
 
 (* [iota_gen] is an extension of [iota_red] where we allow to
@@ -881,7 +890,7 @@ let rec simpl o = function
       if
 	(is_atomic c) || (is_atomic e) ||
 	(let n = nb_occur_match e in
-	 (n = 0 || (n=1 && expand_linear_let o id e)))
+	 (Int.equal n 0 || (Int.equal n 1 && expand_linear_let o id e)))
       then
 	simpl o (ast_subst c e)
       else
@@ -934,14 +943,14 @@ and simpl_case o typ br e =
     (* Swap the case and the lam if possible *)
     let ids,br = if o.opt_case_fun then permut_case_fun br [] else [],br in
     let n = List.length ids in
-    if n <> 0 then
+    if not (Int.equal n 0) then
       simpl o (named_lams ids (MLcase (typ, ast_lift n e, br)))
     else
       (* Can we merge several branches as the same constant or function ? *)
-      if lang() = Scheme || is_custom_match br
+      if lang() == Scheme || is_custom_match br
       then MLcase (typ, e, br)
       else match factor_branches o typ br with
-	| Some (f,ints) when Int.Set.cardinal ints = Array.length br ->
+	| Some (f,ints) when Int.equal (Int.Set.cardinal ints) (Array.length br) ->
 	  (* If all branches have been factorized, we remove the match *)
 	  simpl o (MLletin (Tmp anonymous_name, e, f))
 	| Some (f,ints) ->
@@ -976,9 +985,9 @@ let rec select_via_bl l args = match l,args with
 
 let kill_some_lams bl (ids,c) =
   let n = List.length bl in
-  let n' = List.fold_left (fun n b -> if b=Keep then (n+1) else n) 0 bl in
-  if n = n' then ids,c
-  else if n' = 0 then [],ast_lift (-n) c
+  let n' = List.fold_left (fun n b -> if b == Keep then (n+1) else n) 0 bl in
+  if Int.equal n n' then ids,c
+  else if Int.equal n' 0 then [],ast_lift (-n) c
   else begin
     let v = Array.make n None in
     let rec parse_ids i j = function
@@ -1041,10 +1050,10 @@ let case_expunge s e =
   if all lambdas are logical dummy and the target language is strict. *)
 
 let term_expunge s (ids,c) =
-  if s = [] then c
+  if List.is_empty s then c
   else
     let ids,c = kill_some_lams (List.rev s) (ids,c) in
-    if ids = [] && lang () <> Haskell && List.mem (Kill Kother) s then
+    if List.is_empty ids && lang () != Haskell && List.mem (Kill Kother) s then
       MLlam (Dummy, ast_lift 1 c)
     else named_lams ids c
 
@@ -1056,7 +1065,7 @@ let kill_dummy_args ids r t =
   let m = List.length ids in
   let bl = List.rev_map sign_of_id ids in
   let rec found n = function
-    | MLrel r' when r' = r + n -> true
+    | MLrel r' when Int.equal r' (r + n) -> true
     | MLmagic e -> found n e
     | _ -> false
   in
@@ -1133,7 +1142,7 @@ let normalize a =
   let o = optims () in
   let rec norm a =
     let a' = if o.opt_kill_dum then kill_dummy (simpl o a) else simpl o a in
-    if a = a' then a else norm a'
+    if Pervasives.(=) a a' then a else norm a' (** FIXME *)
   in norm a
 
 (*S Special treatment of fixpoint for pretty-printing purpose. *)
@@ -1156,7 +1165,7 @@ let optimize_fix a =
   else
     let ids,a' = collect_lams a in
     let n = List.length ids in
-    if n = 0 then a
+    if Int.equal n 0 then a
     else match a' with
       | MLfix(_,[|f|],[|c|]) ->
 	  let new_f = MLapp (MLrel (n+1),eta_args n) in
@@ -1224,7 +1233,7 @@ let rec non_stricts add cand = function
       let cand = if add then 1::cand else cand in
       pop 1 (non_stricts add cand t)
   | MLrel n ->
-      List.filter ((<>) n) cand
+      List.filter (fun m -> not (Int.equal m n)) cand
   | MLapp (t,l)->
       let cand = non_stricts false cand t in
       List.fold_left (non_stricts false) cand l
@@ -1334,6 +1343,6 @@ let inline r t =
   not (to_keep r) (* The user DOES want to keep it *)
   && not (is_inline_custom r)
   && (to_inline r (* The user DOES want to inline it *)
-     || (lang () <> Haskell && not (is_projection r) &&
+     || (lang () != Haskell && not (is_projection r) &&
          (is_recursor r || manual_inline r || inline_test r t)))