diff options
Diffstat (limited to 'kernel/term_typing.ml')
| -rw-r--r-- | kernel/term_typing.ml | 87 |
1 files changed, 53 insertions, 34 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 70dd6438d4..5f501bff10 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -227,17 +227,15 @@ 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 + let sbst = Univ.make_instance_subst sbst 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 +243,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 { @@ -306,22 +301,29 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry 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 poly, univsctx = match c.const_entry_universes with - | Monomorphic_const_entry univs -> false, univs - | Polymorphic_const_entry univs -> true, Univ.ContextSet.of_context univs - in - let ctx = Univ.ContextSet.union univsctx ctx in let body, ctx, _ = match trust with | Pure -> body, ctx, [] | 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 + let env, usubst, univs = match c.const_entry_universes with + | Monomorphic_const_entry univs -> + let ctx = Univ.ContextSet.union univs ctx in + let env = push_context_set ~strict:true ctx env in + env, Univ.empty_level_subst, Monomorphic_const ctx + | Polymorphic_const_entry uctx -> + (** Ensure not to generate internal constraints in polymorphic mode. + The only way for this to happen would be that either the body + contained deferred universes, or that it contains monomorphic + side-effects. The first property is ruled out by upper layers, + and the second one is ensured by the fact we currently + unconditionally export side-effects from polymorphic definitions, + i.e. [trust] is always [Pure]. *) + let () = assert (Univ.ContextSet.is_empty ctx) in + let env = push_context ~strict:false uctx env in + let sbst, auctx = Univ.abstract_universes uctx in + let sbst = Univ.make_instance_subst sbst in + env, sbst, Polymorphic_const auctx in - let usubst, univs = abstract_constant_universes abstract ctx in let j = infer env body in let typ = match typ with | None -> @@ -493,7 +495,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 = @@ -533,14 +535,10 @@ type side_effect_role = type exported_side_effect = Constant.t * constant_body * side_effect_role -let export_side_effects mb env ce = - match ce with - | ParameterEntry e -> [], ParameterEntry e - | ProjectionEntry e -> [], ProjectionEntry e - | DefinitionEntry c -> +let export_side_effects mb env c = let { const_entry_body = body } = c in let _, eff = Future.force body in - let ce = DefinitionEntry { c with + let ce = { c with const_entry_body = Future.chain body (fun (b_ctx, _) -> b_ctx, ()) } in let not_exists (c,_,_,_) = @@ -609,9 +607,19 @@ let translate_recipe env kn r = let hcons = DirPath.is_empty dir in build_constant_declaration kn env (Cooking.cook_constant ~hcons env r) -let translate_local_def mb env id centry = +let translate_local_def env id centry = let open Cooking in - let decl = infer_declaration ~trust:mb env None (DefinitionEntry centry) 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 = Monomorphic_const_entry Univ.ContextSet.empty; + const_entry_opaque = false; + const_entry_inline_code = false; + } 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 @@ -623,11 +631,22 @@ let translate_local_def mb 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. *) |