diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/indTyping.ml | 365 | ||||
| -rw-r--r-- | kernel/indTyping.mli | 24 | ||||
| -rw-r--r-- | kernel/indtypes.ml | 344 | ||||
| -rw-r--r-- | kernel/indtypes.mli | 7 | ||||
| -rw-r--r-- | kernel/kernel.mllib | 1 |
5 files changed, 392 insertions, 349 deletions
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml new file mode 100644 index 0000000000..8bf34398d7 --- /dev/null +++ b/kernel/indTyping.ml @@ -0,0 +1,365 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open CErrors +open Util +open Names +open Univ +open Term +open Constr +open Vars +open Declarations +open Environ +open Reduction +open Typeops +open Entries +open Pp +open Type_errors +open Context.Rel.Declaration + +let is_constructor_head t = + isRel(fst(decompose_app t)) + +(************************************************************************) +(* Various well-formedness check for inductive declarations *) + +(* [check_constructors_names id s cl] checks that all the constructors names + appearing in [l] are not present in the set [s], and returns the new set + of names. The name [id] is the name of the current inductive type, used + when reporting the error. *) + +let check_constructors_names = + let rec check idset = function + | [] -> idset + | c::cl -> + if Id.Set.mem c idset then + raise (InductiveError (SameNamesConstructors c)) + else + check (Id.Set.add c idset) cl + in + check + +(* [mind_check_names mie] checks the names of an inductive types declaration, + and raises the corresponding exceptions when two types or two constructors + have the same name. *) + +let mind_check_names mie = + let rec check indset cstset = function + | [] -> () + | ind::inds -> + let id = ind.mind_entry_typename in + let cl = ind.mind_entry_consnames in + if Id.Set.mem id indset then + raise (InductiveError (SameNamesTypes id)) + else + let cstset' = check_constructors_names cstset cl in + check (Id.Set.add id indset) cstset' inds + in + check Id.Set.empty Id.Set.empty mie.mind_entry_inds +(* The above verification is not necessary from the kernel point of + vue since inductive and constructors are not referred to by their + name, but only by the name of the inductive packet and an index. *) + +(************************************************************************) +(************************************************************************) + +(* Typing the arities and constructor types *) + +let infos_and_sort env t = + let rec aux env t max = + let t = whd_all env t in + match kind t with + | Prod (name,c1,c2) -> + let varj = infer_type env c1 in + let env1 = Environ.push_rel (LocalAssum (name,varj.utj_val)) env in + let max = Universe.sup max (Sorts.univ_of_sort varj.utj_type) in + aux env1 c2 max + | _ when is_constructor_head t -> max + | _ -> (* don't fail if not positive, it is tested later *) max + in aux env t Universe.type0m + +(* 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 + + 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 +*) + +(* 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_par params lc = + (* type-check the constructors *) + let jlc = List.map (infer_type env_ar_par) lc in + let jlc = Array.of_list jlc in + (* generalize the constructor over the parameters *) + let lc'' = Array.map (fun j -> Term.it_mkProd_or_LetIn j.utj_val params) jlc in + (* compute the max of the sorts of the products of the constructors types *) + let levels = List.map (infos_and_sort env_ar_par) lc in + let min = if Array.length jlc > 1 then Universe.type0 else Universe.type0m in + let level = List.fold_left (fun max l -> Universe.sup max l) min levels in + (lc'', level) + +(* If indices matter *) +let cumulate_arity_large_levels env sign = + fst (List.fold_right + (fun d (lev,env) -> + match d with + | LocalAssum (_,t) -> + let tj = infer_type env t in + let u = Sorts.univ_of_sort tj.utj_type in + (Universe.sup u lev, push_rel d env) + | LocalDef _ -> + lev, push_rel d env) + sign (Universe.type0m,env)) + +let is_impredicative env u = + is_type0m_univ u || (is_type0_univ u && is_impredicative_set env) + +(* Returns the list [x_1, ..., x_n] of levels contributing to template + polymorphism. The elements x_k is None if the k-th parameter (starting + from the most recent and ignoring let-definitions) is not contributing + or is Some u_k if its level is u_k and is contributing. *) +let param_ccls paramsctxt = + let fold acc = function + | (LocalAssum (_, p)) -> + (let c = Term.strip_prod_assum p in + match kind c with + | Sort (Type u) -> Univ.Universe.level u + | _ -> None) :: acc + | LocalDef _ -> acc + in + List.fold_left fold [] paramsctxt + +(* Check arities and constructors *) +let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : types) numparams is_arity = + let numchecked = ref 0 in + let basic_check ev tp = + if !numchecked < numparams then () else conv_leq ev tp (subst tp); + numchecked := !numchecked + 1 + in + let check_typ typ typ_env = + match typ with + | LocalAssum (_, typ') -> + begin + try + basic_check typ_env typ'; Environ.push_rel typ typ_env + with NotConvertible -> + anomaly ~label:"bad inductive subtyping relation" (Pp.str "Invalid subtyping relation") + end + | _ -> anomaly (Pp.str "") + in + let typs, codom = dest_prod env arcn in + let last_env = Context.Rel.fold_outside check_typ typs ~init:env in + if not is_arity then basic_check last_env codom else () + +(* Check that the subtyping information inferred for inductive types in the block is correct. *) +(* This check produces a value of the unit type if successful or raises an anomaly if check fails. *) +let check_subtyping cumi paramsctxt env_ar inds = + let numparams = Context.Rel.nhyps paramsctxt in + let uctx = CumulativityInfo.univ_context cumi in + let new_levels = Array.init (UContext.size uctx) + (fun i -> Level.(make (UGlobal.make DirPath.empty i))) + in + let lmap = Array.fold_left2 (fun lmap u u' -> LMap.add u u' lmap) + LMap.empty (Instance.to_array @@ UContext.instance uctx) new_levels + in + let dosubst = subst_univs_level_constr lmap in + let instance_other = Instance.of_array new_levels in + let constraints_other = Univ.subst_univs_level_constraints lmap (Univ.UContext.constraints uctx) in + let uctx_other = Univ.UContext.make (instance_other, constraints_other) in + let env = Environ.push_context uctx_other env_ar in + let subtyp_constraints = + CumulativityInfo.leq_constraints cumi + (UContext.instance uctx) instance_other + Constraint.empty + in + let env = Environ.add_constraints subtyp_constraints env in + (* process individual inductive types: *) + Array.iter (fun (_id,_cn,lc,(_sign,arity)) -> + match arity with + | RegularArity (_, full_arity, _) -> + check_subtyping_arity_constructor env dosubst full_arity numparams true; + Array.iter (fun cnt -> check_subtyping_arity_constructor env dosubst cnt numparams false) lc + | TemplateArity _ -> + anomaly ~label:"check_subtyping" + Pp.(str "template polymorphism and cumulative polymorphism are not compatible") + ) inds + +(* Type-check an inductive definition. Does not check positivity + conditions. *) +(* TODO check that we don't overgeneralize construcors/inductive arities with + universes that are absent from them. Is it possible? +*) +let typecheck_inductive env mie = + let () = match mie.mind_entry_inds with + | [] -> anomaly (Pp.str "empty inductive types declaration.") + | _ -> () + in + (* Check unicity of names *) + mind_check_names mie; + (* Params are typed-checked here *) + let env' = + match mie.mind_entry_universes with + | Monomorphic_ind_entry ctx -> push_context_set ctx env + | Polymorphic_ind_entry (_, ctx) -> push_context ctx env + | Cumulative_ind_entry (_, cumi) -> push_context (Univ.CumulativityInfo.univ_context cumi) env + in + let env_params = check_context env' mie.mind_entry_params in + let paramsctxt = mie.mind_entry_params in + (* We first type arity of each inductive definition *) + (* This allows building the environment of arities and to share *) + (* the set of constraints *) + let env_arities, rev_arity_list = + List.fold_left + (fun (env_ar,l) ind -> + (* Arities (without params) are typed-checked here *) + let template = ind.mind_entry_template in + let arity = + if isArity ind.mind_entry_arity then + let (ctx,s) = dest_arity env_params ind.mind_entry_arity in + match s with + | Type u when Univ.universe_level u = None -> + (** We have an algebraic universe as the conclusion of the arity, + typecheck the dummy Π ctx, Prop and do a special case for the conclusion. + *) + let proparity = infer_type env_params (mkArity (ctx, Sorts.prop)) in + let (cctx, _) = destArity proparity.utj_val in + (* Any universe is well-formed, we don't need to check [s] here *) + mkArity (cctx, s) + | _ -> + let arity = infer_type env_params ind.mind_entry_arity in + arity.utj_val + else let arity = infer_type env_params ind.mind_entry_arity in + arity.utj_val + in + let (sign, deflev) = dest_arity env_params arity in + let inflev = + (* The level of the inductive includes levels of indices if + in indices_matter mode *) + if indices_matter env + then Some (cumulate_arity_large_levels env_params sign) + else None + 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 full_arity = it_mkProd_or_LetIn arity paramsctxt in + let id = ind.mind_entry_typename in + let env_ar' = + push_rel (LocalAssum (Name id, full_arity)) env_ar in + (* (add_constraints cst2 env_ar) in *) + (env_ar', (id,full_arity,sign @ paramsctxt,template,deflev,inflev)::l)) + (env',[]) + mie.mind_entry_inds in + + 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 paramsctxt env_arities in + + (* Now, we type the constructors (without params) *) + let inds = + List.fold_right2 + (fun ind arity_data inds -> + let (lc',cstrs_univ) = + infer_constructor_packet env_ar_par paramsctxt ind.mind_entry_lc in + let consnames = ind.mind_entry_consnames in + let ind' = (arity_data,consnames,lc',cstrs_univ) in + ind'::inds) + mie.mind_entry_inds + arity_list + ([]) in + + let inds = Array.of_list inds in + + (* Compute/check the sorts of the inductive types *) + + let inds = + Array.map (fun ((id,full_arity,sign,template,def_level,inf_level),cn,lc,clev) -> + let infu = + (** Inferred level, with parameters and constructors. *) + match inf_level with + | Some alev -> Universe.sup clev alev + | None -> clev + in + let full_polymorphic () = + let defu = Sorts.univ_of_sort def_level in + let is_natural = + type_in_type env || (UGraph.check_leq (universes env') infu defu) + in + let _ = + (** Impredicative sort, always allow *) + if is_impredicative env defu then () + else (** Predicative case: the inferred level must be lower or equal to the + declared level. *) + if not is_natural then + anomaly ~label:"check_inductive" + (Pp.str"Incorrect universe " ++ + Universe.pr defu ++ Pp.str " declared for inductive type, inferred level is " + ++ Universe.pr infu ++ Pp.str ".") + in + RegularArity (not is_natural,full_arity,defu) + in + let template_polymorphic () = + let _sign, s = + try dest_arity env full_arity + with NotArity -> raise (InductiveError (NotAnArity (env, full_arity))) + in + let u = Sorts.univ_of_sort s in + (* The polymorphic level is a function of the level of the *) + (* conclusions of the parameters *) + (* We enforce [u >= lev] in case [lev] has a strict upper *) + (* constraints over [u] *) + let b = type_in_type env || UGraph.check_leq (universes env') infu u in + if not b then + anomaly ~label:"check_inductive" + (Pp.str"Incorrect universe " ++ + Universe.pr u ++ Pp.str " declared for inductive type, inferred level is " + ++ Universe.pr clev ++ Pp.str ".") + else + TemplateArity (param_ccls paramsctxt, infu) + in + let arity = + match mie.mind_entry_universes with + | Monomorphic_ind_entry _ -> + if template then template_polymorphic () + else full_polymorphic () + | Polymorphic_ind_entry _ | Cumulative_ind_entry _ -> + if template + then anomaly ~label:"polymorphic_template_ind" + Pp.(strbrk "Template polymorphism and full polymorphism are incompatible.") + else full_polymorphic () + in + (id,cn,lc,(sign,arity))) + inds + in + (* Check that the subtyping information inferred for inductive types in the block is correct. *) + (* This check produces a value of the unit type if successful or raises an anomaly if check fails. *) + let () = + match mie.mind_entry_universes with + | Monomorphic_ind_entry _ -> () + | Polymorphic_ind_entry _ -> () + | Cumulative_ind_entry (_, cumi) -> check_subtyping cumi paramsctxt env_arities inds + in (env_arities, env_ar_par, paramsctxt, inds) diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli new file mode 100644 index 0000000000..b16ada5ee8 --- /dev/null +++ b/kernel/indTyping.mli @@ -0,0 +1,24 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Names +open Constr +open Environ + +val typecheck_inductive : + env -> + Entries.mutual_inductive_entry -> + env * env * rel_context * + (Id.t * Id.t list * types array * + (rel_context * + (bool * types * Univ.Universe.t, + Univ.Level.t option list * Univ.Universe.t) + Declarations.declaration_arity)) + array diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index e0f60a3731..16ba6e81fa 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -11,7 +11,6 @@ open CErrors open Util open Names -open Univ open Term open Constr open Vars @@ -20,9 +19,7 @@ open Declareops open Inductive open Environ open Reduction -open Typeops open Entries -open Pp open Context.Rel.Declaration (* Terminology: @@ -49,9 +46,6 @@ let weaker_noccur_between env x nvars t = if noccur_between x nvars t' then Some t' else None -let is_constructor_head t = - isRel(fst(decompose_app t)) - (************************************************************************) (* Various well-formedness check for inductive declarations *) @@ -68,341 +62,7 @@ type inductive_error = Type_errors.inductive_error = | BadEntry | LargeNonPropInductiveNotInType -exception InductiveError of inductive_error - -(* [check_constructors_names id s cl] checks that all the constructors names - appearing in [l] are not present in the set [s], and returns the new set - of names. The name [id] is the name of the current inductive type, used - when reporting the error. *) - -let check_constructors_names = - let rec check idset = function - | [] -> idset - | c::cl -> - if Id.Set.mem c idset then - raise (InductiveError (SameNamesConstructors c)) - else - check (Id.Set.add c idset) cl - in - check - -(* [mind_check_names mie] checks the names of an inductive types declaration, - and raises the corresponding exceptions when two types or two constructors - have the same name. *) - -let mind_check_names mie = - let rec check indset cstset = function - | [] -> () - | ind::inds -> - let id = ind.mind_entry_typename in - let cl = ind.mind_entry_consnames in - if Id.Set.mem id indset then - raise (InductiveError (SameNamesTypes id)) - else - let cstset' = check_constructors_names cstset cl in - check (Id.Set.add id indset) cstset' inds - in - check Id.Set.empty Id.Set.empty mie.mind_entry_inds -(* The above verification is not necessary from the kernel point of - vue since inductive and constructors are not referred to by their - name, but only by the name of the inductive packet and an index. *) - -(************************************************************************) -(************************************************************************) - -(* Typing the arities and constructor types *) - -let infos_and_sort env t = - let rec aux env t max = - let t = whd_all env t in - match kind t with - | Prod (name,c1,c2) -> - let varj = infer_type env c1 in - let env1 = Environ.push_rel (LocalAssum (name,varj.utj_val)) env in - let max = Universe.sup max (Sorts.univ_of_sort varj.utj_type) in - aux env1 c2 max - | _ when is_constructor_head t -> max - | _ -> (* don't fail if not positive, it is tested later *) max - in aux env t Universe.type0m - -(* 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 - - 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 -*) - -(* 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_par params lc = - (* type-check the constructors *) - let jlc = List.map (infer_type env_ar_par) lc in - let jlc = Array.of_list jlc in - (* generalize the constructor over the parameters *) - let lc'' = Array.map (fun j -> Term.it_mkProd_or_LetIn j.utj_val params) jlc in - (* compute the max of the sorts of the products of the constructors types *) - let levels = List.map (infos_and_sort env_ar_par) lc in - let min = if Array.length jlc > 1 then Universe.type0 else Universe.type0m in - let level = List.fold_left (fun max l -> Universe.sup max l) min levels in - (lc'', level) - -(* If indices matter *) -let cumulate_arity_large_levels env sign = - fst (List.fold_right - (fun d (lev,env) -> - match d with - | LocalAssum (_,t) -> - let tj = infer_type env t in - let u = Sorts.univ_of_sort tj.utj_type in - (Universe.sup u lev, push_rel d env) - | LocalDef _ -> - lev, push_rel d env) - sign (Universe.type0m,env)) - -let is_impredicative env u = - is_type0m_univ u || (is_type0_univ u && is_impredicative_set env) - -(* Returns the list [x_1, ..., x_n] of levels contributing to template - polymorphism. The elements x_k is None if the k-th parameter (starting - from the most recent and ignoring let-definitions) is not contributing - or is Some u_k if its level is u_k and is contributing. *) -let param_ccls paramsctxt = - let fold acc = function - | (LocalAssum (_, p)) -> - (let c = Term.strip_prod_assum p in - match kind c with - | Sort (Type u) -> Univ.Universe.level u - | _ -> None) :: acc - | LocalDef _ -> acc - in - List.fold_left fold [] paramsctxt - -(* Check arities and constructors *) -let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : types) numparams is_arity = - let numchecked = ref 0 in - let basic_check ev tp = - if !numchecked < numparams then () else conv_leq ev tp (subst tp); - numchecked := !numchecked + 1 - in - let check_typ typ typ_env = - match typ with - | LocalAssum (_, typ') -> - begin - try - basic_check typ_env typ'; Environ.push_rel typ typ_env - with NotConvertible -> - anomaly ~label:"bad inductive subtyping relation" (Pp.str "Invalid subtyping relation") - end - | _ -> anomaly (Pp.str "") - in - let typs, codom = dest_prod env arcn in - let last_env = Context.Rel.fold_outside check_typ typs ~init:env in - if not is_arity then basic_check last_env codom else () - -(* Check that the subtyping information inferred for inductive types in the block is correct. *) -(* This check produces a value of the unit type if successful or raises an anomaly if check fails. *) -let check_subtyping cumi paramsctxt env_ar inds = - let numparams = Context.Rel.nhyps paramsctxt in - let uctx = CumulativityInfo.univ_context cumi in - let new_levels = Array.init (UContext.size uctx) - (fun i -> Level.make (Level.UGlobal.make DirPath.empty i)) - in - let lmap = Array.fold_left2 (fun lmap u u' -> LMap.add u u' lmap) - LMap.empty (Instance.to_array @@ UContext.instance uctx) new_levels - in - let dosubst = subst_univs_level_constr lmap in - let instance_other = Instance.of_array new_levels in - let constraints_other = Univ.subst_univs_level_constraints lmap (Univ.UContext.constraints uctx) in - let uctx_other = Univ.UContext.make (instance_other, constraints_other) in - let env = Environ.push_context uctx_other env_ar in - let subtyp_constraints = - CumulativityInfo.leq_constraints cumi - (UContext.instance uctx) instance_other - Constraint.empty - in - let env = Environ.add_constraints subtyp_constraints env in - (* process individual inductive types: *) - Array.iter (fun (_id,_cn,lc,(_sign,arity)) -> - match arity with - | RegularArity (_, full_arity, _) -> - check_subtyping_arity_constructor env dosubst full_arity numparams true; - Array.iter (fun cnt -> check_subtyping_arity_constructor env dosubst cnt numparams false) lc - | TemplateArity _ -> - anomaly ~label:"check_subtyping" - Pp.(str "template polymorphism and cumulative polymorphism are not compatible") - ) inds - -(* Type-check an inductive definition. Does not check positivity - conditions. *) -(* TODO check that we don't overgeneralize construcors/inductive arities with - universes that are absent from them. Is it possible? -*) -let typecheck_inductive env mie = - let () = match mie.mind_entry_inds with - | [] -> anomaly (Pp.str "empty inductive types declaration.") - | _ -> () - in - (* Check unicity of names *) - mind_check_names mie; - (* Params are typed-checked here *) - let env' = - match mie.mind_entry_universes with - | Monomorphic_ind_entry ctx -> push_context_set ctx env - | Polymorphic_ind_entry (_, ctx) -> push_context ctx env - | Cumulative_ind_entry (_, cumi) -> push_context (Univ.CumulativityInfo.univ_context cumi) env - in - let env_params = check_context env' mie.mind_entry_params in - let paramsctxt = mie.mind_entry_params in - (* We first type arity of each inductive definition *) - (* This allows building the environment of arities and to share *) - (* the set of constraints *) - let env_arities, rev_arity_list = - List.fold_left - (fun (env_ar,l) ind -> - (* Arities (without params) are typed-checked here *) - let template = ind.mind_entry_template in - let arity = - if isArity ind.mind_entry_arity then - let (ctx,s) = dest_arity env_params ind.mind_entry_arity in - match s with - | Type u when Univ.universe_level u = None -> - (** We have an algebraic universe as the conclusion of the arity, - typecheck the dummy Π ctx, Prop and do a special case for the conclusion. - *) - let proparity = infer_type env_params (mkArity (ctx, Sorts.prop)) in - let (cctx, _) = destArity proparity.utj_val in - (* Any universe is well-formed, we don't need to check [s] here *) - mkArity (cctx, s) - | _ -> - let arity = infer_type env_params ind.mind_entry_arity in - arity.utj_val - else let arity = infer_type env_params ind.mind_entry_arity in - arity.utj_val - in - let (sign, deflev) = dest_arity env_params arity in - let inflev = - (* The level of the inductive includes levels of indices if - in indices_matter mode *) - if indices_matter env - then Some (cumulate_arity_large_levels env_params sign) - else None - 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 full_arity = it_mkProd_or_LetIn arity paramsctxt in - let id = ind.mind_entry_typename in - let env_ar' = - push_rel (LocalAssum (Name id, full_arity)) env_ar in - (* (add_constraints cst2 env_ar) in *) - (env_ar', (id,full_arity,sign @ paramsctxt,template,deflev,inflev)::l)) - (env',[]) - mie.mind_entry_inds in - - 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 paramsctxt env_arities in - - (* Now, we type the constructors (without params) *) - let inds = - List.fold_right2 - (fun ind arity_data inds -> - let (lc',cstrs_univ) = - infer_constructor_packet env_ar_par paramsctxt ind.mind_entry_lc in - let consnames = ind.mind_entry_consnames in - let ind' = (arity_data,consnames,lc',cstrs_univ) in - ind'::inds) - mie.mind_entry_inds - arity_list - ([]) in - - let inds = Array.of_list inds in - - (* Compute/check the sorts of the inductive types *) - - let inds = - Array.map (fun ((id,full_arity,sign,template,def_level,inf_level),cn,lc,clev) -> - let infu = - (** Inferred level, with parameters and constructors. *) - match inf_level with - | Some alev -> Universe.sup clev alev - | None -> clev - in - let full_polymorphic () = - let defu = Sorts.univ_of_sort def_level in - let is_natural = - type_in_type env || (UGraph.check_leq (universes env') infu defu) - in - let _ = - (** Impredicative sort, always allow *) - if is_impredicative env defu then () - else (** Predicative case: the inferred level must be lower or equal to the - declared level. *) - if not is_natural then - anomaly ~label:"check_inductive" - (Pp.str"Incorrect universe " ++ - Universe.pr defu ++ Pp.str " declared for inductive type, inferred level is " - ++ Universe.pr infu ++ Pp.str ".") - in - RegularArity (not is_natural,full_arity,defu) - in - let template_polymorphic () = - let _sign, s = - try dest_arity env full_arity - with NotArity -> raise (InductiveError (NotAnArity (env, full_arity))) - in - let u = Sorts.univ_of_sort s in - (* The polymorphic level is a function of the level of the *) - (* conclusions of the parameters *) - (* We enforce [u >= lev] in case [lev] has a strict upper *) - (* constraints over [u] *) - let b = type_in_type env || UGraph.check_leq (universes env') infu u in - if not b then - anomaly ~label:"check_inductive" - (Pp.str"Incorrect universe " ++ - Universe.pr u ++ Pp.str " declared for inductive type, inferred level is " - ++ Universe.pr clev ++ Pp.str ".") - else - TemplateArity (param_ccls paramsctxt, infu) - in - let arity = - match mie.mind_entry_universes with - | Monomorphic_ind_entry _ -> - if template then template_polymorphic () - else full_polymorphic () - | Polymorphic_ind_entry _ | Cumulative_ind_entry _ -> - if template - then anomaly ~label:"polymorphic_template_ind" - Pp.(strbrk "Template polymorphism and full polymorphism are incompatible.") - else full_polymorphic () - in - (id,cn,lc,(sign,arity))) - inds - in - (* Check that the subtyping information inferred for inductive types in the block is correct. *) - (* This check produces a value of the unit type if successful or raises an anomaly if check fails. *) - let () = - match mie.mind_entry_universes with - | Monomorphic_ind_entry _ -> () - | Polymorphic_ind_entry _ -> () - | Cumulative_ind_entry (_, cumi) -> check_subtyping cumi paramsctxt env_arities inds - in (env_arities, env_ar_par, paramsctxt, inds) +exception InductiveError = Type_errors.InductiveError (************************************************************************) (************************************************************************) @@ -965,7 +625,7 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r let check_inductive env kn mie = (* First type-check the inductive definition *) - let (env_ar, env_ar_par, paramsctxt, inds) = typecheck_inductive env mie in + let (env_ar, env_ar_par, paramsctxt, inds) = IndTyping.typecheck_inductive env mie in (* Then check positivity conditions *) let chkpos = (Environ.typing_flags env).check_guarded in let (nmr,recargs) = check_positivity ~chkpos kn env_ar_par paramsctxt mie.mind_entry_finite inds in diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index b4879611a3..5e37df6976 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -16,13 +16,6 @@ open Entries (** Inductive type checking and errors *) -(** The different kinds of errors that may result of a malformed inductive - definition. *) - -val infos_and_sort : env -> constr -> Univ.Universe.t - -val check_subtyping_arity_constructor : env -> (constr -> constr) -> types -> int -> bool -> unit - val check_positivity : chkpos:bool -> Names.MutInd.t -> Environ.env -> diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 54c239349d..0b10e788b6 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -39,6 +39,7 @@ Type_errors Modops Inductive Typeops +IndTyping Indtypes Cooking Term_typing |