diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/entries.mli | 8 | ||||
| -rw-r--r-- | kernel/indtypes.ml | 6 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 48 | ||||
| -rw-r--r-- | kernel/univ.ml | 5 | ||||
| -rw-r--r-- | kernel/univ.mli | 1 |
5 files changed, 40 insertions, 28 deletions
diff --git a/kernel/entries.mli b/kernel/entries.mli index 0a06eef167..2d7b7bb0f3 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -57,14 +57,13 @@ type const_entry_body = proof_output Future.computation type definition_entry = { const_entry_body : const_entry_body; - (* List of sectoin variables *) + (* List of section variables *) const_entry_secctx : Context.section_context option; (* State id on which the completion of type checking is reported *) const_entry_feedback : Stateid.t option; const_entry_type : types option; const_entry_polymorphic : bool; const_entry_universes : Univ.universe_context; - const_entry_proj : (mutual_inductive * int) option; const_entry_opaque : bool; const_entry_inline_code : bool } @@ -73,9 +72,14 @@ type inline = int option (* inlining level, None for no inlining *) type parameter_entry = Context.section_context option * bool * types Univ.in_universe_context * inline +type projection_entry = { + proj_entry_ind : mutual_inductive; + proj_entry_arg : int } + type constant_entry = | DefinitionEntry of definition_entry | ParameterEntry of parameter_entry + | ProjectionEntry of projection_entry (** {6 Modules } *) diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 7ae787d224..759d712061 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -782,7 +782,11 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re | Some true when pkt.mind_kelim == all_sorts && Array.length pkt.mind_consnames == 1 -> (** The elimination criterion ensures that all projections can be defined. *) let rctx, _ = decompose_prod_assum pkt.mind_nf_lc.(0) in - let u = if p then Univ.UContext.instance ctx else Univ.Instance.empty in + let u = + if p then + subst_univs_level_instance subst (Univ.UContext.instance ctx) + else Univ.Instance.empty + in (try let fields = List.firstn pkt.mind_consnrealdecls.(0) rctx in let kns, projs = diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index b603610ce8..a3c4d98490 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -122,6 +122,7 @@ let infer_declaration env kn dcl = let c = Typeops.assumption_of_judgment env j in let t = hcons_constr (Vars.subst_univs_level_constr usubst c) in Undef nl, RegularArity t, None, poly, univs, false, ctx + | DefinitionEntry ({ const_entry_type = Some typ; const_entry_opaque = true; const_entry_polymorphic = false} as c) -> @@ -143,6 +144,7 @@ let infer_declaration env kn dcl = def, RegularArity typ, None, c.const_entry_polymorphic, c.const_entry_universes, c.const_entry_inline_code, c.const_entry_secctx + | DefinitionEntry c -> let env = push_context c.const_entry_universes env in let { const_entry_type = typ; const_entry_opaque = opaque } = c in @@ -152,35 +154,31 @@ let infer_declaration env kn dcl = let body = handle_side_effects env body side_eff in let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in let usubst, univs = Univ.abstract_universes abstract c.const_entry_universes in - let def, typ, proj = - match c.const_entry_proj with - | Some (ind, i) -> (* Bind c to a checked primitive projection *) - let mib, _ = Inductive.lookup_mind_specif env (ind,0) in - let kn, pb = - match mib.mind_record with - | Some (kns, pbs) -> - if i < Array.length pbs then - kns.(i), pbs.(i) - else assert false - | None -> assert false - in - let term = Vars.subst_univs_level_constr usubst (fst pb.proj_eta) in - let typ = Vars.subst_univs_level_constr usubst (snd pb.proj_eta) in - Def (Mod_subst.from_val (hcons_constr term)), RegularArity typ, Some pb - | None -> - let j = infer env body in - let typ = constrain_type env j c.const_entry_polymorphic usubst (map_option_typ typ) in - let def = hcons_constr (Vars.subst_univs_level_constr usubst j.uj_val) in - let def = - if opaque then OpaqueDef (Opaqueproof.create (Future.from_val (def, Univ.ContextSet.empty))) - else Def (Mod_subst.from_val def) - in - def, typ, None + let j = infer env body in + let typ = constrain_type env j c.const_entry_polymorphic usubst (map_option_typ typ) in + let def = hcons_constr (Vars.subst_univs_level_constr usubst j.uj_val) in + let def = + if opaque then OpaqueDef (Opaqueproof.create (Future.from_val (def, Univ.ContextSet.empty))) + else Def (Mod_subst.from_val def) in feedback_completion_typecheck feedback_id; - def, typ, proj, c.const_entry_polymorphic, + def, typ, None, c.const_entry_polymorphic, univs, c.const_entry_inline_code, c.const_entry_secctx + | ProjectionEntry {proj_entry_ind = ind; proj_entry_arg = i} -> + let mib, _ = Inductive.lookup_mind_specif env (ind,0) in + let kn, pb = + match mib.mind_record with + | Some (kns, pbs) -> + if i < Array.length pbs then + kns.(i), pbs.(i) + else assert false + | None -> assert false + in + let term, typ = pb.proj_eta in + Def (Mod_subst.from_val (hcons_constr term)), RegularArity typ, Some pb, + mib.mind_polymorphic, mib.mind_universes, false, None + let global_vars_set_constant_type env = function | RegularArity t -> global_vars_set env t | TemplateArity (ctx,_) -> diff --git a/kernel/univ.ml b/kernel/univ.ml index fbdb5bb0d7..b2f251283e 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1937,6 +1937,11 @@ let subst_univs_level_universe subst u = let u' = Universe.smartmap f u in if u == u' then u else Universe.sort u' + +let subst_univs_level_instance subst i = + let i' = Instance.subst_fn (subst_univs_level_level subst) i in + if i == i' then i + else i' let subst_univs_level_constraint subst (u,d,v) = let u' = subst_univs_level_level subst u diff --git a/kernel/univ.mli b/kernel/univ.mli index c9b7547f29..7c0c9536fd 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -374,6 +374,7 @@ val is_empty_level_subst : universe_level_subst -> bool val subst_univs_level_level : universe_level_subst -> universe_level -> universe_level val subst_univs_level_universe : universe_level_subst -> universe -> universe val subst_univs_level_constraints : universe_level_subst -> constraints -> constraints +val subst_univs_level_instance : universe_level_subst -> universe_instance -> universe_instance (** Level to universe substitutions. *) |