More monomorphization.

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

5 files changed, 52 insertions, 49 deletions

diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 932b490e35..5bdb339d2a 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -292,14 +292,14 @@ let fv_lam l =
 
 
 let mkMLlam params body =
-  if Array.length params = 0 then body 
+  if Array.is_empty params then body 
   else
     match body with
     | MLlam (params', body) -> MLlam(Array.append params params', body)
     | _ -> MLlam(params,body)
 
 let mkMLapp f args =
-  if Array.length args = 0 then f
+  if Array.is_empty args then f
   else
     match f with
     | MLapp(f,args') -> MLapp(f,Array.append args' args)
@@ -404,18 +404,18 @@ let get_lname (_,l) =
 let fv_params env = 
   let fvn, fvr = !(env.env_named), !(env.env_urel) in 
   let size = List.length fvn + List.length fvr in
-  if size = 0 then empty_params 
+  if Int.equal size 0 then empty_params 
   else begin
     let params = Array.make size dummy_lname in
     let fvn = ref fvn in
     let i = ref 0 in
-    while !fvn <> [] do
+    while not (List.is_empty !fvn) do
       params.(!i) <- get_lname (List.hd !fvn);
       fvn := List.tl !fvn;
       incr i
     done;
     let fvr = ref fvr in
-    while !fvr <> [] do
+    while not (List.is_empty !fvr) do
       params.(!i) <- get_lname (List.hd !fvr);
       fvr := List.tl !fvr;
       incr i
@@ -430,19 +430,19 @@ let empty_args = [||]
 
 let fv_args env fvn fvr =
   let size = List.length fvn + List.length fvr in
-  if size = 0 then empty_args 
+  if Int.equal size 0 then empty_args 
   else 
     begin
       let args = Array.make size (MLint (false,0)) in
       let fvn = ref fvn in
       let i = ref 0 in
-      while !fvn <> [] do
+      while not (List.is_empty !fvn) do
 	args.(!i) <- get_var env (fst (List.hd !fvn));
 	fvn := List.tl !fvn;
 	incr i
       done;
       let fvr = ref fvr in
-      while !fvr <> [] do
+      while not (List.is_empty !fvr) do
 	let (k,_ as kml) = List.hd !fvr in
 	let n = get_lname kml in 
 	args.(!i) <- get_rel env n.lname k;
