From 15ed739c91a22e91ae88d54215f6862fc1074a88 Mon Sep 17 00:00:00 2001 From: filliatr Date: Thu, 26 Aug 1999 12:29:28 +0000 Subject: mach -> typing; machops -> typeops git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@27 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/typeops.ml | 909 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 909 insertions(+) create mode 100644 kernel/typeops.ml (limited to 'kernel/typeops.ml') diff --git a/kernel/typeops.ml b/kernel/typeops.ml new file mode 100644 index 0000000000..23bac0b277 --- /dev/null +++ b/kernel/typeops.ml @@ -0,0 +1,909 @@ + +(* $Id$ *) + +open Pp +open Util +open Names +open Univ +open Generic +open Term +open Evd +open Constant +open Inductive +open Sign +open Environ +open Reduction +open Instantiate +open Type_errors + +let make_judge v tj = + { uj_val = v; + uj_type = tj.body; + uj_kind= DOP0 (Sort tj.typ) } + +let j_val_only j = j.uj_val +(* Faut-il caster ? *) +let j_val = j_val_only + +let j_val_cast j = mkCast j.uj_val j.uj_type + +let typed_type_of_judgment env j = + match whd_betadeltaiota env j.uj_type with + | DOP0(Sort s) -> { body = j.uj_val; typ = s } + | _ -> error_not_type CCI env j.uj_val + +let assumption_of_judgement env j = + match whd_betadeltaiota env j.uj_type with + | DOP0(Sort s) -> { body = j.uj_val; typ = s } + | _ -> error_assumption CCI env j.uj_val + +(* Type of a de Bruijn index. *) + +let relative env n = + try + let (_,typ) = lookup_rel n env in + { uj_val = Rel n; + uj_type = lift n typ.body; + uj_kind = DOP0 (Sort typ.typ) } + with Not_found -> + error_unbound_rel CCI env n + +(* Management of context of variables. *) + +(* Checks if a context of variable is included in another one. *) + +let hyps_inclusion env (idl1,tyl1) (idl2,tyl2) = + let rec aux = function + | ([], [], _, _) -> true + | (_, _, [], []) -> false + | ((id1::idl1), (ty1::tyl1), idl2, tyl2) -> + let rec search = function + | ([], []) -> false + | ((id2::idl2), (ty2::tyl2)) -> + if id1 = id2 then + (is_conv env (body_of_type ty1) (body_of_type ty2)) + & aux (idl1,tyl1,idl2,tyl2) + else + search (idl2,tyl2) + | (_, _) -> invalid_arg "hyps_inclusion" + in + search (idl2,tyl2) + | (_, _, _, _) -> invalid_arg "hyps_inclusion" + in + aux (idl1,tyl1,idl2,tyl2) + +(* Checks if the given context of variables [hyps] is included in the + current context of [env]. *) + +let construct_reference id env hyps = + let hyps' = get_globals (context env) in + if hyps_inclusion env hyps hyps' then + Array.of_list (List.map (fun id -> VAR id) (ids_of_sign hyps)) + else + error_reference_variables CCI env id + +let check_hyps id env hyps = + let hyps' = get_globals (context env) in + if not (hyps_inclusion env hyps hyps') then + error_reference_variables CCI env id + +(* Instantiation of terms on real arguments. *) + +let type_of_constant env c = + let (sp,args) = destConst c in + let cb = lookup_constant sp env in + let hyps = cb.const_hyps in + check_hyps (basename sp) env hyps; + instantiate_type (ids_of_sign hyps) cb.const_type (Array.to_list args) + +(* Existentials. *) + +let type_of_existential env c = + let (sp,args) = destConst c in + let info = Evd.map (evar_map env) sp in + let hyps = info.evar_hyps in + check_hyps (basename sp) env hyps; + instantiate_type (ids_of_sign hyps) info.evar_concl (Array.to_list args) + +(* Constants or existentials. *) + +let type_of_constant_or_existential env c = + if is_existential c then + type_of_existential env c + else + type_of_constant env c + +(* Inductive types. *) + +let instantiate_arity mis = + let ids = ids_of_sign mis.mis_mib.mind_hyps in + let args = Array.to_list mis.mis_args in + let arity = mis.mis_mip.mind_arity in + { body = instantiate_constr ids arity.body args; + typ = arity.typ } + +let type_of_inductive env i = + let mis = lookup_mind_specif i env in + let hyps = mis.mis_mib.mind_hyps in + check_hyps (basename mis.mis_sp) env hyps; + instantiate_arity mis + +(* Constructors. *) + +let instantiate_lc mis = + let hyps = mis.mis_mib.mind_hyps in + let lc = mis.mis_mip.mind_lc in + instantiate_constr (ids_of_sign hyps) lc (Array.to_list mis.mis_args) + +let type_of_constructor env c = + let (sp,i,j,args) = destMutConstruct c in + let mind = DOPN (MutInd (sp,i), args) in + let recmind = check_mrectype_spec env mind in + let mis = lookup_mind_specif recmind env in + check_hyps (basename mis.mis_sp) env (mis.mis_mib.mind_hyps); + let specif = instantiate_lc mis in + let make_ik k = DOPN (MutInd (mis.mis_sp,k), mis.mis_args) in + if j > mis_nconstr mis then + anomaly "type_of_constructor" + else + sAPPViList (j-1) specif (list_tabulate make_ik (mis_ntypes mis)) + +(* gives the vector of constructors and of + types of constructors of an inductive definition + correctly instanciated *) + +let mis_type_mconstructs mis = + let specif = instantiate_lc mis + and ntypes = mis_ntypes mis + and nconstr = mis_nconstr mis in + let make_ik k = DOPN (MutInd (mis.mis_sp,k), mis.mis_args) + and make_ck k = + DOPN (MutConstruct ((mis.mis_sp,mis.mis_tyi),k+1), mis.mis_args) + in + (Array.init nconstr make_ck, + sAPPVList specif (list_tabulate make_ik ntypes)) + +let type_mconstructs env mind = + let redmind = check_mrectype_spec env mind in + let mis = lookup_mind_specif redmind env in + mis_type_mconstructs mis + +(* Case. *) + +let rec sort_of_arity env c = + match whd_betadeltaiota env c with + | DOP0(Sort( _)) as c' -> c' + | DOP2(Prod,_,DLAM(_,c2)) -> sort_of_arity env c2 + | _ -> invalid_arg "sort_of_arity" + +let make_arity_dep env k = + let rec mrec c m = match whd_betadeltaiota env c with + | DOP0(Sort _) -> mkArrow m k + | DOP2(Prod,b,DLAM(n,c_0)) -> + prod_name env (n,b,mrec c_0 (applist(lift 1 m,[Rel 1]))) + | _ -> invalid_arg "make_arity_dep" + in + mrec + +let make_arity_nodep env k = + let rec mrec c = match whd_betadeltaiota env c with + | DOP0(Sort _) -> k + | DOP2(Prod,b,DLAM(x,c_0)) -> DOP2(Prod,b,DLAM(x,mrec c_0)) + | _ -> invalid_arg "make_arity_nodep" + in + mrec + +let error_elim_expln env kp ki = + if is_info_sort env kp && not (is_info_sort env ki) then + "non-informative objects may not construct informative ones." + else + match (kp,ki) with + | (DOP0(Sort (Type _)), DOP0(Sort (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 kd kn (c,p) = + let rec srec ind (pt,t) = + try + (match whd_betadeltaiota env pt, whd_betadeltaiota env t with + | DOP2(Prod,a1,DLAM(_,a2)), DOP2(Prod,a1',DLAM(_,a2')) -> + if is_conv env a1 a1' then + srec (applist(lift 1 ind,[Rel 1])) (a2,a2') + else + raise (Arity None) + | DOP2(Prod,a1,DLAM(_,a2)), ki -> + let k = whd_betadeltaiota env a2 in + let ksort = (match k with DOP0(Sort s) -> s + | _ -> raise (Arity None)) in + if is_conv env a1 ind then + if List.exists (base_sort_cmp CONV ksort) kd then + (true,k) + else + raise (Arity (Some(k,ki,error_elim_expln env k ki))) + else + raise (Arity None) + | k, DOP2(Prod,_,_) -> + raise (Arity None) + | k, ki -> + let ksort = (match k with DOP0(Sort s) -> s + | _ -> raise (Arity None)) in + if List.exists (base_sort_cmp CONV ksort) kn then + false,k + else + raise (Arity (Some(k,ki,error_elim_expln env k ki)))) + with Arity kinds -> + let listarity = + (List.map (fun s -> make_arity_dep env (DOP0(Sort s)) t ind) kd) + @(List.map (fun s -> make_arity_nodep env (DOP0(Sort s)) t) kn) + in error_elim_arity CCI env ind listarity c p pt kinds + in srec + +let cast_instantiate_arity mis = + let tty = instantiate_arity mis in + DOP2 (Cast, tty.body, DOP0 (Sort tty.typ)) + +let find_case_dep_nparams env (c,p) (mind,largs) typP = + let mis = lookup_mind_specif mind env in + let nparams = mis_nparams mis + and kd = mis_kd mis + and kn = mis_kn mis + and t = cast_instantiate_arity mis in + let (globargs,la) = list_chop nparams largs in + let glob_t = hnf_prod_applist env "find_elim_boolean" t globargs in + let arity = applist(mind,globargs) in + let (dep,_) = is_correct_arity env kd kn (c,p) arity (typP,glob_t) in + (dep, (nparams, globargs,la)) + +let type_one_branch_dep (env,nparams,globargs,p) co t = + let rec typrec n c = + match whd_betadeltaiota env c with + | DOP2(Prod,a1,DLAM(x,a2)) -> prod_name env (x,a1,typrec (n+1) a2) + | x -> let lAV = destAppL (ensure_appl x) in + let (_,vargs) = array_chop (nparams+1) lAV in + applist + (appvect ((lift n p),vargs), + [applist(co,((List.map (lift n) globargs)@(rel_list 0 n)))]) + in + typrec 0 (hnf_prod_applist env "type_case" t globargs) + +let type_one_branch_nodep (env,nparams,globargs,p) t = + let rec typrec n c = + match whd_betadeltaiota env c with + | DOP2(Prod,a1,DLAM(x,a2)) -> DOP2(Prod,a1,DLAM(x,typrec (n+1) a2)) + | x -> let lAV = destAppL(ensure_appl x) in + let (_,vargs) = array_chop (nparams+1) lAV in + appvect (lift n p,vargs) + in + typrec 0 (hnf_prod_applist env "type_case" t globargs) + +(* type_case_branches type un

Case c of ... end + ct = type de c, si inductif il a la forme APP(mI,largs), sinon raise Induc + 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 ct pt p c = + try + let ((mI,largs) as indt) = find_mrectype env ct in + let (dep,(nparams,globargs,la)) = + find_case_dep_nparams env (c,p) indt pt + in + let (lconstruct,ltypconstr) = type_mconstructs env mI in + if dep then + (mI, + array_map2 (type_one_branch_dep (env,nparams,globargs,p)) + lconstruct ltypconstr, + beta_applist (p,(la@[c]))) + else + (mI, + Array.map (type_one_branch_nodep (env,nparams,globargs,p)) + ltypconstr, + beta_applist (p,la)) + with Induc -> + error_case_not_inductive CCI env c ct + +let check_branches_message env (c,ct) (explft,lft) = + let n = Array.length explft + and expn = Array.length lft in + let rec check_conv i = + if not (i = n) then + if not (is_conv_leq env lft.(i) (explft.(i))) then + error_ill_formed_branch CCI env c i (nf_betaiota env lft.(i)) + (nf_betaiota env explft.(i)) + else + check_conv (i+1) + in + if n<>expn then error_number_branches CCI env c ct expn else check_conv 0 + +let type_of_case env pj cj lfj = + let lft = Array.map (fun j -> j.uj_type) lfj in + let (mind,bty,rslty) = + type_case_branches env cj.uj_type pj.uj_type pj.uj_val cj.uj_val in + let kind = sort_of_arity env pj.uj_type in + check_branches_message env (cj.uj_val,cj.uj_type) (bty,lft); + { uj_val = + mkMutCaseA (ci_of_mind mind) (j_val pj) (j_val cj) (Array.map j_val lfj); + uj_type = rslty; + uj_kind = kind } + +(* Prop and Set *) + +let type_of_prop_or_set cts = + { uj_val = DOP0(Sort(Prop cts)); + uj_type = DOP0(Sort type_0); + uj_kind = DOP0(Sort type_1) } + +(* Type of Type(i). *) + +let type_of_type u g = + let (uu,g') = super u g in + let (uuu,g'') = super uu g' in + { uj_val = DOP0 (Sort (Type u)); + uj_type = DOP0 (Sort (Type uu)); + uj_kind = DOP0 (Sort (Type uuu)) }, + g'' + +let type_of_sort c g = + match c with + | DOP0 (Sort (Type u)) -> let (uu,g') = super u g in mkType uu, g' + | DOP0 (Sort (Prop _)) -> mkType prop_univ, g + | DOP0 (Implicit) -> mkImplicit, g + | _ -> invalid_arg "type_of_sort" + +(* Type of a lambda-abstraction. *) + +let sort_of_product domsort rangsort g0 = + match rangsort with + (* Product rule (s,Prop,Prop) *) + | Prop _ -> rangsort, g0 + | Type u2 -> + (match domsort with + (* Product rule (Prop,Type_i,Type_i) *) + | Prop _ -> rangsort, g0 + (* Product rule (Type_i,Type_i,Type_i) *) + | Type u1 -> let (u12,g1) = sup u1 u2 g0 in Type u12, g1) + +let abs_rel env name var j = + let rngtyp = whd_betadeltaiota env j.uj_kind in + let cvar = incast_type var in + let (s,g) = sort_of_product var.typ (destSort rngtyp) (universes env) in + { uj_val = mkLambda name cvar (j_val j); + uj_type = mkProd name cvar j.uj_type; + uj_kind = mkSort s }, + g + +(* Type of a product. *) + +let gen_rel env name var j = + let jtyp = whd_betadeltaiota env j.uj_type in + let jkind = whd_betadeltaiota env j.uj_kind in + let j = { uj_val = j.uj_val; uj_type = jtyp; uj_kind = jkind } in + if isprop jkind then + error "Proof objects can only be abstracted" + else + match jtyp with + | DOP0(Sort s) -> + let (s',g) = sort_of_product var.typ s (universes env) in + let res_type = mkSort s' in + let (res_kind,g') = type_of_sort res_type g in + { uj_val = + mkProd name (mkCast var.body (mkSort var.typ)) (j_val_cast j); + uj_type = res_type; + uj_kind = res_kind }, g' + | _ -> + error_generalization CCI env (name,var) j.uj_val + +(* Type of a cast. *) + +let cast_rel env cj tj = + if is_conv_leq env cj.uj_type tj.uj_val then + { uj_val = j_val_only cj; + uj_type = tj.uj_val; + uj_kind = whd_betadeltaiota env tj.uj_type } + else + error_actual_type CCI env cj tj + +(* Type of an application. *) + +let apply_rel_list env0 nocheck argjl funj = + let rec apply_rec env typ = function + | [] -> + { uj_val = applist (j_val_only funj, List.map j_val_only argjl); + uj_type = typ; + uj_kind = funj.uj_kind }, + universes env + | hj::restjl -> + match whd_betadeltaiota env typ with + | DOP2(Prod,c1,DLAM(_,c2)) -> + if nocheck then + apply_rec env (subst1 hj.uj_val c2) restjl + else + (match conv_leq env hj.uj_type c1 with + | Convertible g -> + let env' = set_universes g env in + apply_rec env' (subst1 hj.uj_val c2) restjl + | NotConvertible -> + error_cant_apply CCI env "Type Error" funj argjl) + | _ -> + error_cant_apply CCI env "Non-functional construction" funj argjl + in + apply_rec env0 funj.uj_type argjl + + +(* Fixpoints. *) + +(* Checking function for terms containing existential variables. + The function noccur_with_meta consideres the fact that + each existential variable (as well as each isevar) + in the term appears applied to its local context, + which may contain the CoFix variables. These occurrences of CoFix variables + are not considered *) + +let noccur_with_meta sigma n m term = + let rec occur_rec n = function + | Rel(p) -> if n<=p & p () + | DOPN(AppL,cl) -> + (match strip_outer_cast cl.(0) with + | DOP0 (Meta _) -> () + | _ -> Array.iter (occur_rec n) cl) + | DOPN(Const sp, cl) when Evd.in_dom sigma sp -> () + | DOPN(op,cl) -> Array.iter (occur_rec n) cl + | DOPL(_,cl) -> List.iter (occur_rec n) cl + | DOP0(_) -> () + | DOP1(_,c) -> occur_rec n c + | DOP2(_,c1,c2) -> occur_rec n c1; occur_rec n c2 + | DLAM(_,c) -> occur_rec (n+1) c + | DLAMV(_,v) -> Array.iter (occur_rec (n+1)) v + in + try (occur_rec n term; true) with Occur -> false + +(* 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(sp1,k,l) -> Imbr(sp1,k, List.map (instantiate_recarg sp lrc) l) + | Norec -> Norec + | Param(k) -> List.nth lrc k + +(* propagate checking for F,incorporating recursive arguments *) +let check_term env mind_recvec f = + let rec crec n l (lrec,c) = + match (lrec,strip_outer_cast c) with + | (Param(_)::lr,DOP2(Lambda,_,DLAM(_,b))) -> + let l' = map_lift_fst l in + crec (n+1) l' (lr,b) + | (Norec::lr,DOP2(Lambda,_,DLAM(_,b))) -> + let l' = map_lift_fst l in + crec (n+1) l' (lr,b) + | (Mrec(i)::lr,DOP2(Lambda,_,DLAM(_,b))) -> + let l' = map_lift_fst l in + crec (n+1) ((1,mind_recvec.(i))::l') (lr,b) + | (Imbr(sp,i,lrc)::lr,DOP2(Lambda,_,DLAM(_,b))) -> + let l' = map_lift_fst l in + let sprecargs = + mis_recargs (lookup_mind_specif (mkMutInd sp i [||]) env) in + let lc = + Array.map (List.map (instantiate_recarg sp lrc)) sprecargs.(i) + in + crec (n+1) ((1,lc)::l') (lr,b) + | _,f_0 -> f n l f_0 + in + crec + +let is_inst_var env k c = + match whd_betadeltaiota_stack env c [] with + | (Rel n,_) -> n=k + | _ -> false + +let is_subterm_specif env lcx mind_recvec = + let rec crec n lst c = + match whd_betadeltaiota_stack env c [] with + | ((Rel k),_) -> find_sorted_assoc k lst + | (DOPN(MutCase _,_) as x,_) -> + let ( _,_,c,br) = destCase x in + if Array.length br = 0 then + [||] + else + let lcv = + (try + if is_inst_var env n c then lcx else (crec n lst c) + with Not_found -> (Array.create (Array.length br) [])) + 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 + stl.(0) + + | (DOPN(Fix(_),la) as mc,l) -> + let (recindxs,i,typarray,funnames,bodies) = destUntypedFix mc in + let nbfix = List.length funnames in + let decrArg = recindxs.(i) in + 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 = + if List.length l < (decrArg+1) then + ((nbOfAbst,lcx) :: (map_lift_fst_n nbOfAbst lst)) + else + let theDecrArg = List.nth l decrArg in + let recArgsDecrArg = + try (crec n lst theDecrArg) + with Not_found -> Array.create 0 [] + in + if (Array.length recArgsDecrArg)=0 then + (nbOfAbst,lcx) :: (map_lift_fst_n nbOfAbst lst) + else + (1,recArgsDecrArg) :: + (nbOfAbst,lcx) :: + (map_lift_fst_n nbOfAbst lst) + in + crec (n+nbOfAbst) newlst strippedBody + + | (DOP2(Lambda,_,DLAM(_,b)),[]) -> + let lst' = map_lift_fst lst in + crec (n+1) lst' b + + (*** Experimental change *************************) + | (DOP0(Meta _),_) -> [||] + | _ -> raise Not_found + in + crec + +let is_subterm env lcx mind_recvec n lst c = + try + let _ = is_subterm_specif env lcx mind_recvec n lst c in true + with Not_found -> + false + +(* 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 vectn k def = + (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 n def = + (match strip_outer_cast def with + | DOP2(Lambda,a,DLAM(_,b)) -> + if noccur_with_meta (evar_map env) n nfi a then + if n = k+1 then (a,b) else check_occur (n+1) b + else + error "Bad occurrence of recursive call" + | _ -> error "Not enough abstractions in the definition") in + let (c,d) = check_occur 1 def in + let (mI, largs) = + (try find_minductype env c + with Induc -> error "Recursive definition on a non inductive type") in + let (sp,tyi,_) = destMutInd mI in + let mind_recvec = mis_recargs (lookup_mind_specif mI 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 = + (* n gives the index of the recursive variable *) + (noccur_with_meta (evar_map env) (n+k+1) nfi t) or + (* no recursive call in the term *) + (match whd_betadeltaiota_stack env t [] with + | (Rel p,l) -> + 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 lcx mind_recvec n lst z) + then List.for_all (check_rec_call n lst) (la@lrest) + else error "Recursive call applied to an illegal term" + | _ -> assert false) + else error "Not enough arguments for the recursive call" + else List.for_all (check_rec_call n lst) l + | (DOPN(MutCase _,_) as mc,l) -> + let (ci,p,c_0,lrest) = destCase mc in + let lc = + (try + if is_inst_var env n c_0 then + lcx + else + is_subterm_specif env lcx mind_recvec n lst c_0 + with Not_found -> + 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)) + lc lrest) + && (List.for_all (check_rec_call 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 *) + + | (DOPN(Fix(_),la) as mc,l) -> + (List.for_all (check_rec_call n lst) l) && + let (recindxs,i,typarray,funnames,bodies) = destUntypedFix mc in + 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) la) + else + let theDecrArg = List.nth l decrArg in + let recArgsDecrArg = + try (is_subterm_specif env lcx mind_recvec n lst theDecrArg) + with Not_found -> Array.create 0 [] + in + if (Array.length recArgsDecrArg)=0 then + array_for_all (check_rec_call n lst) la + 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)) + + + | (DOP2(_,a,b),l) -> + (check_rec_call n lst a) && + (check_rec_call n lst b) && + (List.for_all (check_rec_call n lst) l) + + | (DOPN(_,la),l) -> + (array_for_all (check_rec_call n lst) la) && + (List.for_all (check_rec_call n lst) l) + + | (DOP0 (Meta _),l) -> true + + | (DLAM(_,t),l) -> + (check_rec_call (n+1) (map_lift_fst lst) t) && + (List.for_all (check_rec_call n lst) l) + + | (DLAMV(_,vt),l) -> + (array_for_all (check_rec_call (n+1) (map_lift_fst lst)) vt) && + (List.for_all (check_rec_call n lst) l) + + | (_,l) -> List.for_all (check_rec_call n lst) l + ) + + in + check_rec_call 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 = function + | DOPN(Fix(nvect,j),vargs) -> + let nbfix = let nv = Array.length vargs in + if nv < 2 then error "Ill-formed recursive definition" else nv-1 in + let varit = Array.sub vargs 0 nbfix in + let ldef = array_last vargs in + let ln = Array.length nvect + and la = Array.length varit in + if ln <> la then + error "Ill-formed fix term" + else + let (lna,vdefs) = decomp_DLAMV_name ln ldef in + let vlna = Array.of_list lna in + let check_type i = + try + let _ = check_subterm_rec_meta env nvect nvect.(i) vdefs.(i) in () + with UserError (s,str) -> + error_ill_formed_rec_body CCI env str lna i vdefs + in + for i = 0 to ln-1 do check_type i done + + | _ -> assert false + +(* Co-fixpoints. *) + +let check_guard_rec_meta env nbfix def deftype = + let rec codomain_is_coind c = + match whd_betadeltaiota env (strip_outer_cast c) with + | DOP2(Prod,a,DLAM(_,b)) -> codomain_is_coind b + | b -> + (try find_mcoinductype env b + with + | Induc -> error "The codomain is not a coinductive type" + | _ -> error "Type of Cofix function not as expected") + in + let (mI, _) = codomain_is_coind deftype in + let (sp,tyi,_) = destMutInd mI in + let lvlra = (mis_recargs (lookup_mind_specif mI env)) in + let vlra = lvlra.(tyi) in + let evd = evar_map env in + let rec check_rec_call alreadygrd n vlra t = + if (noccur_with_meta evd n nbfix t) then + true + else + match whd_betadeltaiota_stack env t [] with + | (DOP0 (Meta _), l) -> true + + | (Rel p,l) -> + if n <= p && p < n+nbfix then + (* recursive call *) + if alreadygrd then + if List.for_all (noccur_with_meta evd n nbfix) l then + true + else + error "Nested recursive occurrences" + else + error "Unguarded recursive call" + else + error "check_guard_rec_meta: ???" + + | (DOPN ((MutConstruct((x,y),i)),l), args) -> + let lra =vlra.(i-1) in + let mI = DOPN(MutInd(x,y),l) in + let _,realargs = list_chop (mind_nparams env mI) 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 true n newvlra t) && + (process_args_of_constr lr lrar) + + | (Imbr(sp,i,lrc)::lrar) -> + let mis = + lookup_mind_specif (mkMutInd sp i [||]) env in + let sprecargs = mis_recargs mis in + let lc = (Array.map + (List.map + (instantiate_recarg sp lrc)) + sprecargs.(i)) + in (check_rec_call true n lc t) & + (process_args_of_constr lr lrar) + + | _::lrar -> + if (noccur_with_meta evd n nbfix t) + then (process_args_of_constr lr lrar) + else error "Recursive call inside a non-recursive argument of constructor") + in (process_args_of_constr realargs lra) + + + | (DOP2(Lambda,a,DLAM(_,b)),[]) -> + if (noccur_with_meta evd n nbfix a) then + check_rec_call alreadygrd (n+1) vlra b + else + error "Recursive call in the type of an abstraction" + + | (DOPN(CoFix(j),vargs),l) -> + let nbfix = let nv = Array.length vargs in + if nv < 2 then + error "Ill-formed recursive definition" + else + nv-1 + in + let varit = Array.sub vargs 0 nbfix in + let ldef = array_last vargs in + let la = Array.length varit in + let (lna,vdefs) = decomp_DLAMV_name la ldef in + let vlna = Array.of_list lna + in + if (array_for_all (noccur_with_meta evd n nbfix) varit) then + (array_for_all (check_rec_call alreadygrd (n+1) vlra) vdefs) + && + (List.for_all (check_rec_call alreadygrd (n+1) vlra) l) + else + error "Recursive call in the type of a declaration" + + | (DOPN(MutCase _,_) as mc,l) -> + let (_,p,c,vrest) = destCase mc in + if (noccur_with_meta evd n nbfix p) then + if (noccur_with_meta evd n nbfix c) then + if (List.for_all (noccur_with_meta evd n nbfix) l) then + (array_for_all (check_rec_call alreadygrd n vlra) vrest) + else + error "Recursive call in the argument of a function defined by cases" + else + error "Recursive call in the argument of a case expression" + else + error "Recursive call in the type of a Case expression" + + | _ -> error "Definition not in guarded form" + + in + check_rec_call false 1 vlra def + +(* The function which checks that the whole block of definitions + satisfies the guarded condition *) + +let check_cofix env f = + match f with + | DOPN(CoFix(j),vargs) -> + let nbfix = let nv = Array.length vargs in + if nv < 2 then + error "Ill-formed recursive definition" + else + nv-1 + in + let varit = Array.sub vargs 0 nbfix in + let ldef = array_last vargs in + let la = Array.length varit in + let (lna,vdefs) = decomp_DLAMV_name la ldef in + let vlna = Array.of_list lna in + let check_type i = + (try + let _ = check_guard_rec_meta env nbfix vdefs.(i) varit.(i) in () + with UserError (s,str) -> + error_ill_formed_rec_body CCI env str lna i vdefs) + in + for i = 0 to nbfix-1 do check_type i done + | _ -> assert false + +(* 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 lna lar vdefj = + let lt = Array.length vdefj in + assert (Array.length lar = lt); + try + let cv = + conv_forall2_i + (fun i e def ar -> + let c = conv_leq e def (lift lt ar) in + if c = NotConvertible then raise (IllBranch i) else c) + env (Array.map (fun j -> j.uj_type) vdefj) (Array.map body_of_type lar) + in + begin match cv with + | Convertible g -> g + | NotConvertible -> assert false + end + with IllBranch i -> + error_ill_typed_rec_body CCI env i lna vdefj lar -- cgit v1.2.3