More monomorphization.

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

2 files changed, 42 insertions, 29 deletions

diff --git a/checker/declarations.ml b/checker/declarations.ml
index 2ff570a4a..503460422 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -41,6 +41,7 @@ type delta_hint =
 module Deltamap = struct
   type t = module_path MPmap.t * delta_hint KNmap.t
   let empty = MPmap.empty, KNmap.empty
+  let is_empty (mm, km) = MPmap.is_empty mm && KNmap.is_empty km
   let add_kn kn hint (mm,km) = (mm,KNmap.add kn hint km)
   let add_mp mp mp' (mm,km) = (MPmap.add mp mp' mm, km)
   let remove_mp mp (mm,km) = (MPmap.remove mp mm, km)
@@ -347,7 +348,7 @@ let from_val a = ref (LSval a)
  
 let rec replace_mp_in_mp mpfrom mpto mp =
   match mp with
-    | _ when mp = mpfrom -> mpto
+    | _ when ModPath.equal mp mpfrom -> mpto
     | MPdot (mp1,l) ->
 	let mp1' = replace_mp_in_mp mpfrom mpto mp1 in
 	  if mp1==mp1' then mp
@@ -356,7 +357,7 @@ let rec replace_mp_in_mp mpfrom mpto mp =
 
 let rec mp_in_mp mp mp1 =
   match mp1 with
-    | _ when mp1 = mp -> true
+    | _ when ModPath.equal mp1 mp -> true
     | MPdot (mp2,l) -> mp_in_mp mp mp2
     | _ -> false
 
@@ -429,14 +430,14 @@ let update_delta_resolver resolver1 resolver2 =
 let add_delta_resolver resolver1 resolver2 =
   if resolver1 == resolver2 then
     resolver2
-  else if resolver2 = empty_delta_resolver then
+  else if Deltamap.is_empty resolver2 then
     resolver1
   else
     Deltamap.join (update_delta_resolver resolver1 resolver2) resolver2
 
 let substition_prefixed_by k mp subst =
   let mp_prefixmp kmp (mp_to,reso) sub =
-    if mp_in_mp mp kmp && mp <> kmp then
+    if mp_in_mp mp kmp && not (ModPath.equal mp kmp) then
       let new_key = replace_mp_in_mp mp k kmp in
       Umap.add_mp new_key (mp_to,reso) sub
     else sub
@@ -722,7 +723,7 @@ let subst_arity sub = function
 (* NB: we leave bytecode and native code fields untouched *)
 let subst_const_body sub cb =
  { cb with
-    const_hyps = (assert (cb.const_hyps=[]); []);
+    const_hyps = (assert (List.is_empty cb.const_hyps); []);
     const_body = subst_constant_def sub cb.const_body;
     const_type = subst_arity sub cb.const_type }
 
@@ -755,7 +756,7 @@ let subst_mind sub mib =
   { mind_record = mib.mind_record ;
     mind_finite = mib.mind_finite ;
     mind_ntypes = mib.mind_ntypes ;
-    mind_hyps = (assert (mib.mind_hyps=[]); []) ;
+    mind_hyps = (assert (List.is_empty mib.mind_hyps); []) ;
     mind_nparams = mib.mind_nparams;
     mind_nparams_rec = mib.mind_nparams_rec;
     mind_params_ctxt =
diff --git a/checker/term.ml b/checker/term.ml
index 8e968904b..bdbc7f8ec 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -197,7 +197,7 @@ let closed0 = closedn 0
 
 let noccurn n term =
   let rec occur_rec n c = match c with
-    | Rel m -> if m = n then raise LocalOccur
+    | Rel m -> if Int.equal m n then raise LocalOccur
     | _ -> iter_constr_with_binders succ occur_rec n c
   in
   try occur_rec n term; true with LocalOccur -> false
@@ -221,7 +221,7 @@ let noccur_between n m term =
 
 let noccur_with_meta n m term =
   let rec occur_rec n c = match c with
-    | Rel p -> if n<=p & p<n+m then raise LocalOccur
+    | Rel p -> if n<=p && p<n+m then raise LocalOccur
     | App(f,cl) ->
 	(match f with
            | (Cast (Meta _,_,_)| Meta _) -> ()
@@ -291,7 +291,7 @@ let make_substituend c = { sinfo=Unknown; sit=c }
 
 let substn_many lamv n c =
   let lv = Array.length lamv in
-  if lv = 0 then c
+  if Int.equal lv 0 then c
   else
     let rec substrec depth c = match c with
       | Rel k     ->
@@ -383,7 +383,7 @@ let decompose_lam_n_assum n =
   if n < 0 then
     error "decompose_lam_n_assum: integer parameter must be positive";
   let rec lamdec_rec l n c =
-    if n=0 then l,c
+    if Int.equal n 0 then l,c
     else match c with
     | Lambda (x,t,c)  -> lamdec_rec ((x,None,t) :: l) (n-1) c
     | LetIn (x,b,t,c) -> lamdec_rec ((x,Some b,t) :: l) n c
@@ -416,7 +416,7 @@ let decompose_prod_n_assum n =
   if n < 0 then
     error "decompose_prod_n_assum: integer parameter must be positive";
   let rec prodec_rec l n c =
-    if n=0 then l,c
+    if Int.equal n 0 then l,c
     else match c with
     | Prod (x,t,c)    -> prodec_rec ((x,None,t) :: l) (n-1) c
     | LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t) :: l) (n-1) c
