diff options
Diffstat (limited to 'kernel/indtypes.ml')
| -rw-r--r-- | kernel/indtypes.ml | 141 |
1 files changed, 48 insertions, 93 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 85be2146..14decafc 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -120,16 +120,6 @@ 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 @@ -174,10 +164,9 @@ let infer_constructor_packet env_ar_par params lc = 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 = @@ -353,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,(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 @@ -424,7 +413,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 @@ -796,69 +785,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 = MutInd.repr3 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 + 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 - 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 @@ -867,23 +834,14 @@ 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 = @@ -968,33 +926,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 = - match aiu 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 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; @@ -1006,6 +940,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 } (************************************************************************) (************************************************************************) |