From 8c26c46da941016b929a542aadd14542ec0bc431 Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 11 Oct 2000 20:01:09 +0000 Subject: Prise en compte de l'environnement dans les tests de bonne fondaison git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@691 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/typeops.ml | 237 ++++++++++++++++++++++++++++++------------------------ 1 file changed, 130 insertions(+), 107 deletions(-) (limited to 'kernel/typeops.ml') diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 5aaa47847..31a31a9d9 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -364,28 +364,29 @@ let rec instantiate_recarg sp lrc ra = (* propagate checking for F,incorporating recursive arguments *) let check_term env mind_recvec f = - let rec crec n l (lrec,c) = + let rec crec env n l (lrec,c) = match lrec, kind_of_term (strip_outer_cast c) with - | (Param(_)::lr, IsLambda (_,_,b)) -> + | (Param(_)::lr, IsLambda (x,a,b)) -> let l' = map_lift_fst l in - crec (n+1) l' (lr,b) - | (Norec::lr, IsLambda (_,_,b)) -> + crec (push_rel_decl (x,outcast_type a) env) (n+1) l' (lr,b) + | (Norec::lr, IsLambda (x,a,b)) -> let l' = map_lift_fst l in - crec (n+1) l' (lr,b) - | (Mrec(i)::lr, IsLambda (_,_,b)) -> + crec (push_rel_decl (x,outcast_type a) env) (n+1) l' (lr,b) + | (Mrec(i)::lr, IsLambda (x,a,b)) -> let l' = map_lift_fst l in - crec (n+1) ((1,mind_recvec.(i))::l') (lr,b) - | (Imbr((sp,i) as ind_sp,lrc)::lr, IsLambda (_,_,b)) -> + crec (push_rel_decl (x,outcast_type a) env) (n+1) + ((1,mind_recvec.(i))::l') (lr,b) + | (Imbr((sp,i) as ind_sp,lrc)::lr, IsLambda (x,a,b)) -> let l' = map_lift_fst l in let sprecargs = mis_recargs (lookup_mind_specif (ind_sp,[||]) env) in let lc = Array.map (List.map (instantiate_recarg sp lrc)) sprecargs.(i) in - crec (n+1) ((1,lc)::l') (lr,b) - | _,_ -> f n l (strip_outer_cast c) + crec (push_rel_decl (x,outcast_type a) env) (n+1) ((1,lc)::l') (lr,b) + | _,_ -> f env n l (strip_outer_cast c) in - crec + crec env let is_inst_var env sigma k c = match kind_of_term (fst (whd_betadeltaiota_stack env sigma c)) with @@ -393,7 +394,7 @@ let is_inst_var env sigma k c = | _ -> false let is_subterm_specif env sigma lcx mind_recvec = - let rec crec n lst c = + let rec crec env n lst c = let f,l = whd_betadeltaiota_stack env sigma c in match kind_of_term f with | IsRel k -> find_sorted_assoc k lst @@ -404,7 +405,7 @@ let is_subterm_specif env sigma lcx mind_recvec = else let lcv = (try - if is_inst_var env sigma n c then lcx else (crec n lst c) + if is_inst_var env sigma n c then lcx else crec env n lst c with Not_found -> (Array.create (Array.length br) [])) in assert (Array.length br = Array.length lcv); @@ -415,11 +416,11 @@ let is_subterm_specif env sigma lcx mind_recvec = in stl.(0) - | IsFix ((recindxs,i),(typarray,funnames,bodies)) -> + | IsFix ((recindxs,i),(typarray,funnames,bodies as recdef)) -> let nbfix = List.length funnames in let decrArg = recindxs.(i) in let theBody = bodies.(i) in - let (_,strippedBody) = decompose_lam_n (decrArg+1) theBody in + let sign,strippedBody = decompose_lam_n_assum (decrArg+1) theBody in let nbOfAbst = nbfix+decrArg+1 in let newlst = if List.length l < (decrArg+1) then @@ -427,7 +428,7 @@ let is_subterm_specif env sigma lcx mind_recvec = else let theDecrArg = List.nth l decrArg in let recArgsDecrArg = - try (crec n lst theDecrArg) + try (crec env n lst theDecrArg) with Not_found -> Array.create 0 [] in if (Array.length recArgsDecrArg)=0 then @@ -437,17 +438,19 @@ let is_subterm_specif env sigma lcx mind_recvec = (nbOfAbst,lcx) :: (map_lift_fst_n nbOfAbst lst) in - crec (n+nbOfAbst) newlst strippedBody + let env' = push_rec_types recdef env in + let env'' = push_rels sign env' in + crec env'' (n+nbOfAbst) newlst strippedBody - | IsLambda (_,_,b) when l=[] -> + | IsLambda (x,a,b) when l=[] -> let lst' = map_lift_fst lst in - crec (n+1) lst' b + crec (push_rel_decl (x,outcast_type a) env) (n+1) lst' b (*** Experimental change *************************) | IsMeta _ -> [||] | _ -> raise Not_found in - crec + crec env let is_subterm env sigma lcx mind_recvec n lst c = try @@ -466,25 +469,27 @@ let rec check_subterm_rec_meta env sigma vectn k def = (let nfi = Array.length vectn in (* check fi does not appear in the k+1 first abstractions, gives the type of the k+1-eme abstraction *) - let rec check_occur n def = + let rec check_occur env n def = match kind_of_term (strip_outer_cast def) with - | IsLambda (_,a,b) -> + | IsLambda (x,a,b) -> if noccur_with_meta n nfi a then - if n = k+1 then (a,b) else check_occur (n+1) b + let env' = push_rel_decl (x,outcast_type a) env in + if n = k+1 then (env',a,b) + else check_occur env' (n+1) b else anomaly "check_subterm_rec_meta: Bad occurrence of recursive call" | _ -> raise (FixGuardError NotEnoughAbstractionInFixBody) in - let (c,d) = check_occur 1 def in + let (env',c,d) = check_occur env 1 def in let ((sp,tyi),_ as mind, largs) = - try find_minductype env sigma c + try find_inductive env' sigma c with Induc -> raise (FixGuardError RecursionNotOnInductiveType) in - let mind_recvec = mis_recargs (lookup_mind_specif mind env) in + let mind_recvec = mis_recargs (lookup_mind_specif mind env') in let lcx = mind_recvec.(tyi) in (* n = decreasing argument in the definition; lst = a mapping var |-> recargs t = the term to be checked *) - let rec check_rec_call n lst t = + let rec check_rec_call env n lst t = (* n gives the index of the recursive variable *) (noccur_with_meta (n+k+1) nfi t) or (* no recursive call in the term *) @@ -499,11 +504,11 @@ let rec check_subterm_rec_meta env sigma vectn k def = (match list_chop np l with (la,(z::lrest)) -> if (is_subterm env sigma lcx mind_recvec n lst z) - then List.for_all (check_rec_call n lst) (la@lrest) + then List.for_all (check_rec_call env n lst) (la@lrest) else raise (FixGuardError RecursionOnIllegalTerm) | _ -> assert false) else raise (FixGuardError NotEnoughArgumentsForFixCall) - else List.for_all (check_rec_call n lst) l + else List.for_all (check_rec_call env n lst) l | IsMutCase (ci,p,c_0,lrest) -> let lc = @@ -516,10 +521,10 @@ let rec check_subterm_rec_meta env sigma vectn k def = Array.create (Array.length lrest) []) in (array_for_all2 - (fun c_0 a -> - check_term env mind_recvec (check_rec_call) n lst (c_0,a)) + (fun c0 a -> + check_term env mind_recvec check_rec_call n lst (c0,a)) lc lrest) - && (List.for_all (check_rec_call n lst) (c_0::p::l)) + && (List.for_all (check_rec_call env n lst) (c_0::p::l)) (* Enables to traverse Fixpoint definitions in a more intelligent way, ie, the rule : @@ -536,15 +541,15 @@ let rec check_subterm_rec_meta env sigma vectn k def = Eduardo 7/9/98 *) - | IsFix ((recindxs,i),(typarray,funnames,bodies)) -> - (List.for_all (check_rec_call n lst) l) && + | IsFix ((recindxs,i),(typarray,funnames,bodies as recdef)) -> + (List.for_all (check_rec_call env n lst) l) && let nbfix = List.length funnames in let decrArg = recindxs.(i) in if (List.length l < (decrArg+1)) then - (array_for_all (check_rec_call n lst) typarray) + (array_for_all (check_rec_call env n lst) typarray) && (array_for_all - (check_rec_call (n+nbfix) (map_lift_fst_n nbfix lst)) + (check_rec_call env (n+nbfix) (map_lift_fst_n nbfix lst)) bodies) else let theDecrArg = List.nth l decrArg in @@ -555,85 +560,95 @@ let rec check_subterm_rec_meta env sigma vectn k def = Array.create 0 [] in if (Array.length recArgsDecrArg)=0 then - (array_for_all (check_rec_call n lst) typarray) + (array_for_all (check_rec_call env n lst) typarray) && (array_for_all - (check_rec_call (n+nbfix) (map_lift_fst_n nbfix lst)) + (check_rec_call env (n+nbfix) (map_lift_fst_n nbfix lst)) bodies) else let theBody = bodies.(i) in - let (gamma,strippedBody) = - decompose_lam_n (decrArg+1) theBody in - let absTypes = List.map snd gamma in - let nbOfAbst = nbfix+decrArg+1 in - let newlst = - ((1,recArgsDecrArg)::(map_lift_fst_n nbOfAbst lst)) - in - ((array_for_all - (fun t -> check_rec_call n lst t) - typarray) && - (list_for_all_i (fun n -> check_rec_call n lst) n absTypes) & - (check_rec_call (n+nbOfAbst) newlst strippedBody)) + let env' = push_rec_types recdef env in + (array_for_all + (fun t -> check_rec_call env n lst t) typarray) && + (check_rec_call_fix_body env' (n+nbfix) + (map_lift_fst_n nbfix lst) (decrArg+1) recArgsDecrArg + theBody) | IsCast (a,b) -> - (check_rec_call n lst a) && - (check_rec_call n lst b) && - (List.for_all (check_rec_call n lst) l) - - | IsLambda (_,a,b) -> - (check_rec_call n lst a) && - (check_rec_call (n+1) (map_lift_fst lst) b) && - (List.for_all (check_rec_call n lst) l) - - | IsProd (_,a,b) -> - (check_rec_call n lst a) && - (check_rec_call (n+1) (map_lift_fst lst) b) && - (List.for_all (check_rec_call n lst) l) - - | IsLetIn (_,a,b,c) -> - (check_rec_call n lst a) && - (check_rec_call n lst b) && - (check_rec_call (n+1) (map_lift_fst lst) c) && - (List.for_all (check_rec_call n lst) l) + (check_rec_call env n lst a) && + (check_rec_call env n lst b) && + (List.for_all (check_rec_call env n lst) l) + + | IsLambda (x,a,b) -> + (check_rec_call env n lst a) && + (check_rec_call (push_rel_decl (x,outcast_type a) env) + (n+1) (map_lift_fst lst) b) && + (List.for_all (check_rec_call env n lst) l) + + | IsProd (x,a,b) -> + (check_rec_call env n lst a) && + (check_rec_call (push_rel_decl (x,outcast_type a) env) + (n+1) (map_lift_fst lst) b) && + (List.for_all (check_rec_call env n lst) l) + + | IsLetIn (x,a,b,c) -> + (check_rec_call env n lst a) && + (check_rec_call env n lst b) && + (check_rec_call (push_rel_def (x,a,outcast_type b) env) + (n+1) (map_lift_fst lst) c) && + (List.for_all (check_rec_call env n lst) l) | IsMutInd (_,la) -> - (array_for_all (check_rec_call n lst) la) && - (List.for_all (check_rec_call n lst) l) + (array_for_all (check_rec_call env n lst) la) && + (List.for_all (check_rec_call env n lst) l) | IsMutConstruct (_,la) -> - (array_for_all (check_rec_call n lst) la) && - (List.for_all (check_rec_call n lst) l) + (array_for_all (check_rec_call env n lst) la) && + (List.for_all (check_rec_call env n lst) l) | IsConst (_,la) -> - (array_for_all (check_rec_call n lst) la) && - (List.for_all (check_rec_call n lst) l) + (array_for_all (check_rec_call env n lst) la) && + (List.for_all (check_rec_call env n lst) l) | IsApp (f,la) -> - (check_rec_call n lst f) && - (array_for_all (check_rec_call n lst) la) && - (List.for_all (check_rec_call n lst) l) + (check_rec_call env n lst f) && + (array_for_all (check_rec_call env n lst) la) && + (List.for_all (check_rec_call env n lst) l) - | IsCoFix (i,(typarray,funnames,bodies)) -> + | IsCoFix (i,(typarray,funnames,bodies as recdef)) -> let nbfix = Array.length bodies in - (array_for_all (check_rec_call n lst) typarray) && - (List.for_all (check_rec_call n lst) l) && + let env' = push_rec_types recdef env in + (array_for_all (check_rec_call env n lst) typarray) && + (List.for_all (check_rec_call env n lst) l) && (array_for_all - (check_rec_call (n+nbfix) (map_lift_fst_n nbfix lst)) + (check_rec_call env' (n+nbfix) (map_lift_fst_n nbfix lst)) bodies) | IsEvar (_,la) -> - (array_for_all (check_rec_call n lst) la) && - (List.for_all (check_rec_call n lst) l) + (array_for_all (check_rec_call env n lst) la) && + (List.for_all (check_rec_call env n lst) l) | IsMeta _ -> true - | IsVar _ | IsSort _ -> List.for_all (check_rec_call n lst) l + | IsVar _ | IsSort _ -> List.for_all (check_rec_call env n lst) l - | IsXtra _ -> List.for_all (check_rec_call n lst) l + | IsXtra _ -> List.for_all (check_rec_call env n lst) l ) - + + and check_rec_call_fix_body env n lst decr recArgsDecrArg body = + if decr = 0 then + check_rec_call env n ((1,recArgsDecrArg)::lst) body + else + match kind_of_term body with + | IsLambda (x,a,b) -> + (check_rec_call env n lst a) & + (check_rec_call_fix_body + (push_rel_decl (x,outcast_type a) env) (n+1) + (map_lift_fst lst) (decr-1) recArgsDecrArg b) + | _ -> anomaly "Not enough abstractions in fix body" + in - check_rec_call 1 [] d) + check_rec_call env' 1 [] d) (* vargs is supposed to be built from A1;..Ak;[f1]..[fk][|d1;..;dk|] and vdeft is [|t1;..;tk|] such that f1:A1,..,fk:Ak |- di:ti @@ -641,7 +656,7 @@ nvect is [|n1;..;nk|] which gives for each recursive definition the inductive-decreasing index the function checks the convertibility of ti with Ai *) -let check_fix env sigma ((nvect,bodynum),(types,names,bodies)) = +let check_fix env sigma ((nvect,bodynum),(types,names,bodies as recdef)) = let nbfix = Array.length bodies in if nbfix = 0 or Array.length nvect <> nbfix @@ -652,7 +667,9 @@ let check_fix env sigma ((nvect,bodynum),(types,names,bodies)) = then anomaly "Ill-formed fix term"; for i = 0 to nbfix - 1 do try - let _ = check_subterm_rec_meta env sigma nvect nvect.(i) bodies.(i) in () + let fixenv = push_rec_types recdef env in + let _ = check_subterm_rec_meta fixenv sigma nvect nvect.(i) bodies.(i) + in () with FixGuardError err -> error_ill_formed_rec_body CCI env err (List.rev names) i bodies done @@ -662,21 +679,22 @@ let check_fix env sigma ((nvect,bodynum),(types,names,bodies)) = exception CoFixGuardError of guard_error let check_guard_rec_meta env sigma nbfix def deftype = - let rec codomain_is_coind c = + let rec codomain_is_coind env c = let b = whd_betadeltaiota env sigma (strip_outer_cast c) in match kind_of_term b with - | IsProd (_,a,b) -> codomain_is_coind b + | IsProd (x,a,b) -> + codomain_is_coind (push_rel_decl (x,outcast_type a) env) b | _ -> try - find_mcoinductype env sigma b + find_coinductive env sigma b with Induc -> raise (CoFixGuardError (CodomainNotInductiveType b)) in - let (mind, _) = codomain_is_coind deftype in + let (mind, _) = codomain_is_coind env deftype in let ((sp,tyi),_) = mind in - let lvlra = (mis_recargs (lookup_mind_specif mind env)) in + let lvlra = mis_recargs (lookup_mind_specif mind env) in let vlra = lvlra.(tyi) in - let rec check_rec_call alreadygrd n vlra t = + let rec check_rec_call env alreadygrd n vlra t = if noccur_with_meta n nbfix t then true else @@ -713,7 +731,7 @@ let check_guard_rec_meta env sigma nbfix def deftype = 'sTR "of recargs is being applied" >] | (Mrec i)::lrar -> let newvlra = lvlra.(i) in - (check_rec_call true n newvlra t) && + (check_rec_call env true n newvlra t) && (process_args_of_constr lr lrar) | (Imbr((sp,i) as ind_sp,lrc)::lrar) -> @@ -724,7 +742,7 @@ let check_guard_rec_meta env sigma nbfix def deftype = (List.map (instantiate_recarg sp lrc)) sprecargs.(i)) - in (check_rec_call true n lc t) & + in (check_rec_call env true n lc t) & (process_args_of_constr lr lrar) | _::lrar -> @@ -735,21 +753,24 @@ let check_guard_rec_meta env sigma nbfix def deftype = in (process_args_of_constr realargs lra) - | IsLambda (_,a,b) -> + | IsLambda (x,a,b) -> assert (args = []); if (noccur_with_meta n nbfix a) then - check_rec_call alreadygrd (n+1) vlra b + check_rec_call (push_rel_decl (x,outcast_type a) env) + alreadygrd (n+1) vlra b else raise (CoFixGuardError (RecCallInTypeOfAbstraction t)) - | IsCoFix (j,(varit,lna,vdefs)) -> + | IsCoFix (j,(varit,lna,vdefs as recdef)) -> if (List.for_all (noccur_with_meta n nbfix) args) then let nbfix = Array.length vdefs in if (array_for_all (noccur_with_meta n nbfix) varit) then - (array_for_all (check_rec_call alreadygrd (n+1) vlra) vdefs) + let env' = push_rec_types recdef env in + (array_for_all + (check_rec_call env' alreadygrd (n+1) vlra) vdefs) && - (List.for_all (check_rec_call alreadygrd (n+1) vlra) args) + (List.for_all (check_rec_call env alreadygrd (n+1) vlra) args) else raise (CoFixGuardError (RecCallInTypeOfDef c)) else @@ -759,7 +780,7 @@ let check_guard_rec_meta env sigma nbfix def deftype = if (noccur_with_meta n nbfix p) then if (noccur_with_meta n nbfix tm) then if (List.for_all (noccur_with_meta n nbfix) args) then - (array_for_all (check_rec_call alreadygrd n vlra) vrest) + (array_for_all (check_rec_call env alreadygrd n vlra) vrest) else raise (CoFixGuardError (RecCallInCaseFun c)) else @@ -770,16 +791,18 @@ let check_guard_rec_meta env sigma nbfix def deftype = | _ -> raise (CoFixGuardError NotGuardedForm) in - check_rec_call false 1 vlra def + check_rec_call env false 1 vlra def (* The function which checks that the whole block of definitions satisfies the guarded condition *) -let check_cofix env sigma (bodynum,(types,names,bodies)) = +let check_cofix env sigma (bodynum,(types,names,bodies as recdef)) = let nbfix = Array.length bodies in for i = 0 to nbfix-1 do try - let _ = check_guard_rec_meta env sigma nbfix bodies.(i) types.(i) in () + let fixenv = push_rec_types recdef env in + let _ = check_guard_rec_meta fixenv sigma nbfix bodies.(i) types.(i) + in () with CoFixGuardError err -> error_ill_formed_rec_body CCI env err (List.rev names) i bodies done -- cgit v1.2.3