From 44f462aa380de847452c0809d15c86649d5d6a7a Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Tue, 28 Mar 2017 19:24:02 +0200 Subject: Extend definition of inductives to include subtyping info --- kernel/indtypes.ml | 29 +++++++++++++++++------------ 1 file changed, 17 insertions(+), 12 deletions(-) (limited to 'kernel/indtypes.ml') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 1e13239bfc..5d928facc7 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -220,7 +220,7 @@ let typecheck_inductive env mie = (* Check unicity of names *) mind_check_names mie; (* Params are typed-checked here *) - let env' = push_context mie.mind_entry_universes env in + let env' = push_context (fst mie.mind_entry_universes) env in let (env_params,paramsctxt) = infer_local_decls env' mie.mind_entry_params in (* We first type arity of each inductive definition *) (* This allows building the environment of arities and to share *) @@ -822,17 +822,18 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm let hyps = used_section_variables env inds in let nparamargs = Context.Rel.nhyps paramsctxt in let nparamsctxt = Context.Rel.length paramsctxt in - let subst, ctx = Univ.abstract_universes p ctx in - let paramsctxt = Vars.subst_univs_level_context subst paramsctxt in + let substunivs, ctxunivs = Univ.abstract_universes p (fst ctx) in + let substsbt, ctxsbt = Univ.abstract_universes p (snd ctx) in + let paramsctxt = Vars.subst_univs_level_context substunivs paramsctxt in let env_ar = - let ctx = Environ.rel_context env_ar in - let ctx' = Vars.subst_univs_level_context subst ctx in - Environ.push_rel_context ctx' env + 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 = (* Type of constructors in normal form *) - let lc = Array.map (Vars.subst_univs_level_constr subst) lc in + 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 consnrealdecls = @@ -841,6 +842,9 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm let consnrealargs = Array.map (fun (d,_) -> Context.Rel.nhyps d - nparamargs) splayed_lc in + (* Check that the subtyping constraints (inferred outside kernel) + are valid. If so return (), otherwise raise an anomaly! *) + let () = () in (* Elimination sorts *) let arkind,kelim = match ar_kind with @@ -851,8 +855,8 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm let s = sort_of_univ defs in let kelim = allowed_sorts info s in let ar = RegularArity - { mind_user_arity = Vars.subst_univs_level_constr subst ar; - mind_sort = sort_of_univ (Univ.subst_univs_level_universe subst defs); } in + { mind_user_arity = Vars.subst_univs_level_constr substunivs ar; + mind_sort = 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 @@ -871,7 +875,7 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm (* Build the inductive packet *) { mind_typename = id; mind_arity = arkind; - mind_arity_ctxt = Vars.subst_univs_level_context subst ar_sign; + 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_kelim = kelim; @@ -895,7 +899,7 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm (** The elimination criterion ensures that all projections can be defined. *) let u = if p then - subst_univs_level_instance subst (Univ.UContext.instance ctx) + subst_univs_level_instance substunivs (Univ.UContext.instance ctxunivs) else Univ.Instance.empty in let indsp = ((kn, 0), u) in @@ -920,7 +924,8 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm mind_params_ctxt = paramsctxt; mind_packets = packets; mind_polymorphic = p; - mind_universes = ctx; + mind_universes = ctxunivs; + mind_subtyping = ctxsbt; mind_private = prv; mind_typing_flags = Environ.typing_flags env; } -- cgit v1.2.3 From fd1f420aef96822bed2ce14214c34e41ceda9b4e Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Sat, 1 Apr 2017 17:35:39 +0200 Subject: Using UInfoInd for universes in inductive types It stores both universe constraints and subtyping information for blocks of inductive declarations. At this stage the there is no inference or checking implemented. The subtyping information simply encodes equality of levels for the condition of subtyping. --- kernel/indtypes.ml | 14 +++++--------- 1 file changed, 5 insertions(+), 9 deletions(-) (limited to 'kernel/indtypes.ml') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 5d928facc7..94bf1a7704 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -220,7 +220,7 @@ let typecheck_inductive env mie = (* Check unicity of names *) mind_check_names mie; (* Params are typed-checked here *) - let env' = push_context (fst mie.mind_entry_universes) env in + let env' = push_context (Univ.UInfoInd.univ_context mie.mind_entry_universes) env in let (env_params,paramsctxt) = infer_local_decls env' mie.mind_entry_params in (* We first type arity of each inductive definition *) (* This allows building the environment of arities and to share *) @@ -822,10 +822,10 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm let hyps = used_section_variables env inds in let nparamargs = Context.Rel.nhyps paramsctxt in let nparamsctxt = Context.Rel.length paramsctxt in - let substunivs, ctxunivs = Univ.abstract_universes p (fst ctx) in - let substsbt, ctxsbt = Univ.abstract_universes p (snd ctx) in + let substunivs, ctxunivs = Univ.abstract_universes p (Univ.UInfoInd.univ_context ctx) in + let substsubtyp, ctxsubtyp = Univ.abstract_universes p (Univ.UInfoInd.subtyp_context ctx) in let paramsctxt = Vars.subst_univs_level_context substunivs paramsctxt in - let env_ar = + 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 @@ -842,9 +842,6 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm let consnrealargs = Array.map (fun (d,_) -> Context.Rel.nhyps d - nparamargs) splayed_lc in - (* Check that the subtyping constraints (inferred outside kernel) - are valid. If so return (), otherwise raise an anomaly! *) - let () = () in (* Elimination sorts *) let arkind,kelim = match ar_kind with @@ -924,8 +921,7 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm mind_params_ctxt = paramsctxt; mind_packets = packets; mind_polymorphic = p; - mind_universes = ctxunivs; - mind_subtyping = ctxsbt; + mind_universes = Univ.UInfoInd.make (ctxunivs, ctxsubtyp); mind_private = prv; mind_typing_flags = Environ.typing_flags env; } -- cgit v1.2.3 From f27f3ca3a39f5320a60c82c601525e7f0fe666cb Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Mon, 3 Apr 2017 16:06:07 +0200 Subject: Check subtyping of inductive types in Kernel --- kernel/indtypes.ml | 34 ++++++++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) (limited to 'kernel/indtypes.ml') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 94bf1a7704..068332406e 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -207,6 +207,24 @@ let param_ccls paramsctxt = in List.fold_left fold [] paramsctxt +(* Check arities and constructors *) +let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : Term.types) is_arity = + let basic_check ev tp = conv_leq ev tp (subst tp) in + let check_typ typ typ_env = + match typ with + | LocalAssum (_, typ') -> + begin + try + basic_check 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 () + (* Type-check an inductive definition. Does not check positivity conditions. *) (* TODO check that we don't overgeneralize construcors/inductive arities with @@ -345,6 +363,22 @@ let typecheck_inductive env mie = 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 () = + let sbsubst = UInfoInd.subtyping_susbst mie.mind_entry_universes in + let dosubst = subst_univs_level_constr sbsubst in + let envsb = push_context (UInfoInd.subtyp_context mie.mind_entry_universes) env_ar_par in + (* process individual inductive types: *) + Array.iter (fun (id,cn,lc,(sign,arity)) -> + match arity with + | RegularArity (_, full_arity, _) -> + check_subtyping_arity_constructor envsb dosubst full_arity true; + Array.iter (fun cnt -> check_subtyping_arity_constructor envsb dosubst cnt true) lc + | TemplateArity _ -> () + (* TODO: When disabling template polumorphism raise anomaly if this constructor is not removed from the code base *) + ) inds in (env_arities, env_ar_par, paramsctxt, inds) (************************************************************************) -- cgit v1.2.3 From 47e010c2dd0ab6370704d8ab24552753e4e1b1dc Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Mon, 3 Apr 2017 16:28:20 +0200 Subject: Fix typo in error message --- kernel/indtypes.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/indtypes.ml') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 068332406e..91e6ec2855 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -217,7 +217,7 @@ let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : Ter try basic_check env typ'; Environ.push_rel typ typ_env with NotConvertible -> - anomaly ~label:"bad inductive subtyping relation" (Pp.str "Invalid subtyping relation!") + anomaly ~label:"bad inductive subtyping relation" (Pp.str "Invalid subtyping relation") end | _ -> anomaly (Pp.str "") in -- cgit v1.2.3 From 34c1fee1c980b433b069a59f408792142ba00f6e Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Tue, 4 Apr 2017 11:54:37 +0200 Subject: Correct subtyping check for constructors --- kernel/indtypes.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/indtypes.ml') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 91e6ec2855..17ce5483c7 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -375,7 +375,7 @@ let typecheck_inductive env mie = match arity with | RegularArity (_, full_arity, _) -> check_subtyping_arity_constructor envsb dosubst full_arity true; - Array.iter (fun cnt -> check_subtyping_arity_constructor envsb dosubst cnt true) lc + Array.iter (fun cnt -> check_subtyping_arity_constructor envsb dosubst cnt false) lc | TemplateArity _ -> () (* TODO: When disabling template polumorphism raise anomaly if this constructor is not removed from the code base *) ) inds -- cgit v1.2.3 From d83a4a93202c91095c5528fe4b54c83737e5a151 Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Tue, 4 Apr 2017 19:44:31 +0200 Subject: Add subtyping inference for inductive types --- kernel/indtypes.ml | 21 ++++++++++++++++----- 1 file changed, 16 insertions(+), 5 deletions(-) (limited to 'kernel/indtypes.ml') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 17ce5483c7..15fe908359 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -208,8 +208,12 @@ let param_ccls paramsctxt = List.fold_left fold [] paramsctxt (* Check arities and constructors *) -let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : Term.types) is_arity = - let basic_check ev tp = conv_leq ev tp (subst tp) in +let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : Term.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') -> @@ -367,15 +371,22 @@ let typecheck_inductive env mie = (* 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 () = + let numparams = List.length paramsctxt in let sbsubst = UInfoInd.subtyping_susbst mie.mind_entry_universes in let dosubst = subst_univs_level_constr sbsubst in - let envsb = push_context (UInfoInd.subtyp_context mie.mind_entry_universes) env_ar_par in + let uctx = UInfoInd.univ_context mie.mind_entry_universes in + let instance_other = Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) in + let constraints_other = Univ.subst_univs_level_constraints sbsubst (Univ.UContext.constraints uctx) in + let uctx_other = Univ.UContext.make (instance_other, constraints_other) in + let env' = Environ.push_context uctx env_ar_par in + let env'' = Environ.push_context uctx_other env' in + let envsb = push_context (UInfoInd.subtyp_context mie.mind_entry_universes) env'' in (* process individual inductive types: *) Array.iter (fun (id,cn,lc,(sign,arity)) -> match arity with | RegularArity (_, full_arity, _) -> - check_subtyping_arity_constructor envsb dosubst full_arity true; - Array.iter (fun cnt -> check_subtyping_arity_constructor envsb dosubst cnt false) lc + check_subtyping_arity_constructor envsb dosubst full_arity numparams true; + Array.iter (fun cnt -> check_subtyping_arity_constructor envsb dosubst cnt numparams false) lc | TemplateArity _ -> () (* TODO: When disabling template polumorphism raise anomaly if this constructor is not removed from the code base *) ) inds -- cgit v1.2.3 From 7b5fcef8a0fb3b97a3980f10596137234061990f Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Wed, 26 Apr 2017 15:24:35 +0200 Subject: Fix bugs --- kernel/indtypes.ml | 61 ++++++++++++++++++++++++++++-------------------------- 1 file changed, 32 insertions(+), 29 deletions(-) (limited to 'kernel/indtypes.ml') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 15fe908359..a4c7a0573c 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -215,20 +215,42 @@ let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : Ter numchecked := !numchecked + 1 in let check_typ typ typ_env = - match typ with - | LocalAssum (_, typ') -> - begin - try - basic_check 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 "") + 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 mie paramsctxt env_ar inds = + let numparams = Context.Rel.nhyps paramsctxt in + let sbsubst = UInfoInd.subtyping_susbst mie.mind_entry_universes in + let dosubst = subst_univs_level_constr sbsubst in + let uctx = UInfoInd.univ_context mie.mind_entry_universes in + let instance_other = Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) in + let constraints_other = Univ.subst_univs_level_constraints sbsubst (Univ.UContext.constraints uctx) in + let uctx_other = Univ.UContext.make (instance_other, constraints_other) in + let env' = Environ.push_context uctx env_ar in + let env'' = Environ.push_context uctx_other env' in + let envsb = push_context (UInfoInd.subtyp_context mie.mind_entry_universes) env'' in + (* process individual inductive types: *) + Array.iter (fun (id,cn,lc,(sign,arity)) -> + match arity with + | RegularArity (_, full_arity, _) -> + check_subtyping_arity_constructor envsb dosubst full_arity numparams true; + Array.iter (fun cnt -> check_subtyping_arity_constructor envsb dosubst cnt numparams false) lc + | TemplateArity _ -> () + ) inds + (* Type-check an inductive definition. Does not check positivity conditions. *) (* TODO check that we don't overgeneralize construcors/inductive arities with @@ -370,26 +392,7 @@ let typecheck_inductive env mie = 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 () = - let numparams = List.length paramsctxt in - let sbsubst = UInfoInd.subtyping_susbst mie.mind_entry_universes in - let dosubst = subst_univs_level_constr sbsubst in - let uctx = UInfoInd.univ_context mie.mind_entry_universes in - let instance_other = Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) in - let constraints_other = Univ.subst_univs_level_constraints sbsubst (Univ.UContext.constraints uctx) in - let uctx_other = Univ.UContext.make (instance_other, constraints_other) in - let env' = Environ.push_context uctx env_ar_par in - let env'' = Environ.push_context uctx_other env' in - let envsb = push_context (UInfoInd.subtyp_context mie.mind_entry_universes) env'' in - (* process individual inductive types: *) - Array.iter (fun (id,cn,lc,(sign,arity)) -> - match arity with - | RegularArity (_, full_arity, _) -> - check_subtyping_arity_constructor envsb dosubst full_arity numparams true; - Array.iter (fun cnt -> check_subtyping_arity_constructor envsb dosubst cnt numparams false) lc - | TemplateArity _ -> () - (* TODO: When disabling template polumorphism raise anomaly if this constructor is not removed from the code base *) - ) inds + let () = check_subtyping mie paramsctxt env_arities inds in (env_arities, env_ar_par, paramsctxt, inds) (************************************************************************) -- cgit v1.2.3 From 9468e4b49bd2f397b5e1bd2b7994cc84929fb6ac Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Thu, 27 Apr 2017 20:16:35 +0200 Subject: Fix bugs and add an option for cumulativity --- kernel/indtypes.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'kernel/indtypes.ml') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index a4c7a0573c..5cfcbba606 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -392,7 +392,7 @@ let typecheck_inductive env mie = 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 () = check_subtyping mie paramsctxt env_arities inds + let () = if mie.mind_entry_cumulative then check_subtyping mie paramsctxt env_arities inds in (env_arities, env_ar_par, paramsctxt, inds) (************************************************************************) @@ -864,7 +864,7 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params Array.of_list (List.rev kns), Array.of_list (List.rev pbs) -let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nmr recargs = +let build_inductive env cum p prv ctx env_ar 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 @@ -969,6 +969,7 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm mind_params_ctxt = paramsctxt; mind_packets = packets; mind_polymorphic = p; + mind_cumulative = cum; mind_universes = Univ.UInfoInd.make (ctxunivs, ctxsubtyp); mind_private = prv; mind_typing_flags = Environ.typing_flags env; @@ -984,7 +985,7 @@ let check_inductive env kn mie = 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 (* Build the inductive packets *) - build_inductive env mie.mind_entry_polymorphic mie.mind_entry_private + build_inductive env mie.mind_entry_cumulative mie.mind_entry_polymorphic mie.mind_entry_private mie.mind_entry_universes env_ar paramsctxt kn mie.mind_entry_record mie.mind_entry_finite inds nmr recargs -- cgit v1.2.3 From ff918e4bb0ae23566e038f4b55d84dd2c343f95e Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Thu, 1 Jun 2017 16:18:19 +0200 Subject: Clean up universes of constants and inductives --- kernel/indtypes.ml | 69 ++++++++++++++++++++++++++++++++++-------------------- 1 file changed, 44 insertions(+), 25 deletions(-) (limited to 'kernel/indtypes.ml') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 5cfcbba606..00fbe27a70 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -231,23 +231,23 @@ let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : Ter (* 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 mie paramsctxt env_ar inds = +let check_subtyping cumi paramsctxt env_ar inds = let numparams = Context.Rel.nhyps paramsctxt in - let sbsubst = UInfoInd.subtyping_susbst mie.mind_entry_universes in + let sbsubst = CumulativityInfo.subtyping_susbst cumi in let dosubst = subst_univs_level_constr sbsubst in - let uctx = UInfoInd.univ_context mie.mind_entry_universes in + let uctx = CumulativityInfo.univ_context cumi in let instance_other = Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) in let constraints_other = Univ.subst_univs_level_constraints sbsubst (Univ.UContext.constraints uctx) in let uctx_other = Univ.UContext.make (instance_other, constraints_other) in - let env' = Environ.push_context uctx env_ar in - let env'' = Environ.push_context uctx_other env' in - let envsb = push_context (UInfoInd.subtyp_context mie.mind_entry_universes) env'' in + let env = Environ.push_context uctx env_ar in + let env = Environ.push_context uctx_other env in + let env = push_context (CumulativityInfo.subtyp_context cumi) env in (* process individual inductive types: *) Array.iter (fun (id,cn,lc,(sign,arity)) -> match arity with | RegularArity (_, full_arity, _) -> - check_subtyping_arity_constructor envsb dosubst full_arity numparams true; - Array.iter (fun cnt -> check_subtyping_arity_constructor envsb dosubst cnt numparams false) lc + 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 _ -> () ) inds @@ -264,7 +264,13 @@ let typecheck_inductive env mie = (* Check unicity of names *) mind_check_names mie; (* Params are typed-checked here *) - let env' = push_context (Univ.UInfoInd.univ_context mie.mind_entry_universes) env in + let univctx = + match mie.mind_entry_universes with + | Monomorphic_ind_entry ctx -> ctx + | Polymorphic_ind_entry ctx -> ctx + | Cumulative_ind_entry cumi -> Univ.CumulativityInfo.univ_context cumi + in + let env' = push_context univctx env in let (env_params,paramsctxt) = infer_local_decls env' mie.mind_entry_params in (* We first type arity of each inductive definition *) (* This allows building the environment of arities and to share *) @@ -383,16 +389,21 @@ let typecheck_inductive env mie = | _ (* Not an explicit occurrence of Type *) -> full_polymorphic () in - let arity = - if mie.mind_entry_polymorphic then full_polymorphic () - else template_polymorphic () + let arity = + match mie.mind_entry_universes with + | Monomorphic_ind_entry _ -> template_polymorphic () + | Polymorphic_ind_entry _ | Cumulative_ind_entry _ -> 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 () = if mie.mind_entry_cumulative then check_subtyping mie paramsctxt env_arities inds + 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) (************************************************************************) @@ -864,14 +875,21 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params Array.of_list (List.rev kns), Array.of_list (List.rev pbs) -let build_inductive env cum p prv ctx env_ar paramsctxt kn isrecord isfinite inds nmr recargs = +let abstract_inductive_universes iu = + match iu with + | Monomorphic_ind_entry ctx -> (Univ.empty_level_subst, Monomorphic_ind ctx) + | Polymorphic_ind_entry ctx -> + let (inst, auctx) = Univ.abstract_universes ctx in (inst, Polymorphic_ind auctx) + | Cumulative_ind_entry cumi -> + let (inst, acumi) = Univ.abstract_cumulativity_info cumi in (inst, Cumulative_ind acumi) + +let build_inductive env prv iu env_ar 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, ctxunivs = Univ.abstract_universes p (Univ.UInfoInd.univ_context ctx) in - let substsubtyp, ctxsubtyp = Univ.abstract_universes p (Univ.UInfoInd.subtyp_context ctx) 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 @@ -942,10 +960,14 @@ let build_inductive env cum p prv ctx env_ar paramsctxt kn isrecord isfinite ind && Array.length pkt.mind_consnames == 1 && pkt.mind_consnrealargs.(0) > 0 -> (** The elimination criterion ensures that all projections can be defined. *) - let u = - if p then - subst_univs_level_instance substunivs (Univ.UContext.instance ctxunivs) - else Univ.Instance.empty + let u = + let process auctx = + subst_univs_level_instance substunivs (Univ.AUContext.instance auctx) + in + match aiu with + | Monomorphic_ind _ -> Univ.Instance.empty + | Polymorphic_ind auctx -> process auctx + | Cumulative_ind acumi -> process (Univ.ACumulativityInfo.univ_context acumi) in let indsp = ((kn, 0), u) in let rctx, indty = decompose_prod_assum (subst1 (mkIndU indsp) pkt.mind_nf_lc.(0)) in @@ -968,9 +990,7 @@ let build_inductive env cum p prv ctx env_ar paramsctxt kn isrecord isfinite ind mind_nparams_rec = nmr; mind_params_ctxt = paramsctxt; mind_packets = packets; - mind_polymorphic = p; - mind_cumulative = cum; - mind_universes = Univ.UInfoInd.make (ctxunivs, ctxsubtyp); + mind_universes = aiu; mind_private = prv; mind_typing_flags = Environ.typing_flags env; } @@ -985,7 +1005,6 @@ let check_inductive env kn mie = 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 (* Build the inductive packets *) - build_inductive env mie.mind_entry_cumulative mie.mind_entry_polymorphic mie.mind_entry_private - mie.mind_entry_universes + build_inductive env mie.mind_entry_private mie.mind_entry_universes env_ar paramsctxt kn mie.mind_entry_record mie.mind_entry_finite inds nmr recargs -- cgit v1.2.3