diff options
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 69 |
1 files changed, 39 insertions, 30 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 9f7466902d..0b0f14eee7 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -231,8 +231,7 @@ let check_engagement env expected_impredicative_set = type side_effect = { from_env : Declarations.structure_body CEphemeron.key; seff_constant : Constant.t; - seff_body : (Constr.t * Univ.ContextSet.t) Declarations.constant_body; - seff_role : Entries.side_effect_role; + seff_body : Constr.t Declarations.constant_body; } module SideEffects : @@ -299,11 +298,6 @@ let concat_private = SideEffects.concat let universes_of_private eff = let fold acc eff = - let acc = match eff.seff_body.const_body with - | Def _ -> acc - | OpaqueDef (_, ctx) -> ctx :: acc - | Primitive _ | Undef _ -> assert false - in match eff.seff_body.const_universes with | Monomorphic ctx -> ctx :: acc | Polymorphic _ -> acc @@ -541,8 +535,7 @@ type 'a effect_entry = type global_declaration = | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration -type exported_private_constant = - Constant.t * Entries.side_effect_role +type exported_private_constant = Constant.t let add_constant_aux ~in_section senv (kn, cb) = let l = Constant.label kn in @@ -601,7 +594,7 @@ let inline_side_effects env body side_eff = let fold (subst, var, ctx, args) (c, cb) = let (b, opaque) = match cb.const_body with | Def b -> (Mod_subst.force_constr b, false) - | OpaqueDef (b, _) -> (b, true) + | OpaqueDef b -> (b, true) | _ -> assert false in match cb.const_universes with @@ -689,13 +682,13 @@ let constant_entry_of_side_effect eff = | Polymorphic auctx -> Polymorphic_entry (Univ.AUContext.names auctx, Univ.AUContext.repr auctx) in - let pt = + let p = match cb.const_body with - | OpaqueDef (b, c) -> b, c - | Def b -> Mod_subst.force_constr b, Univ.ContextSet.empty + | OpaqueDef b -> b + | Def b -> Mod_subst.force_constr b | _ -> assert false in DefinitionEntry { - const_entry_body = Future.from_val (pt, ()); + const_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ()); const_entry_secctx = None; const_entry_feedback = None; const_entry_type = Some cb.const_type; @@ -704,7 +697,7 @@ let constant_entry_of_side_effect eff = const_entry_inline_code = cb.const_inline_code } let export_eff eff = - (eff.seff_constant, eff.seff_body, eff.seff_role) + (eff.seff_constant, eff.seff_body) let export_side_effects mb env (b_ctx, eff) = let not_exists e = @@ -721,11 +714,6 @@ let export_side_effects mb env (b_ctx, eff) = match cb.const_universes with | Polymorphic _ -> env | Monomorphic ctx -> - let ctx = match eff.seff_body.const_body with - | Def _ -> ctx - | OpaqueDef (_, ctx') -> Univ.ContextSet.union ctx' ctx - | Undef _ | Primitive _ -> assert false - in Environ.push_context_set ~strict:true ctx env in let rec translate_seff sl seff acc env = @@ -737,7 +725,12 @@ let export_side_effects mb env (b_ctx, eff) = let kn = eff.seff_constant in let ce = constant_entry_of_side_effect eff in let cb = Term_typing.translate_constant Term_typing.Pure env kn ce in - let cb = map_constant Future.force cb in + let map cu = + let (c, u) = Future.force cu in + let () = assert (Univ.ContextSet.is_empty u) in + c + in + let cb = map_constant map cb in let eff = { eff with seff_body = cb } in (push_seff env eff, export_eff eff) in @@ -749,11 +742,15 @@ let export_side_effects mb env (b_ctx, eff) = in translate_seff trusted seff [] env +let n_univs cb = match cb.const_universes with +| Monomorphic _ -> 0 +| Polymorphic auctx -> Univ.AUContext.size auctx + let export_private_constants ~in_section ce senv = let exported, ce = export_side_effects senv.revstruct senv.env ce in - let map (kn, cb, _) = (kn, map_constant (fun p -> Opaqueproof.create (Future.from_val p)) cb) in + let map (kn, cb) = (kn, map_constant (fun p -> Opaqueproof.create ~univs:(n_univs cb) (Future.from_val (p, Univ.ContextSet.empty))) cb) in let bodies = List.map map exported in - let exported = List.map (fun (kn, _, r) -> (kn, r)) exported in + let exported = List.map (fun (kn, _) -> kn) exported in let senv = List.fold_left (add_constant_aux ~in_section) senv bodies in (ce, exported), senv @@ -763,7 +760,7 @@ let add_recipe ~in_section l r senv = let senv = add_constant_aux ~in_section senv (kn, cb) in kn, senv -let add_constant ?role ~in_section l decl senv = +let add_constant (type a) ~(side_effect : a effect_entry) ~in_section l decl senv : (Constant.t * a) * safe_environment = let kn = Constant.make2 senv.modpath l in let cb = match decl with @@ -778,7 +775,7 @@ let add_constant ?role ~in_section l decl senv = Term_typing.translate_constant Term_typing.Pure senv.env kn ce in let senv = - let cb = map_constant Opaqueproof.create cb in + let cb = map_constant (fun c -> Opaqueproof.create ~univs:(n_univs cb) c) cb in add_constant_aux ~in_section senv (kn, cb) in let senv = match decl with @@ -787,16 +784,28 @@ let add_constant ?role ~in_section l decl senv = add_retroknowledge (Retroknowledge.Register_type(t,kn)) senv | _ -> senv in - let eff = match role with - | None -> empty_private_constants - | Some role -> - let cb = map_constant Future.force cb in + let eff : a = match side_effect with + | PureEntry -> () + | EffectEntry -> + let body, univs = match cb.const_body with + | (Primitive _ | Undef _) -> assert false + | Def c -> (Def c, cb.const_universes) + | OpaqueDef o -> + let (b, ctx) = Future.force o in + match cb.const_universes with + | Monomorphic ctx' -> + OpaqueDef b, Monomorphic (Univ.ContextSet.union ctx ctx') + | Polymorphic auctx -> + (* Upper layers enforce that there are no internal constraints *) + let () = assert (Univ.ContextSet.is_empty ctx) in + OpaqueDef b, Polymorphic auctx + in + let cb = { cb with const_body = body; const_universes = univs } in let from_env = CEphemeron.create senv.revstruct in let eff = { from_env = from_env; seff_constant = kn; seff_body = cb; - seff_role = role; } in SideEffects.add eff empty_private_constants in |