aboutsummaryrefslogtreecommitdiff
path: root/kernel/indtypes.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/indtypes.ml')
-rw-r--r--kernel/indtypes.ml230
1 files changed, 99 insertions, 131 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 04971f83dc..d7eb865e0a 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * 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 *)
+(* // * 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
@@ -11,6 +13,7 @@ open Util
open Names
open Univ
open Term
+open Constr
open Vars
open Declarations
open Declareops
@@ -117,24 +120,14 @@ let mind_check_names mie =
(* Typing the arities and constructor types *)
-(* An inductive definition is a "unit" if it has only one constructor
- and that all arguments expected by this constructor are
- logical, this is the case for equality, conjunction of logical properties
-*)
-let is_unit constrsinfos =
- match constrsinfos with (* One info = One constructor *)
- | [level] -> is_type0m_univ level
- | [] -> (* type without constructors *) true
- | _ -> false
-
let infos_and_sort env t =
let rec aux env t max =
let t = whd_all env t in
- match kind_of_term t with
+ 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 (univ_of_sort varj.utj_type) 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
@@ -168,13 +161,12 @@ let infer_constructor_packet env_ar_par params lc =
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 -> it_mkProd_or_LetIn j.utj_val params) jlc in
+ 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 isunit = is_unit levels 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'', (isunit, level))
+ (lc'', level)
(* If indices matter *)
let cumulate_arity_large_levels env sign =
@@ -183,7 +175,7 @@ let cumulate_arity_large_levels env sign =
match d with
| LocalAssum (_,t) ->
let tj = infer_type env t in
- let u = univ_of_sort tj.utj_type 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)
@@ -199,8 +191,8 @@ let is_impredicative env u =
let param_ccls paramsctxt =
let fold acc = function
| (LocalAssum (_, p)) ->
- (let c = strip_prod_assum p in
- match kind_of_term c with
+ (let c = Term.strip_prod_assum p in
+ match kind c with
| Sort (Type u) -> Univ.Universe.level u
| _ -> None) :: acc
| LocalDef _ -> acc
@@ -208,7 +200,7 @@ 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) numparams is_arity =
+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);
@@ -233,22 +225,32 @@ let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : Ter
(* 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 sbsubst = CumulativityInfo.subtyping_susbst cumi in
- let dosubst = subst_univs_level_constr sbsubst 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 new_levels = Array.init (UContext.size uctx) (Level.make DirPath.empty) 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 env_ar in
let env = Environ.push_context uctx_other env in
- let env = push_context (CumulativityInfo.subtyp_context cumi) env 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 _ -> ()
+ | 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
@@ -264,13 +266,12 @@ let typecheck_inductive env mie =
(* Check unicity of names *)
mind_check_names mie;
(* Params are typed-checked here *)
- let univctx =
+ let env' =
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
+ | 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' = 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 *)
@@ -288,7 +289,7 @@ let typecheck_inductive env mie =
(** 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, prop_sort)) in
+ 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)
@@ -342,7 +343,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,(is_unit,clev)) ->
+ Array.map (fun ((id,full_arity,sign,expltype,def_level,inf_level),cn,lc,clev) ->
let infu =
(** Inferred level, with parameters and constructors. *)
match inf_level with
@@ -350,7 +351,7 @@ let typecheck_inductive env mie =
| None -> clev
in
let full_polymorphic () =
- let defu = Term.univ_of_sort def_level in
+ let defu = Sorts.univ_of_sort def_level in
let is_natural =
type_in_type env || (UGraph.check_leq (universes env') infu defu)
in
@@ -413,7 +414,7 @@ let typecheck_inductive env mie =
type ill_formed_ind =
| LocalNonPos of int
| LocalNotEnoughArgs of int
- | LocalNotConstructor of Context.Rel.t * int
+ | LocalNotConstructor of Constr.rel_context * int
| LocalNonPar of int * int * int
exception IllFormedInd of ill_formed_ind
@@ -468,7 +469,7 @@ let check_correct_par (env,n,ntypes,_) paramdecls ind_index args =
| LocalDef _ :: paramdecls ->
check param_index (paramdecl_index+1) paramdecls
| _::paramdecls ->
- match kind_of_term (whd_all env params.(param_index)) with
+ match kind (whd_all env params.(param_index)) with
| Rel w when Int.equal w paramdecl_index ->
check (param_index-1) (paramdecl_index+1) paramdecls
| _ ->
@@ -495,7 +496,7 @@ if Int.equal nmr 0 then 0 else
| (_,[]) -> assert false (* |paramsctxt|>=nmr *)
| (lp, LocalDef _ :: paramsctxt) -> find k (index-1) (lp,paramsctxt)
| (p::lp,_::paramsctxt) ->
- ( match kind_of_term (whd_all env p) with
+ ( match kind (whd_all env p) with
| Rel w when Int.equal w index -> find (k+1) (index-1) (lp,paramsctxt)
| _ -> k)
in find 0 (n-1) (lpar,List.rev paramsctxt)
@@ -526,7 +527,7 @@ let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lrecparams) =
let rec ienv_decompose_prod (env,_,_,_ as ienv) n c =
if Int.equal n 0 then (ienv,c) else
let c' = whd_all env c in
- match kind_of_term c' with
+ match kind c' with
Prod(na,a,b) ->
let ienv' = ienv_push_var ienv (na,a,mk_norec) in
ienv_decompose_prod ienv' (n-1) b
@@ -555,7 +556,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt (
more generally, the arrows may be dependent). *)
let rec check_pos (env, n, ntypes, ra_env as ienv) nmr c =
let x,largs = decompose_app (whd_all env c) in
- match kind_of_term x with
+ match kind x with
| Prod (na,b,d) ->
let () = assert (List.is_empty largs) in
(** If one of the inductives of the mutually inductive
@@ -663,7 +664,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt (
and check_constructors ienv check_head nmr 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_of_term x with
+ match kind x with
| Prod (na,b,d) ->
let () = assert (List.is_empty largs) in
@@ -710,7 +711,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt (
best-effort fashion. *)
let check_positivity ~chkpos kn env_ar_par paramsctxt finite inds =
let ntypes = Array.length inds in
- let recursive = finite != Decl_kinds.BiFinite 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
@@ -746,7 +747,7 @@ let allowed_sorts is_smashed s =
as well. *)
all_sorts
else
- match family_of_sort s with
+ match Sorts.family s with
(* Type: all elimination allowed: above and below *)
| InType -> all_sorts
(* Smashed Set is necessarily impredicative: forbids large elimination *)
@@ -785,69 +786,47 @@ exception UndefinableExpansion
build an expansion function.
The term built is expecting to be substituted first by
a substitution of the form [params, x : ind params] *)
-let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
- mind_consnrealdecls mind_consnrealargs paramslet ctx =
- let mp, dp, l = repr_mind kn in
+let compute_projections (kn, i as ind) mib =
+ let pkt = mib.mind_packets.(i) in
+ let u = match mib.mind_universes with
+ | Monomorphic_ind _ -> Univ.Instance.empty
+ | Polymorphic_ind auctx -> Univ.make_abstract_instance auctx
+ | Cumulative_ind acumi -> Univ.make_abstract_instance (Univ.ACumulativityInfo.univ_context acumi)
+ in
+ 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
(** 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. *)
- let indty, paramsletsubst =
- (* [ty] = [Ind inst] is typed in context [params] *)
- let inst = Context.Rel.to_extended_vect mkRel 0 paramslet in
- let ty = mkApp (mkIndU indu, inst) in
+ let paramsletsubst =
(* [Ind inst] is typed in context [params-wo-let] *)
- let inst' = rel_list 0 nparamargs in
+ let inst' = rel_list 0 mib.mind_nparams in
(* {params-wo-let |- subst:params] *)
let subst = subst_of_rel_context_instance paramslet inst' in
(* {params-wo-let, x:Ind inst' |- subst':(params,x:Ind inst)] *)
let subst = (* For the record parameter: *)
mkRel 1 :: List.map (lift 1) subst in
- ty, subst
- in
- let ci =
- let print_info =
- { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in
- { ci_ind = ind;
- ci_npar = nparamargs;
- ci_cstr_ndecls = mind_consnrealdecls;
- ci_cstr_nargs = mind_consnrealargs;
- ci_pp_info = print_info }
- in
- let len = List.length ctx in
- let x = Name x in
- let compat_body ccl i =
- (* [ccl] is defined in context [params;x:indty] *)
- (* [ccl'] is defined in context [params;x:indty;x:indty] *)
- let ccl' = liftn 1 2 ccl in
- let p = mkLambda (x, lift 1 indty, ccl') in
- let branch = it_mkLambda_or_LetIn (mkRel (len - i)) ctx in
- let body = mkCase (ci, p, mkRel 1, [|lift 1 branch|]) in
- it_mkLambda_or_LetIn (mkLambda (x,indty,body)) params
+ subst
in
- let projections decl (i, j, kns, pbs, subst, letsubst) =
+ let projections decl (i, j, labs, pbs, letsubst) =
match decl with
| 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
(* From [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)]
- to [params, x:I |- c(params,proj1 x,..,projj x)] *)
- let c1 = substl subst c in
- (* From [params, x:I |- subst:field1,..,fieldj]
- to [params, x:I |- subst:field1,..,fieldj+1] where [subst]
- is represented with instance of field1 last *)
- let subst = c1 :: subst in
- (* From [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)]
to [params-wo-let, x:I |- c(params,proj1 x,..,projj x)] *)
let c2 = substl letsubst c in
(* 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, subst, 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
@@ -856,32 +835,27 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
let projty = substl letsubst t in
(* from [params, x:I, field1,..,fieldj |- t(field1,..,fieldj)]
to [params, x:I |- t(proj1 x,..,projj x)] *)
- let ty = substl subst t in
- let term = mkProj (Projection.make kn true, mkRel 1) in
let fterm = mkProj (Projection.make kn false, mkRel 1) in
- let compat = compat_body ty (j - 1) in
- let etab = it_mkLambda_or_LetIn (mkLambda (x, indty, term)) params in
- let etat = it_mkProd_or_LetIn (mkProd (x, indty, ty)) params in
- let body = { proj_ind = fst ind; proj_npars = nparamargs;
- proj_arg = i; proj_type = projty; proj_eta = etab, etat;
- proj_body = compat } in
- (i + 1, j + 1, kn :: kns, body :: pbs,
- fterm :: subst, fterm :: letsubst)
+ (i + 1, j + 1, lab :: labs, projty :: pbs, fterm :: letsubst)
| Anonymous -> raise UndefinableExpansion
in
- let (_, _, kns, pbs, subst, letsubst) =
- List.fold_right projections ctx (0, 1, [], [], [], paramsletsubst)
+ 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 =
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)
+ let (inst, auctx) = Univ.abstract_universes ctx in
+ let inst = Univ.make_instance_subst inst in
+ (inst, Polymorphic_ind auctx)
| Cumulative_ind_entry cumi ->
- let (inst, acumi) = Univ.abstract_cumulativity_info cumi in (inst, Cumulative_ind acumi)
+ let (inst, acumi) = Univ.abstract_cumulativity_info 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 ntypes = Array.length inds in
@@ -915,11 +889,11 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r
let ar = {template_param_levels = paramlevs; template_level = lev} in
TemplateArity ar, all_sorts
| RegularArity (info,ar,defs) ->
- let s = sort_of_univ defs in
+ 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 = sort_of_univ (Univ.subst_univs_level_universe substunivs defs); } in
+ 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
@@ -953,36 +927,9 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r
mind_reloc_tbl = rtbl;
} in
let packets = Array.map2 build_one_packet inds recargs in
- let pkt = packets.(0) in
- let isrecord =
- match isrecord with
- | Some (Some rid) when pkt.mind_kelim == all_sorts
- && Array.length pkt.mind_consnames == 1
- && pkt.mind_consnrealargs.(0) > 0 ->
- (** The elimination criterion ensures that all projections can be defined. *)
- 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
- (try
- let fields, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in
- let kns, projs =
- compute_projections indsp pkt.mind_typename rid nparamargs paramsctxt
- pkt.mind_consnrealdecls pkt.mind_consnrealargs paramslet fields
- in Some (Some (rid, kns, projs))
- with UndefinableExpansion -> Some None)
- | Some _ -> Some None
- | None -> None
- in
- (* Build the mutual inductive *)
- { mind_record = isrecord;
+ let mib =
+ (* Build the mutual inductive *)
+ { mind_record = NotRecord;
mind_ntypes = ntypes;
mind_finite = isfinite;
mind_hyps = hyps;
@@ -994,6 +941,27 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r
mind_private = prv;
mind_typing_flags = Environ.typing_flags env;
}
+ in
+ let record_info = match isrecord with
+ | Some (Some rid) ->
+ let is_record pkt =
+ pkt.mind_kelim == all_sorts
+ && Array.length pkt.mind_consnames == 1
+ && pkt.mind_consnrealargs.(0) > 0
+ in
+ (** The elimination criterion ensures that all projections can be defined. *)
+ if Array.for_all is_record packets then
+ let map i id =
+ let labs, projs = compute_projections (kn, i) mib in
+ (id, labs, projs)
+ in
+ try PrimRecord (Array.mapi map rid)
+ with UndefinableExpansion -> FakeRecord
+ else FakeRecord
+ | Some None -> FakeRecord
+ | None -> NotRecord
+ in
+ { mib with mind_record = record_info }
(************************************************************************)
(************************************************************************)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-17 01:56:26 +0000