diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /kernel/indtypes.ml | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'kernel/indtypes.ml')
-rw-r--r-- | kernel/indtypes.ml | 191 |
1 files changed, 104 insertions, 87 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 941ab046..dd9720b3 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: indtypes.ml 12616 2009-12-30 15:02:26Z herbelin $ *) +(* $Id$ *) open Util open Names @@ -58,8 +58,8 @@ exception InductiveError of inductive_error let check_constructors_names = let rec check idset = function | [] -> idset - | c::cl -> - if Idset.mem c idset then + | c::cl -> + if Idset.mem c idset then raise (InductiveError (SameNamesConstructors c)) else check (Idset.add c idset) cl @@ -73,7 +73,7 @@ let check_constructors_names = let mind_check_names mie = let rec check indset cstset = function | [] -> () - | ind::inds -> + | ind::inds -> let id = ind.mind_entry_typename in let cl = ind.mind_entry_consnames in if Idset.mem id indset then @@ -89,7 +89,7 @@ let mind_check_names mie = let mind_check_arities env mie = let check_arity id c = - if not (is_arity env c) then + if not (is_arity env c) then raise (InductiveError (NotAnArity id)) in List.iter @@ -110,12 +110,12 @@ let is_small infos = List.for_all (fun (logic,small) -> small) infos let is_logic_constr infos = List.for_all (fun (logic,small) -> logic) infos (* An inductive definition is a "unit" if it has only one constructor - and that all arguments expected by this constructor are - logical, this is the case for equality, conjunction of logical properties + and that all arguments expected by this constructor are + logical, this is the case for equality, conjunction of logical properties *) let is_unit constrsinfos = match constrsinfos with (* One info = One constructor *) - | [constrinfos] -> is_logic_constr constrinfos + | [constrinfos] -> is_logic_constr constrinfos | [] -> (* type without constructors *) true | _ -> false @@ -132,7 +132,7 @@ let rec infos_and_sort env t = | _ -> (* don't fail if not positive, it is tested later *) [] let small_unit constrsinfos = - let issmall = List.for_all is_small constrsinfos + let issmall = List.for_all is_small constrsinfos and isunit = is_unit constrsinfos in issmall, isunit @@ -154,7 +154,7 @@ let small_unit constrsinfos = w1,w2,w3 <= u1 w1,w2 <= u2 w1,w2,w3 <= u3 -*) +*) let extract_level (_,_,_,lc,lev) = (* Enforce that the level is not in Prop if more than two constructors *) @@ -173,9 +173,7 @@ let inductive_levels arities inds = let constraint_list_union = List.fold_left Constraint.union Constraint.empty -let infer_constructor_packet env_ar params lc = - (* builds the typing context "Gamma, I1:A1, ... In:An, params" *) - let env_ar_par = push_rel_context params env_ar in +let infer_constructor_packet env_ar_par params lc = (* type-check the constructors *) let jlc,cstl = List.split (List.map (infer_type env_ar_par) lc) in let cst = constraint_list_union cstl in @@ -195,7 +193,6 @@ let typecheck_inductive env mie = if mie.mind_entry_inds = [] then anomaly "empty inductive types declaration"; (* Check unicity of names *) mind_check_names mie; - mind_check_arities env mie; (* Params are typed-checked here *) let env_params, params, cst1 = infer_local_decls env mie.mind_entry_params in (* We first type arity of each inductive definition *) @@ -213,11 +210,13 @@ let typecheck_inductive env mie = let full_arity = it_mkProd_or_LetIn arity.utj_val params in let cst = Constraint.union cst cst2 in let id = ind.mind_entry_typename in - let env_ar' = push_rel (Name id, None, full_arity) env_ar in + let env_ar' = + push_rel (Name id, None, full_arity) + (add_constraints cst2 env_ar) in let lev = (* Decide that if the conclusion is not explicitly Type *) (* then the inductive type is not polymorphic *) - match kind_of_term (snd (decompose_prod_assum arity.utj_val)) with + match kind_of_term ((strip_prod_assum arity.utj_val)) with | Sort (Type u) -> Some u | _ -> None in (cst,env_ar',(id,full_arity,lev)::l)) @@ -226,12 +225,16 @@ let typecheck_inductive env mie = let arity_list = List.rev rev_arity_list in + (* builds the typing context "Gamma, I1:A1, ... In:An, params" *) + let env_ar_par = + push_rel_context params (add_constraints cst1 env_arities) in + (* Now, we type the constructors (without params) *) let inds,cst = List.fold_right2 (fun ind arity_data (inds,cst) -> let (info,lc',cstrs_univ,cst') = - infer_constructor_packet env_arities params ind.mind_entry_lc in + infer_constructor_packet env_ar_par params ind.mind_entry_lc in let consnames = ind.mind_entry_consnames in let ind' = (arity_data,consnames,info,lc',cstrs_univ) in (ind'::inds, Constraint.union cst cst')) @@ -242,11 +245,11 @@ let typecheck_inductive env mie = let inds = Array.of_list inds in let arities = Array.of_list arity_list in let param_ccls = List.fold_left (fun l (_,b,p) -> - if b = None then + if b = None then let _,c = dest_prod_assum env p in let u = match kind_of_term c with Sort (Type u) -> Some u | _ -> None in u::l - else + else l) [] params in (* Compute/check the sorts of the inductive types *) @@ -255,7 +258,7 @@ let typecheck_inductive env mie = array_fold_map2' (fun ((id,full_arity,ar_level),cn,info,lc,_) lev cst -> let sign, s = dest_arity env full_arity in let status,cst = match s with - | Type u when ar_level <> None (* Explicitly polymorphic *) + | Type u when ar_level <> None (* Explicitly polymorphic *) && no_upper_constraints u cst -> (* The polymorphic level is a function of the level of the *) (* conclusions of the parameters *) @@ -294,20 +297,20 @@ exception IllFormedInd of ill_formed_ind let mind_extract_params = decompose_prod_n_assum -let explain_ind_err id ntyp env0 nbpar c nargs err = +let explain_ind_err id ntyp env0 nbpar c nargs err = let (lpar,c') = mind_extract_params nbpar c in let env = push_rel_context lpar env0 in match err with - | LocalNonPos kt -> + | LocalNonPos kt -> raise (InductiveError (NonPos (env,c',mkRel (kt+nbpar)))) - | LocalNotEnoughArgs kt -> - raise (InductiveError + | LocalNotEnoughArgs kt -> + raise (InductiveError (NotEnoughArgs (env,c',mkRel (kt+nbpar)))) | LocalNotConstructor -> - raise (InductiveError + raise (InductiveError (NotConstructor (env,id,c',mkRel (ntyp+nbpar),nbpar,nargs))) | LocalNonPar (n,l) -> - raise (InductiveError + raise (InductiveError (NonPar (env,c',n,mkRel (nbpar-n+1), mkRel (l+nbpar)))) let failwith_non_pos n ntypes c = @@ -327,7 +330,7 @@ let failwith_non_pos_list n ntypes l = let check_correct_par (env,n,ntypes,_) hyps l largs = let nparams = rel_context_nhyps hyps in let largs = Array.of_list largs in - if Array.length largs < nparams then + if Array.length largs < nparams then raise (IllFormedInd (LocalNotEnoughArgs l)); let (lpar,largs') = array_chop nparams largs in let nhyps = List.length hyps in @@ -339,20 +342,20 @@ let check_correct_par (env,n,ntypes,_) hyps l largs = | Rel w when w = index -> check (k-1) (index+1) hyps | _ -> raise (IllFormedInd (LocalNonPar (k+1,l))) in check (nparams-1) (n-nhyps) hyps; - if not (array_for_all (noccur_between n ntypes) largs') then + 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 +(* 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 = +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 + let rec find k index = + function ([],_) -> nmr | (_,[]) -> assert false (* |hyps|>=nmr *) | (lp,(_,Some _,_)::hyps) -> find k (index-1) (lp,hyps) @@ -364,14 +367,14 @@ if nmr = 0 then 0 else (* This removes global parameters of the inductive types in lc (for nested inductive types only ) *) -let abstract_mind_lc env ntyps npars lc = - if npars = 0 then +let abstract_mind_lc env ntyps npars lc = + if npars = 0 then lc - else - let make_abs = + else + let make_abs = list_tabulate - (function i -> lambda_implicit_lift npars (mkRel (i+1))) ntyps - in + (function i -> lambda_implicit_lift npars (mkRel (i+1))) ntyps + in Array.map (substl make_abs) lc (* [env] is the typing environment @@ -379,7 +382,7 @@ let abstract_mind_lc env ntyps npars lc = [ntypes] is the number of inductive types in the definition (i.e. range of inductives is [n; n+ntypes-1]) [lra] is the list of recursive tree of each variable - *) + *) let ienv_push_var (env, n, ntypes, lra) (x,a,ra) = (push_rel (x,None,a) env, n+1, ntypes, (Norec,ra)::lra) @@ -389,13 +392,22 @@ let ienv_push_inductive (env, n, ntypes, ra_env) (mi,lpar) = let env' = push_rel (Anonymous,None, hnf_prod_applist env (type_of_inductive env specif) lpar) env in - let ra_env' = + let ra_env' = (Imbr mi,(Rtree.mk_rec_calls 1).(0)) :: List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in (* New index of the inductive types *) let newidx = n + auxntyp in (env', newidx, ntypes, ra_env') +let rec ienv_decompose_prod (env,_,_,_ as ienv) n c = + if n=0 then (ienv,c) else + let c' = whd_betadeltaiota env c in + match kind_of_term c' with + Prod(na,a,b) -> + let ienv' = ienv_push_var ienv (na,a,mk_norec) in + ienv_decompose_prod ienv' (n-1) b + | _ -> assert false + let array_min nmr a = if nmr = 0 then 0 else Array.fold_left (fun k (nmri,_) -> min k nmri) nmr a @@ -404,8 +416,8 @@ let array_min nmr a = if nmr = 0 then 0 else let check_positivity_one (env, _,ntypes,_ as ienv) hyps i nargs lcnames indlc = 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) nmr c = + (* Checking the (strict) positivity of a constructor argument type [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) -> @@ -415,40 +427,41 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps i nargs lcnames indlc = | Some b -> check_pos (ienv_push_var ienv (na, b, mk_norec)) nmr d) | Rel k -> - (try let (ra,rarg) = List.nth ra_env (k-1) in + (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 + 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 *) + parameter, then we have a nested indtype *) if List.for_all (noccur_between n ntypes) largs then (nmr,mk_norec) - else check_positive_imbr ienv nmr (ind_kn, largs) - | err -> + else check_positive_nested ienv nmr (ind_kn, largs) + | err -> if noccur_between n ntypes x && - List.for_all (noccur_between n ntypes) largs + List.for_all (noccur_between n ntypes) largs then (nmr,mk_norec) else failwith_non_pos_list n ntypes (x::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) = + and check_positive_nested (env,n,ntypes,ra_env as ienv) nmr (mi, largs) = let (mib,mip) = lookup_mind_specif env mi in let auxnpar = mib.mind_nparams_rec in + let nonrecpar = mib.mind_nparams - auxnpar in let (lpar,auxlargs) = - try list_chop auxnpar largs - with Failure _ -> raise (IllFormedInd (LocalNonPos n)) in + try list_chop auxnpar largs + with Failure _ -> raise (IllFormedInd (LocalNonPos n)) in (* If the inductive appears in the args (non params) then the definition is not positive. *) if not (List.for_all (noccur_between n ntypes) auxlargs) then - raise (IllFormedInd (LocalNonPos n)); + failwith_non_pos_list n ntypes auxlargs; (* We do not deal with imbricated mutual inductive types *) - let auxntyp = mib.mind_ntypes in + let auxntyp = mib.mind_ntypes in if auxntyp <> 1 then raise (IllFormedInd (LocalNonPos n)); (* The nested inductive type with parameters removed *) let auxlcvect = abstract_mind_lc env auxntyp auxnpar mip.mind_nf_lc in @@ -457,35 +470,37 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps i nargs lcnames 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_nmr = + 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 nmr c') + (* with recursive parameters substituted *) + Array.map + (function c -> + let c' = hnf_prod_applist env' c lpar' in + (* skip non-recursive parameters *) + let (ienv',c') = ienv_decompose_prod ienv' nonrecpar c' in + check_constructors ienv' false nmr c') auxlcvect in let irecargs = Array.map snd irecargs_nmr and nmr' = array_min nmr irecargs_nmr - in + in (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 nmr c = - let rec check_constr_rec (env,n,ntypes,ra_env as ienv) nmr lrec c = + the ith type *) + + 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) -> + | Prod (na,b,d) -> assert (largs = []); - let nmr',recarg = check_pos ienv nmr 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' nmr' (recarg::lrec) d - + | hd -> if check_head then if hd = Rel (n+ntypes-i-1) then @@ -504,7 +519,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps i nargs lcnames indlc = let _,rawc = mind_extract_params lparams c in try check_constructors ienv true nmr rawc - with IllFormedInd err -> + with IllFormedInd err -> explain_ind_err id (ntypes-i) env lparams c nargs err) (Array.of_list lcnames) indlc in @@ -523,9 +538,9 @@ let check_positivity env_ar params inds = list_tabulate (fun _ -> (Norec,mk_norec)) lparams @ lra_ind in let ienv = (env_ar, 1+lparams, ntypes, ra_env) in let nargs = rel_context_nhyps sign - nmr in - check_positivity_one ienv params i nargs lcnames lc + check_positivity_one ienv params i nargs lcnames lc in - let irecargs_nmr = Array.mapi check_one inds 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) @@ -534,14 +549,14 @@ let check_positivity env_ar params inds = (************************************************************************) (************************************************************************) (* Build the inductive packet *) - + (* Elimination sorts *) let is_recursive = Rtree.is_infinite -(* let rec one_is_rec rvec = - List.exists (function Mrec(i) -> List.mem i listind +(* let rec one_is_rec rvec = + List.exists (function Mrec(i) -> List.mem i listind | Imbr(_,lvec) -> array_exists one_is_rec lvec | Norec -> false) rvec - in + in array_exists one_is_rec *) @@ -585,6 +600,7 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst = (* Compute the set of used section variables *) let hyps = used_section_variables env inds in let nparamargs = rel_context_nhyps params in + let nparamdecls = rel_context_length params in (* Check one inductive *) let build_one_packet (id,cnames,lc,(ar_sign,ar_kind)) recarg = (* Type of constructors in normal form *) @@ -594,37 +610,39 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst = let consnrealargs = Array.map (fun (d,_) -> rel_context_length d - rel_context_length params) splayed_lc in - (* Elimination sorts *) + (* Elimination sorts *) let arkind,kelim = match ar_kind with | Inr (param_levels,lev) -> Polymorphic { poly_param_levels = param_levels; - poly_level = lev; + poly_level = lev; }, all_sorts | Inl ((issmall,isunit),ar,s) -> let kelim = allowed_sorts issmall isunit s in Monomorphic { mind_user_arity = ar; - mind_sort = s; + mind_sort = s; }, kelim in - let nconst, nblock = ref 0, ref 0 in + (* Assigning VM tags to constructors *) + let nconst, nblock = ref 0, ref 0 in let transf num = let arity = List.length (dest_subterms recarg).(num) in - if arity = 0 then + if arity = 0 then let p = (!nconst, 0) in incr nconst; p - else + 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 + in let rtbl = Array.init (List.length cnames) transf in (* Build the inductive packet *) { mind_typename = id; mind_arity = arkind; mind_arity_ctxt = ar_sign; mind_nrealargs = rel_context_nhyps ar_sign - nparamargs; + mind_nrealargs_ctxt = rel_context_length ar_sign - nparamdecls; mind_kelim = kelim; mind_consnames = Array.of_list cnames; mind_consnrealdecls = consnrealargs; @@ -642,11 +660,10 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst = mind_finite = isfinite; mind_hyps = hyps; mind_nparams = nparamargs; - mind_nparams_rec = nmr; + mind_nparams_rec = nmr; mind_params_ctxt = params; mind_packets = packets; - mind_constraints = cst; - mind_equiv = None; + mind_constraints = cst } (************************************************************************) |