From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 28 Apr 2006 14:59:16 +0000 Subject: Imported Upstream version 8.0pl3+8.1alpha --- kernel/indtypes.ml | 268 +++++++++++++++++++++++++++++++---------------------- 1 file changed, 156 insertions(+), 112 deletions(-) (limited to 'kernel/indtypes.ml') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 0b1d49f5..a3fc0db4 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: indtypes.ml,v 1.59.2.4 2005/12/30 15:58:59 barras Exp $ *) +(* $Id: indtypes.ml 8653 2006-03-22 09:41:17Z herbelin $ *) open Util open Names @@ -26,14 +26,14 @@ let weaker_noccur_between env x nvars t = if noccur_between x nvars t then Some t else let t' = whd_betadeltaiota env t in - if noccur_between x nvars t then Some t' + if noccur_between x nvars t' then Some t' else None (************************************************************************) (* Various well-formedness check for inductive declarations *) +(* Errors related to inductive constructions *) type inductive_error = - (* These are errors related to inductive constructions in this module *) | NonPos of env * constr * constr | NotEnoughArgs of env * constr * constr | NotConstructor of env * constr * constr @@ -43,10 +43,6 @@ type inductive_error = | SameNamesOverlap of identifier list | NotAnArity of identifier | BadEntry - (* These are errors related to recursors building in Indrec *) - | NotAllowedCaseAnalysis of bool * sorts * inductive - | BadInduction of bool * identifier * sorts - | NotMutualInScheme exception InductiveError of inductive_error @@ -141,7 +137,7 @@ let rec infos_and_sort env t = let logic = not (is_info_type env varj) in let small = Term.is_small varj.utj_type in (logic,small) :: (infos_and_sort env1 c2) - | Cast (c,_) -> infos_and_sort env c + | Cast (c,_,_) -> infos_and_sort env c | _ -> [] let small_unit constrsinfos = @@ -175,19 +171,19 @@ let type_one_constructor env_ar_par params arsort c = (infos, full_cstr_type, cst2) -let infer_constructor_packet env_ar params arsort vc = +let infer_constructor_packet env_ar params arsort lc = let env_ar_par = push_rel_context params env_ar in let (constrsinfos,jlc,cst) = List.fold_right (fun c (infosl,l,cst) -> - let (infos,ct,cst') = + let (infos,ct,cst') = type_one_constructor env_ar_par params arsort c in (infos::infosl,ct::l, Constraint.union cst cst')) - vc + lc ([],[],Constraint.empty) in - let vc' = Array.of_list jlc in + let lc' = Array.of_list jlc in let issmall,isunit = small_unit constrsinfos in - (issmall,isunit,vc', cst) + (issmall,isunit,lc',cst) (* Type-check an inductive definition. Does not check positivity conditions. *) @@ -196,16 +192,15 @@ let typecheck_inductive env mie = (* Check unicity of names *) mind_check_names mie; mind_check_arities env mie; - (* We first type params and arity of each inductive definition *) + (* Params are typed-checked here *) + let params = mie.mind_entry_params in + let env_params, params, cstp = infer_local_decls env params in + (* We first type arity of each inductive definition *) (* This allows to build the environment of arities and to share *) (* the set of constraints *) let cst, arities, rev_params_arity_list = List.fold_left (fun (cst,arities,l) ind -> - (* Params are typed-checked here *) - let params = ind.mind_entry_params in - let env_params, params, cst1 = - infer_local_decls env params in (* Arities (without params) are typed-checked here *) let arity, cst2 = infer_type env_params ind.mind_entry_arity in @@ -215,10 +210,10 @@ let typecheck_inductive env mie = upper universe will be generated *) let id = ind.mind_entry_typename in let full_arity = it_mkProd_or_LetIn arity.utj_val params in - Constraint.union cst (Constraint.union cst1 cst2), + Constraint.union cst cst2, Sign.add_rel_decl (Name id, None, full_arity) arities, (params, id, full_arity, arity.utj_val)::l) - (Constraint.empty,empty_rel_context,[]) + (cstp,empty_rel_context,[]) mie.mind_entry_inds in let env_arities = push_rel_context arities env in @@ -234,13 +229,13 @@ let typecheck_inductive env mie = let (issmall,isunit,lc',cst') = infer_constructor_packet env_arities params arsort lc in let consnames = ind.mind_entry_consnames in - let ind' = (params,id,full_arity,consnames,issmall,isunit,lc') + let ind' = (id,full_arity,consnames,issmall,isunit,lc') in (ind'::inds, Constraint.union cst cst')) mie.mind_entry_inds params_arity_list ([],cst) in - (env_arities, Array.of_list inds, cst) + (env_arities, params, Array.of_list inds, cst) (************************************************************************) (************************************************************************) @@ -276,13 +271,18 @@ let explain_ind_err ntyp env0 nbpar c err = raise (InductiveError (NonPar (env,c',n,mkRel (nbpar-n+1), mkRel (l+nbpar)))) +let failwith_non_pos n ntypes c = + for k = n to n + ntypes - 1 do + if not (noccurn k c) then raise (IllFormedInd (LocalNonPos (k-n+1))) + done + let failwith_non_pos_vect n ntypes v = - for i = 0 to Array.length v - 1 do - for k = n to n + ntypes - 1 do - if not (noccurn k v.(i)) then raise (IllFormedInd (LocalNonPos (k-n+1))) - done - done; - anomaly "failwith_non_pos_vect: some k in [n;n+ntypes-1] should occur in v" + Array.iter (failwith_non_pos n ntypes) v; + anomaly "failwith_non_pos_vect: some k in [n;n+ntypes-1] should occur" + +let failwith_non_pos_list n ntypes l = + List.iter (failwith_non_pos n ntypes) l; + anomaly "failwith_non_pos_list: some k in [n;n+ntypes-1] should occur" (* Check the inductive type is called with the expected parameters *) let check_correct_par (env,n,ntypes,_) hyps l largs = @@ -303,6 +303,26 @@ let check_correct_par (env,n,ntypes,_) hyps l largs = if not (array_for_all (noccur_between n ntypes) largs') then failwith_non_pos_vect n ntypes largs' +(* Computes the maximum number of recursive parameters : + the first parameters which are constant in recursive arguments + n is the current depth, nmr is the maximum number of possible + recursive parameters *) + +let compute_rec_par (env,n,_,_) hyps nmr largs = +if nmr = 0 then 0 else +(* start from 0, hyps will be in reverse order *) + let (lpar,_) = list_chop nmr largs in + let rec find k index = + function + ([],_) -> nmr + | (_,[]) -> assert false (* |hyps|>=nmr *) + | (lp,(_,Some _,_)::hyps) -> find k (index-1) (lp,hyps) + | (p::lp,_::hyps) -> + ( match kind_of_term (whd_betadeltaiota env p) with + | Rel w when w = index -> find (k+1) (index-1) (lp,hyps) + | _ -> k) + in find 0 (n-1) (lpar,List.rev hyps) + (* This removes global parameters of the inductive types in lc (for nested inductive types only ) *) let abstract_mind_lc env ntyps npars lc = @@ -326,9 +346,10 @@ let ienv_push_var (env, n, ntypes, lra) (x,a,ra) = let ienv_push_inductive (env, n, ntypes, ra_env) (mi,lpar) = let auxntyp = 1 in + let specif = lookup_mind_specif env mi in let env' = push_rel (Anonymous,None, - hnf_prod_applist env (type_of_inductive env mi) lpar) env in + hnf_prod_applist env (type_of_inductive specif) lpar) env in let ra_env' = (Imbr mi,Rtree.mk_param 0) :: List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in @@ -336,46 +357,50 @@ let ienv_push_inductive (env, n, ntypes, ra_env) (mi,lpar) = let newidx = n + auxntyp in (env', newidx, ntypes, ra_env') +let array_min nmr a = if nmr = 0 then 0 else + Array.fold_left (fun k (nmri,_) -> min k nmri) nmr a + (* The recursive function that checks positivity and builds the list of recursive arguments *) let check_positivity_one (env, _,ntypes,_ as ienv) hyps i indlc = - let nparams = rel_context_length hyps in + let lparams = rel_context_length hyps in + let nmr = rel_context_nhyps hyps in (* check the inductive types occur positively in [c] *) - let rec check_pos (env, n, ntypes, ra_env as ienv) c = + let rec check_pos (env, n, ntypes, ra_env as ienv) nmr c = let x,largs = decompose_app (whd_betadeltaiota env c) in match kind_of_term x with | Prod (na,b,d) -> assert (largs = []); (match weaker_noccur_between env n ntypes b with - None -> raise (IllFormedInd (LocalNonPos n)); + None -> failwith_non_pos_list n ntypes [b] | Some b -> - check_pos (ienv_push_var ienv (na, b, mk_norec)) d) + check_pos (ienv_push_var ienv (na, b, mk_norec)) nmr d) | Rel k -> - let (ra,rarg) = - try List.nth ra_env (k-1) - with Failure _ | Invalid_argument _ -> (Norec,mk_norec) in - (match ra with - Mrec _ -> check_correct_par ienv hyps (k-n+1) largs - | _ -> - if not (List.for_all (noccur_between n ntypes) largs) - then raise (IllFormedInd (LocalNonPos n))); - rarg + (try let (ra,rarg) = List.nth ra_env (k-1) in + let nmr1 = + (match ra with + Mrec _ -> compute_rec_par ienv hyps nmr largs + | _ -> nmr) + in + if not (List.for_all (noccur_between n ntypes) largs) + then failwith_non_pos_list n ntypes largs + else (nmr1,rarg) + with Failure _ | Invalid_argument _ -> (nmr,mk_norec)) | Ind ind_kn -> (* If the inductive type being defined appears in a parameter, then we have an imbricated type *) - if List.for_all (noccur_between n ntypes) largs then mk_norec - else check_positive_imbr ienv (ind_kn, largs) + if List.for_all (noccur_between n ntypes) largs then (nmr,mk_norec) + else check_positive_imbr ienv nmr (ind_kn, largs) | err -> if noccur_between n ntypes x && List.for_all (noccur_between n ntypes) largs - then mk_norec - else raise (IllFormedInd (LocalNonPos n)) + then (nmr,mk_norec) + else failwith_non_pos_list n ntypes (x::largs) - (* accesses to the environment are not factorised, but does it worth - it? *) - and check_positive_imbr (env,n,ntypes,ra_env as ienv) (mi, largs) = + (* accesses to the environment are not factorised, but is it worth? *) + and check_positive_imbr (env,n,ntypes,ra_env as ienv) nmr (mi, largs) = let (mib,mip) = lookup_mind_specif env mi in - let auxnpar = mip.mind_nparams in + let auxnpar = mib.mind_nparams_rec in let (lpar,auxlargs) = try list_chop auxnpar largs with Failure _ -> raise (IllFormedInd (LocalNonPos n)) in @@ -393,31 +418,34 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps i indlc = let (env',_,_,_ as ienv') = ienv_push_inductive ienv (mi,lpar) in (* Parameters expressed in env' *) let lpar' = List.map (lift auxntyp) lpar in - let irecargs = + let irecargs_nmr = (* fails if the inductive type occurs non positively *) (* when substituted *) Array.map (function c -> let c' = hnf_prod_applist env' c lpar' in - check_constructors ienv' false c') + check_constructors ienv' false nmr c') auxlcvect + in + let irecargs = Array.map snd irecargs_nmr + and nmr' = array_min nmr irecargs_nmr in - (Rtree.mk_rec [|mk_paths (Imbr mi) irecargs|]).(0) + (nmr',(Rtree.mk_rec [|mk_paths (Imbr mi) irecargs|]).(0)) (* check the inductive types occur positively in the products of C, if check_head=true, also check the head corresponds to a constructor of the ith type *) - and check_constructors ienv check_head c = - let rec check_constr_rec (env,n,ntypes,ra_env as ienv) lrec c = + and check_constructors ienv check_head nmr c = + let rec check_constr_rec (env,n,ntypes,ra_env as ienv) nmr lrec c = let x,largs = decompose_app (whd_betadeltaiota env c) in match kind_of_term x with | Prod (na,b,d) -> assert (largs = []); - let recarg = check_pos ienv b in + let nmr',recarg = check_pos ienv nmr b in let ienv' = ienv_push_var ienv (na,b,mk_norec) in - check_constr_rec ienv' (recarg::lrec) d + check_constr_rec ienv' nmr' (recarg::lrec) d | hd -> if check_head then @@ -428,32 +456,39 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps i indlc = else if not (List.for_all (noccur_between n ntypes) largs) then raise (IllFormedInd (LocalNonPos n)); - List.rev lrec - in check_constr_rec ienv [] c + (nmr,List.rev lrec) + in check_constr_rec ienv nmr [] c in - mk_paths (Mrec i) - (Array.map + let irecargs_nmr = + Array.map (fun c -> - let c = body_of_type c in - let sign, rawc = mind_extract_params nparams c in - let env' = push_rel_context sign env in + let _,rawc = mind_extract_params lparams c in try - check_constructors ienv true rawc + check_constructors ienv true nmr rawc with IllFormedInd err -> - explain_ind_err (ntypes-i) env nparams c err) - indlc) + explain_ind_err (ntypes-i) env lparams c err) + indlc + in + let irecargs = Array.map snd irecargs_nmr + and nmr' = array_min nmr irecargs_nmr + in (nmr', mk_paths (Mrec i) irecargs) -let check_positivity env_ar inds = +let check_positivity env_ar params inds = let ntypes = Array.length inds in let lra_ind = List.rev (list_tabulate (fun j -> (Mrec j, Rtree.mk_param j)) ntypes) in - let check_one i (params,_,_,_,_,_,lc) = - let nparams = rel_context_length params in + let lparams = rel_context_length params in + let nmr = rel_context_nhyps params in + let check_one i (_,_,_,_,_,lc) = let ra_env = - list_tabulate (fun _ -> (Norec,mk_norec)) nparams @ lra_ind in - let ienv = (env_ar, 1+nparams, ntypes, ra_env) in - check_positivity_one ienv params i lc in - Rtree.mk_rec (Array.mapi check_one inds) + list_tabulate (fun _ -> (Norec,mk_norec)) lparams @ lra_ind in + let ienv = (env_ar, 1+lparams, ntypes, ra_env) in + check_positivity_one ienv params i lc + in + let irecargs_nmr = Array.mapi check_one inds in + let irecargs = Array.map snd irecargs_nmr + and nmr' = array_min nmr irecargs_nmr + in (nmr',Rtree.mk_rec irecargs) (************************************************************************) @@ -480,67 +515,77 @@ let allowed_sorts env issmall isunit = function if issmall then all_sorts else impredicative_sorts | Prop Null -> -(* Added InType which is derivable :when the type is unit and small *) -(* unit+small types have all elimination - In predicative system, the - other inductive definitions have only Prop elimination. - In impredicative system, large unit type have also Set elimination -*) if isunit then - if issmall then all_sorts - else if Environ.engagement env = None - then logical_sorts else impredicative_sorts +(* 29/1/02: added InType which is derivable when the type is unit and small *) + if isunit then all_sorts else logical_sorts -let build_inductive env env_ar record finite inds recargs cst = +let fold_inductive_blocks f = + Array.fold_left (fun acc (_,ar,_,_,_,lc) -> f (Array.fold_left f acc lc) ar) + +let used_section_variables env inds = + let ids = fold_inductive_blocks + (fun l c -> Idset.union (Environ.global_vars_set env c) l) + Idset.empty inds in + keep_hyps env ids + +let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst = let ntypes = Array.length inds in (* Compute the set of used section variables *) - let ids = - Array.fold_left - (fun acc (_,_,ar,_,_,_,lc) -> - Idset.union (Environ.global_vars_set env (body_of_type ar)) - (Array.fold_left - (fun acc c -> - Idset.union (global_vars_set env (body_of_type c)) acc) - acc - lc)) - Idset.empty inds in - let hyps = keep_hyps env ids in + let hyps = used_section_variables env inds in + let nparamargs = rel_context_nhyps params in (* Check one inductive *) - let build_one_packet (params,id,ar,cnames,issmall,isunit,lc) recarg = + let build_one_packet (id,ar,cnames,issmall,isunit,lc) recarg = (* Arity in normal form *) - let nparamargs = rel_context_nhyps params in let (ar_sign,ar_sort) = dest_arity env ar in - let nf_ar = - if isArity (body_of_type ar) then ar - else it_mkProd_or_LetIn (mkSort ar_sort) ar_sign in + let nf_ar = if isArity ar then ar else mkArity (ar_sign,ar_sort) in (* Type of constructors in normal form *) let splayed_lc = Array.map (dest_prod_assum env_ar) lc in - let nf_lc = - array_map2 (fun (d,b) c -> it_mkProd_or_LetIn b d) splayed_lc lc in + let nf_lc = Array.map (fun (d,b) -> it_mkProd_or_LetIn b d) splayed_lc in let nf_lc = if nf_lc = lc then lc else nf_lc in + let consnrealargs = + Array.map (fun (d,_) -> rel_context_length d - rel_context_length params) + splayed_lc in (* Elimination sorts *) let isunit = isunit && ntypes = 1 && (not (is_recursive recargs.(0))) in let kelim = allowed_sorts env issmall isunit ar_sort in + let nconst, nblock = ref 0, ref 0 in + let transf num = + let arity = List.length (dest_subterms recarg).(num) in + if arity = 0 then + let p = (!nconst, 0) in + incr nconst; p + else + let p = (!nblock + 1, arity) in + incr nblock; p + (* les tag des constructeur constant commence a 0, + les tag des constructeur non constant a 1 (0 => accumulator) *) + in + let rtbl = Array.init (List.length cnames) transf in (* Build the inductive packet *) { mind_typename = id; - mind_nparams = nparamargs; - mind_params_ctxt = params; mind_user_arity = ar; mind_nf_arity = nf_ar; mind_nrealargs = rel_context_nhyps ar_sign - nparamargs; mind_sort = ar_sort; mind_kelim = kelim; mind_consnames = Array.of_list cnames; + mind_consnrealdecls = consnrealargs; mind_user_lc = lc; mind_nf_lc = nf_lc; - mind_recargs = recarg; + mind_recargs = recarg; + mind_nb_constant = !nconst; + mind_nb_args = !nblock; + mind_reloc_tbl = rtbl; } in let packets = array_map2 build_one_packet inds recargs in (* Build the mutual inductive *) - { mind_record = record; + { mind_record = isrecord; mind_ntypes = ntypes; - mind_finite = finite; + mind_finite = isfinite; mind_hyps = hyps; + mind_nparams = nparamargs; + mind_nparams_rec = nmr; + mind_params_ctxt = params; mind_packets = packets; mind_constraints = cst; mind_equiv = None; @@ -551,10 +596,9 @@ let build_inductive env env_ar record finite inds recargs cst = let check_inductive env mie = (* First type-check the inductive definition *) - let (env_arities, inds, cst) = typecheck_inductive env mie in + let (env_ar, params, inds, cst) = typecheck_inductive env mie in (* Then check positivity conditions *) - let recargs = check_positivity env_arities inds in + let (nmr,recargs) = check_positivity env_ar params inds in (* Build the inductive packets *) - build_inductive env env_arities mie.mind_entry_record mie.mind_entry_finite - inds recargs cst - + build_inductive env env_ar params mie.mind_entry_record mie.mind_entry_finite + inds nmr recargs cst -- cgit v1.2.3