@@ -459,40 +459,52 @@ let rec isArity c =
 
 (* alpha conversion : ignore print names and casts *)
 
+let compare_sorts s1 s2 = match s1, s2 with
+| Prop c1, Prop c2 ->
+  begin match c1, c2 with
+  | Pos, Pos | Null, Null -> true
+  | Pos, Null -> false
+  | Null, Pos -> false
+  end
+| Type u1, Type u2 -> Universe.equal u1 u2
+| Prop _, Type _ -> false
+| Type _, Prop _ -> false
+
 let compare_constr f t1 t2 =
   match t1, t2 with
-  | Rel n1, Rel n2 -> n1 = n2
-  | Meta m1, Meta m2 -> m1 = m2
-  | Var id1, Var id2 -> id1 = id2
-  | Sort s1, Sort s2 -> s1 = s2
+  | Rel n1, Rel n2 -> Int.equal n1 n2
+  | Meta m1, Meta m2 -> Int.equal m1 m2
+  | Var id1, Var id2 -> Id.equal id1 id2
+  | Sort s1, Sort s2 -> compare_sorts s1 s2
   | Cast (c1,_,_), _ -> f c1 t2
   | _, Cast (c2,_,_) -> f t1 c2
-  | Prod (_,t1,c1), Prod (_,t2,c2) -> f t1 t2 & f c1 c2
-  | Lambda (_,t1,c1), Lambda (_,t2,c2) -> f t1 t2 & f c1 c2
-  | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> f b1 b2 & f t1 t2 & f c1 c2
+  | Prod (_,t1,c1), Prod (_,t2,c2) -> f t1 t2 && f c1 c2
+  | Lambda (_,t1,c1), Lambda (_,t2,c2) -> f t1 t2 && f c1 c2
+  | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> f b1 b2 && f t1 t2 && f c1 c2
   | App (c1,l1), App (c2,l2) ->
-      if Array.length l1 = Array.length l2 then
-        f c1 c2 & Array.for_all2 f l1 l2
+      if Int.equal (Array.length l1) (Array.length l2) then
+        f c1 c2 && Array.for_all2 f l1 l2
       else
         let (h1,l1) = decompose_app t1 in
         let (h2,l2) = decompose_app t2 in
-        if List.length l1 = List.length l2 then
-          f h1 h2 & List.for_all2 f l1 l2
+        if Int.equal (List.length l1) (List.length l2) then
+          f h1 h2 && List.for_all2 f l1 l2
         else false
-  | Evar (e1,l1), Evar (e2,l2) -> e1 = e2 & Array.for_all2 f l1 l2
+  | Evar (e1,l1), Evar (e2,l2) -> Int.equal e1 e2 && Array.equal f l1 l2
   | Const c1, Const c2 -> eq_con_chk c1 c2
   | Ind c1, Ind c2 -> eq_ind_chk c1 c2
-  | Construct (c1,i1), Construct (c2,i2) -> i1=i2 && eq_ind_chk c1 c2
+  | Construct (c1,i1), Construct (c2,i2) -> Int.equal i1 i2 && eq_ind_chk c1 c2
   | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
-      f p1 p2 & f c1 c2 & Array.for_all2 f bl1 bl2
-  | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) ->
-      ln1 = ln2 & Array.for_all2 f tl1 tl2 & Array.for_all2 f bl1 bl2
+      f p1 p2 && f c1 c2 && Array.equal f bl1 bl2
+  | Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) ->
+      Int.equal i1 i2 && Array.equal Int.equal ln1 ln2 &&
+      Array.equal f tl1 tl2 && Array.equal f bl1 bl2
   | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
-      ln1 = ln2 & Array.for_all2 f tl1 tl2 & Array.for_all2 f bl1 bl2
+      Int.equal ln1 ln2 && Array.equal f tl1 tl2 && Array.equal f bl1 bl2
   | _ -> false
 
 let rec eq_constr m n =
-  (m==n) or
+  (m == n) ||
   compare_constr eq_constr m n
 
 let eq_constr m n = eq_constr m n (* to avoid tracing a recursive fun *)