(* $Id$ *) open Pp open Util open Names open Univ open Term open Declarations open Sign open Environ open Reduction open Inductive open Type_errors let make_judge v tj = { uj_val = v; uj_type = tj } let j_val j = j.uj_val (* This should be a type intended to be assumed *) let assumption_of_judgment env sigma j = match kind_of_term(whd_betadeltaiota env sigma (body_of_type j.uj_type)) with | IsSort s -> j.uj_val | _ -> error_assumption CCI env j.uj_val (* let aojkey = Profile.declare_profile "assumption_of_judgment";; let assumption_of_judgment env sigma j = Profile.profile3 aojkey assumption_of_judgment env sigma j;; *) (* This should be a type (a priori without intension to be an assumption) *) let type_judgment env sigma j = match kind_of_term(whd_betadeltaiota env sigma (body_of_type j.uj_type)) with | IsSort s -> {utj_val = j.uj_val; utj_type = s } | _ -> error_not_type CCI env j (* Type of a de Bruijn index. *) let relative env sigma n = try let (_,typ) = lookup_rel_type n env in { uj_val = mkRel n; uj_type = type_app (lift n) typ } with Not_found -> error_unbound_rel CCI env sigma n (* let relativekey = Profile.declare_profile "relative";; let relative env sigma n = Profile.profile3 relativekey relative env sigma n;; *) (* Management of context of variables. *) (* Checks if a context of variable is included in another one. *) (* let rec hyps_inclusion env sigma sign1 sign2 = if sign1 = empty_named_context then true else let (id1,ty1) = hd_sign sign1 in let rec search sign2 = if sign2 = empty_named_context then false else let (id2,ty2) = hd_sign sign2 in if id1 = id2 then (is_conv env sigma (body_of_type ty1) (body_of_type ty2)) & hyps_inclusion env sigma (tl_sign sign1) (tl_sign sign2) else search (tl_sign sign2) in search sign2 *) (* Checks if the given context of variables [hyps] is included in the current context of [env]. *) (* let check_hyps id env sigma hyps = let hyps' = named_context env in if not (hyps_inclusion env sigma hyps hyps') then error_reference_variables CCI env id *) (* Instantiation of terms on real arguments. *) let type_of_constant = Instantiate.constant_type (* let tockey = Profile.declare_profile "type_of_constant";; let type_of_constant env sigma c = Profile.profile3 tockey type_of_constant env sigma c;; *) (* Inductive types. *) let type_of_inductive env sigma i = (* TODO: check args *) mis_arity (lookup_mind_specif i env) (* let toikey = Profile.declare_profile "type_of_inductive";; let type_of_inductive env sigma i = Profile.profile3 toikey type_of_inductive env sigma i;; *) (* Constructors. *) let type_of_constructor env sigma cstr = mis_constructor_type (index_of_constructor cstr) (lookup_mind_specif (inductive_of_constructor cstr) env) (* let tockey = Profile.declare_profile "type_of_constructor";; let type_of_constructor env sigma cstr = Profile.profile3 tockey type_of_constructor env sigma cstr;; *) let type_of_existential env sigma ev = Instantiate.existential_type sigma ev (* Case. *) let rec mysort_of_arity env sigma c = match kind_of_term (whd_betadeltaiota env sigma c) with | IsSort s -> s | IsProd(_,_,c2) -> mysort_of_arity env sigma c2 | _ -> invalid_arg "mysort_of_arity" let error_elim_expln env sigma kp ki = if is_info_arity env sigma kp && not (is_info_arity env sigma ki) then "non-informative objects may not construct informative ones." else match (kind_of_term kp,kind_of_term ki) with | IsSort (Type _), IsSort (Prop _) -> "strong elimination on non-small inductive types leads to paradoxes." | _ -> "wrong arity" exception Arity of (constr * constr * string) option let is_correct_arity env sigma kelim (c,p) indf (pt,t) = let rec srec (pt,t) = let pt' = whd_betadeltaiota env sigma pt in let t' = whd_betadeltaiota env sigma t in match kind_of_term pt', kind_of_term t' with | IsProd (_,a1,a2), IsProd (_,a1',a2') -> if is_conv env sigma a1 a1' then srec (a2,a2') else raise (Arity None) | IsProd (_,a1,a2), _ -> let k = whd_betadeltaiota env sigma a2 in let ksort = (match kind_of_term k with IsSort s -> s | _ -> raise (Arity None)) in let ind = build_dependent_inductive indf in if is_conv env sigma a1 ind then if List.exists (base_sort_cmp CONV ksort) kelim then (true,k) else raise (Arity (Some(k,t',error_elim_expln env sigma k t'))) else raise (Arity None) | k, IsProd (_,_,_) -> raise (Arity None) | k, ki -> let ksort = (match k with IsSort s -> s | _ -> raise (Arity None)) in if List.exists (base_sort_cmp CONV ksort) kelim then false, pt' else raise (Arity (Some(pt',t',error_elim_expln env sigma pt' t'))) in try srec (pt,t) with Arity kinds -> let listarity = (List.map (make_arity env true indf) kelim) @(List.map (make_arity env false indf) kelim) in let ind = mis_inductive (fst (dest_ind_family indf)) in error_elim_arity CCI env ind listarity c p pt kinds let find_case_dep_nparams env sigma (c,p) (IndFamily (mis,_) as indf) typP = let kelim = mis_kelim mis in let arsign,s = get_arity indf in let glob_t = it_mkProd_or_LetIn (mkSort s) arsign in let (dep,_) = is_correct_arity env sigma kelim (c,p) indf (typP,glob_t) in dep (* type_case_branches type un

