From ccbbdd4aad7674b1fcf917d5ee1834d3fe3926f8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Fri, 28 Jun 2024 14:55:55 +0200 Subject: [PATCH] also use hconstr to hcons Qed bodies --- kernel/constant_typing.ml | 6 ++++-- kernel/constant_typing.mli | 3 ++- kernel/safe_typing.ml | 9 ++++++--- 3 files changed, 12 insertions(+), 6 deletions(-) diff --git a/kernel/constant_typing.ml b/kernel/constant_typing.ml index d2ac472669c4a..8ae509e314e1c 100644 --- a/kernel/constant_typing.ml +++ b/kernel/constant_typing.ml @@ -277,7 +277,8 @@ let check_delayed (type a) (handle : a effect_handler) tyenv (body : a proof_out in (* Note: non-trivial trusted side-effects only in monomorphic case *) let body,env,ectx = skip_trusted_seff valid_signatures body env in - let j = Typeops.infer env body in + let hbody = HConstr.of_constr env body in + let j = Typeops.infer_hconstr env hbody in let j = unzip ectx j in let _ = Typeops.judge_of_cast env j DEFAULTcast tyj in let declared = @@ -287,7 +288,8 @@ let check_delayed (type a) (handle : a effect_handler) tyenv (body : a proof_out let () = assert (Id.Set.equal declared declared') in (* Note: non-trivial usubst only in polymorphic case *) let def = Vars.subst_univs_level_constr usubst j.uj_val in - def, univs + let hbody = if def == j.uj_val && List.is_empty ectx then Some hbody else None in + hbody, def, univs (*s Global and local constant declaration. *) diff --git a/kernel/constant_typing.mli b/kernel/constant_typing.mli index d67c45cfe863c..d15df0ea45316 100644 --- a/kernel/constant_typing.mli +++ b/kernel/constant_typing.mli @@ -45,4 +45,5 @@ val infer_opaque : sec_univs:UVars.Instance.t option -> env -> 'a opaque_entry -> (unit, unit) pconstant_body * typing_context -val check_delayed : 'a effect_handler -> typing_context -> 'a proof_output -> (Constr.t * Univ.ContextSet.t Opaqueproof.delayed_universes) +val check_delayed : 'a effect_handler -> typing_context -> 'a proof_output -> + HConstr.t option * Constr.t * Univ.ContextSet.t Opaqueproof.delayed_universes diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 7511f9c61f328..039760999cbfa 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -838,7 +838,7 @@ let infer_direct_opaque ~sec_univs env ce = let cb, ctx = Constant_typing.infer_opaque ~sec_univs env 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) = Constant_typing.check_delayed handle ctx (body, ()) in + let (_hbody, c, u) = Constant_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 } @@ -973,8 +973,11 @@ let check_opaque senv (i : Opaqueproof.opaque_handle) pf = in body, uctx, trusted in - let (c, ctx) = Constant_typing.check_delayed handle ty_ctx pf in - let c = Constr.hcons c in + let (hbody, c, ctx) = Constant_typing.check_delayed handle ty_ctx pf in + let c = match hbody with + | Some hbody -> assert (c == HConstr.self hbody); HConstr.hcons hbody + | None -> Constr.hcons c + in let ctx = match ctx with | Opaqueproof.PrivateMonomorphic u -> Opaqueproof.PrivateMonomorphic (Univ.hcons_universe_context_set u)