diff options
Diffstat (limited to 'kernel/indtypes.ml')
| -rw-r--r-- | kernel/indtypes.ml | 66 |
1 files changed, 43 insertions, 23 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 750ac86908..3771454db5 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -379,17 +379,25 @@ let check_positivity ~chkpos kn names env_ar_par paramsctxt finite inds = (************************************************************************) (* Build the inductive packet *) -let repair_arity indices = function - | RegularArity ar -> ar.mind_user_arity - | TemplateArity ar -> mkArity (indices,Sorts.sort_of_univ ar.template_level) +let fold_arity f acc params arity indices = match arity with + | RegularArity ar -> f acc ar.mind_user_arity + | TemplateArity _ -> + let fold_ctx acc ctx = + List.fold_left (fun acc d -> + Context.Rel.Declaration.fold_constr (fun c acc -> f acc c) d acc) + acc + ctx + in + fold_ctx (fold_ctx acc params) indices -let fold_inductive_blocks f = +let fold_inductive_blocks f acc params inds = Array.fold_left (fun acc ((arity,lc),(indices,_),_) -> - f (Array.fold_left f acc lc) (repair_arity indices arity)) + fold_arity f (Array.fold_left f acc lc) params arity indices) + acc inds -let used_section_variables env inds = +let used_section_variables env params inds = 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 + let ids = fold_inductive_blocks fold Id.Set.empty params inds in keep_hyps env ids let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i)) @@ -458,10 +466,11 @@ let compute_projections (kn, i as ind) mib = Array.of_list (List.rev rs), Array.of_list (List.rev pbs) -let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite inds nmr recargs = +let build_inductive env ~sec_univs names prv univs variance + 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 hyps = used_section_variables env paramsctxt inds in let nparamargs = Context.Rel.nhyps paramsctxt in (* Check one inductive *) let build_one_packet (id,cnames) ((arity,lc),(indices,splayed_lc),kelim) recarg = @@ -479,18 +488,17 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite in (* Assigning VM tags to constructors *) let nconst, nblock = ref 0, ref 0 in - let transf num = - let arity = List.length (dest_subterms recarg).(num) in - if Int.equal arity 0 then - let p = (!nconst, 0) in - incr nconst; p - else - let p = (!nblock + 1, arity) in - incr nblock; p - (* les tag des constructeur constant commence a 0, - les tag des constructeur non constant a 1 (0 => accumulator) *) + let transf arity = + if Int.equal arity 0 then + let p = (!nconst, 0) in + incr nconst; p + else + let p = (!nblock + 1, arity) in + incr nblock; p + (* les tag des constructeur constant commence a 0, + les tag des constructeur non constant a 1 (0 => accumulator) *) in - let rtbl = Array.init (List.length cnames) transf in + let rtbl = Array.map transf consnrealargs in (* Build the inductive packet *) { mind_typename = id; mind_arity = arity; @@ -510,6 +518,15 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite mind_reloc_tbl = rtbl; } in let packets = Array.map3 build_one_packet names inds recargs in + let variance, sec_variance = match variance with + | None -> None, None + | Some variance -> match sec_univs with + | None -> Some variance, None + | Some sec_univs -> + let nsec = Array.length sec_univs in + Some (Array.sub variance nsec (Array.length variance - nsec)), + Some (Array.sub variance 0 nsec) + in let mib = (* Build the mutual inductive *) { mind_record = NotRecord; @@ -522,6 +539,7 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite mind_packets = packets; mind_universes = univs; mind_variance = variance; + mind_sec_variance = sec_variance; mind_private = prv; mind_typing_flags = Environ.typing_flags env; } @@ -542,9 +560,11 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite (************************************************************************) (************************************************************************) -let check_inductive env kn mie = +let check_inductive env ~sec_univs kn mie = (* First type-check the inductive definition *) - let (env_ar_par, univs, variance, record, paramsctxt, inds) = IndTyping.typecheck_inductive env mie in + let (env_ar_par, univs, variance, record, paramsctxt, inds) = + IndTyping.typecheck_inductive env ~sec_univs mie + in (* Then check positivity conditions *) let chkpos = (Environ.typing_flags env).check_positive in let names = Array.map_of_list (fun entry -> entry.mind_entry_typename, entry.mind_entry_consnames) @@ -555,6 +575,6 @@ let check_inductive env kn mie = (Array.map (fun ((_,lc),(indices,_),_) -> Context.Rel.nhyps indices,lc) inds) in (* Build the inductive packets *) - build_inductive env names mie.mind_entry_private univs variance + build_inductive env ~sec_univs names mie.mind_entry_private univs variance paramsctxt kn record mie.mind_entry_finite inds nmr recargs |