From 7ac3d69bcfc973219d2a87622e1cbf45883bb4ca Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 7 Mar 2000 17:03:38 +0000 Subject: Nettoyage check_pos git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@294 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/indtypes.ml | 120 +++++++++++++++++++---------------------------------- 1 file changed, 42 insertions(+), 78 deletions(-) (limited to 'kernel') 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 - 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 + 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 - 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 -- cgit v1.2.3