From e978da8c41d8a3c19a29036d9c569fbe2a4616b0 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 16 Jun 2006 14:41:51 +0000 Subject: Imported Upstream version 8.0pl3+8.1beta --- kernel/indtypes.ml | 222 +++++++++++++++++++++++++++++++++-------------------- 1 file changed, 140 insertions(+), 82 deletions(-) (limited to 'kernel/indtypes.ml') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index a3fc0db4..e7dc09ee 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: indtypes.ml 8653 2006-03-22 09:41:17Z herbelin $ *) +(* $Id: indtypes.ml 8871 2006-05-28 16:46:48Z herbelin $ *) open Util open Names @@ -116,12 +116,10 @@ let is_info_type env t = 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 -let is_logic_arity infos = - List.for_all (fun (logic,small) -> logic || small) 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, conjonction of logical properties + logical, this is the case for equality, conjunction of logical properties *) let is_unit constrsinfos = match constrsinfos with (* One info = One constructor *) @@ -145,45 +143,54 @@ let small_unit constrsinfos = and isunit = is_unit constrsinfos in issmall, isunit -(* This (re)computes informations relevant to extraction and the sort of an - arity or type constructor; we do not to recompute universes constraints *) +(* Computing the levels of polymorphic inductive types -(* [smax] is the max of the sorts of the products of the constructor type *) + For each inductive type of a block that is of level u_i, we have + the constraints that u_i >= v_i where v_i is the type level of the + types of the constructors of this inductive type. Each v_i depends + of some of the u_i and of an extra (maybe non variable) universe, + say w_i that summarize all the other constraints. Typically, for + three inductive types, we could have -let enforce_type_constructor env arsort smax cst = - match smax, arsort with - | Type uc, Type ua -> enforce_geq ua uc cst - | Type uc, Prop Pos when engagement env <> Some ImpredicativeSet -> - error "Large non-propositional inductive types must be in Type" - | _,_ -> cst + u1,u2,u3,w1 <= u1 + u1 w2 <= u2 + u2,u3,w3 <= u3 -let type_one_constructor env_ar_par params arsort c = - let infos = infos_and_sort env_ar_par c in + From this system of inequations, we shall deduce - (* Each constructor is typed-checked here *) - let (j,cst) = infer_type env_ar_par c in - let full_cstr_type = it_mkProd_or_LetIn j.utj_val params in + w1,w2,w3 <= u1 + w1,w2 <= u2 + w1,w2,w3 <= u3 +*) - (* If the arity is at some level Type arsort, then the sort of the - constructor must be below arsort; here we consider constructors with the - global parameters (which add a priori more constraints on their sort) *) - let cst2 = enforce_type_constructor env_ar_par arsort j.utj_type cst in +let inductive_levels arities inds = + let levels = Array.map pi3 arities in + let cstrs_levels = Array.map (fun (_,_,_,_,lev) -> lev) inds in + (* Take the transitive closure of the system of constructors *) + (* level constraints and remove the recursive dependencies *) + solve_constraints_system levels cstrs_levels - (infos, full_cstr_type, cst2) +(* This (re)computes informations relevant to extraction and the sort of an + arity or type constructor; we do not to recompute universes constraints *) -let infer_constructor_packet env_ar params arsort lc = +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 (constrsinfos,jlc,cst) = - List.fold_right - (fun c (infosl,l,cst) -> - let (infos,ct,cst') = - type_one_constructor env_ar_par params arsort c in - (infos::infosl,ct::l, Constraint.union cst cst')) - lc - ([],[],Constraint.empty) in - let lc' = Array.of_list jlc in - let issmall,isunit = small_unit constrsinfos in - (issmall,isunit,lc',cst) + (* 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 + let jlc = Array.of_list jlc in + (* generalize the constructor over the parameters *) + let lc'' = Array.map (fun j -> it_mkProd_or_LetIn j.utj_val params) jlc in + (* compute the max of the sorts of the products of the constructor type *) + let level = max_inductive_sort (Array.map (fun j -> j.utj_type) jlc) in + (* compute *) + let info = small_unit (List.map (infos_and_sort env_ar_par) lc) in + + (info,lc'',level,cst) (* Type-check an inductive definition. Does not check positivity conditions. *) @@ -192,50 +199,82 @@ let typecheck_inductive env mie = (* Check unicity of names *) mind_check_names mie; mind_check_arities env mie; - (* Params are typed-checked here *) - let params = mie.mind_entry_params in - let env_params, params, cstp = infer_local_decls env params in + (* 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 *) (* This allows to build the environment of arities and to share *) (* the set of constraints *) - let cst, arities, rev_params_arity_list = + let cst, env_arities, rev_arity_list = List.fold_left - (fun (cst,arities,l) ind -> + (fun (cst,env_ar,l) ind -> (* Arities (without params) are typed-checked here *) - let arity, cst2 = - infer_type env_params ind.mind_entry_arity in + let arity, cst2 = infer_type env_params ind.mind_entry_arity in (* We do not need to generate the universe of full_arity; if later, after the validation of the inductive definition, full_arity is used as argument or subject to cast, an 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 cst2, - Sign.add_rel_decl (Name id, None, full_arity) arities, - (params, id, full_arity, arity.utj_val)::l) - (cstp,empty_rel_context,[]) + 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 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 + | Sort (Type u) -> Some u + | _ -> None in + (cst,env_ar',(id,full_arity,lev)::l)) + (cst1,env,[]) mie.mind_entry_inds in - let env_arities = push_rel_context arities env in - - let params_arity_list = List.rev rev_params_arity_list in + let arity_list = List.rev rev_arity_list in (* Now, we type the constructors (without params) *) let inds,cst = List.fold_right2 - (fun ind (params,id,full_arity,short_arity) (inds,cst) -> - let (_,arsort) = dest_arity env full_arity in - let lc = ind.mind_entry_lc in - let (issmall,isunit,lc',cst') = - infer_constructor_packet env_arities params arsort lc in + (fun ind arity_data (inds,cst) -> + let (info,lc',cstrs_univ,cst') = + infer_constructor_packet env_arities params ind.mind_entry_lc in let consnames = ind.mind_entry_consnames in - let ind' = (id,full_arity,consnames,issmall,isunit,lc') - in + let ind' = (arity_data,consnames,info,lc',cstrs_univ) in (ind'::inds, Constraint.union cst cst')) mie.mind_entry_inds - params_arity_list + arity_list ([],cst) in - (env_arities, params, Array.of_list inds, cst) + + 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 + 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 + l) [] params in + + (* Compute/check the sorts of the inductive types *) + let ind_min_levels = inductive_levels arities inds in + let inds, cst = + 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 _ when ar_level <> None (* Explicitly polymorphic *) -> + (* The polymorphic level is a function of the level of the *) + (* conclusions of the parameters *) + Inr (param_ccls, lev), cst + | Type u (* Not an explicit occurrence of Type *) -> + Inl (info,full_arity,s), enforce_geq u lev cst + | Prop Pos when engagement env <> Some ImpredicativeSet -> + (* Predicative set: check that the content is indeed predicative *) + if not (is_empty_univ lev) & not (is_base_univ lev) then + error "Large non-propositional inductive types must be in Type"; + Inl (info,full_arity,s), cst + | Prop _ -> + Inl (info,full_arity,s), cst in + (id,cn,lc,(sign,status)),cst) + inds ind_min_levels cst in + + (env_arities, params, inds, cst) (************************************************************************) (************************************************************************) @@ -479,7 +518,7 @@ let check_positivity env_ar params inds = List.rev (list_tabulate (fun j -> (Mrec j, Rtree.mk_param j)) ntypes) in let lparams = rel_context_length params in let nmr = rel_context_nhyps params in - let check_one i (_,_,_,_,_,lc) = + let check_one i (_,_,lc,_) = let ra_env = list_tabulate (fun _ -> (Norec,mk_norec)) lparams @ lra_ind in let ienv = (env_ar, 1+lparams, ntypes, ra_env) in @@ -505,22 +544,34 @@ let is_recursive = Rtree.is_infinite array_exists one_is_rec *) +(* Allowed eliminations *) + let all_sorts = [InProp;InSet;InType] -let impredicative_sorts = [InProp;InSet] +let small_sorts = [InProp;InSet] let logical_sorts = [InProp] -let allowed_sorts env issmall isunit = function - | Type _ -> all_sorts - | Prop Pos -> - if issmall then all_sorts - else impredicative_sorts - | Prop Null -> -(* 29/1/02: added InType which is derivable when the type is unit and small *) - if isunit then all_sorts - else logical_sorts +let allowed_sorts issmall isunit s = + match family_of_sort s with + (* Type: all elimination allowed *) + | InType -> all_sorts + + (* Small Set is predicative: all elimination allowed *) + | InSet when issmall -> all_sorts + + (* Large Set is necessarily impredicative: forbids large elimination *) + | InSet -> small_sorts + + (* Unitary/empty Prop: elimination to all sorts are realizable *) + (* unless the type is large. If it is large, forbids large elimination *) + (* which otherwise allows to simulate the inconsistent system Type:Type *) + | InProp when isunit -> if issmall then all_sorts else small_sorts + + (* Other propositions: elimination only to Prop *) + | InProp -> logical_sorts let fold_inductive_blocks f = - Array.fold_left (fun acc (_,ar,_,_,_,lc) -> f (Array.fold_left f acc lc) ar) + Array.fold_left (fun acc (_,_,lc,(arsign,_)) -> + f (Array.fold_left f acc lc) (it_mkProd_or_LetIn (* dummy *) mkSet arsign)) let used_section_variables env inds = let ids = fold_inductive_blocks @@ -534,10 +585,7 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst = let hyps = used_section_variables env inds in let nparamargs = rel_context_nhyps params in (* Check one inductive *) - let build_one_packet (id,ar,cnames,issmall,isunit,lc) recarg = - (* Arity in normal form *) - let (ar_sign,ar_sort) = dest_arity env ar in - let nf_ar = if isArity ar then ar else mkArity (ar_sign,ar_sort) in + let build_one_packet (id,cnames,lc,(ar_sign,ar_kind)) recarg = (* Type of constructors in normal form *) let splayed_lc = Array.map (dest_prod_assum env_ar) lc in let nf_lc = Array.map (fun (d,b) -> it_mkProd_or_LetIn b d) splayed_lc in @@ -546,8 +594,19 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst = 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 arkind,kelim = match ar_kind with + | Inr (param_levels,lev) -> + Polymorphic { + mind_param_levels = param_levels; + mind_level = lev; + }, all_sorts + | Inl ((issmall,isunit),ar,s) -> + let isunit = isunit && ntypes = 1 && not (is_recursive recargs.(0)) in + let kelim = allowed_sorts issmall isunit s in + Monomorphic { + mind_user_arity = ar; + mind_sort = s; + }, kelim in let nconst, nblock = ref 0, ref 0 in let transf num = let arity = List.length (dest_subterms recarg).(num) in @@ -563,16 +622,15 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst = let rtbl = Array.init (List.length cnames) transf in (* Build the inductive packet *) { mind_typename = id; - mind_user_arity = ar; - mind_nf_arity = nf_ar; + mind_arity = arkind; + mind_arity_ctxt = ar_sign; 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; @@ -600,5 +658,5 @@ let check_inductive env mie = (* Then check positivity conditions *) let (nmr,recargs) = check_positivity env_ar params inds in (* Build the inductive packets *) - build_inductive env env_ar params mie.mind_entry_record mie.mind_entry_finite + build_inductive env env_ar params mie.mind_entry_record mie.mind_entry_finite inds nmr recargs cst -- cgit v1.2.3