Case c of ... end IndType (indf,realargs) = type de c pt = sorte de p type_case_branches retourne (lb, lr); lb est le vecteur des types attendus dans les branches du Case; lr est le type attendu du resultat *) let type_case_branches env sigma (IndType (indf,realargs)) pt p c = let dep = find_case_dep_nparams env sigma (c,p) indf pt in let constructs = get_constructors indf in let lc = Array.map (build_branch_type env dep p) constructs in if dep then (lc, beta_applist (p,(realargs@[c]))) else (lc, beta_applist (p,realargs)) let check_branches_message env sigma (c,ct) (explft,lft) = let expn = Array.length explft and n = Array.length lft in if n<>expn then error_number_branches CCI env c ct expn; for i = 0 to n-1 do if not (is_conv_leq env sigma lft.(i) (explft.(i))) then error_ill_formed_branch CCI env c i (nf_betaiota env sigma lft.(i)) (nf_betaiota env sigma explft.(i)) done let type_of_case env sigma ci pj cj lfj = let lft = Array.map (fun j -> body_of_type j.uj_type) lfj in let indspec = try find_rectype env sigma (body_of_type cj.uj_type) with Induc -> error_case_not_inductive CCI env cj.uj_val (body_of_type cj.uj_type) in let (bty,rslty) = type_case_branches env sigma indspec (body_of_type pj.uj_type) pj.uj_val cj.uj_val in let kind = mysort_of_arity env sigma (body_of_type pj.uj_type) in check_branches_message env sigma (cj.uj_val,body_of_type cj.uj_type) (bty,lft); { uj_val = mkMutCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj); uj_type = rslty } (* let tocasekey = Profile.declare_profile "type_of_case";; let type_of_case env sigma ci pj cj lfj = Profile.profile6 tocasekey type_of_case env sigma ci pj cj lfj;; *) (* Prop and Set *) let judge_of_prop = { uj_val = mkSort prop; uj_type = mkSort type_0 } let judge_of_set = { uj_val = mkSort spec; uj_type = mkSort type_0 } let judge_of_prop_contents = function | Null -> judge_of_prop | Pos -> judge_of_set (* Type of Type(i). *) let judge_of_type u = let (uu,uuu,c) = super_super u in { uj_val = mkSort (Type u); uj_type = mkSort (Type uu) }, c let type_of_sort c = match kind_of_term c with | IsSort (Type u) -> let (uu,cst) = super u in Type uu, cst | IsSort (Prop _) -> Type prop_univ, Constraint.empty | _ -> invalid_arg "type_of_sort" (* Type of a lambda-abstraction. *) let sort_of_product domsort rangsort g = match rangsort with (* Product rule (s,Prop,Prop) *) | Prop _ -> rangsort, Constraint.empty | Type u2 -> (match domsort with (* Product rule (Prop,Type_i,Type_i) *) | Prop _ -> rangsort, Constraint.empty (* Product rule (Type_i,Type_i,Type_i) *) | Type u1 -> let (u12,cst) = sup u1 u2 g in Type u12, cst) (* [abs_rel env sigma name var j] implements the rule env, name:typ |- j.uj_val:j.uj_type env, |- (name:typ)j.uj_type : s ----------------------------------------------------------------------- env |- [name:typ]j.uj_val : (name:typ)j.uj_type Since all products are defined in the Calculus of Inductive Constructions and no upper constraint exists on the sort $s$, we don't need to compute $s$ *) let abs_rel env sigma name var j = { uj_val = mkLambda (name, var, j.uj_val); uj_type = mkProd (name, var, j.uj_type) }, Constraint.empty (* [gen_rel env sigma name (typ1,s1) (typ2,s2)] implements the rule env |- typ1:s1 env, name:typ |- typ2 : s2 ------------------------------------------------------------------------- s' >= (s1,s2), env |- (name:typ)j.uj_val : s' where j.uj_type is convertible to a sort s2 *) let gen_rel env sigma name t1 t2 = let (s,g) = sort_of_product t1.utj_type t2.utj_type (universes env) in { uj_val = mkProd (name, t1.utj_val, t2.utj_val); uj_type = mkSort s }, g (* [cast_rel env sigma (typ1,s1) j] implements the rule env, sigma |- cj.uj_val:cj.uj_type cst, env, sigma |- cj.uj_type = t --------------------------------------------------------------------- cst, env, sigma |- cj.uj_val:t *) let cast_rel env sigma cj t = try let cst = conv_leq env sigma (body_of_type cj.uj_type) t in { uj_val = j_val cj; uj_type = t }, cst with NotConvertible -> error_actual_type CCI env cj.uj_val (body_of_type cj.uj_type) t (* Type of an application. *) let apply_rel_list env sigma nocheck argjl funj = let rec apply_rec n typ cst = function | [] -> { uj_val = applist (j_val funj, List.map j_val argjl); uj_type = type_app (fun _ -> typ) funj.uj_type }, cst | hj::restjl -> match kind_of_term (whd_betadeltaiota env sigma typ) with | IsProd (_,c1,c2) -> if nocheck then apply_rec (n+1) (subst1 hj.uj_val c2) cst restjl else (try let c = conv_leq env sigma (body_of_type hj.uj_type) c1 in let cst' = Constraint.union cst c in apply_rec (n+1) (subst1 hj.uj_val c2) cst' restjl with NotConvertible -> error_cant_apply_bad_type CCI env sigma (n,c1,body_of_type hj.uj_type) funj argjl) | _ -> error_cant_apply_not_functional CCI env funj argjl in apply_rec 1 (body_of_type funj.uj_type) Constraint.empty argjl (* let applykey = Profile.declare_profile "apply_rel_list";; let apply_rel_list env sigma nocheck argjl funj = Profile.profile5 applykey apply_rel_list env sigma nocheck argjl funj;; *) (* Fixpoints. *) (* Check if t is a subterm of Rel n, and gives its specification, assuming lst already gives index of subterms with corresponding specifications of recursive arguments *) (* A powerful notion of subterm *) let find_sorted_assoc p = let rec findrec = function | (a,ta)::l -> if a < p then findrec l else if a = p then ta else raise Not_found | _ -> raise Not_found in findrec let map_lift_fst_n m = List.map (function (n,t)->(n+m,t)) let map_lift_fst = map_lift_fst_n 1 let rec instantiate_recarg sp lrc ra = match ra with | Mrec(j) -> Imbr((sp,j),lrc) | Imbr(ind_sp,l) -> Imbr(ind_sp, List.map (instantiate_recarg sp lrc) l) | Norec -> Norec | Param(k) -> List.nth lrc k (* To each inductive definition corresponds an array describing the structure of recursive arguments for each constructor, we call it the recursive spec of the type (it has type recargs vect). For checking the guard, we start from the decreasing argument (Rel n) with its recursive spec. During checking the guardness condition, we collect patterns variables corresponding to subterms of n, each of them with its recursive spec. They are organised in a list lst of type (int * recargs) list which is sorted with respect to the first argument. *) (* f is a function of type env -> int -> (int * recargs) list -> constr -> 'a c is a branch of an inductive definition corresponding to the spec lrec. mind_recvec is the recursive spec of the inductive definition of the decreasing argument n. check_term env mind_recvec f n lst (lrec,c) will pass the lambdas of c corresponding to pattern variables and collect possibly new subterms variables and apply f to the body of the branch with the correct env and decreasing arg. *) let check_term env mind_recvec f = let rec crec env n lst (lrec,c) = let c' = strip_outer_cast c in match lrec, kind_of_term c' with (ra::lr,IsLambda (x,a,b)) -> let lst' = map_lift_fst lst and env' = push_rel_assum (x,a) env and n'=n+1 in begin match ra with Mrec(i) -> crec env' n' ((1,mind_recvec.(i))::lst') (lr,b) | Imbr((sp,i) as ind_sp,lrc) -> 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 env' n' ((1,lc)::lst') (lr,b) | _ -> crec env' n' lst' (lr,b) end | (_,_) -> f env n lst c' in crec env (* c is supposed to be in beta-delta-iota head normal form *) let is_inst_var k c = match kind_of_term (fst (decomp_app c)) with | IsRel n -> n=k | _ -> false (* is_subterm_specif env sigma lcx mind_recvec n lst c n is the principal arg and has recursive spec lcx, lst is the list of subterms of n with spec. is_subterm_specif should test if c is a subterm of n and fails with Not_found if not. In case it is, it should send its recursive specification. This recursive spec should be the same size as the number of constructors of the type of c. A problem occurs when c is built by contradiction. In that case no spec is given. *) let is_subterm_specif env sigma lcx mind_recvec = 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 -> Some (find_sorted_assoc k lst) | IsMutCase ( _,_,c,br) -> if Array.length br = 0 then None else let def = Array.create (Array.length br) [] in let lcv = (try if is_inst_var n c then lcx else match crec env n lst c with Some lr -> lr | None -> def with Not_found -> def) in assert (Array.length br = Array.length lcv); let stl = array_map2 (fun lc a -> check_term env mind_recvec crec n lst (lc,a)) lcv br in let stl0 = stl.(0) in if array_for_all (fun st -> st=stl0) stl then stl0 else None | 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 sign,strippedBody = decompose_lam_n_assum (decrArg+1) theBody in let nbOfAbst = nbfix+decrArg+1 in (* when proving that the fixpoint f(x)=e is less than n, it is enough to prove that e is less than n assuming f is less than n furthermore when f is applied to a term which is strictly less than n, one may assume that x itself is strictly less than n *) let newlst = let lst' = (nbOfAbst,lcx) :: (map_lift_fst_n nbOfAbst lst) in if List.length l < (decrArg+1) then lst' else let theDecrArg = List.nth l decrArg in try match crec env n lst theDecrArg with (Some recArgsDecrArg) -> (1,recArgsDecrArg) :: lst' | None -> lst' with Not_found -> lst' in let env' = push_rec_types recdef env in let env'' = push_rels sign env' in crec env'' (n+nbOfAbst) newlst strippedBody | IsLambda (x,a,b) when l=[] -> let lst' = map_lift_fst lst in crec (push_rel_assum (x, a) env) (n+1) lst' b (*** Experimental change *************************) | IsMeta _ -> None | _ -> raise Not_found in crec env let spec_subterm_strict env sigma lcx mind_recvec n lst c nb = try match is_subterm_specif env sigma lcx mind_recvec n lst c with Some lr -> lr | None -> Array.create nb [] with Not_found -> Array.create nb [] let spec_subterm_large env sigma lcx mind_recvec n lst c nb = if is_inst_var n c then lcx else spec_subterm_strict env sigma lcx mind_recvec n lst c nb let is_subterm env sigma lcx mind_recvec n lst c = try let _ = is_subterm_specif env sigma lcx mind_recvec n lst c in true with Not_found -> false exception FixGuardError of guard_error (* Auxiliary function: it checks a condition f depending on a deBrujin index for a certain number of abstractions *) let rec check_subterm_rec_meta env sigma vectn k def = (* If k<0, it is a general fixpoint *) (k < 0) or (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 env n def = match kind_of_term (strip_outer_cast def) with | IsLambda (x,a,b) -> if noccur_with_meta n nfi a then let env' = push_rel_assum (x, 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 (env',c,d) = check_occur env 1 def in let ((sp,tyi),_ as mind, largs) = try find_inductive env' sigma c with Induc -> raise (FixGuardError RecursionNotOnInductiveType) 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 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 *) (let f,l = whd_betaiota_stack t in match kind_of_term f with | IsRel p -> if n+k+1 <= p & p < n+k+nfi+1 then (* recursive call *) let glob = nfi+n+k-p in (* the index of the recursive call *) let np = vectn.(glob) in (* the decreasing arg of the rec call *) if List.length l > np then (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 env n lst) (la@lrest) else raise (FixGuardError RecursionOnIllegalTerm) | _ -> assert false) else raise (FixGuardError NotEnoughArgumentsForFixCall) else List.for_all (check_rec_call env n lst) l | IsMutCase (ci,p,c_0,lrest) -> let lc = spec_subterm_large env sigma lcx mind_recvec n lst c_0 (Array.length lrest) in (array_for_all2 (fun c0 a -> check_term env mind_recvec check_rec_call n lst (c0,a)) lc lrest) && (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 : if - g = Fix g/1 := [y1:T1]...[yp:Tp]e & - f is guarded with respect to the set of pattern variables S in a1 ... am & - f is guarded with respect to the set of pattern variables S in T1 ... Tp & - ap is a sub-term of the formal argument of f & - f is guarded with respect to the set of pattern variables S+{yp} in e then f is guarded with respect to S in (g a1 ... am). Eduardo 7/9/98 *) | IsFix ((recindxs,i),(typarray,funnames,bodies as recdef)) -> (List.for_all (check_rec_call env n lst) l) && (array_for_all (check_rec_call env n lst) typarray) && let nbfix = List.length funnames in let decrArg = recindxs.(i) and env' = push_rec_types recdef env and n' = n+nbfix and lst' = map_lift_fst_n nbfix lst in if (List.length l < (decrArg+1)) then array_for_all (check_rec_call env' n' lst') bodies else let theDecrArg = List.nth l decrArg in begin try match is_subterm_specif env sigma lcx mind_recvec n lst theDecrArg with Some recArgsDecrArg -> let theBody = bodies.(i) in check_rec_call_fix_body env' n' lst' (decrArg+1) recArgsDecrArg theBody | None -> array_for_all (check_rec_call env' n' lst') bodies with Not_found -> array_for_all (check_rec_call env' n' lst') bodies end | IsCast (a,b) -> (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_assum (x, 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_assum (x, a) env) (n+1) (map_lift_fst lst) b) && (List.for_all (check_rec_call env n lst) l) | IsLetIn (x,a,b,c) as cst -> (try (check_rec_call env n lst a) && (check_rec_call env n lst b) && (check_rec_call (push_rel_def (x,a, b) env) (n+1) (map_lift_fst lst) c) && (List.for_all (check_rec_call env n lst) l) with (FixGuardError NotEnoughArgumentsForFixCall) as e -> check_rec_call env n lst (whd_betadeltaiota env sigma t) ) | IsMutInd (_,la) -> (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 env n lst) la) && (List.for_all (check_rec_call env n lst) l) | IsConst (sp,la) as c -> (try (array_for_all (check_rec_call env n lst) la) && (List.for_all (check_rec_call env n lst) l) with (FixGuardError _ ) as e -> if evaluable_constant env sp then check_rec_call env n lst (whd_betadeltaiota env sigma t) else raise e) | IsApp (f,la) -> (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 as recdef)) -> let nbfix = Array.length bodies in 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 env' (n+nbfix) (map_lift_fst_n nbfix lst)) bodies) | IsEvar (_,la) -> (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 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_assum (x, a) env) (n+1) (map_lift_fst lst) (decr-1) recArgsDecrArg b) | _ -> anomaly "Not enough abstractions in fix body" in 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 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 as recdef)) = let nbfix = Array.length bodies in if nbfix = 0 or Array.length nvect <> nbfix or Array.length types <> nbfix or List.length names <> nbfix or bodynum < 0 or bodynum >= nbfix then anomaly "Ill-formed fix term"; for i = 0 to nbfix - 1 do try 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 (* let cfkey = Profile.declare_profile "check_fix";; let check_fix env sigma fix = Profile.profile3 cfkey check_fix env sigma fix;; *) (* Co-fixpoints. *) exception CoFixGuardError of guard_error let check_guard_rec_meta env sigma nbfix def deftype = 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 (x,a,b) -> codomain_is_coind (push_rel_assum (x, a) env) b | _ -> try find_coinductive env sigma b with Induc -> raise (CoFixGuardError (CodomainNotInductiveType b)) 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 vlra = lvlra.(tyi) in let rec check_rec_call env alreadygrd n vlra t = if noccur_with_meta n nbfix t then true else let c,args = whd_betadeltaiota_stack env sigma t in match kind_of_term c with | IsMeta _ -> true | IsRel p -> if n <= p && p < n+nbfix then (* recursive call *) if alreadygrd then if List.for_all (noccur_with_meta n nbfix) args then true else raise (CoFixGuardError NestedRecursiveOccurrences) else raise (CoFixGuardError (UnguardedRecursiveCall t)) else error "check_guard_rec_meta: ???" (* ??? *) | IsMutConstruct ((_,i as cstr_sp),l) -> let lra =vlra.(i-1) in let mI = inductive_of_constructor (cstr_sp,l) in let mis = lookup_mind_specif mI env in let _,realargs = list_chop (mis_nparams mis) args in let rec process_args_of_constr l lra = match l with | [] -> true | t::lr -> (match lra with | [] -> anomalylabstrm "check_guard_rec_meta" [< 'sTR "a constructor with an empty list"; 'sTR "of recargs is being applied" >] | (Mrec i)::lrar -> let newvlra = lvlra.(i) in (check_rec_call env true n newvlra t) && (process_args_of_constr lr lrar) | (Imbr((sp,i) as ind_sp,lrc)::lrar) -> let mis = lookup_mind_specif (ind_sp,[||]) env in let sprecargs = mis_recargs mis in let lc = (Array.map (List.map (instantiate_recarg sp lrc)) sprecargs.(i)) in (check_rec_call env true n lc t) & (process_args_of_constr lr lrar) | _::lrar -> if (noccur_with_meta n nbfix t) then (process_args_of_constr lr lrar) else raise (CoFixGuardError (RecCallInNonRecArgOfConstructor t))) in (process_args_of_constr realargs lra) | IsLambda (x,a,b) -> assert (args = []); if (noccur_with_meta n nbfix a) then check_rec_call (push_rel_assum (x, a) env) alreadygrd (n+1) vlra b else raise (CoFixGuardError (RecCallInTypeOfAbstraction t)) | 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 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 env alreadygrd (n+1) vlra) args) else raise (CoFixGuardError (RecCallInTypeOfDef c)) else raise (CoFixGuardError (UnguardedRecursiveCall c)) | IsMutCase (_,p,tm,vrest) -> 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 env alreadygrd n vlra) vrest) else raise (CoFixGuardError (RecCallInCaseFun c)) else raise (CoFixGuardError (RecCallInCaseArg c)) else raise (CoFixGuardError (RecCallInCasePred c)) | _ -> raise (CoFixGuardError NotGuardedForm) in 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 as recdef)) = let nbfix = Array.length bodies in for i = 0 to nbfix-1 do try 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 (* Checks the type of a (co)fixpoint. Fix and CoFix are typed the same way; only the guard condition differs. *) exception IllBranch of int let type_fixpoint env sigma lna lar vdefj = let lt = Array.length vdefj in assert (Array.length lar = lt); try conv_forall2_i (fun i env sigma def ar -> try conv_leq env sigma def (lift lt ar) with NotConvertible -> raise (IllBranch i)) env sigma (Array.map (fun j -> body_of_type j.uj_type) vdefj) (Array.map body_of_type lar) with IllBranch i -> error_ill_typed_rec_body CCI env i lna vdefj lar (* A function which checks that a term well typed verifies both syntaxic conditions *) let control_only_guard env sigma = let rec control_rec c = match kind_of_term c with | IsRel _ | IsVar _ -> () | IsSort _ | IsMeta _ -> () | IsCoFix (_,(tys,_,bds) as cofix) -> check_cofix env sigma cofix; Array.iter control_rec tys; Array.iter control_rec bds; | IsFix (_,(tys,_,bds) as fix) -> check_fix env sigma fix; Array.iter control_rec tys; Array.iter control_rec bds; | IsMutCase(_,p,c,b) ->control_rec p;control_rec c;Array.iter control_rec b | IsMutInd (_,cl) -> Array.iter control_rec cl | IsMutConstruct (_,cl) -> Array.iter control_rec cl | IsConst (_,cl) -> Array.iter control_rec cl | IsEvar (_,cl) -> Array.iter control_rec cl | IsApp (_,cl) -> Array.iter control_rec cl | IsCast (c1,c2) -> control_rec c1; control_rec c2 | IsProd (_,c1,c2) -> control_rec c1; control_rec c2 | IsLambda (_,c1,c2) -> control_rec c1; control_rec c2 | IsLetIn (_,c1,c2,c3) -> control_rec c1; control_rec c2; control_rec c3 in control_rec