diff options
37 files changed, 519 insertions, 415 deletions
diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml index 1d1383f60..1f6a07a6d 100644 --- a/contrib/extraction/common.ml +++ b/contrib/extraction/common.ml @@ -112,7 +112,8 @@ let contents_first_level mp = | Extraction.Term -> add false (id_of_label l)) | (_, SPBmind mib) -> Array.iter - (fun mip -> if mip.mind_sort <> (Prop Null) then begin + (fun mip -> if snd (Inductive.mind_arity mip) <> InProp + then begin add upper_type mip.mind_typename; Array.iter (add true) mip.mind_consnames end) diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index 0485c1368..485b75b9f 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -316,9 +316,10 @@ and extract_ind env kn = (* kn is supposed to be in long form *) (* their type var list. *) let packets = Array.map - (fun mip -> - let b = mip.mind_sort <> (Prop Null) in - let s,v = if b then type_sign_vl env mip.mind_nf_arity else [],[] in + (fun mip -> + let b = snd (mind_arity mip) <> InProp in + let ar = Inductive.type_of_inductive (mib,mip) in + let s,v = if b then type_sign_vl env ar else [],[] in let t = Array.make (Array.length mip.mind_nf_lc) [] in { ip_typename = mip.mind_typename; ip_consnames = mip.mind_consnames; @@ -397,7 +398,8 @@ and extract_ind env kn = (* kn is supposed to be in long form *) (* Is this record officially declared with its projections ? *) (* If so, we use this information. *) begin try - let n = nb_default_params env mip0.mind_nf_arity in + let n = nb_default_params env (Inductive.type_of_inductive(mib,mip0)) + in List.iter (option_iter (fun kn -> if Cset.mem kn !projs then add_projection n kn)) diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml index 21f977f1c..9e4500686 100644 --- a/contrib/interface/blast.ml +++ b/contrib/interface/blast.ml @@ -86,7 +86,7 @@ let rec def_const_in_term_rec vl x = | Sort(c) -> c | Ind(ind) -> let (mib, mip) = Global.lookup_inductive ind in - mip.mind_sort + new_sort_in_family (inductive_sort_family mip) | Construct(c) -> def_const_in_term_rec vl (mkInd (inductive_of_constructor c)) | Case(_,x,t,a) diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml index b7da5c1b7..ce2ee1e7d 100644 --- a/contrib/interface/showproof.ml +++ b/contrib/interface/showproof.ml @@ -719,7 +719,7 @@ let rec nsortrec vl x = | Sort(c) -> c | Ind(ind) -> let (mib,mip) = lookup_mind_specif vl ind in - mip.mind_sort + new_sort_in_family (inductive_sort_family mip) | Construct(c) -> nsortrec vl (mkInd (inductive_of_constructor c)) | Case(_,x,t,a) diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index 871a7f15c..2235be4a0 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -395,7 +395,7 @@ let mk_constant_obj id bo ty variables hyps = ty,params) ;; -let mk_inductive_obj sp packs variables nparams hyps finite = +let mk_inductive_obj sp mib packs variables nparams hyps finite = let module D = Declarations in let hyps = string_list_of_named_context_list hyps in let params = filter_params variables hyps in @@ -406,9 +406,9 @@ let mk_inductive_obj sp packs variables nparams hyps finite = (fun p i -> decr tyno ; let {D.mind_consnames=consnames ; - D.mind_typename=typename ; - D.mind_nf_arity=arity} = p + D.mind_typename=typename } = p in + let arity = Inductive.type_of_inductive (mib,p) in let lc = Inductiveops.arities_of_constructors (Global.env ()) (sp,!tyno) in let cons = (Array.fold_right (fun (name,lc) i -> (name,lc)::i) @@ -524,11 +524,12 @@ let print internal glob_ref kind xml_library_root = G.lookup_constant kn in Cic2acic.Constant kn,mk_constant_obj id val0 typ variables hyps | Ln.IndRef (kn,_) -> + let mib = G.lookup_mind kn in let {D.mind_nparams=nparams; D.mind_packets=packs ; D.mind_hyps=hyps; - D.mind_finite=finite} = G.lookup_mind kn in - Cic2acic.Inductive kn,mk_inductive_obj kn packs variables nparams hyps finite + D.mind_finite=finite} = mib in + Cic2acic.Inductive kn,mk_inductive_obj kn mib packs variables nparams hyps finite | Ln.ConstructRef _ -> Util.anomaly ("print: this should not happen") in diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 8eb29c4dd..17a8d5ac9 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -45,6 +45,13 @@ type constant_body = { (*s Inductive types (internal representation with redundant information). *) +let subst_rel_declaration sub (id,copt,t as x) = + let copt' = option_smartmap (subst_mps sub) copt in + let t' = subst_mps sub t in + if copt == copt' & t == t' then x else (id,copt',t') + +let subst_rel_context sub = list_smartmap (subst_rel_declaration sub) + type recarg = | Norec | Mrec of int @@ -83,6 +90,20 @@ let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p with In (params) : Un := cn1 : Tn1 | ... | cnpn : Tnpn *) +type polymorphic_inductive_arity = { + mind_param_levels : universe option list; + mind_level : universe; +} + +type monomorphic_inductive_arity = { + mind_user_arity : constr; + mind_sort : sorts; +} + +type inductive_arity = +| Monomorphic of monomorphic_inductive_arity +| Polymorphic of polymorphic_inductive_arity + type one_inductive_body = { (* Primitive datas *) @@ -90,8 +111,11 @@ type one_inductive_body = { (* Name of the type: [Ii] *) mind_typename : identifier; - (* Arity of [Ii] with parameters: [forall params, Ui] *) - mind_user_arity : types; + (* Arity context of [Ii] with parameters: [forall params, Ui] *) + mind_arity_ctxt : rel_context; + + (* Arity sort, original user arity, and allowed elim sorts, if monomorphic *) + mind_arity : inductive_arity; (* Names of the constructors: [cij] *) mind_consnames : identifier array; @@ -103,15 +127,9 @@ type one_inductive_body = { (* Derived datas *) - (* Head normalized arity so that the conclusion is a sort *) - mind_nf_arity : types; - (* Number of expected real arguments of the type (no let, no params) *) mind_nrealargs : int; - (* Conclusion of the arity *) - mind_sort : sorts; - (* List of allowed elimination sorts *) mind_kelim : sorts_family list; @@ -172,23 +190,28 @@ type mutual_inductive_body = { let subst_const_body sub cb = { const_hyps = (assert (cb.const_hyps=[]); []); const_body = option_map (subst_constr_subst sub) cb.const_body; - const_type = type_app (subst_mps sub) cb.const_type; + const_type = subst_mps sub cb.const_type; const_body_code = Cemitcodes.subst_to_patch_subst sub cb.const_body_code; (*const_type_code = Cemitcodes.subst_to_patch sub cb.const_type_code;*) const_constraints = cb.const_constraints; const_opaque = cb.const_opaque } +let subst_arity sub = function +| Monomorphic s -> + Monomorphic { + mind_user_arity = subst_mps sub s.mind_user_arity; + mind_sort = s.mind_sort; + } +| Polymorphic s as x -> x + let subst_mind_packet sub mbp = { mind_consnames = mbp.mind_consnames; mind_consnrealdecls = mbp.mind_consnrealdecls; mind_typename = mbp.mind_typename; - mind_nf_lc = - array_smartmap (type_app (subst_mps sub)) mbp.mind_nf_lc; - mind_nf_arity = type_app (subst_mps sub) mbp.mind_nf_arity; - mind_user_lc = - array_smartmap (type_app (subst_mps sub)) mbp.mind_user_lc; - mind_user_arity = type_app (subst_mps sub) mbp.mind_user_arity; - mind_sort = mbp.mind_sort; + mind_nf_lc = array_smartmap (subst_mps sub) mbp.mind_nf_lc; + mind_arity_ctxt = subst_rel_context sub mbp.mind_arity_ctxt; + mind_arity = subst_arity sub mbp.mind_arity; + mind_user_lc = array_smartmap (subst_mps sub) mbp.mind_user_lc; mind_nrealargs = mbp.mind_nrealargs; mind_kelim = mbp.mind_kelim; mind_recargs = subst_wf_paths sub mbp.mind_recargs (*wf_paths*); diff --git a/kernel/declarations.mli b/kernel/declarations.mli index bd689ced3..2cbdc3eb3 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -70,6 +70,20 @@ val subst_wf_paths : substitution -> wf_paths -> wf_paths \end{verbatim} *) +type polymorphic_inductive_arity = { + mind_param_levels : universe option list; + mind_level : universe; +} + +type monomorphic_inductive_arity = { + mind_user_arity : constr; + mind_sort : sorts; +} + +type inductive_arity = +| Monomorphic of monomorphic_inductive_arity +| Polymorphic of polymorphic_inductive_arity + type one_inductive_body = { (* Primitive datas *) @@ -77,8 +91,11 @@ type one_inductive_body = { (* Name of the type: [Ii] *) mind_typename : identifier; - (* Arity of [Ii] with parameters: [forall params, Ui] *) - mind_user_arity : types; + (* Arity context of [Ii] with parameters: [forall params, Ui] *) + mind_arity_ctxt : rel_context; + + (* Arity sort and original user arity if monomorphic *) + mind_arity : inductive_arity; (* Names of the constructors: [cij] *) mind_consnames : identifier array; @@ -90,15 +107,9 @@ type one_inductive_body = { (* Derived datas *) - (* Head normalized arity so that the conclusion is a sort *) - mind_nf_arity : types; - (* Number of expected real arguments of the type (no let, no params) *) mind_nrealargs : int; - (* Conclusion of the arity *) - mind_sort : sorts; - (* List of allowed elimination sorts *) mind_kelim : sorts_family list; diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index d47a796ef..b5de04221 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -119,7 +119,7 @@ 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, 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 *) @@ -143,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 + + 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 -(* [smax] is the max of the sorts of the products of the constructor type *) + u1,u2,u3,w1 <= u1 + u1 w2 <= u2 + u2,u3,w3 <= u3 -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 + From this system of inequations, we shall deduce -let type_one_constructor env_ar_par params arsort c = - let infos = infos_and_sort env_ar_par c in + w1,w2,w3 <= u1 + w1,w2 <= u2 + w1,w2,w3 <= u3 +*) - (* 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 +let inductive_levels arities inds = + let levels = Array.map (function _,_,Type u -> Some u | _ -> None) 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 - (* 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 +(* This (re)computes informations relevant to extraction and the sort of an + arity or type constructor; we do not to recompute universes constraints *) - (infos, full_cstr_type, cst2) +let constraint_list_union = + List.fold_left Constraint.union Constraint.empty -let infer_constructor_packet env_ar params arsort lc = +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. *) @@ -190,50 +199,75 @@ 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 = snd (dest_arity env_params arity.utj_val) 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 (id,full_arity,_) (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' = (id,full_arity,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 = + array_map2 (fun (id,full_arity,cn,info,lc,_) lev -> + let sign, s = dest_arity env full_arity in + let status = match s with + | Type _ -> + (* The polymorphic level is a function of the level of the *) + (* conclusions of the parameters *) + Inr (param_ccls, lev) + | 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) + | Prop _ -> + Inl (info,full_arity,s) in + (id,cn,lc,(sign,status))) + inds ind_min_levels in + + (env_arities, params, inds, cst) (************************************************************************) (************************************************************************) @@ -477,7 +511,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 @@ -509,26 +543,28 @@ let all_sorts = [InProp;InSet;InType] let small_sorts = [InProp;InSet] let logical_sorts = [InProp] -let allowed_sorts issmall isunit = function +let allowed_sorts issmall isunit s = + match family_of_sort s with (* Type: all elimination allowed *) - | Type _ -> all_sorts + | InType -> all_sorts (* Small Set is predicative: all elimination allowed *) - | Prop Pos when issmall -> all_sorts + | InSet when issmall -> all_sorts (* Large Set is necessarily impredicative: forbids large elimination *) - | Prop Pos -> small_sorts + | 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 *) - | Prop Null when isunit -> if issmall then all_sorts else small_sorts + | InProp when isunit -> if issmall then all_sorts else small_sorts (* Other propositions: elimination only to Prop *) - | Prop Null -> logical_sorts + | 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 @@ -542,10 +578,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 @@ -554,8 +587,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 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 @@ -571,16 +615,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; @@ -608,5 +651,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 diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 7896b170a..efae466f8 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -47,6 +47,8 @@ let find_coinductive env c = when not (fst (lookup_mind_specif env ind)).mind_finite -> (ind, l) | _ -> raise Not_found +let inductive_params (mib,_) = mib.mind_nparams + (************************************************************************) (* Build the substitution that replaces Rels by the appropriate *) @@ -80,10 +82,12 @@ let instantiate_params full t args sign = let instantiate_partial_params = instantiate_params false -let full_inductive_instantiate mib params t = - instantiate_params true t params mib.mind_params_ctxt +let full_inductive_instantiate mib params sign = + let dummy = mk_Prop in + let t = mkArity (sign,dummy) in + fst (destArity (instantiate_params true t params mib.mind_params_ctxt)) -let full_constructor_instantiate (((mind,_),mib,_),params) = +let full_constructor_instantiate ((mind,_),(mib,_),params) = let inst_ind = constructor_instantiate mind mib in (fun t -> instantiate_params true (inst_ind t) params mib.mind_params_ctxt) @@ -93,22 +97,6 @@ let full_constructor_instantiate (((mind,_),mib,_),params) = (* Functions to build standard types related to inductive *) -(* 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. Typically, for three inductive types, we could have - - u1,u2,u3,w1 <= u1 - u1 w2 <= u2 - u2,u3,w3 <= u3 - - From this system of inequations, we shall deduce - - w1,w2,w3 <= u1 - w1,w2 <= u2 - w1,w2,w3 <= u3 -*) let number_of_inductives mib = Array.length mib.mind_packets let number_of_constructors mip = Array.length mip.mind_consnames @@ -134,17 +122,6 @@ where Remark: Set (predicative) is encoded as Type(0) *) -let find_constraint levels level_bounds i nci = - if nci = 0 then mk_Prop - else - let level_bounds' = solve_constraints_system levels level_bounds in - let level = level_bounds'.(i) in - if nci = 1 & is_empty_universe level then mk_Prop - else if Univ.is_base level then mk_Set else Type level - -let find_inductive_level env (mib,mip) (_,i) levels level_bounds = - find_constraint levels level_bounds i (number_of_constructors mip) - let set_inductive_level env s t = let sign,s' = dest_prod_assum env t in if family_of_sort s <> family_of_sort (destSort s') then @@ -153,45 +130,69 @@ let set_inductive_level env s t = else t -let constructor_instances env (mib,mip) (_,i) args = - let nargs = Array.length args in - let args = Array.to_list args in - let uargs = - if nargs > mib.mind_nparams_rec then - fst (list_chop mib.mind_nparams_rec args) - else args in - let arities = - Array.map (fun mip -> destArity mip.mind_nf_arity) mib.mind_packets in - (* Compute the minimal type *) - let levels = Array.init - (number_of_inductives mib) (fun _ -> fresh_local_univ ()) in - let arities = list_tabulate (fun i -> - let ctx,s = arities.(i) in - let s = match s with Type _ -> Type (levels.(i)) | s -> s in - (Name mib.mind_packets.(i).mind_typename,None,mkArity (ctx,s))) - (number_of_inductives mib) in - (* Remark: all arities are closed hence no need for lift *) - let env_ar = push_rel_context (List.rev arities) env in - let uargs = List.map (lift (number_of_inductives mib)) uargs in - let lc = - Array.map (fun mip -> - Array.map (fun c -> - instantiate_partial_params c uargs mib.mind_params_ctxt) - mip.mind_nf_lc) - mib.mind_packets in - env_ar, lc, levels - -let is_small_inductive (mip,mib) = is_small (snd (destArity mib.mind_nf_arity)) - -let max_inductive_sort v = - let v = Array.map (function - | Type u -> u - | _ -> anomaly "Only type levels when computing the minimal sort of an inductive type") v in - Univ.sup_array v - -(* Type of an inductive type *) - -let type_of_inductive (_,mip) = mip.mind_user_arity +let sort_as_univ = function +| Type u -> u +| Prop Null -> neutral_univ +| Prop Pos -> base_univ + +let rec make_subst env exp act = + match exp, act with + (* Bind expected levels of parameters to actual levels *) + | None :: exp, _ :: act -> + make_subst env exp act + | Some u :: exp, t :: act -> + (u, sort_as_univ (snd (dest_arity env t))) :: make_subst env exp act + (* Not enough parameters, create a fresh univ *) + | Some u :: exp, [] -> + (u, fresh_local_univ ()) :: make_subst env exp [] + | None :: exp, [] -> + make_subst env exp [] + (* Uniform parameters are exhausted *) + | [], _ -> [] + +let sort_of_instantiated_universe mip subst level = + let level = subst_large_constraints subst level in + let nci = number_of_constructors mip in + if nci = 0 then mk_Prop + else + if is_empty_univ level then if nci = 1 then mk_Prop else mk_Set + else if is_base_univ level then mk_Set + else Type level + +let instantiate_inductive_with_param_levels env ar mip paramtyps = + let args = Array.to_list paramtyps in + let subst = make_subst env ar.mind_param_levels args in + sort_of_instantiated_universe mip subst ar.mind_level + +let type_of_applied_inductive env mip paramtyps = + match mip.mind_arity with + | Monomorphic s -> + s.mind_user_arity + | Polymorphic ar -> + let s = instantiate_inductive_with_param_levels env ar mip paramtyps in + mkArity (mip.mind_arity_ctxt,s) + +(* The max of an array of universes *) + +let cumulate_constructor_univ u = function + | Prop Null -> u + | Prop Pos -> sup base_univ u + | Type u' -> sup u u' + +let max_inductive_sort = + Array.fold_left cumulate_constructor_univ neutral_univ + +(* Type of a (non applied) inductive type *) + +let type_of_inductive (_,mip) = + match mip.mind_arity with + | Monomorphic s -> s.mind_user_arity + | Polymorphic s -> + let subst = map_succeed (function + | Some u -> (u, fresh_local_univ ()) + | None -> failwith "") s.mind_param_levels in + let s = mkSort (sort_of_instantiated_universe mip subst s.mind_level) in + it_mkProd_or_LetIn s mip.mind_arity_ctxt (************************************************************************) (* Type of a constructor *) @@ -215,19 +216,11 @@ let arities_of_constructors ind specif = (************************************************************************) -let is_info_arity env c = - match dest_arity env c with - | (_,Prop Null) -> false - | (_,Prop Pos) -> true - | (_,Type _) -> true - -let error_elim_expln env kp ki = - if is_info_arity env kp && not (is_info_arity env ki) then - NonInformativeToInformative - else - match (kind_of_term kp,kind_of_term ki) with - | Sort (Type _), Sort (Prop _) -> StrongEliminationOnNonSmallType - | _ -> WrongArity +let error_elim_expln kp ki = + match kp,ki with + | (InType | InSet), InProp -> NonInformativeToInformative + | InType, InSet -> StrongEliminationOnNonSmallType (* if Set impredicative *) + | _ -> WrongArity (* Type of case predicates *) @@ -244,9 +237,20 @@ let local_rels ctxt = rels (* Get type of inductive, with parameters instantiated *) -let get_arity mib mip params = - let arity = mip.mind_nf_arity in - destArity (full_inductive_instantiate mib params arity) + +let inductive_sort_family mip = + match mip.mind_arity with + | Monomorphic s -> family_of_sort s.mind_sort + | Polymorphic _ -> InType + +let mind_arity mip = + mip.mind_arity_ctxt, inductive_sort_family mip + +let get_instantiated_arity (mib,mip) params = + let sign, s = mind_arity mip in + full_inductive_instantiate mib params sign, s + +let elim_sorts (_,mip) = mip.mind_kelim let rel_list n m = let rec reln l p = @@ -254,66 +258,48 @@ let rel_list n m = in reln [] 1 -let build_dependent_inductive ind mib mip params = +let build_dependent_inductive ind (_,mip) params = let nrealargs = mip.mind_nrealargs in applist (mkInd ind, (List.map (lift nrealargs) params)@(rel_list 0 nrealargs)) - (* This exception is local *) -exception LocalArity of (constr * constr * arity_error) option +exception LocalArity of (sorts_family * sorts_family * arity_error) option -let is_correct_arity env c pj ind mib mip params = - let kelim = mip.mind_kelim in - let arsign,s = get_arity mib mip params in - let nodep_ar = it_mkProd_or_LetIn (mkSort s) arsign in - let rec srec env pt t u = +let check_allowed_sort ksort specif = + if not (List.exists ((=) ksort) (elim_sorts specif)) then + let s = inductive_sort_family (snd specif) in + raise (LocalArity (Some(ksort,s,error_elim_expln ksort s))) + +let is_correct_arity env c pj ind specif params = + let arsign,_ = get_instantiated_arity specif params in + let rec srec env pt ar u = let pt' = whd_betadeltaiota env pt in - let t' = whd_betadeltaiota env t in - match kind_of_term pt', kind_of_term t' with - | Prod (na1,a1,a2), Prod (_,a1',a2') -> + match kind_of_term pt', ar with + | Prod (na1,a1,t), (_,None,a1')::ar' -> let univ = try conv env a1 a1' with NotConvertible -> raise (LocalArity None) in - srec (push_rel (na1,None,a1) env) a2 a2' (Constraint.union u univ) - | Prod (_,a1,a2), _ -> (* whnf of t was not needed here! *) - let k = whd_betadeltaiota env a2 in - let ksort = match kind_of_term k with + srec (push_rel (na1,None,a1) env) t ar' (Constraint.union u univ) + | Prod (_,a1,a2), [] -> (* whnf of t was not needed here! *) + let ksort = match kind_of_term (whd_betadeltaiota env a2) with | Sort s -> family_of_sort s | _ -> raise (LocalArity None) in - - let dep_ind = build_dependent_inductive ind mib mip params - in + let dep_ind = build_dependent_inductive ind specif params in let univ = try conv env a1 dep_ind with NotConvertible -> raise (LocalArity None) in - if List.exists ((=) ksort) kelim then - (true, Constraint.union u univ) - else - raise (LocalArity (Some(k,t',error_elim_expln env k t'))) - | k, Prod (_,_,_) -> + check_allowed_sort ksort specif; + (true, Constraint.union u univ) + | Sort s', [] -> + check_allowed_sort (family_of_sort s') specif; + (false, u) + | _ -> raise (LocalArity None) - | k, ki -> - let ksort = match k with - | Sort s -> family_of_sort s - | _ -> raise (LocalArity None) in - if List.exists ((=) ksort) kelim then - (false, u) - else - raise (LocalArity (Some(pt',t',error_elim_expln env pt' t'))) in - try srec env pj.uj_type nodep_ar Constraint.empty + try srec env pj.uj_type (List.rev arsign) Constraint.empty with LocalArity kinds -> - let create_sort = function - | InProp -> mkProp - | InSet -> mkSet - | InType -> mkSort type_0 in - let listarity = List.map create_sort kelim -(* let listarity = - (List.map (fun s -> make_arity env true indf (create_sort s)) kelim) - @(List.map (fun s -> make_arity env false indf (create_sort s)) kelim)*) - in - error_elim_arity env ind listarity c pj kinds + error_elim_arity env ind (elim_sorts specif) c pj kinds (************************************************************************) @@ -321,13 +307,13 @@ let is_correct_arity env c pj ind mib mip params = (* [p] is the predicate, [i] is the constructor number (starting from 0), and [cty] is the type of the constructor (params not instantiated) *) -let build_branches_type ind mib mip params dep p = +let build_branches_type ind (_,mip as specif) params dep p = let build_one_branch i cty = - let typi = full_constructor_instantiate ((ind,mib,mip),params) cty in + let typi = full_constructor_instantiate (ind,specif,params) cty in let (args,ccl) = decompose_prod_assum typi in let nargs = rel_context_length args in let (_,allargs) = decompose_app ccl in - let (lparams,vargs) = list_chop mib.mind_nparams allargs in + let (lparams,vargs) = list_chop (inductive_params specif) allargs in let cargs = if dep then let cstr = ith_constructor_of_inductive ind (i+1) in @@ -346,12 +332,12 @@ let build_case_type dep p c realargs = beta_appvect p (Array.of_list args) let type_case_branches env (ind,largs) pj c = - let (mib,mip) = lookup_mind_specif env ind in - let nparams = mib.mind_nparams in + let specif = lookup_mind_specif env ind in + let nparams = inductive_params specif in let (params,realargs) = list_chop nparams largs in let p = pj.uj_val in - let (dep,univ) = is_correct_arity env c pj ind mib mip params in - let lc = build_branches_type ind mib mip params dep p in + let (dep,univ) = is_correct_arity env c pj ind specif params in + let lc = build_branches_type ind specif params dep p in let ty = build_case_type dep p c realargs in (lc, ty, univ) diff --git a/kernel/inductive.mli b/kernel/inductive.mli index b4adbf093..c0a138bde 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -38,6 +38,8 @@ val lookup_mind_specif : env -> inductive -> mind_specif val type_of_inductive : mind_specif -> types +val elim_sorts : mind_specif -> sorts_family list + (* Return type as quoted by the user *) val type_of_constructor : constructor -> mind_specif -> types @@ -58,6 +60,11 @@ val type_case_branches : env -> inductive * constr list -> unsafe_judgment -> constr -> types array * types * constraints +(* Return the arity of an inductive type *) +val mind_arity : one_inductive_body -> Sign.rel_context * sorts_family + +val inductive_sort_family : one_inductive_body -> sorts_family + (* Check a [case_info] actually correspond to a Case expression on the given inductive type. *) val check_case_info : env -> inductive -> case_info -> unit @@ -68,16 +75,11 @@ val check_cofix : env -> cofixpoint -> unit (*s Support for sort-polymorphic inductive types *) -val constructor_instances : env -> mind_specif -> inductive -> - constr array -> env * types array array * universe array +val type_of_applied_inductive : + env -> one_inductive_body -> types array -> types val set_inductive_level : env -> sorts -> types -> types -val find_inductive_level : env -> mind_specif -> inductive -> - universe array -> universe array -> sorts - -val is_small_inductive : mind_specif -> bool - val max_inductive_sort : sorts array -> universe (***************************************************************) diff --git a/kernel/reduction.ml b/kernel/reduction.ml index e72942608..5b69ac7b6 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -438,7 +438,7 @@ let dest_prod_assum env = prodec_rec env Sign.empty_rel_context let dest_arity env c = - let l, c = dest_prod env c in + let l, c = dest_prod_assum env c in match kind_of_term c with | Sort s -> l,s | _ -> error "not an arity" diff --git a/kernel/sign.ml b/kernel/sign.ml index dbf52498d..52af09b5a 100644 --- a/kernel/sign.ml +++ b/kernel/sign.ml @@ -191,3 +191,4 @@ let decompose_lam_n_assum n = | c -> error "decompose_lam_n_assum: not enough abstractions" in lamdec_rec empty_rel_context n + diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 0c339e8b8..6de7819af 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -89,14 +89,15 @@ let check_inductive cst env msid1 l info1 mib2 spec2 = (* nf_arity later *) (* user_lc ignored *) (* user_arity ignored *) - let cst = check_conv cst conv_sort env p1.mind_sort p2.mind_sort in check (fun p -> p.mind_nrealargs); (* kelim ignored *) (* listrec ignored *) (* finite done *) (* nparams done *) (* params_ctxt done *) - let cst = check_conv cst conv env p1.mind_nf_arity p2.mind_nf_arity in + (* Don't check the sort of the type if polymorphic *) + let cst = check_conv cst conv env (type_of_inductive (mib1,p1)) (type_of_inductive (mib2,p2)) + in cst in let check_cons_types i cst p1 p2 = @@ -181,7 +182,7 @@ let check_constant cst env msid1 l info1 cb2 spec2 = "name.") ; assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ; if cb2.const_body <> None then error () ; - let arity1 = mind1.mind_packets.(i).mind_user_arity in + let arity1 = type_of_inductive (mind1,mind1.mind_packets.(i)) in check_conv cst conv_leq env arity1 cb2.const_type | IndConstr (((kn,i),j) as cstr,mind1) -> Util.error ("The kernel does not recognize yet that a parameter can be " ^ diff --git a/kernel/term.ml b/kernel/term.ml index 87c319a1b..f59a6c183 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -769,17 +769,16 @@ let substkey = Profile.declare_profile "substn_many";; let substn_many lamv n c = Profile.profile3 substkey substn_many lamv n c;; *) -let substnl laml k = - substn_many (Array.map make_substituend (Array.of_list laml)) k -let substl laml = - substn_many (Array.map make_substituend (Array.of_list laml)) 0 +let substnl laml n = + substn_many (Array.map make_substituend (Array.of_list laml)) n +let substl laml = substnl laml 0 let subst1 lam = substl [lam] -let substl_decl laml (id,bodyopt,typ) = - match bodyopt with - | None -> (id,None,substl laml typ) - | Some body -> (id, Some (substl laml body), type_app (substl laml) typ) +let substnl_decl laml k (id,bodyopt,typ) = + (id,option_map (substnl laml k) bodyopt,substnl laml k typ) +let substl_decl laml = substnl_decl laml 0 let subst1_decl lam = substl_decl [lam] +let subst1_named_decl = subst1_decl (* (thin_val sigma) removes identity substitutions from sigma *) diff --git a/kernel/term.mli b/kernel/term.mli index 160ef767b..0982ee456 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -460,8 +460,11 @@ val substnl : constr list -> int -> constr -> constr val substl : constr list -> constr -> constr val subst1 : constr -> constr -> constr -val substl_decl : constr list -> named_declaration -> named_declaration -val subst1_decl : constr -> named_declaration -> named_declaration +val substnl_decl : constr list -> int -> rel_declaration -> rel_declaration +val substl_decl : constr list -> rel_declaration -> rel_declaration +val subst1_decl : constr -> rel_declaration -> rel_declaration + +val subst1_named_decl : constr -> named_declaration -> named_declaration val replace_vars : (identifier * constr) list -> constr -> constr val subst_var : identifier -> constr -> constr diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index 7049a8afe..bbd3e4bf4 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -45,8 +45,8 @@ type type_error = | NotAType of unsafe_judgment | BadAssumption of unsafe_judgment | ReferenceVariables of constr - | ElimArity of inductive * types list * constr * unsafe_judgment - * (constr * constr * arity_error) option + | ElimArity of inductive * sorts_family list * constr * unsafe_judgment + * (sorts_family * sorts_family * arity_error) option | CaseNotInductive of unsafe_judgment | WrongCaseInfo of inductive * case_info | NumberBranches of unsafe_judgment * int diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index ffa16968c..6e480479e 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -47,8 +47,8 @@ type type_error = | NotAType of unsafe_judgment | BadAssumption of unsafe_judgment | ReferenceVariables of constr - | ElimArity of inductive * types list * constr * unsafe_judgment - * (constr * constr * arity_error) option + | ElimArity of inductive * sorts_family list * constr * unsafe_judgment + * (sorts_family * sorts_family * arity_error) option | CaseNotInductive of unsafe_judgment | WrongCaseInfo of inductive * case_info | NumberBranches of unsafe_judgment * int @@ -75,8 +75,8 @@ val error_assumption : env -> unsafe_judgment -> 'a val error_reference_variables : env -> constr -> 'a val error_elim_arity : - env -> inductive -> types list -> constr - -> unsafe_judgment -> (constr * constr * arity_error) option -> 'a + env -> inductive -> sorts_family list -> constr -> unsafe_judgment -> + (sorts_family * sorts_family * arity_error) option -> 'a val error_case_not_inductive : env -> unsafe_judgment -> 'a diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 29ec5007a..435b3e31c 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -245,14 +245,16 @@ let judge_of_cast env cj k tj = (* Inductive types. *) -let judge_of_inductive env i = - let constr = mkInd i in - let _ = - let (kn,_) = i in - let mib = lookup_mind kn env in - check_args env constr mib.mind_hyps in - let specif = lookup_mind_specif env i in - make_judge constr (type_of_inductive specif) +let judge_of_applied_inductive env ind jl = + let c = mkInd ind in + let (mib,mip) = lookup_mind_specif env ind in + check_args env c mib.mind_hyps; + let paramstyp = Array.map (fun j -> j.uj_type) jl in + let t = Inductive.type_of_applied_inductive env mip paramstyp in + make_judge c t + +let judge_of_inductive env ind = + judge_of_applied_inductive env ind [||] (* Constructors. *) @@ -334,14 +336,15 @@ let rec execute env cstr cu = (* Lambda calculus operators *) | App (f,args) -> - let (j,cu1) = execute env f cu in - let (jl,cu2) = execute_array env args cu1 in - let (j',cu) = univ_combinator cu2 (judge_of_apply env j jl) in - if isInd f then - (* Sort-polymorphism of inductive types *) - adjust_inductive_level env (destInd f) args (j',cu) - else - (j',cu) + let (jl,cu1) = execute_array env args cu in + let (j,cu2) = + if isInd f then + (* Sort-polymorphism of inductive types *) + judge_of_applied_inductive env (destInd f) jl, cu1 + else + execute env f cu1 + in + univ_combinator cu2 (judge_of_apply env j jl) | Lambda (name,c1,c2) -> let (varj,cu1) = execute_type env c1 cu in @@ -421,22 +424,6 @@ and execute_array env = array_fold_map' (execute env) and execute_list env = list_fold_map' (execute env) -and adjust_inductive_level env ind args (j,cu) = - let specif = lookup_mind_specif env ind in - if is_small_inductive specif then - (* No polymorphism *) - (j,cu) - else - (* Retyping constructor with the actual arguments *) - let env',llc,ls0 = constructor_instances env specif ind args in - let (llj,cu1) = array_fold_map' (execute_array env') llc cu in - let ls = - Array.map (fun lj -> - max_inductive_sort (Array.map (sort_judgment env) lj)) llj - in - let s = find_inductive_level env specif ind ls0 ls in - (on_judgment_type (set_inductive_level env s) j, cu1) - (* Derived functions *) let infer env constr = let (j,(cst,_)) = diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 412998f6e..25f7d15db 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -78,6 +78,9 @@ val judge_of_cast : val judge_of_inductive : env -> inductive -> unsafe_judgment +val judge_of_applied_inductive : + env -> inductive -> unsafe_judgment array -> unsafe_judgment + val judge_of_constructor : env -> constructor -> unsafe_judgment (*s Type of Cases. *) diff --git a/kernel/univ.ml b/kernel/univ.ml index 1e0991e3d..906354b04 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -8,6 +8,10 @@ (* $Id$ *) +(* Initial Caml version originates from CoC 4.8 [Dec 1988] *) +(* Extension with algebraic universes by HH [Sep 2001] *) +(* Additional support for sort-polymorphic inductive types by HH [Mar 2006] *) + (* Universes are stratified by a partial ordering $\le$. Let $\~{}$ be the associated equivalence. We also have a strict ordering $<$ between equivalence classes, and we maintain that $<$ is acyclic, @@ -92,7 +96,7 @@ let sup u v = let gtl'' = list_union gtl gtl' in Max (list_subtract gel'' gtl'',gtl'') -let sup_array ls = Array.fold_right sup ls (Max ([],[])) +let neutral_univ = Max ([],[]) (* Comparison on this type is pointer equality *) type canonical_arc = @@ -125,7 +129,7 @@ let declare_univ u g = (* The level of Set *) let base_univ = Atom Base -let is_base = function +let is_base_univ = function | Atom Base -> true | Max ([Base],[]) -> warning "Non canonical Set"; true | u -> false @@ -428,11 +432,11 @@ let make_max = function | ([u],[]) -> Atom u | (le,lt) -> Max (le,lt) -let remove_constraint u = function +let remove_large_constraint u = function | Atom u' as x -> if u = u' then Max ([],[]) else x | Max (le,lt) -> make_max (list_remove u le,lt) -let is_empty_universe = function +let is_empty_univ = function | Max ([],[]) -> true | _ -> false @@ -454,22 +458,40 @@ where - the wi are arbitrary complex universes that do not mention the ui. *) +let is_direct_sort_constraint s v = match s with + | Some u -> is_direct_constraint u v + | None -> false + let solve_constraints_system levels level_bounds = let levels = - Array.map (function Atom u -> u | _ -> anomaly "expects Atom") levels in + Array.map (option_map (function Atom u -> u | _ -> anomaly "expects Atom")) + levels in let v = Array.copy level_bounds in let nind = Array.length v in for i=0 to nind-1 do for j=0 to nind-1 do - if i<>j & is_direct_constraint levels.(j) v.(i) then - v.(i) <- sup v.(i) v.(j) + if i<>j & is_direct_sort_constraint levels.(j) v.(i) then + v.(i) <- sup v.(i) level_bounds.(j) done; for j=0 to nind-1 do - v.(i) <- remove_constraint levels.(j) v.(i) + match levels.(j) with + | Some u -> v.(i) <- remove_large_constraint u v.(i) + | None -> () done done; v +let subst_large_constraint u u' v = + match u with + | Atom u -> + if is_direct_constraint u v then sup u' (remove_large_constraint u v) + else v + | _ -> + anomaly "expect a universe level" + +let subst_large_constraints = + List.fold_right (fun (u,u') -> subst_large_constraint u u') + (* Pretty-printing *) let num_universes g = diff --git a/kernel/univ.mli b/kernel/univ.mli index 0fb1a4ca8..a7d27f47c 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -14,9 +14,10 @@ type universe val base_univ : universe val prop_univ : universe +val neutral_univ : universe val make_univ : Names.dir_path * int -> universe -val is_base : universe -> bool +val is_base_univ : universe -> bool (* The type of a universe *) val super : universe -> universe @@ -24,9 +25,6 @@ val super : universe -> universe (* The max of 2 universes *) val sup : universe -> universe -> universe -(* The max of an array of universes *) -val sup_array : universe array -> universe - (*s Graphs of universes. *) type universes @@ -58,10 +56,15 @@ val merge_constraints : constraints -> universes -> universes val fresh_local_univ : unit -> universe -val solve_constraints_system : universe array -> universe array -> +val solve_constraints_system : universe option array -> universe array -> universe array -val is_empty_universe : universe -> bool +val is_empty_univ : universe -> bool + +val subst_large_constraint : universe -> universe -> universe -> universe + +val subst_large_constraints : + (universe * universe) list -> universe -> universe (*s Pretty-printing of universes. *) diff --git a/kernel/vconv.ml b/kernel/vconv.ml index f038c04f1..653f8978c 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -342,8 +342,8 @@ let constr_type_of_idkey env idkey = mkRel n, lift n ty let type_of_ind env ind = - let (_,mip) = Inductive.lookup_mind_specif env ind in - mip.mind_nf_arity + let specif = Inductive.lookup_mind_specif env ind in + Inductive.type_of_inductive specif let build_branches_type (mind,_ as _ind) mib mip params dep p rtbl = (* [build_one_branch i cty] construit le type de la ieme branche (commence @@ -461,7 +461,8 @@ and nf_stk env c t stk = in let aux = nf_predicate env (type_of_switch sw) - (hnf_prod_applist env mip.mind_nf_arity (Array.to_list params)) in + (hnf_prod_applist env (type_of_ind env ind) (Array.to_list params)) + in !dep,aux in (* Calcul du type des branches *) let btypes = diff --git a/library/impargs.ml b/library/impargs.ml index 404e06f99..ffdeb0b88 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -282,14 +282,15 @@ let compute_mib_implicits kn = let ar = Array.to_list (Array.map (* No need to lift, arities contain no de Bruijn *) - (fun mip -> (Name mip.mind_typename, None, mip.mind_user_arity)) + (fun mip -> (Name mip.mind_typename, None, type_of_inductive (mib,mip))) mib.mind_packets) in let env_ar = push_rel_context ar env in let imps_one_inductive i mip = let ind = (kn,i) in - ((IndRef ind,auto_implicits env (body_of_type mip.mind_user_arity)), + let ar = type_of_inductive (mib,mip) in + ((IndRef ind,auto_implicits env ar), Array.mapi (fun j c -> (ConstructRef (ind,j+1),auto_implicits env_ar c)) - mip.mind_user_lc) + mip.mind_nf_lc) in Array.mapi imps_one_inductive mib.mind_packets diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 593595a23..d05f4ffd4 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -278,11 +278,11 @@ let print_constructors envpar names types = hv 0 (str " " ++ pc) let build_inductive sp tyi = - let (mib,mip) = Global.lookup_inductive (sp,tyi) in + let (mib,mip as specif) = Global.lookup_inductive (sp,tyi) in let params = mib.mind_params_ctxt in let args = extended_rel_list 0 params in let env = Global.env() in - let arity = hnf_prod_applist env mip.mind_user_arity args in + let arity = hnf_prod_applist env (Inductive.type_of_inductive specif) args in let cstrtypes = arities_of_constructors env (sp,tyi) in let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 39b26a2b7..7a77d6eab 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -313,16 +313,21 @@ let rec find_row_ind = function | PatCstr(loc,c,_,_) :: _ -> Some (loc,c) let inductive_template isevars env tmloc ind = - let (mib,mip) = Inductive.lookup_mind_specif env ind in - let (ntys,_) = splay_prod env (Evd.evars_of !isevars) mip.mind_nf_arity in + let arsign = get_full_arity_sign env ind in let hole_source = match tmloc with | Some loc -> fun i -> (loc, Evd.TomatchTypeParameter (ind,i)) | None -> fun _ -> (dummy_loc, Evd.InternalHole) in - let (evarl,_) = + let (_,evarl,_) = List.fold_right - (fun (na,ty) (evl,n) -> - (e_new_evar isevars env ~src:(hole_source n) (substl evl ty))::evl,n+1) - ntys ([],1) in + (fun (na,b,ty) (subst,evarl,n) -> + match b with + | None -> + let ty' = substl subst ty in + let e = e_new_evar isevars env ~src:(hole_source n) ty' in + (e::subst,e::evarl,n+1) + | Some b -> + (b::subst,evarl,n+1)) + arsign ([],[],1) in applist (mkInd ind,List.rev evarl) let inh_coerce_to_ind isevars env ty tyi = diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index ef6fccfc4..f3e3b6d2c 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -48,13 +48,13 @@ let mkLambda_string s t c = mkLambda (Name (id_of_string s), t, c) lift_constructor et lift_inductive_family qui ne se contentent pas de lifter les paramètres globaux *) -let mis_make_case_com depopt env sigma (ind,mib,mip) kind = +let mis_make_case_com depopt env sigma ind (mib,mip as specif) kind = let lnamespar = mib.mind_params_ctxt in let dep = match depopt with - | None -> mip.mind_sort <> (Prop Null) + | None -> inductive_sort_family mip <> InProp | Some d -> d in - if not (List.exists ((=) kind) mip.mind_kelim) then + if not (List.mem kind (elim_sorts specif)) then raise (RecursionSchemeError (NotAllowedCaseAnalysis @@ -431,7 +431,7 @@ let mis_make_indrec env sigma listdepkind mib = it_mkLambda_or_LetIn_name env (put_arity env' 0 listdepkind) lnamesparrec else - mis_make_case_com (Some dep) env sigma (indi,mibi,mipi) kind + mis_make_case_com (Some dep) env sigma indi (mibi,mipi) kind in (* Body of mis_make_indrec *) list_tabulate make_one_rec nrec @@ -441,7 +441,7 @@ let mis_make_indrec env sigma listdepkind mib = let make_case_com depopt env sigma ity kind = let (mib,mip) = lookup_mind_specif env ity in - mis_make_case_com depopt env sigma (ity,mib,mip) kind + mis_make_case_com depopt env sigma ity (mib,mip) kind let make_case_dep env = make_case_com (Some true) env let make_case_nodep env = make_case_com (Some false) env @@ -504,7 +504,7 @@ let check_arities listdepkind = let _ = List.fold_left (fun ln ((_,ni),mibi,mipi,dep,kind) -> let id = mipi.mind_typename in - let kelim = mipi.mind_kelim in + let kelim = elim_sorts (mibi,mipi) in if not (List.exists ((=) kind) kelim) then raise (RecursionSchemeError (BadInduction (dep,id,new_sort_in_family kind))) else if List.mem ni ln then raise @@ -534,7 +534,7 @@ let build_mutual_indrec env sigma = function let build_indrec env sigma ind = let (mib,mip) = lookup_mind_specif env ind in - let kind = family_of_sort mip.mind_sort in + let kind = inductive_sort_family mip in let dep = kind <> InProp in List.hd (mis_make_indrec env sigma [(ind,mib,mip,dep,kind)] mib) @@ -596,7 +596,7 @@ let lookup_eliminator ind_sp s = pr_id id ++ spc () ++ str "The elimination of the inductive definition " ++ pr_id id ++ spc () ++ str "on sort " ++ - spc () ++ print_sort_family s ++ + spc () ++ pr_sort_family s ++ str " is probably not allowed") @@ -617,6 +617,6 @@ let lookup_eliminator ind_sp s = pr_id id ++ spc () ++ str "The elimination of the inductive definition " ++ pr_id base ++ spc () ++ str "on sort " ++ - spc () ++ print_sort_family s ++ + spc () ++ pr_sort_family s ++ str " is probably not allowed") *) diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 1c290e877..737bb18ed 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -116,6 +116,10 @@ let constructor_nrealhyps env (ind,j) = let (mib,mip) = Inductive.lookup_mind_specif env ind in mip.mind_consnrealdecls.(j-1) +let get_full_arity_sign env ind = + let (mib,mip) = Inductive.lookup_mind_specif env ind in + mip.mind_arity_ctxt + (* Length of arity (w/o local defs) *) let inductive_nargs env ind = @@ -196,10 +200,40 @@ let rec instantiate args c = match kind_of_term c, args with | _, [] -> c | _ -> anomaly "too short arity" +(* substitution in a signature *) + +let substnl_rel_context subst n sign = + let rec aux n = function + | d::sign -> substnl_decl subst n d :: aux (n+1) sign + | [] -> [] + in List.rev (aux n (List.rev sign)) + +let substl_rel_context subst = substnl_rel_context subst 0 + +let rec instantiate_context sign args = + let rec aux subst = function + | (_,None,_)::sign, a::args -> aux (a::subst) (sign,args) + | (_,Some b,_)::sign, args -> aux (substl subst b::subst) (sign,args) + | [], [] -> subst + | _ -> anomaly "Signature/instance mismatch in inductive family" + in aux [] (List.rev sign,args) + let get_arity env (ind,params) = let (mib,mip) = Inductive.lookup_mind_specif env ind in - let arity = mip.mind_nf_arity in - destArity (instantiate params arity) + let parsign = + (* Dynamically detect if called with an instance of recursively + uniform parameter only or also of non recursively uniform + parameters *) + let parsign = mib.mind_params_ctxt in + let nnonrecparams = mib.mind_nparams - mib.mind_nparams_rec in + if List.length params = rel_context_nhyps parsign - nnonrecparams then + snd (list_chop nnonrecparams mib.mind_params_ctxt) + else + parsign in + let arproperlength = List.length mip.mind_arity_ctxt - List.length parsign in + let arsign,_ = list_chop arproperlength mip.mind_arity_ctxt in + let subst = instantiate_context parsign params in + (substl_rel_context subst arsign, Inductive.inductive_sort_family mip) (* Functions to build standard types related to inductive *) let build_dependent_constructor cs = @@ -284,12 +318,12 @@ let find_coinductive env sigma c = (* find appropriate names for pattern variables. Useful in the Case and Inversion (case_then_using et case_nodep_then_using) tactics. *) -let is_predicate_explicitly_dep env pred nodep_ar = - let rec srec env pval nodep_ar = +let is_predicate_explicitly_dep env pred arsign = + let rec srec env pval arsign = let pv' = whd_betadeltaiota env Evd.empty pval in - match kind_of_term pv', kind_of_term nodep_ar with - | Lambda (na,t,b), Prod (_,_,a') -> - srec (push_rel_assum (na,t) env) b a' + match kind_of_term pv', arsign with + | Lambda (na,t,b), (_,None,_)::arsign -> + srec (push_rel_assum (na,t) env) b arsign | Lambda (na,_,_), _ -> (* The following code has impact on the introduction names @@ -317,12 +351,11 @@ let is_predicate_explicitly_dep env pred nodep_ar = | _ -> anomaly "Non eta-expanded dep-expanded \"match\" predicate" in - srec env pred nodep_ar + srec env pred arsign let is_elim_predicate_explicitly_dependent env pred indf = - let arsign,s = get_arity env indf in - let glob_t = it_mkProd_or_LetIn (mkSort s) arsign in - is_predicate_explicitly_dep env pred glob_t + let arsign,_ = get_arity env indf in + is_predicate_explicitly_dep env pred arsign let set_names env n brty = let (ctxt,cl) = decompose_prod_n_assum n brty in diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index b4acaafbb..f84c95c6a 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -13,6 +13,7 @@ open Term open Declarations open Environ open Evd +open Sign (* The following three functions are similar to the ones defined in Inductive, but they expect an env *) @@ -42,8 +43,7 @@ val dest_ind_type : inductive_type -> inductive_family * constr list val map_inductive_type : (constr -> constr) -> inductive_type -> inductive_type val liftn_inductive_type : int -> int -> inductive_type -> inductive_type val lift_inductive_type : int -> inductive_type -> inductive_type -val substnl_ind_type : - constr list -> int -> inductive_type -> inductive_type +val substnl_ind_type : constr list -> int -> inductive_type -> inductive_type val mkAppliedInd : inductive_type -> constr val mis_is_recursive_subset : int list -> wf_paths -> bool @@ -51,17 +51,22 @@ val mis_is_recursive : inductive * mutual_inductive_body * one_inductive_body -> bool val mis_nf_constructor_type : inductive * mutual_inductive_body * one_inductive_body -> int -> constr -val mis_constr_nargs : inductive -> int array +(* Extract information from an inductive name *) + +val mis_constr_nargs : inductive -> int array val mis_constr_nargs_env : env -> inductive -> int array -val mis_constructor_nargs_env : env -> constructor -> int +(* Return number of expected parameters and of expected real arguments *) +val inductive_nargs : env -> inductive -> int * int +val mis_constructor_nargs_env : env -> constructor -> int val constructor_nrealargs : env -> constructor -> int val constructor_nrealhyps : env -> constructor -> int -(* Return number of expected parameters and of expected real arguments *) -val inductive_nargs : env -> inductive -> int * int +val get_full_arity_sign : env -> inductive -> rel_context + +(* Extract information from an inductive family *) type constructor_summary = { cs_cstr : constructor; @@ -69,17 +74,16 @@ type constructor_summary = { cs_nargs : int; cs_args : Sign.rel_context; cs_concl_realargs : constr array; -} +} val lift_constructor : int -> constructor_summary -> constructor_summary val get_constructor : inductive * mutual_inductive_body * one_inductive_body * constr list -> int -> constructor_summary -val get_arity : env -> inductive_family -> Sign.arity +val get_arity : env -> inductive_family -> rel_context * sorts_family val get_constructors : env -> inductive_family -> constructor_summary array val build_dependent_constructor : constructor_summary -> constr val build_dependent_inductive : env -> inductive_family -> constr -val make_arity_signature : - env -> bool -> inductive_family -> Sign.rel_context +val make_arity_signature : env -> bool -> inductive_family -> Sign.rel_context val make_arity : env -> bool -> inductive_family -> sorts -> types val build_branch_type : env -> bool -> constr -> constructor_summary -> types diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 187a8840c..386d3d5e0 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -846,7 +846,7 @@ let is_arity env sigma c = match find_conclusion env sigma c with | Sort _ -> true | _ -> false - + (*************************************) (* Metas *) diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 776f1313f..2fdb4148a 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -118,17 +118,9 @@ let typeur sigma metamap = | _ -> family_of_sort (decomp_sort env sigma (type_of env t)) and type_of_applied_inductive env ind args = - let specif = lookup_mind_specif env ind in - let t = Inductive.type_of_inductive specif in - if is_small_inductive specif then - (* No polymorphism *) - t - else - (* Retyping constructor with the actual arguments *) - let env',llc,ls0 = constructor_instances env specif ind args in - let lls = Array.map (Array.map (sort_of env')) llc in - let ls = Array.map max_inductive_sort lls in - set_inductive_level env (find_inductive_level env specif ind ls0 ls) t + let (_,mip) = lookup_mind_specif env ind in + let argtyps = Array.map (fun c -> nf_evar sigma (type_of env c)) args in + Inductive.type_of_applied_inductive env mip argtyps in type_of, sort_of, sort_family_of, type_of_applied_inductive diff --git a/pretyping/termops.ml b/pretyping/termops.ml index faf91247e..af90b91d3 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -25,7 +25,7 @@ let print_sort = function | Prop Null -> (str "Prop") | Type u -> (str "Type(" ++ Univ.pr_uni u ++ str ")") -let print_sort_family = function +let pr_sort_family = function | InSet -> (str "Set") | InProp -> (str "Prop") | InType -> (str "Type") diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 5ecd0b685..5bd79a8ee 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -24,7 +24,7 @@ val refresh_universes : types -> types (* printers *) val print_sort : sorts -> std_ppcmds -val print_sort_family : sorts_family -> std_ppcmds +val pr_sort_family : sorts_family -> std_ppcmds (* debug printer: do not use to display terms to the casual user... *) val set_print_constr : (env -> constr -> std_ppcmds) -> unit val print_constr : constr -> std_ppcmds diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 85e75586b..8e10b0aff 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -88,14 +88,16 @@ let rec execute env evd cstr = judge_of_type u | App (f,args) -> - let j = execute env evd f in let jl = execute_array env evd args in - let (j,_) = judge_of_apply env j jl in + let j = if isInd f then (* Sort-polymorphism of inductive types *) - adjust_inductive_level env evd (destInd f) args j + judge_of_applied_inductive env (destInd f) + (jv_nf_evar (evars_of evd) jl) else - j + execute env evd f + in + fst (judge_of_apply env j jl) | Lambda (name,c1,c2) -> let j = execute env evd c1 in @@ -141,25 +143,6 @@ and execute_array env evd = Array.map (execute env evd) and execute_list env evd = List.map (execute env evd) -and adjust_inductive_level env evd ind args j = - let specif = lookup_mind_specif env ind in - if is_small_inductive specif then - (* No polymorphism *) - j - else - (* Retyping constructor with the actual arguments *) - let env',llc,ls0 = constructor_instances env specif ind args in - let llj = Array.map (execute_array env' evd) llc in - let ls = - Array.map (fun lj -> - let ls = - Array.map (fun c -> decomp_sort env (evars_of evd) c.uj_type) lj - in - max_inductive_sort ls) llj - in - let s = find_inductive_level env specif ind ls0 ls in - on_judgment_type (set_inductive_level env s) j - let mcheck env evd c t = let sigma = Evd.evars_of evd in let j = execute env evd (nf_evar sigma c) in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 0314c960c..b86562493 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1001,7 +1001,7 @@ let letin_abstract id c occs gl = then raise (RefinerError (DoesNotOccurIn (c,hyp))) else raise Not_found else - (subst1_decl (mkVar id) newdecl, true) + (subst1_named_decl (mkVar id) newdecl, true) with Not_found -> (d,List.exists (fun ((id,_,_),dep) -> dep && occur_var_in_decl env id d) ctxt) @@ -1053,7 +1053,7 @@ let letin_abstract id c occs gl = then raise (RefinerError (DoesNotOccurIn (c,hyp))) else depdecls else - (subst1_decl (mkVar id) newdecl)::depdecls in + (subst1_named_decl (mkVar id) newdecl)::depdecls in let depdecls = fold_named_context compute_dependency env ~init:[] in let ccl = match occurrences_of_goal occs with | None -> pf_concl gl diff --git a/toplevel/command.ml b/toplevel/command.ml index b70cfb62f..bfead59aa 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -219,7 +219,7 @@ let declare_one_elimination ind = let elim_scheme = Indrec.build_indrec env sigma ind in let npars = mib.mind_nparams_rec in let make_elim s = Indrec.instantiate_indrec_scheme s npars elim_scheme in - let kelim = mip.mind_kelim in + let kelim = elim_sorts (mib,mip) in (* in case the inductive has a type elimination, generates only one induction scheme, the other ones share the same code with the apropriate type *) diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index f10a461d6..ede095fbe 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -73,7 +73,7 @@ let process_inductive sechyps modlist mib = let inds = array_map_to_list (fun mip -> - let arity = expmod_constr modlist mip.mind_user_arity in + let arity = expmod_constr modlist (Termops.refresh_universes (Inductive.type_of_inductive (mib,mip))) in let lc = Array.map (expmod_constr modlist) mip.mind_user_lc in (mip.mind_typename, arity, diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index a67fab04b..4da5d2f53 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -81,14 +81,14 @@ let rec pr_disjunction pr = function | a::l -> pr a ++ str "," ++ spc () ++ pr_disjunction pr l | [] -> assert false -let explain_elim_arity ctx ind aritylst c pj okinds = +let explain_elim_arity ctx ind sorts c pj okinds = let ctx = make_all_name_different ctx in let pi = pr_inductive ctx ind in let pc = pr_lconstr_env ctx c in let msg = match okinds with | Some(kp,ki,explanation) -> - let pki = pr_lconstr_env ctx ki in - let pkp = pr_lconstr_env ctx kp in + let pki = pr_sort_family ki in + let pkp = pr_sort_family kp in let explanation = match explanation with | NonInformativeToInformative -> "proofs can be eliminated only to build proofs" @@ -107,13 +107,10 @@ let explain_elim_arity ctx ind aritylst c pj okinds = hov 0 ( str "Incorrect elimination of" ++ spc() ++ pc ++ spc () ++ str "in the inductive type " ++ spc() ++ quote pi ++ - (let sorts = List.map (fun x -> mkSort (new_sort_in_family x)) - (list_uniquize (List.map (fun ar -> - family_of_sort (destSort (snd (decompose_prod_assum ar)))) aritylst)) in - let ppar = pr_disjunction (pr_lconstr_env ctx) sorts in - let ppt = pr_lconstr_env ctx (snd (decompose_prod_assum pj.uj_type)) in - str "," ++ spc() ++ str "the return type has sort" ++ spc() ++ ppt ++ - spc () ++ str "while it should be " ++ ppar)) + (let ppar = pr_disjunction (fun s -> quote (pr_sort_family s)) sorts in + let ppt = pr_lconstr_env ctx (snd (decompose_prod_assum pj.uj_type)) in + str "," ++ spc() ++ str "the return type has sort" ++ spc() ++ ppt ++ + spc () ++ str "while it should be " ++ ppar)) ++ fnl () ++ msg let explain_case_not_inductive ctx cj = @@ -565,14 +562,14 @@ let error_bad_entry () = let error_not_allowed_case_analysis dep kind i = str (if dep then "Dependent" else "Non Dependent") ++ - str " case analysis on sort: " ++ print_sort kind ++ fnl () ++ + str " case analysis on sort: " ++ pr_sort kind ++ fnl () ++ str "is not allowed for inductive definition: " ++ pr_inductive (Global.env()) i let error_bad_induction dep indid kind = str (if dep then "Dependent" else "Non dependent") ++ str " induction for type " ++ pr_id indid ++ - str " and sort " ++ print_sort kind ++ spc () ++ + str " and sort " ++ pr_sort kind ++ spc () ++ str "is not allowed" let error_not_mutual_in_scheme () = |