diff options
| -rw-r--r-- | kernel/safe_typing.ml | 72 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 2 | ||||
| -rw-r--r-- | tactics/declare.ml | 24 |
3 files changed, 49 insertions, 49 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index d2a7703648..659f9cd1c4 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -693,7 +693,7 @@ let check_signatures curmb sl = type side_effect_declaration = | DefinitionEff : Entries.definition_entry -> side_effect_declaration -| OpaqueEff : unit Entries.const_entry_body Entries.opaque_entry -> side_effect_declaration +| OpaqueEff : Constr.constr Entries.opaque_entry -> side_effect_declaration let constant_entry_of_side_effect eff = let cb = eff.seff_body in @@ -712,7 +712,7 @@ let constant_entry_of_side_effect eff = | _ -> assert false in if Declareops.is_opaque cb then OpaqueEff { - opaque_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ()); + opaque_entry_body = p; opaque_entry_secctx = Context.Named.to_vars cb.const_hyps; opaque_entry_feedback = None; opaque_entry_type = cb.const_type; @@ -730,6 +730,25 @@ let constant_entry_of_side_effect eff = let export_eff eff = (eff.seff_constant, eff.seff_body) +let is_empty_private = function +| Opaqueproof.PrivateMonomorphic ctx -> Univ.ContextSet.is_empty ctx +| Opaqueproof.PrivatePolymorphic (_, ctx) -> Univ.ContextSet.is_empty ctx + +let empty_private univs = match univs with +| Monomorphic _ -> Opaqueproof.PrivateMonomorphic Univ.ContextSet.empty +| Polymorphic auctx -> Opaqueproof.PrivatePolymorphic (Univ.AUContext.size auctx, Univ.ContextSet.empty) + +(* Special function to call when the body of an opaque definition is provided. + It performs the type-checking of the body immediately. *) +let translate_direct_opaque env kn ce = + let cb, ctx = Term_typing.translate_opaque env kn ce in + let body = ce.Entries.opaque_entry_body, Univ.ContextSet.empty in + let handle _env c () = (c, Univ.ContextSet.empty, 0) in + let (c, u) = Term_typing.check_delayed handle ctx (body, ()) in + (* No constraints can be generated, we set it empty everywhere *) + let () = assert (is_empty_private u) in + { cb with const_body = OpaqueDef c } + let export_side_effects mb env (b_ctx, eff) = let not_exists e = try ignore(Environ.lookup_constant e.seff_constant env); false @@ -760,16 +779,7 @@ let export_side_effects mb env (b_ctx, eff) = | DefinitionEff ce -> Term_typing.translate_constant env kn (DefinitionEntry ce) | OpaqueEff ce -> - let cb, ctx = Term_typing.translate_opaque env kn ce in - let body = Future.force ce.Entries.opaque_entry_body in - let handle _env c () = (c, Univ.ContextSet.empty, 0) in - let (c, u) = Term_typing.check_delayed handle ctx body in - let () = match u with - | Opaqueproof.PrivateMonomorphic ctx - | Opaqueproof.PrivatePolymorphic (_, ctx) -> - assert (Univ.ContextSet.is_empty ctx) - in - { cb with const_body = OpaqueDef c } + translate_direct_opaque env kn ce in let eff = { eff with seff_body = cb } in (push_seff env eff, export_eff eff) @@ -791,10 +801,7 @@ let export_private_constants ce senv = let exported, ce = export_side_effects senv.revstruct senv.env ce in let map senv (kn, c) = match c.const_body with | OpaqueDef p -> - let local = match c.const_universes with - | Monomorphic _ -> Opaqueproof.PrivateMonomorphic Univ.ContextSet.empty - | Polymorphic auctx -> Opaqueproof.PrivatePolymorphic (Univ.AUContext.size auctx, Univ.ContextSet.empty) - in + let local = empty_private c.const_universes in let senv, o = push_opaque_proof (Future.from_val (p, local)) senv in senv, (kn, { c with const_body = OpaqueDef o }) | Def _ | Undef _ | Primitive _ as body -> @@ -861,39 +868,20 @@ let add_private_constant l decl senv : (Constant.t * private_constants) * safe_e let cb = match decl with | OpaqueEff ce -> - let handle _env body () = body, Univ.ContextSet.empty, 0 in - let cb, ctx = Term_typing.translate_opaque senv.env kn ce in - let map pf = Term_typing.check_delayed handle ctx pf in - let pf = Future.chain ce.Entries.opaque_entry_body map in - { cb with const_body = OpaqueDef pf } + translate_direct_opaque senv.env kn ce | DefinitionEff ce -> Term_typing.translate_constant senv.env kn (Entries.DefinitionEntry ce) in - let senv, cb, body = match cb.const_body with - | Def _ as const_body -> senv, { cb with const_body }, const_body + let senv, dcb = match cb.const_body with + | Def _ as const_body -> senv, { cb with const_body } | OpaqueDef c -> - let senv, o = push_opaque_proof c senv in - senv, { cb with const_body = OpaqueDef o }, cb.const_body + let local = empty_private cb.const_universes in + let senv, o = push_opaque_proof (Future.from_val (c, local)) senv in + senv, { cb with const_body = OpaqueDef o } | Undef _ | Primitive _ -> assert false in - let senv = add_constant_aux senv (kn, cb) in + let senv = add_constant_aux senv (kn, dcb) in let eff = - let body, univs = match body with - | (Primitive _ | Undef _) -> assert false - | Def c -> (Def c, cb.const_universes) - | OpaqueDef o -> - let (b, delayed) = Future.force o in - match cb.const_universes, delayed with - | Monomorphic ctx', Opaqueproof.PrivateMonomorphic ctx -> - OpaqueDef b, Monomorphic (Univ.ContextSet.union ctx ctx') - | Polymorphic auctx, Opaqueproof.PrivatePolymorphic (_, ctx) -> - (* Upper layers enforce that there are no internal constraints *) - let () = assert (Univ.ContextSet.is_empty ctx) in - OpaqueDef b, Polymorphic auctx - | (Monomorphic _ | Polymorphic _), (Opaqueproof.PrivateMonomorphic _ | Opaqueproof.PrivatePolymorphic _) -> - assert false - 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; diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index c60e7e893f..ec86495db8 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -79,7 +79,7 @@ type global_declaration = type side_effect_declaration = | DefinitionEff : Entries.definition_entry -> side_effect_declaration -| OpaqueEff : unit Entries.const_entry_body Entries.opaque_entry -> side_effect_declaration +| OpaqueEff : Constr.constr Entries.opaque_entry -> side_effect_declaration type exported_private_constant = Constant.t diff --git a/tactics/declare.ml b/tactics/declare.ml index c9da88988f..63a93d3dc3 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -204,11 +204,11 @@ let cast_proof_entry e = const_entry_inline_code = e.proof_entry_inline_code; } -type 'a effect_entry = -| EffectEntry : private_constants effect_entry -| PureEntry : unit effect_entry +type ('a, 'b) effect_entry = +| EffectEntry : (private_constants, private_constants Entries.const_entry_body) effect_entry +| PureEntry : (unit, Constr.constr) effect_entry -let cast_opaque_proof_entry (type a) (entry : a effect_entry) (e : a proof_entry) = +let cast_opaque_proof_entry (type a b) (entry : (a, b) effect_entry) (e : a proof_entry) : b opaque_entry = let typ = match e.proof_entry_type with | None -> assert false | Some typ -> typ @@ -238,12 +238,24 @@ let cast_opaque_proof_entry (type a) (entry : a effect_entry) (e : a proof_entry Environ.really_needed env (Id.Set.union hyp_typ hyp_def) | Some hyps -> hyps in + let (body, univs : b * _) = match entry with + | PureEntry -> + let (body, uctx), () = Future.force e.proof_entry_body in + let univs = match e.proof_entry_universes with + | Monomorphic_entry uctx' -> Monomorphic_entry (Univ.ContextSet.union uctx uctx') + | Polymorphic_entry _ -> + assert (Univ.ContextSet.is_empty uctx); + e.proof_entry_universes + in + body, univs + | EffectEntry -> e.proof_entry_body, e.proof_entry_universes + in { - opaque_entry_body = e.proof_entry_body; + opaque_entry_body = body; opaque_entry_secctx = secctx; opaque_entry_feedback = e.proof_entry_feedback; opaque_entry_type = typ; - opaque_entry_universes = e.proof_entry_universes; + opaque_entry_universes = univs; } let get_roles export eff = |