@@ -486,7 +486,7 @@ let rec insert cargs body rl =
      let params = rm_params fv params in
      rl:= Rcons(ref [(c,params)], fv, body, ref Rnil)
  | Rcons(l,fv,body',rl) ->
-     if body = body' then 
+     if Pervasives.(=) body body' then (** FIXME *)
        let (c,params) = cargs in
        let params = rm_params fv params in
        l := (c,params)::!l
@@ -761,7 +761,7 @@ let mllambda_of_lambda auxdefs l t =
    | _ -> assert false in
   let params = 
     List.append (List.map get_lname fv_rel) (List.map get_lname fv_named) in
-  if params = [] then
+  if List.is_empty params then
     (!global_stack, ([],[]), ml)
   (* final result : global list, fv, ml *)
   else
@@ -803,12 +803,12 @@ let subst s l =
 
 let add_subst id v s =
   match v with
-  | MLlocal id' when id.luid = id'.luid -> s
+  | MLlocal id' when Int.equal id.luid id'.luid -> s
   | _ -> LNmap.add id v s
 
 let subst_norm params args s =
   let len = Array.length params in
-  assert (Array.length args = len && Array.for_all can_subst args);
+  assert (Int.equal (Array.length args) len && Array.for_all can_subst args);
   let s = ref s in
   for i = 0 to len - 1 do
     s := add_subst params.(i) args.(i) !s
@@ -818,7 +818,7 @@ let subst_norm params args s =
 let subst_case params args s =
   let len = Array.length params in
   assert (len > 0 && 
-	  Array.length args = len && 
+	  Int.equal (Array.length args) len && 
 	  let r = ref true and i = ref 0 in
 	  (* we test all arguments excepted the last *)
 	  while !i < len - 1  && !r do r := can_subst args.(!i); incr i done;
@@ -836,7 +836,7 @@ let get_case (_, gcase) i = Int.Map.find i gcase
 let all_lam n bs = 
   let f (_, l) = 
     match l with
-    | MLlam(params, _) -> Array.length params = n
+    | MLlam(params, _) -> Int.equal (Array.length params) n
     | _ -> false in
   Array.for_all f bs
 
@@ -894,7 +894,7 @@ let optimize gdef l =
 	let b2 = optimize s b2 in
 	begin match t, b2 with
 	| MLapp(MLprimitive Is_accu,[| l1 |]), MLmatch(annot, l2, _, bs)
-	    when l1 = l2 -> MLmatch(annot, l1, b1, bs)	
+	    when Pervasives.(=) l1 l2 -> MLmatch(annot, l1, b1, bs) (** FIXME *)
         | _, _ -> MLif(t, b1, b2)
 	end
     | MLmatch(annot,a,accu,bs) ->
@@ -1190,8 +1190,8 @@ let pp_mllam fmt l =
     | Ceq o -> pp_vprim o "eq"
     | Clt o -> pp_vprim o "lt"
     | Cle o -> pp_vprim o "le"
-    | Clt_b  -> if Sys.word_size = 64 then Format.fprintf fmt "(<)" else Format.fprintf fmt "lt_b"
-    | Cle_b -> if Sys.word_size = 64 then Format.fprintf fmt "(<=)" else Format.fprintf fmt "le_b"
+    | Clt_b  -> if Int.equal (Sys.word_size) 64 then Format.fprintf fmt "(<)" else Format.fprintf fmt "lt_b"
+    | Cle_b -> if Int.equal (Sys.word_size) 64 then Format.fprintf fmt "(<=)" else Format.fprintf fmt "le_b"
     | Ccompare o -> pp_vprim o "compare"
     | Cprint o -> pp_vprim o "print"
     | Carraymake o -> pp_vprim o "arraymake"
@@ -1243,7 +1243,7 @@ let pp_global fmt g =
   | Gtype ((mind, i), lar) ->
       let l = string_of_mind mind in
       let rec aux s ar = 
-	if ar = 0 then s else aux (s^" * Nativevalues.t") (ar-1) in
+	if Int.equal ar 0 then s else aux (s^" * Nativevalues.t") (ar-1) in
       let pp_const_sig i fmt j ar =
         let sig_str = if ar > 0 then aux "of Nativevalues.t" (ar-1) else "" in
         Format.fprintf fmt "  | Construct_%s_%i_%i %s@\n" l i j sig_str
@@ -1267,7 +1267,7 @@ let pp_global fmt g =
 (** Compilation of elements in environment {{{**)
 let rec compile_with_fv env auxdefs l t =
   let (auxdefs,(fv_named,fv_rel),ml) = mllambda_of_lambda auxdefs l t in
-  if fv_named = [] && fv_rel = [] then (auxdefs,ml)
+  if List.is_empty fv_named && List.is_empty fv_rel then (auxdefs,ml)
   else apply_fv env (fv_named,fv_rel) auxdefs ml
 
 and apply_fv env (fv_named,fv_rel) auxdefs ml =
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 1c931ab85e..14b55e91a2 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -30,13 +30,14 @@ let rec conv_val pb lvl v1 v2 cu =
 	let v = mk_rel_accu lvl in
 	conv_val CONV (lvl+1) (f1 v) (f2 v) cu
     | Vconst i1, Vconst i2 -> 
-	if i1 = i2 then cu else raise NotConvertible
+	if Int.equal i1 i2 then cu else raise NotConvertible
     | Vblock b1, Vblock b2 ->
 	let n1 = block_size b1 in
-	if block_tag b1 <> block_tag b2 || n1 <> block_size b2 then
+        let n2 = block_size b2 in
+	if not (Int.equal (block_tag b1) (block_tag b2)) || not (Int.equal n1 n2) then
 	  raise NotConvertible;
 	let rec aux lvl max b1 b2 i cu =
-	  if i = max then 
+	  if Int.equal i max then 
 	    conv_val CONV lvl (block_field b1 i) (block_field b2 i) cu
 	  else
 	    let cu = 
@@ -51,8 +52,9 @@ let rec conv_val pb lvl v1 v2 cu =
 
 and conv_accu pb lvl k1 k2 cu = 
   let n1 = accu_nargs k1 in
-  if n1 <> accu_nargs k2 then raise NotConvertible;
-  if n1 = 0 then 
+  let n2 = accu_nargs k2 in
+  if not (Int.equal n1 n2) then raise NotConvertible;
+  if Int.equal n1 0 then 
     conv_atom pb lvl (atom_of_accu k1) (atom_of_accu k2) cu
   else
     let cu = conv_atom pb lvl (atom_of_accu k1) (atom_of_accu k2) cu in
@@ -63,7 +65,7 @@ and conv_atom pb lvl a1 a2 cu =
   else
     match a1, a2 with
     | Arel i1, Arel i2 -> 
-	if i1 <> i2 then raise NotConvertible;
+	if not (Int.equal i1 i2) then raise NotConvertible;
 	cu
     | Aind ind1, Aind ind2 ->
 	if not (eq_ind ind1 ind2) then raise NotConvertible;
@@ -74,36 +76,36 @@ and conv_atom pb lvl a1 a2 cu =
     | Asort s1, Asort s2 -> 
 	sort_cmp pb s1 s2 cu
     | Avar id1, Avar id2 ->
-	if id1 <> id2 then raise NotConvertible;
+	if not (Id.equal id1 id2) then raise NotConvertible;
 	cu
     | Acase(a1,ac1,p1,bs1), Acase(a2,ac2,p2,bs2) ->
-	if a1.asw_ind <> a2.asw_ind then raise NotConvertible;
+	if not (eq_ind a1.asw_ind a2.asw_ind) then raise NotConvertible;
 	let cu = conv_accu CONV lvl ac1 ac2 cu in
 	let tbl = a1.asw_reloc in
 	let len = Array.length tbl in
-	if len = 0 then conv_val CONV lvl p1 p2 cu 
+	if Int.equal len 0 then conv_val CONV lvl p1 p2 cu 
 	else
 	  let cu = conv_val CONV lvl p1 p2 cu in
 	  let max = len - 1 in
 	  let rec aux i cu =
 	    let tag,arity = tbl.(i) in
 	    let ci = 
-	      if arity = 0 then mk_const tag
+	      if Int.equal arity 0 then mk_const tag
 	      else mk_block tag (mk_rels_accu lvl arity) in
 	    let bi1 = bs1 ci and bi2 = bs2 ci in
-	    if i = max then conv_val CONV (lvl + arity) bi1 bi2 cu
+	    if Int.equal i max then conv_val CONV (lvl + arity) bi1 bi2 cu
 	    else aux (i+1) (conv_val CONV (lvl + arity) bi1 bi2 cu) in
 	  aux 0 cu
     | Afix(t1,f1,rp1,s1), Afix(t2,f2,rp2,s2) ->
-	if s1 <> s2 || rp1 <> rp2 then raise NotConvertible;
+	if not (Int.equal s1 s2) || not (Array.equal Int.equal rp1 rp2) then raise NotConvertible;
 	if f1 == f2 then cu
 	else conv_fix lvl t1 f1 t2 f2 cu
     | (Acofix(t1,f1,s1,_) | Acofixe(t1,f1,s1,_)),
       (Acofix(t2,f2,s2,_) | Acofixe(t2,f2,s2,_)) ->
-	if s1 <> s2 then raise NotConvertible;
+	if not (Int.equal s1 s2) then raise NotConvertible;
 	if f1 == f2 then cu
 	else
-	  if Array.length f1 <> Array.length f2 then raise NotConvertible
+	  if not (Int.equal (Array.length f1) (Array.length f2)) then raise NotConvertible
 	  else conv_fix lvl t1 f1 t2 f2 cu 
     | Aprod(_,d1,c1), Aprod(_,d2,c2) ->
 	let cu = conv_val CONV lvl d1 d2 cu in
@@ -121,7 +123,7 @@ and conv_fix lvl t1 f1 t2 f2 cu =
     let cu = conv_val CONV lvl t1.(i) t2.(i) cu in
     let fi1 = napply f1.(i) fargs in
     let fi2 = napply f2.(i) fargs in
-    if i = max then conv_val CONV flvl fi1 fi2 cu 
+    if Int.equal i max then conv_val CONV flvl fi1 fi2 cu 
     else aux (i+1) (conv_val CONV flvl fi1 fi2 cu) in
   aux 0 cu
 
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 9c400e4c03..b8580f2b3a 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -48,14 +48,14 @@ and fix_decl =  name array * lambda array * lambda array
 (*s Constructors *)
   
 let mkLapp f args =
-  if Array.length args = 0 then f
+  if Array.is_empty args then f
   else
     match f with
     | Lapp(f', args') -> Lapp (f', Array.append args' args)
     | _ -> Lapp(f, args)
 	  
 let mkLlam ids body =
-  if Array.length ids = 0 then body
+  if Array.is_empty ids then body
   else 
     match body with
     | Llam(ids', body) -> Llam(Array.append ids ids', body)
@@ -134,8 +134,7 @@ let map_lam_with_binders g f n lam =
       let on_b b = 
 	let (cn,ids,body) = b in
 	let body' = 
-	  let len = Array.length ids in
-	  if len = 0 then f n body 
+	  if Array.is_empty ids then f n body 
 	  else f (g (Array.length ids) n) body in
 	if body == body' then b else (cn,ids,body') in
       let br' = Array.smartmap on_b br in
@@ -172,7 +171,7 @@ let rec lam_exlift el lam =
   | _ -> map_lam_with_binders el_liftn lam_exlift el lam
 
 let lam_lift k lam =
-  if k = 0 then lam
+  if Int.equal k 0 then lam
   else lam_exlift (el_shft k el_id) lam
 
 let lam_subst_rel lam id n subst =
@@ -226,7 +225,7 @@ let merge_if t bt bf =
   let nt = Array.length idst in
   let nf = Array.length idsf in
   let common,idst,idsf = 
-    if nt = nf then idst, [||], [||] 
+    if Int.equal nt nf then idst, [||], [||] 
     else
       if nt < nf then idst,[||], Array.sub idsf nt (nf - nt)
       else idsf, Array.sub idst nf (nt - nf), [||] in
@@ -315,7 +314,7 @@ and reduce_lapp substf lids body substa largs =
 let rec occurence k kind lam =   
   match lam with
   | Lrel (_,n) -> 
-      if n = k then 
+      if Int.equal n k then 
 	if kind then false else raise Not_found
       else kind
   | Lvar _  | Lconst _  | Lval _ | Lsort _ | Lind _
@@ -379,13 +378,13 @@ let rec remove_let subst lam =
 let is_value lc =
   match lc with
   | Lval _ -> true
-  | Lmakeblock(_,_,_,args) when Array.length args = 0 -> true
+  | Lmakeblock(_,_,_,args) when Array.is_empty args -> true
   | _ -> false
 	
 let get_value lc =
   match lc with
   | Lval v -> v
-  | Lmakeblock(_,_,tag,args) when Array.length args = 0 -> 
+  | Lmakeblock(_,_,tag,args) when Array.is_empty args -> 
       Nativevalues.mk_int tag
   | _ -> raise Not_found
 	
@@ -436,7 +435,7 @@ module Vect =
     let length v = v.size
 
     let extend v =
-      if v.size = Array.length v.elems then 
+      if Int.equal v.size (Array.length v.elems) then 
 	let new_size = min (2*v.size) Sys.max_array_length in
 	if new_size <= v.size then raise (Invalid_argument "Vect.extend");
 	let new_elems = Array.make new_size v.elems.(0) in
@@ -470,7 +469,7 @@ module Vect =
 
 
     let last v =
-      if v.size = 0 then raise
+      if Int.equal v.size 0 then raise
 	  (Invalid_argument "Vect.last:index out of bounds");
       v.elems.(v.size - 1)
 
@@ -598,10 +597,10 @@ let rec lambda_of_constr env c =
 	let cn = (ind,i+1) in
 	let _, arity = tbl.(i) in
 	let b = lambda_of_constr env b in
-	if arity = 0 then (cn, empty_ids, b)
+	if Int.equal arity 0 then (cn, empty_ids, b)
 	else 
 	  match b with
-	  | Llam(ids, body) when Array.length ids = arity -> (cn, ids, body)
+	  | Llam(ids, body) when Int.equal (Array.length ids) arity -> (cn, ids, body)
 	  | _ -> 
 	      let ids = Array.make arity Anonymous in
 	      let args = make_args arity 1 in
@@ -649,7 +648,7 @@ and lambda_of_app env f args =
       let tag, nparams, arity = Renv.get_construct_info env c in
       let expected = nparams + arity in
       let nargs = Array.length args in
-      if nargs = expected then 
+      if Int.equal nargs expected then 
 	let args = lambda_of_args env nparams args in
 	makeblock !global_env c tag args
       else
diff --git a/kernel/term.ml b/kernel/term.ml
index 14154b6c88..a052d6dfc9 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -76,6 +76,8 @@ let sorts_ord s1 s2 =
   | Prop _, Type _ -> -1
   | Type _, Prop _ -> 1
 
+let sorts_eq s1 s2 = Int.equal (sorts_ord s1 s2) 0
+
 let is_prop_sort = function
 | Prop Null -> true
 | _ -> false
diff --git a/kernel/univ.ml b/kernel/univ.ml
index f1d44a9a53..f0501358bc 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -510,7 +510,7 @@ let merge g arcu arcv =
 let merge_disc g arc1 arc2 =
   let arcu, arcv = if arc1.rank < arc2.rank then arc2, arc1 else arc1, arc2 in
   let arcu, g = 
-    if arc1.rank <> arc2.rank then arcu, g
+    if not (Int.equal arc1.rank arc2.rank) then arcu, g
     else
       let arcu = {arcu with rank = succ arcu.rank} in 
       arcu, enter_arc arcu g