diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-04 13:38:22 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-26 15:11:13 +0200 |
commit | 4457e6d75affd20c1c13c0d798c490129525bcb5 (patch) | |
tree | b5eeffe5f1a07c439fe704a6d60b2b036110df7f /kernel | |
parent | a960c4db9ae93a6445f9db620f96f62b397ba8b5 (diff) |
More precise type for universe entries.
We use an algebraic type instead of a pair of a boolean and the corresponding
data. For now, this is isomorphic, but this allows later change in the structure.
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/entries.ml | 7 | ||||
-rw-r--r-- | kernel/safe_typing.ml | 10 | ||||
-rw-r--r-- | kernel/term_typing.ml | 30 | ||||
-rw-r--r-- | kernel/term_typing.mli | 2 |
4 files changed, 30 insertions, 19 deletions
diff --git a/kernel/entries.ml b/kernel/entries.ml index 3fa25c142..a1ccbdbc1 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -64,6 +64,10 @@ type mutual_inductive_entry = { type 'a proof_output = constr Univ.in_universe_context_set * 'a type 'a const_entry_body = 'a proof_output Future.computation +type constant_universes_entry = + | Monomorphic_const_entry of Univ.universe_context + | Polymorphic_const_entry of Univ.universe_context + type 'a definition_entry = { const_entry_body : 'a const_entry_body; (* List of section variables *) @@ -71,8 +75,7 @@ type 'a definition_entry = { (* 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_universes : constant_universes_entry; const_entry_opaque : bool; const_entry_inline_code : bool } diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index ed4c7d57a..074122b03 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -382,12 +382,12 @@ let safe_push_named d env = let push_named_def (id,de) senv = - let c,typ,univs = - match Term_typing.translate_local_def senv.revstruct senv.env id de with - | c, typ, Monomorphic_const ctx -> c, typ, ctx - | _, _, Polymorphic_const _ -> assert false + let open Entries in + let c,typ,univs = Term_typing.translate_local_def senv.revstruct senv.env id de in + let poly = match de.Entries.const_entry_universes with + | Monomorphic_const_entry _ -> false + | Polymorphic_const_entry _ -> true in - let poly = de.Entries.const_entry_polymorphic in let univs = Univ.ContextSet.of_context univs in let c, univs = match c with | Def c -> Mod_subst.force_constr c, univs diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index cf82d54ec..910223465 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -251,8 +251,8 @@ let infer_declaration ~trust env kn dcl = delay even in the polymorphic case. *) | DefinitionEntry ({ const_entry_type = Some typ; const_entry_opaque = true; - const_entry_polymorphic = false} as c) -> - let env = push_context ~strict:true c.const_entry_universes env in + const_entry_universes = Monomorphic_const_entry univs } as c) -> + let env = push_context ~strict:true univs env in let { const_entry_body = body; const_entry_feedback = feedback_id } = c in let tyj = infer_type env typ in let proofterm = @@ -271,7 +271,7 @@ let infer_declaration ~trust env kn dcl = c, uctx) in let def = OpaqueDef (Opaqueproof.create proofterm) in def, RegularArity typ, None, - (Monomorphic_const c.const_entry_universes), + (Monomorphic_const univs), c.const_entry_inline_code, c.const_entry_secctx (** Other definitions have to be processed immediately. *) @@ -279,18 +279,22 @@ let infer_declaration ~trust env kn dcl = let { const_entry_type = typ; const_entry_opaque = opaque } = c in let { const_entry_body = body; const_entry_feedback = feedback_id } = c in let (body, ctx), side_eff = Future.join body in - let univsctx = Univ.ContextSet.of_context c.const_entry_universes in + let poly, univs = match c.const_entry_universes with + | Monomorphic_const_entry univs -> false, univs + | Polymorphic_const_entry univs -> true, univs + in + let univsctx = Univ.ContextSet.of_context univs in let body, ctx, _ = inline_side_effects env body (Univ.ContextSet.union univsctx ctx) side_eff in - let env = push_context_set ~strict:(not c.const_entry_polymorphic) ctx env in - let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in + let env = push_context_set ~strict:(not poly) ctx env in + let abstract = poly && not (Option.is_empty kn) in let usubst, univs = abstract_constant_universes abstract (Univ.ContextSet.to_context ctx) in let j = infer env body in let typ = match typ with | None -> - if not c.const_entry_polymorphic then (* Old-style polymorphism *) + if not poly then (* Old-style polymorphism *) make_polymorphic_if_constant_for_ind env j else RegularArity (Vars.subst_univs_level_constr usubst j.uj_type) | Some t -> @@ -461,11 +465,12 @@ let translate_constant mb env kn ce = (infer_declaration ~trust:mb env (Some kn) ce) let constant_entry_of_side_effect cb u = - let poly, univs = + let univs = match cb.const_universes with - | Monomorphic_const ctx -> false, ctx + | Monomorphic_const uctx -> + Monomorphic_const_entry uctx | Polymorphic_const auctx -> - true, Univ.AUContext.repr auctx + Polymorphic_const_entry (Univ.AUContext.repr auctx) in let pt = match cb.const_body, u with @@ -478,7 +483,6 @@ let constant_entry_of_side_effect cb u = const_entry_feedback = None; const_entry_type = (match cb.const_type with RegularArity t -> Some t | _ -> None); - const_entry_polymorphic = poly; const_entry_universes = univs; const_entry_opaque = Declareops.is_opaque cb; const_entry_inline_code = cb.const_inline_code } @@ -592,6 +596,10 @@ let translate_local_def mb env id centry = env ids_def ids_typ context_ids in record_aux env ids_typ ids_def expr end; + let univs = match univs with + | Monomorphic_const ctx -> ctx + | Polymorphic_const _ -> assert false + in def, typ, univs (* Insertion of inductive types. *) diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 77d126074..29c991837 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -15,7 +15,7 @@ open Entries type side_effects val translate_local_def : structure_body -> env -> Id.t -> side_effects definition_entry -> - constant_def * types * constant_universes + constant_def * types * Univ.universe_context val translate_local_assum : env -> types -> types |