aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/environ.ml7
-rw-r--r--kernel/environ.mli3
-rw-r--r--kernel/indTyping.ml490
-rw-r--r--kernel/indTyping.mli30
-rw-r--r--kernel/indtypes.ml128
-rw-r--r--kernel/indtypes.mli15
-rw-r--r--kernel/type_errors.ml1
-rw-r--r--kernel/type_errors.mli1
8 files changed, 283 insertions, 392 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 38a428d9a1..77820a301e 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -238,6 +238,13 @@ let is_impredicative_set env =
| ImpredicativeSet -> true
| _ -> false
+let is_impredicative_sort env = function
+ | Sorts.Prop -> true
+ | Sorts.Set -> is_impredicative_set env
+ | Sorts.Type _ -> false
+
+let is_impredicative_univ env u = is_impredicative_sort env (Sorts.sort_of_univ u)
+
let type_in_type env = not (typing_flags env).check_universes
let deactivated_guard env = not (typing_flags env).check_guarded
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 8a2efb2477..6d4d3b282b 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -98,6 +98,9 @@ val type_in_type : env -> bool
val deactivated_guard : env -> bool
val indices_matter : env -> bool
+val is_impredicative_sort : env -> Sorts.t -> bool
+val is_impredicative_univ : env -> Univ.Universe.t -> bool
+
(** is the local context empty *)
val empty_context : env -> bool
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index 8bf34398d7..6976b2019d 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -8,27 +8,19 @@
(* * (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 name unicity.
+ Redundant with safe_typing's add_field checks -> to remove?. *)
(* [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
@@ -67,74 +59,151 @@ let mind_check_names mie =
vue since inductive and constructors are not referred to by their
name, but only by the name of the inductive packet and an index. *)
+
(************************************************************************)
+(************************** Cumulativity checking************************)
(************************************************************************)
-(* 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)
+(* Check arities and constructors *)
+let check_subtyping_arity_constructor env subst arcn numparams is_arity =
+ let numchecked = ref 0 in
+ let basic_check ev tp =
+ if !numchecked < numparams then () else Reduction.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 Reduction.NotConvertible ->
+ CErrors.anomaly ~label:"bad inductive subtyping relation"
+ Pp.(str "Invalid subtyping relation")
+ end
+ | _ -> CErrors.anomaly Pp.(str "")
+ in
+ let typs, codom = Reduction.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 ()
+
+let check_cumulativity univs env_ar params data =
+ let numparams = Context.Rel.nhyps params in
+ let uctx = CumulativityInfo.univ_context univs 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 = Vars.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 univs
+ (UContext.instance uctx) instance_other
+ Constraint.empty
+ in
+ let env = Environ.add_constraints subtyp_constraints env in
+ (* process individual inductive types: *)
+ List.iter (fun (arity,lc) ->
+ check_subtyping_arity_constructor env dosubst arity numparams true;
+ Array.iter (fun cnt -> check_subtyping_arity_constructor env dosubst cnt numparams false) lc)
+ data
+
+(************************************************************************)
+(************************** Type checking *******************************)
+(************************************************************************)
+
+type univ_info = { ind_squashed : bool;
+ ind_min_univ : Universe.t option; (* Some for template *)
+ ind_univ : Universe.t }
+
+let check_univ_leq env u info =
+ let ind_univ = info.ind_univ in
+ if type_in_type env || (UGraph.check_leq (universes env) u ind_univ)
+ then { info with ind_min_univ = Option.map (Universe.sup u) info.ind_min_univ }
+ else if is_impredicative_univ env ind_univ
+ then if Option.is_empty info.ind_min_univ then { info with ind_squashed = true }
+ else raise (InductiveError BadUnivs)
+ else raise (InductiveError BadUnivs)
+
+let check_indices_matter env_params info indices =
+ let check_index d (info,env) =
+ let info = match d with
+ | LocalAssum (_,t) ->
+ (* could be retyping if it becomes available in the kernel *)
+ let tj = Typeops.infer_type env t in
+ check_univ_leq env (Sorts.univ_of_sort tj.utj_type) info
+ | LocalDef _ -> info
+ in
+ info, push_rel d env
+ in
+ if not (indices_matter env_params) then info
+ else fst (Context.Rel.fold_outside ~init:(info,env_params) check_index indices)
+
+(* env_ar contains the inductives before the current ones in the block, and no parameters *)
+let check_arity env_params env_ar ind =
+ let {utj_val=arity;utj_type=_} = Typeops.infer_type env_params ind.mind_entry_arity in
+ let indices, ind_sort = Reduction.dest_arity env_params arity in
+ let ind_min_univ = if ind.mind_entry_template then Some Universe.type0m else None in
+ let univ_info = {ind_squashed=false;ind_min_univ;ind_univ=Sorts.univ_of_sort ind_sort} in
+ let univ_info = check_indices_matter env_params univ_info indices in
+ (* We do not need to generate the universe of the arity with params;
+ 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 arity = it_mkProd_or_LetIn arity (Environ.rel_context env_params) in
+ push_rel (LocalAssum (Name ind.mind_entry_typename, arity)) env_ar,
+ (arity, indices, univ_info)
+
+let check_constructor_univs env_ar_par univ_info (args,_) =
+ (* We ignore the output, positivity will check that it's the expected inductive type *)
+ (* NB: very similar to check_indices_matter but that will change with SProp *)
+ fst (Context.Rel.fold_outside ~init:(univ_info,env_ar_par) (fun d (univ_info,env) ->
+ let univ_info = match d with
+ | LocalDef _ -> univ_info
+ | LocalAssum (_,t) ->
+ (* could be retyping if it becomes available in the kernel *)
+ let tj = Typeops.infer_type env t in
+ check_univ_leq env (Sorts.univ_of_sort tj.utj_type) univ_info
+ in
+ univ_info, push_rel d env)
+ args)
+
+let check_constructors env_ar_par params lc (arity,indices,univ_info) =
+ let lc = Array.map_of_list (fun c -> (Typeops.infer_type env_ar_par c).utj_val) lc in
+ let splayed_lc = Array.map (Reduction.dest_prod_assum env_ar_par) lc in
+ let univ_info = if Array.length lc <= 1 then univ_info
+ else check_univ_leq env_ar_par Univ.Universe.type0 univ_info
+ in
+ let univ_info = Array.fold_left (check_constructor_univs env_ar_par) univ_info splayed_lc in
+ (* generalize the constructors over the parameters *)
+ let lc = Array.map (fun c -> Term.it_mkProd_or_LetIn c params) lc in
+ (arity, lc), (indices, splayed_lc), univ_info
+
+(* Allowed eliminations *)
+
+(* Previous comment: *)
+(* Unitary/empty Prop: elimination to all sorts are realizable *)
+(* unless the type is large. If it is large, forbids large elimination *)
+(* which otherwise allows simulating the inconsistent system Type:Type. *)
+(* -> this is now handled by is_smashed: *)
+(* - all_sorts in case of small, unitary Prop (not smashed) *)
+(* - logical_sorts in case of large, unitary Prop (smashed) *)
+
+let all_sorts = [InProp;InSet;InType]
+let small_sorts = [InProp;InSet]
+let logical_sorts = [InProp]
+
+let allowed_sorts {ind_squashed;ind_univ;ind_min_univ=_} =
+ if not ind_squashed then all_sorts
+ else match Sorts.family (Sorts.sort_of_univ ind_univ) with
+ | InType -> assert false
+ | InSet -> small_sorts
+ | InProp -> logical_sorts
(* 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
@@ -151,215 +220,88 @@ let param_ccls paramsctxt =
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
+let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) =
+ let arity = Vars.subst_univs_level_constr usubst arity in
+ let lc = Array.map (Vars.subst_univs_level_constr usubst) lc in
+ let indices = Vars.subst_univs_level_context usubst indices in
+ let splayed_lc = Array.map (fun (args,out) ->
+ let args = Vars.subst_univs_level_context usubst args in
+ let out = Vars.subst_univs_level_constr usubst out in
+ args,out)
+ splayed_lc
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 "")
+ let ind_univ = Univ.subst_univs_level_universe usubst univ_info.ind_univ in
+
+ let arity = match univ_info.ind_min_univ with
+ | None -> RegularArity {mind_user_arity=arity;mind_sort=Sorts.sort_of_univ ind_univ}
+ | Some min_univ ->
+ ((match univs with
+ | Monomorphic_ind _ -> ()
+ | Polymorphic_ind _ | Cumulative_ind _ ->
+ CErrors.anomaly ~label:"polymorphic_template_ind"
+ Pp.(strbrk "Template polymorphism and full polymorphism are incompatible."));
+ TemplateArity {template_param_levels=param_ccls params; template_level=min_univ})
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 kelim = allowed_sorts univ_info in
+ (arity,lc), (indices,splayed_lc), kelim
+
+let abstract_inductive_universes = function
+ | Monomorphic_ind_entry ctx -> (Univ.empty_level_subst, Monomorphic_ind ctx)
+ | Polymorphic_ind_entry (nas, ctx) ->
+ let (inst, auctx) = Univ.abstract_universes nas ctx in
+ let inst = Univ.make_instance_subst inst in
+ (inst, Polymorphic_ind auctx)
+ | Cumulative_ind_entry (nas, cumi) ->
+ let (inst, acumi) = Univ.abstract_cumulativity_info nas cumi in
+ let inst = Univ.make_instance_subst inst in
+ (inst, Cumulative_ind acumi)
+
+let typecheck_inductive env (mie:mutual_inductive_entry) =
let () = match mie.mind_entry_inds with
- | [] -> anomaly (Pp.str "empty inductive types declaration.")
+ | [] -> CErrors.anomaly Pp.(str "empty inductive types declaration.")
| _ -> ()
in
- (* Check unicity of names *)
+ (* Check unicity of names (redundant with safe_typing's add_field checks) *)
mind_check_names mie;
- (* Params are typed-checked here *)
- let env' =
+ assert (List.is_empty (Environ.rel_context env));
+
+ (* universes *)
+ let env_univs =
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
+
+ (* Params *)
+ let env_params = Typeops.check_context env_univs mie.mind_entry_params in
+ let params = Environ.rel_context env_params in
+
+ (* Arities *)
+ let env_ar, data = List.fold_left_map (check_arity env_params) env_univs mie.mind_entry_inds in
+ let env_ar_par = push_rel_context params env_ar in
+
+ (* Constructors *)
+ let data = List.map2 (fun ind data -> check_constructors env_ar_par params ind.mind_entry_lc data)
+ mie.mind_entry_inds data
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)
+
+ let () = match mie.mind_entry_universes with
+ | Cumulative_ind_entry (_,univs) -> check_cumulativity univs env_ar params (List.map pi1 data)
+ | Monomorphic_ind_entry _ | Polymorphic_ind_entry _ -> ()
+ in
+
+ (* Abstract universes *)
+ let usubst, univs = abstract_inductive_universes mie.mind_entry_universes in
+ let params = Vars.subst_univs_level_context usubst params in
+ let data = List.map (abstract_packets univs usubst params) data in
+
+ let env_ar_par =
+ let ctx = Environ.rel_context env_ar_par in
+ let ctx = Vars.subst_univs_level_context usubst ctx in
+ let env = Environ.pop_rel_context (Environ.nb_rel env_ar_par) env_ar_par in
+ Environ.push_rel_context ctx env
+ in
+
+ env_ar_par, univs, params, Array.of_list data
diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli
index b16ada5ee8..8841e38636 100644
--- a/kernel/indTyping.mli
+++ b/kernel/indTyping.mli
@@ -8,17 +8,25 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open Names
-open Constr
open Environ
+open Entries
+open Declarations
-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))
+(** Type checking for some inductive entry.
+ Returns:
+ - environment with inductives + parameters in rel context
+ - abstracted universes
+ - parameters
+ - for each inductive,
+ (arity * constructors) (with params)
+ * (indices * splayed constructor types) (both without params)
+ * allowed eliminations
+ *)
+val typecheck_inductive : env -> mutual_inductive_entry ->
+ env
+ * abstract_inductive_universes
+ * Constr.rel_context
+ * ((inductive_arity * Constr.types array) *
+ (Constr.rel_context * (Constr.rel_context * Constr.types) array) *
+ Sorts.family list)
array
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 16ba6e81fa..9bb848c6a4 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -61,6 +61,7 @@ type inductive_error = Type_errors.inductive_error =
| NotAnArity of env * constr
| BadEntry
| LargeNonPropInductiveNotInType
+ | BadUnivs
exception InductiveError = Type_errors.InductiveError
@@ -366,21 +367,20 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt (
If [chkpos] is [false] then positivity is assumed, and
[check_positivity_one] computes the subterms occurrences in a
best-effort fashion. *)
-let check_positivity ~chkpos kn env_ar_par paramsctxt finite inds =
+let check_positivity ~chkpos kn names env_ar_par paramsctxt finite inds =
let ntypes = Array.length inds in
let recursive = finite != BiFinite in
let rc = Array.mapi (fun j t -> (Mrec (kn,j),t)) (Rtree.mk_rec_calls ntypes) in
let ra_env_ar = Array.rev_to_list rc in
let nparamsctxt = Context.Rel.length paramsctxt in
let nmr = Context.Rel.nhyps paramsctxt in
- let check_one i (_,lcnames,lc,(sign,_)) =
+ let check_one i (_,lcnames) (nindices,lc) =
let ra_env_ar_par =
List.init nparamsctxt (fun _ -> (Norec,mk_norec)) @ ra_env_ar in
let ienv = (env_ar_par, 1+nparamsctxt, ntypes, ra_env_ar_par) in
- let nnonrecargs = Context.Rel.nhyps sign - nmr in
- check_positivity_one ~chkpos recursive ienv paramsctxt (kn,i) nnonrecargs lcnames lc
+ check_positivity_one ~chkpos recursive ienv paramsctxt (kn,i) nindices lcnames lc
in
- let irecargs_nmr = Array.mapi check_one inds in
+ let irecargs_nmr = Array.map2_i check_one names inds in
let irecargs = Array.map snd irecargs_nmr
and nmr' = array_min nmr irecargs_nmr
in (nmr',Rtree.mk_rec irecargs)
@@ -390,48 +390,17 @@ let check_positivity ~chkpos kn env_ar_par paramsctxt finite inds =
(************************************************************************)
(* Build the inductive packet *)
-(* Allowed eliminations *)
-
-let all_sorts = [InProp;InSet;InType]
-let small_sorts = [InProp;InSet]
-let logical_sorts = [InProp]
-
-let allowed_sorts is_smashed s =
- if not is_smashed
- then (** Naturally in the defined sort.
- If [s] is Prop, it must be small and unitary.
- Unsmashed, predicative Type and Set: all elimination allowed
- as well. *)
- all_sorts
- else
- match Sorts.family s with
- (* Type: all elimination allowed: above and below *)
- | InType -> all_sorts
- (* Smashed Set is necessarily impredicative: forbids large elimination *)
- | InSet -> small_sorts
- (* Smashed to Prop, no informative eliminations allowed *)
- | InProp -> logical_sorts
-
-(* Previous comment: *)
-(* Unitary/empty Prop: elimination to all sorts are realizable *)
-(* unless the type is large. If it is large, forbids large elimination *)
-(* which otherwise allows simulating the inconsistent system Type:Type. *)
-(* -> this is now handled by is_smashed: *)
-(* - all_sorts in case of small, unitary Prop (not smashed) *)
-(* - logical_sorts in case of large, unitary Prop (smashed) *)
-
-let arity_conclusion = function
- | RegularArity (_, c, _) -> c
- | TemplateArity (_, s) -> mkType s
+let repair_arity indices = function
+ | RegularArity ar -> ar.mind_user_arity
+ | TemplateArity ar -> mkArity (indices,Sorts.sort_of_univ ar.template_level)
let fold_inductive_blocks f =
- Array.fold_left (fun acc (_,_,lc,(arsign,ar)) ->
- f (Array.fold_left f acc lc) (it_mkProd_or_LetIn (arity_conclusion ar) arsign))
+ Array.fold_left (fun acc ((arity,lc),(indices,_),_) ->
+ f (Array.fold_left f acc lc) (repair_arity indices arity))
let used_section_variables env inds =
- let ids = fold_inductive_blocks
- (fun l c -> Id.Set.union (Environ.global_vars_set env c) l)
- Id.Set.empty inds in
+ let fold l c = Id.Set.union (Environ.global_vars_set env c) l in
+ let ids = fold_inductive_blocks fold Id.Set.empty inds in
keep_hyps env ids
let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i))
@@ -502,56 +471,21 @@ let compute_projections (kn, i as ind) mib =
Array.of_list (List.rev labs),
Array.of_list (List.rev pbs)
-let abstract_inductive_universes iu =
- match iu with
- | Monomorphic_ind_entry ctx -> (Univ.empty_level_subst, Monomorphic_ind ctx)
- | Polymorphic_ind_entry (nas, ctx) ->
- let (inst, auctx) = Univ.abstract_universes nas ctx in
- let inst = Univ.make_instance_subst inst in
- (inst, Polymorphic_ind auctx)
- | Cumulative_ind_entry (nas, cumi) ->
- let (inst, acumi) = Univ.abstract_cumulativity_info nas cumi in
- let inst = Univ.make_instance_subst inst in
- (inst, Cumulative_ind acumi)
-
-let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr recargs =
+let build_inductive env names prv univs paramsctxt kn isrecord isfinite inds nmr recargs =
let ntypes = Array.length inds in
(* Compute the set of used section variables *)
let hyps = used_section_variables env inds in
let nparamargs = Context.Rel.nhyps paramsctxt in
- let nparamsctxt = Context.Rel.length paramsctxt in
- let substunivs, aiu = abstract_inductive_universes iu in
- let paramsctxt = Vars.subst_univs_level_context substunivs paramsctxt in
- let env_ar =
- let ctxunivs = Environ.rel_context env_ar in
- let ctxunivs' = Vars.subst_univs_level_context substunivs ctxunivs in
- Environ.push_rel_context ctxunivs' env
- in
(* Check one inductive *)
- let build_one_packet (id,cnames,lc,(ar_sign,ar_kind)) recarg =
+ let build_one_packet (id,cnames) ((arity,lc),(indices,splayed_lc),kelim) recarg =
(* Type of constructors in normal form *)
- let lc = Array.map (Vars.subst_univs_level_constr substunivs) lc in
- 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
+ let nf_lc = Array.map (fun (d,b) -> it_mkProd_or_LetIn b (d@paramsctxt)) splayed_lc in
let consnrealdecls =
- Array.map (fun (d,_) -> Context.Rel.length d - nparamsctxt)
+ Array.map (fun (d,_) -> Context.Rel.length d)
splayed_lc in
let consnrealargs =
- Array.map (fun (d,_) -> Context.Rel.nhyps d - nparamargs)
+ Array.map (fun (d,_) -> Context.Rel.nhyps d)
splayed_lc in
- (* Elimination sorts *)
- let arkind,kelim =
- match ar_kind with
- | TemplateArity (paramlevs, lev) ->
- let ar = {template_param_levels = paramlevs; template_level = lev} in
- TemplateArity ar, all_sorts
- | RegularArity (info,ar,defs) ->
- let s = Sorts.sort_of_univ defs in
- let kelim = allowed_sorts info s in
- let ar = RegularArity
- { mind_user_arity = Vars.subst_univs_level_constr substunivs ar;
- mind_sort = Sorts.sort_of_univ (Univ.subst_univs_level_universe substunivs defs); } in
- ar, kelim in
(* Assigning VM tags to constructors *)
let nconst, nblock = ref 0, ref 0 in
let transf num =
@@ -568,10 +502,10 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r
let rtbl = Array.init (List.length cnames) transf in
(* Build the inductive packet *)
{ mind_typename = id;
- mind_arity = arkind;
- mind_arity_ctxt = Vars.subst_univs_level_context substunivs ar_sign;
- mind_nrealargs = Context.Rel.nhyps ar_sign - nparamargs;
- mind_nrealdecls = Context.Rel.length ar_sign - nparamsctxt;
+ mind_arity = arity;
+ mind_arity_ctxt = indices @ paramsctxt;
+ mind_nrealargs = Context.Rel.nhyps indices;
+ mind_nrealdecls = Context.Rel.length indices;
mind_kelim = kelim;
mind_consnames = Array.of_list cnames;
mind_consnrealdecls = consnrealdecls;
@@ -583,7 +517,7 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r
mind_nb_args = !nblock;
mind_reloc_tbl = rtbl;
} in
- let packets = Array.map2 build_one_packet inds recargs in
+ let packets = Array.map3 build_one_packet names inds recargs in
let mib =
(* Build the mutual inductive *)
{ mind_record = NotRecord;
@@ -594,7 +528,7 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r
mind_nparams_rec = nmr;
mind_params_ctxt = paramsctxt;
mind_packets = packets;
- mind_universes = aiu;
+ mind_universes = univs;
mind_private = prv;
mind_typing_flags = Environ.typing_flags env;
}
@@ -602,7 +536,7 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r
let record_info = match isrecord with
| Some (Some rid) ->
let is_record pkt =
- pkt.mind_kelim == all_sorts
+ List.exists (Sorts.family_equal Sorts.InType) pkt.mind_kelim
&& Array.length pkt.mind_consnames == 1
&& pkt.mind_consnrealargs.(0) > 0
in
@@ -625,11 +559,17 @@ 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) = IndTyping.typecheck_inductive env mie in
+ let (env_ar_par, univs, 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
+ let names = Array.map_of_list (fun entry -> entry.mind_entry_typename, entry.mind_entry_consnames)
+ mie.mind_entry_inds
+ in
+ let (nmr,recargs) = check_positivity ~chkpos kn names
+ env_ar_par paramsctxt mie.mind_entry_finite
+ (Array.map (fun ((_,lc),(indices,_),_) -> Context.Rel.nhyps indices,lc) inds)
+ in
(* Build the inductive packets *)
- build_inductive env mie.mind_entry_private mie.mind_entry_universes
- env_ar paramsctxt kn mie.mind_entry_record mie.mind_entry_finite
+ build_inductive env names mie.mind_entry_private univs
+ paramsctxt kn mie.mind_entry_record mie.mind_entry_finite
inds nmr recargs
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 5e37df6976..7810c1723e 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -14,19 +14,7 @@ open Declarations
open Environ
open Entries
-(** Inductive type checking and errors *)
-
-val check_positivity : chkpos:bool ->
- Names.MutInd.t ->
- Environ.env ->
- (Constr.constr, Constr.types) Context.Rel.pt ->
- Declarations.recursivity_kind ->
- ('a * Names.Id.t list * Constr.types array *
- (('b, 'c) Context.Rel.pt * 'd))
- array -> Int.t * Declarations.recarg Rtree.t array
-
-(** The following function does checks on inductive declarations. *)
-
+(** Check an inductive. *)
val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body
(** Deprecated *)
@@ -41,6 +29,7 @@ type inductive_error =
| NotAnArity of env * constr
| BadEntry
| LargeNonPropInductiveNotInType
+ | BadUnivs
[@@ocaml.deprecated "Use [Type_errors.inductive_error]"]
exception InductiveError of Type_errors.inductive_error
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 9289225eb6..fd050085d7 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -79,6 +79,7 @@ type inductive_error =
| NotAnArity of env * constr
| BadEntry
| LargeNonPropInductiveNotInType
+ | BadUnivs
exception InductiveError of inductive_error
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 613ccb78ca..3e954d6a8e 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -82,6 +82,7 @@ type inductive_error =
| NotAnArity of env * constr
| BadEntry
| LargeNonPropInductiveNotInType
+ | BadUnivs
exception InductiveError of inductive_error
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:44:50 +0000