aboutsummaryrefslogtreecommitdiff
path: root/kernel/indtypes.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/indtypes.ml')
-rw-r--r--kernel/indtypes.ml84
1 files changed, 42 insertions, 42 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 5d45c2c1ad..b976469ff7 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -234,8 +234,7 @@ let check_subtyping cumi paramsctxt env_ar inds =
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 env_ar in
- let env = Environ.push_context uctx_other env in
+ let env = Environ.push_context uctx_other env_ar in
let subtyp_constraints =
CumulativityInfo.leq_constraints cumi
(UContext.instance uctx) instance_other
@@ -243,7 +242,7 @@ let check_subtyping cumi paramsctxt env_ar inds =
in
let env = Environ.add_constraints subtyp_constraints env in
(* process individual inductive types: *)
- Array.iter (fun (id,cn,lc,(sign,arity)) ->
+ Array.iter (fun (_id,_cn,lc,(_sign,arity)) ->
match arity with
| RegularArity (_, full_arity, _) ->
check_subtyping_arity_constructor env dosubst full_arity numparams true;
@@ -280,7 +279,7 @@ let typecheck_inductive env mie =
List.fold_left
(fun (env_ar,l) ind ->
(* Arities (without params) are typed-checked here *)
- let expltype = ind.mind_entry_template in
+ 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
@@ -316,7 +315,7 @@ let typecheck_inductive env mie =
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,expltype,deflev,inflev)::l))
+ (env_ar', (id,full_arity,sign @ paramsctxt,template,deflev,inflev)::l))
(env',[])
mie.mind_entry_inds in
@@ -343,7 +342,7 @@ let typecheck_inductive env mie =
(* Compute/check the sorts of the inductive types *)
let inds =
- Array.map (fun ((id,full_arity,sign,expltype,def_level,inf_level),cn,lc,clev) ->
+ 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
@@ -369,31 +368,34 @@ let typecheck_inductive env mie =
RegularArity (not is_natural,full_arity,defu)
in
let template_polymorphic () =
- let sign, s =
+ let _sign, s =
try dest_arity env full_arity
with NotArity -> raise (InductiveError (NotAnArity (env, full_arity)))
- in
- match s with
- | Type u when expltype (* Explicitly polymorphic *) ->
- (* 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)
- | _ (* Not an explicit occurrence of Type *) ->
- full_polymorphic ()
+ 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 _ -> template_polymorphic ()
- | Polymorphic_ind_entry _ | Cumulative_ind_entry _ -> full_polymorphic ()
+ | 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
@@ -426,7 +428,7 @@ exception IllFormedInd of ill_formed_ind
let mind_extract_params = decompose_prod_n_assum
let explain_ind_err id ntyp env nparamsctxt c err =
- let (lparams,c') = mind_extract_params nparamsctxt c in
+ let (_lparams,c') = mind_extract_params nparamsctxt c in
match err with
| LocalNonPos kt ->
raise (InductiveError (NonPos (env,c',mkRel (kt+nparamsctxt))))
@@ -594,7 +596,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt (
discharged to the [check_positive_nested] function. *)
if List.for_all (noccur_between n ntypes) largs then (nmr,mk_norec)
else check_positive_nested ienv nmr (ind_kn, largs)
- | err ->
+ | _err ->
(** If an inductive of the mutually inductive block
appears in any other way, then the positivy check gives
up. *)
@@ -611,7 +613,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt (
defined types, not one of the types of the mutually inductive
block being defined). *)
(* accesses to the environment are not factorised, but is it worth? *)
- and check_positive_nested (env,n,ntypes,ra_env as ienv) nmr ((mi,u), largs) =
+ and check_positive_nested (env,n,ntypes,_ra_env as ienv) nmr ((mi,u), largs) =
let (mib,mip) = lookup_mind_specif env mi in
let auxnrecpar = mib.mind_nparams_rec in
let auxnnonrecpar = mib.mind_nparams - auxnrecpar in
@@ -662,7 +664,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt (
the type [c]) is checked to be the right (properly applied)
inductive type. *)
and check_constructors ienv check_head nmr c =
- let rec check_constr_rec (env,n,ntypes,ra_env as ienv) nmr lrec c =
+ let rec check_constr_rec (env,n,ntypes,_ra_env as ienv) nmr lrec c =
let x,largs = decompose_app (whd_all env c) in
match kind x with
@@ -796,7 +798,6 @@ let compute_projections (kn, i as ind) mib =
let subst = List.init mib.mind_ntypes (fun i -> mkIndU ((kn, mib.mind_ntypes - i - 1), u)) in
let rctx, _ = decompose_prod_assum (substl subst pkt.mind_nf_lc.(0)) in
let ctx, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in
- let mp, dp, l = MutInd.repr3 kn in
(** We build a substitution smashing the lets in the record parameters so
that typechecking projections requires just a substitution and not
matching with a parameter context. *)
@@ -810,9 +811,9 @@ let compute_projections (kn, i as ind) mib =
mkRel 1 :: List.map (lift 1) subst in
subst
in
- let projections decl (i, j, kns, pbs, letsubst) =
+ let projections decl (i, j, labs, pbs, letsubst) =
match decl with
- | LocalDef (na,c,t) ->
+ | LocalDef (_na,c,_t) ->
(* From [params, field1,..,fieldj |- c(params,field1,..,fieldj)]
to [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)] *)
let c = liftn 1 j c in
@@ -822,11 +823,12 @@ let compute_projections (kn, i as ind) mib =
(* From [params-wo-let, x:I |- subst:(params, x:I, field1,..,fieldj)]
to [params-wo-let, x:I |- subst:(params, x:I, field1,..,fieldj+1)] *)
let letsubst = c2 :: letsubst in
- (i, j+1, kns, pbs, letsubst)
+ (i, j+1, labs, pbs, letsubst)
| LocalAssum (na,t) ->
match na with
| Name id ->
- let kn = Constant.make1 (KerName.make mp dp (Label.of_id id)) in
+ let lab = Label.of_id id in
+ let kn = Projection.Repr.make ind ~proj_npars:mib.mind_nparams ~proj_arg:i lab in
(* from [params, field1,..,fieldj |- t(params,field1,..,fieldj)]
to [params, x:I, field1,..,fieldj |- t(params,field1,..,fieldj] *)
let t = liftn 1 j t in
@@ -836,15 +838,13 @@ let compute_projections (kn, i as ind) mib =
(* from [params, x:I, field1,..,fieldj |- t(field1,..,fieldj)]
to [params, x:I |- t(proj1 x,..,projj x)] *)
let fterm = mkProj (Projection.make kn false, mkRel 1) in
- let body = { proj_ind = ind; proj_npars = mib.mind_nparams;
- proj_arg = i; proj_type = projty; } in
- (i + 1, j + 1, kn :: kns, body :: pbs, fterm :: letsubst)
+ (i + 1, j + 1, lab :: labs, projty :: pbs, fterm :: letsubst)
| Anonymous -> raise UndefinableExpansion
in
- let (_, _, kns, pbs, letsubst) =
+ let (_, _, labs, pbs, _letsubst) =
List.fold_right projections ctx (0, 1, [], [], paramsletsubst)
in
- Array.of_list (List.rev kns),
+ Array.of_list (List.rev labs),
Array.of_list (List.rev pbs)
let abstract_inductive_universes iu =
@@ -954,8 +954,8 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r
(** The elimination criterion ensures that all projections can be defined. *)
if Array.for_all is_record packets then
let map i id =
- let kn, projs = compute_projections (kn, i) mib in
- (id, kn, projs)
+ let labs, projs = compute_projections (kn, i) mib in
+ (id, labs, projs)
in
try PrimRecord (Array.mapi map rid)
with UndefinableExpansion -> FakeRecord
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 23:14:23 +0000