From 1de1d505dfd1c5a05a4910cfc872971087de26fb Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 19 Dec 2017 10:11:26 +0100 Subject: Let definitions do not create new universe constraints. We force the upper layers to extrude the universe constraints before sending it to the kernel. This simplifies the suspicious handling of polymorphic constraints for section-local definitions. --- kernel/term_typing.ml | 44 ++++++++++++++++++++++++-------------------- 1 file changed, 24 insertions(+), 20 deletions(-) (limited to 'kernel/term_typing.ml') diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index c2c65d6d4..2e4426d62 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -227,17 +227,14 @@ let feedback_completion_typecheck = Option.iter (fun state_id -> feedback ~id:state_id Feedback.Complete) -let abstract_constant_universes abstract = function +let abstract_constant_universes = function | Monomorphic_const_entry uctx -> Univ.empty_level_subst, Monomorphic_const uctx | Polymorphic_const_entry uctx -> - if not abstract then - Univ.empty_level_subst, Monomorphic_const (Univ.ContextSet.of_context uctx) - else - let sbst, auctx = Univ.abstract_universes uctx in - sbst, Polymorphic_const auctx + let sbst, auctx = Univ.abstract_universes uctx in + sbst, Polymorphic_const auctx -let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry) = +let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = match dcl with | ParameterEntry (ctx,(t,uctx),nl) -> let env = match uctx with @@ -245,10 +242,7 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry | Polymorphic_const_entry uctx -> push_context ~strict:false uctx env in let j = infer env t in - let abstract = not (Option.is_empty kn) in - let usubst, univs = - abstract_constant_universes abstract uctx - in + let usubst, univs = abstract_constant_universes uctx in let c = Typeops.assumption_of_judgment env j in let t = Constr.hcons (Vars.subst_univs_level_constr usubst c) in { @@ -316,12 +310,11 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry | SideEffects _ -> inline_side_effects env body ctx side_eff in let env = push_context_set ~strict:(not poly) ctx env in - let abstract = not (Option.is_empty kn) in let ctx = if poly then Polymorphic_const_entry (Univ.ContextSet.to_context ctx) else Monomorphic_const_entry ctx in - let usubst, univs = abstract_constant_universes abstract ctx in + let usubst, univs = abstract_constant_universes ctx in let j = infer env body in let typ = match typ with | None -> @@ -493,7 +486,7 @@ let build_constant_declaration kn env result = let translate_constant mb env kn ce = build_constant_declaration kn env - (infer_declaration ~trust:mb env (Some kn) ce) + (infer_declaration ~trust:mb env ce) let constant_entry_of_side_effect cb u = let univs = @@ -607,17 +600,17 @@ let translate_recipe env kn r = let translate_local_def env id centry = let open Cooking in - let body = Future.chain centry.secdef_body (fun body -> body, ()) in + let body = Future.from_val ((centry.secdef_body, Univ.ContextSet.empty), ()) in let centry = { const_entry_body = body; const_entry_secctx = centry.secdef_secctx; const_entry_feedback = centry.secdef_feedback; const_entry_type = centry.secdef_type; - const_entry_universes = centry.secdef_universes; + const_entry_universes = Monomorphic_const_entry Univ.ContextSet.empty; const_entry_opaque = false; const_entry_inline_code = false; } in - let decl = infer_declaration ~trust:Pure env None (DefinitionEntry centry) in + let decl = infer_declaration ~trust:Pure env (DefinitionEntry centry) in let typ = decl.cook_type in if Option.is_empty decl.cook_context && !Flags.record_aux_file then begin match decl.cook_body with @@ -629,11 +622,22 @@ let translate_local_def env id centry = (Opaqueproof.force_proof (opaque_tables env) lc) in record_aux env ids_typ ids_def end; - let univs = match decl.cook_universes with - | Monomorphic_const ctx -> ctx + let () = match decl.cook_universes with + | Monomorphic_const ctx -> assert (Univ.ContextSet.is_empty ctx) | Polymorphic_const _ -> assert false in - decl.cook_body, typ, univs + let c = match decl.cook_body with + | Def c -> Mod_subst.force_constr c + | OpaqueDef o -> + let p = Opaqueproof.force_proof (Environ.opaque_tables env) o in + let cst = Opaqueproof.force_constraints (Environ.opaque_tables env) o in + (** Let definitions are ensured to have no extra constraints coming from + the body by virtue of the typing of [Entries.section_def_entry]. *) + let () = assert (Univ.ContextSet.is_empty cst) in + p + | Undef _ -> assert false + in + c, typ (* Insertion of inductive types. *) -- cgit v1.2.3