Nettoyage check_pos

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

1 files changed, 42 insertions, 78 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index cdb45e9d4a..359f92d4b1 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -85,6 +85,7 @@ let check_correct_par env nparams ntypes n l largs =
   if not (array_for_all (noccur_bet n ntypes) largs') then 
     failwith_non_pos_vect n ntypes largs'
 
+(* This removes global parameters of the inductive types in lc *)
 let abstract_mind_lc env ntyps npars lc = 
   let lC = decomp_DLAMV ntyps lc in
   if npars = 0 then 
@@ -99,38 +100,32 @@ let abstract_mind_lc env ntyps npars lc =
 let decomp_par n c = snd (mind_extract_params n c)
       
 let listrec_mconstr env ntypes nparams i indlc =
-  (* check the inductive types occur positively in C *)
+  (* check the inductive types occur positively in [c] *)
   let rec check_pos n c = 
     match whd_betadeltaiota env Evd.empty c with 
       | DOP2(Prod,b,DLAM(na,d)) -> 
           if not (noccur_bet n ntypes b) then raise (IllFormedInd (NonPos n));
 	  check_pos (n+1) d
       | x -> 
-	  (match ensure_appl x with 
-             | DOPN(AppL,cl) -> 
-                 let hd = array_hd cl 
-		 and largs = array_tl cl in
-                 (match hd with 
-                    | Rel k ->
-                        if k >= n && k<n+ntypes then begin
-			  check_correct_par env nparams ntypes n (k-n+1) largs;
-			  Mrec(n+ntypes-k-1) 
-                        end else if noccur_bet n ntypes x then 
-			  if (n-nparams) <= k & k <= (n-1) 
-			  then Param(n-1-k)
-                          else Norec
-			else 
-			  raise (IllFormedInd (NonPos n))
-                    | DOPN(MutInd ind_sp,a) -> 
-                        if (noccur_bet n ntypes x) then
-                          Norec
-                        else 
-			  Imbr(ind_sp,imbr_positive n (ind_sp,a) largs)
-                    | err -> 
-			if noccur_bet n ntypes x then Norec
-			else raise (IllFormedInd (NonPos n)))
-             | _ -> anomaly "check_pos")
-	  
+	  let hd,largs = destApplication (ensure_appl x) in
+          match hd with
+            | Rel k ->
+                if k >= n && k<n+ntypes then begin
+		  check_correct_par env nparams ntypes n (k-n+1) largs;
+		  Mrec(n+ntypes-k-1)
+                end else if noccur_bet n ntypes x then 
+		  if (n-nparams) <= k & k <= (n-1) 
+		  then Param(n-1-k)
+                  else Norec
+		else
+		  raise (IllFormedInd (NonPos n))
+            | DOPN(MutInd ind_sp,a) -> 
+                if (noccur_bet n ntypes x) then Norec
+                else Imbr(ind_sp,imbr_positive n (ind_sp,a) largs)
+            | err -> 
+		if noccur_bet n ntypes x then Norec
+		else raise (IllFormedInd (NonPos n))
+
   and imbr_positive n mi largs =
     let mispeci = lookup_mind_specif mi env in
     let auxnpar = mis_nparams mispeci in
@@ -140,7 +135,7 @@ let listrec_mconstr env ntypes nparams i indlc =
     let auxlc = mis_lc mispeci 
     and auxntyp = mis_ntypes mispeci in 
     if auxntyp <> 1 then raise (IllFormedInd (NonPos n));
-    let lrecargs = array_map_to_list (check_param_pos n) lpar in
+    let lrecargs = array_map_to_list (check_weak_pos n) lpar in
     (* The abstract imbricated inductive type with parameters substituted *)
     let auxlcvect = abstract_mind_lc env auxntyp auxnpar auxlc in
     let newidx = n + auxntyp in
@@ -156,7 +151,7 @@ let listrec_mconstr env ntypes nparams i indlc =
     in 
     lrecargs
 
-  (* The function check_param_pos is exactly the same as check_pos, but
+  (* The function check_weak_pos is exactly the same as check_pos, but
      with an extra case for traversing abstractions, like in Marseille's
      contribution about bisimulations:
      
@@ -170,71 +165,40 @@ let listrec_mconstr env ntypes nparams i indlc =
      Abstractions may occur in imbricated recursive ocurrences, but I am
      not sure if they make sense in a form of constructor. This is why I
      chose to duplicated the code.  Eduardo 13/7/99. *)
-  and check_param_pos n c = 
+  (* Since Lambda can no longer occur after a product or a MutInd,
+     I have branched the remaining cases on check_pos. HH 28/1/00 *)
+
+  and check_weak_pos n c = 
     match whd_betadeltaiota env Evd.empty c with 
       (* The extra case *)
       | DOP2(Lambda,b,DLAM(na,d)) -> 
           if noccur_bet n ntypes b
-          then check_param_pos (n+1) d
+          then check_weak_pos (n+1) d
           else raise (IllFormedInd (NonPos n))
       (******************)
-      | DOP2(Prod,b,DLAM(na,d)) -> 
-          if (noccur_bet n ntypes b) 
-          then check_param_pos (n+1) d
-          else raise (IllFormedInd (NonPos n))
-      | x -> 
-	  (match ensure_appl x with 
-             | DOPN(AppL,cl) -> 
-                 let hd = array_hd cl 
-		 and largs = array_tl cl in 
-		 (match hd with 
-                    | Rel k -> 
-			if k >= n & k<n+ntypes then begin
-                          check_correct_par env nparams ntypes n (k-n+1) largs;
-			  Mrec(n+ntypes-k-1) 
-                        end else if noccur_bet n ntypes x then 
-			  if (n-nparams) <= k & k <= (n-1)
-                          then Param(n-1-k)
-                          else Norec
-			else raise (IllFormedInd (NonPos n))
-                    | DOPN(MutInd ind_sp,a) -> 
-                        if (noccur_bet n ntypes x) 
-                        then Norec
-                        else Imbr(ind_sp,imbr_positive n (ind_sp,a) largs)
-                    | err -> if noccur_bet n ntypes x then Norec
-		      else raise (IllFormedInd (NonPos n)))
-             | _ -> anomaly "check_param_pos")
+      | x -> check_pos n x
   
   (* check the inductive types occur positively in the products of C, if
-     checkhd=true, also check the head corresponds to a constructor of
+     check_head=true, also check the head corresponds to a constructor of
      the ith type *) 
 
-  and check_construct check = 
+  and check_construct check_head = 
     let rec check_constr_rec lrec n c = 
       match whd_betadeltaiota env Evd.empty c with
         | DOP2(Prod,b,DLAM(na,d)) -> 
-            let recarg = (check_pos n b) in 
+            let recarg = check_pos n b in 
 	    check_constr_rec (recarg::lrec) (n+1) d 
 	| x -> 
-	    (match ensure_appl x with 
-               | DOPN(AppL,cl) ->
-                   let hd = array_hd cl 
-                   and largs = array_tl cl in 
-                   if check then 
-                     (match hd with 
-			| Rel k -> 
-                            if k = n+ntypes-i then begin
-			      check_correct_par env nparams 
-				ntypes n (k-n+1) largs;
-			      List.rev lrec 
-                            end else 
-			      raise (IllFormedInd (NonPos n))
-                        | _ -> raise (IllFormedInd (NonPos n)))
-                   else 
-                     if array_for_all (noccur_bet n ntypes) largs 
-                     then List.rev lrec 
-                     else raise (IllFormedInd (NonPos n)) 
-	       | _ -> anomaly "ensure_appl should return an AppL") 
+            let hd,largs = destApplication (ensure_appl x) in
+	    if check_head then
+              match hd with
+		| Rel k when k = n+ntypes-i ->
+		    check_correct_par env nparams ntypes n (k-n+1) largs
+                | _ -> raise (IllFormedInd NotConstructor)
+	    else
+	      if not (array_for_all (noccur_bet n ntypes) largs)
+              then raise (IllFormedInd (NonPos n));
+	    List.rev lrec
     in check_constr_rec []
   in
   let (lna,lC) = decomp_DLAMV_name ntypes indlc in