aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/changelog/01-kernel/10439-uniform-opaque-seff-handling.md4
-rw-r--r--kernel/entries.ml13
-rw-r--r--kernel/safe_typing.ml21
-rw-r--r--kernel/safe_typing.mli2
-rw-r--r--kernel/term_typing.ml40
-rw-r--r--kernel/term_typing.mli2
-rw-r--r--tactics/declare.ml45
7 files changed, 58 insertions, 69 deletions
diff --git a/doc/changelog/01-kernel/10439-uniform-opaque-seff-handling.md b/doc/changelog/01-kernel/10439-uniform-opaque-seff-handling.md
new file mode 100644
index 0000000000..e0573a2c74
--- /dev/null
+++ b/doc/changelog/01-kernel/10439-uniform-opaque-seff-handling.md
@@ -0,0 +1,4 @@
+- Internal definitions generated by abstract-like tactics are now inlined
+ inside universe Qed-terminated polymorphic definitions, similarly to what
+ happens for their monomorphic counterparts,
+ (`#10439 <https://github.com/coq/coq/pull/10439>`_, by Pierre-Marie Pédrot).
diff --git a/kernel/entries.ml b/kernel/entries.ml
index bc389e9fcf..47e2f72b0e 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -99,11 +99,14 @@ type primitive_entry = {
type 'a proof_output = constr Univ.in_universe_context_set * 'a
type 'a const_entry_body = 'a proof_output Future.computation
-type 'a constant_entry =
- | DefinitionEntry of definition_entry
- | OpaqueEntry of 'a const_entry_body opaque_entry
- | ParameterEntry of parameter_entry
- | PrimitiveEntry of primitive_entry
+(** Dummy wrapper type discriminable from unit *)
+type 'a seff_wrap = { seff_wrap : 'a }
+
+type _ constant_entry =
+ | DefinitionEntry : definition_entry -> unit constant_entry
+ | OpaqueEntry : 'a const_entry_body opaque_entry -> 'a seff_wrap constant_entry
+ | ParameterEntry : parameter_entry -> unit constant_entry
+ | PrimitiveEntry : primitive_entry -> unit constant_entry
(** {6 Modules } *)
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 24b3765019..ea45f699ce 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -527,7 +527,7 @@ let update_resolver f senv = { senv with modresolver = f senv.modresolver }
(** Insertion of constants and parameters in environment *)
type 'a effect_entry =
-| EffectEntry : private_constants effect_entry
+| EffectEntry : private_constants Entries.seff_wrap effect_entry
| PureEntry : unit effect_entry
type global_declaration =
@@ -669,6 +669,9 @@ let check_signatures curmb sl =
| None -> 0
| Some (n, _) -> n
+type side_effect_declaration =
+| DefinitionEff : Entries.definition_entry -> side_effect_declaration
+| OpaqueEff : unit Entries.const_entry_body Entries.opaque_entry -> side_effect_declaration
let constant_entry_of_side_effect eff =
let cb = eff.seff_body in
@@ -686,7 +689,7 @@ let constant_entry_of_side_effect eff =
| Def b -> Mod_subst.force_constr b
| _ -> assert false in
if Declareops.is_opaque cb then
- OpaqueEntry {
+ OpaqueEff {
opaque_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ());
opaque_entry_secctx = cb.const_hyps;
opaque_entry_feedback = None;
@@ -694,7 +697,7 @@ let constant_entry_of_side_effect eff =
opaque_entry_universes = univs;
}
else
- DefinitionEntry {
+ DefinitionEff {
const_entry_body = p;
const_entry_secctx = Some cb.const_hyps;
const_entry_feedback = None;
@@ -730,7 +733,15 @@ let export_side_effects mb env (b_ctx, eff) =
let env, cb =
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 open Entries in
+ let open Term_typing in
+ let cb = match ce with
+ | DefinitionEff ce ->
+ Term_typing.translate_constant Pure env kn (DefinitionEntry ce)
+ | OpaqueEff ce ->
+ let handle _env c () = (c, Univ.ContextSet.empty, 0) in
+ Term_typing.translate_constant (SideEffects handle) env kn (OpaqueEntry ce)
+ in
let map cu =
let (c, u) = Future.force cu in
let () = match u with
@@ -822,7 +833,7 @@ let add_constant (type a) ~(side_effect : a effect_entry) ~in_section l decl sen
seff_constant = kn;
seff_body = cb;
} in
- SideEffects.add eff empty_private_constants
+ { Entries.seff_wrap = SideEffects.add eff empty_private_constants }
in
(kn, eff), senv
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index c3d0965857..2406b6add1 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -79,7 +79,7 @@ val push_named_def :
(** Insertion of global axioms or definitions *)
type 'a effect_entry =
-| EffectEntry : private_constants effect_entry
+| EffectEntry : private_constants Entries.seff_wrap effect_entry
| PureEntry : unit effect_entry
type global_declaration =
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 5844bd89f8..b65e62ba30 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -31,7 +31,7 @@ type 'a effect_handler =
type _ trust =
| Pure : unit trust
-| SideEffects : 'a effect_handler -> 'a trust
+| SideEffects : 'a effect_handler -> 'a Entries.seff_wrap trust
let skip_trusted_seff sl b e =
let rec aux sl b e acc =
@@ -124,22 +124,14 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
Future.chain body begin fun ((body,uctx),side_eff) ->
(* don't redeclare universes which are declared for the type *)
let uctx = Univ.ContextSet.diff uctx univs in
- let j, uctx = match trust with
- | Pure ->
- let env = push_context_set uctx env in
- let j = Typeops.infer env body in
- let _ = Typeops.judge_of_cast env j DEFAULTcast tyj in
- j, uctx
- | SideEffects handle ->
- let (body, uctx', valid_signatures) = handle env body side_eff in
- let uctx = Univ.ContextSet.union uctx uctx' in
- let env = push_context_set uctx env in
- let body,env,ectx = skip_trusted_seff valid_signatures body env in
- let j = Typeops.infer env body in
- let j = unzip ectx j in
- let _ = Typeops.judge_of_cast env j DEFAULTcast tyj in
- j, uctx
- in
+ let SideEffects handle = trust in
+ let (body, uctx', valid_signatures) = handle env body side_eff in
+ let uctx = Univ.ContextSet.union uctx uctx' in
+ let env = push_context_set uctx env in
+ let body,env,ectx = skip_trusted_seff valid_signatures body env in
+ let j = Typeops.infer env body in
+ let j = unzip ectx j in
+ let _ = Typeops.judge_of_cast env j DEFAULTcast tyj in
let c = j.uj_val in
feedback_completion_typecheck feedback_id;
c, Opaqueproof.PrivateMonomorphic uctx
@@ -164,12 +156,9 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
let sbst, auctx = Univ.abstract_universes nas uctx in
let usubst = Univ.make_instance_subst sbst in
let proofterm = Future.chain body begin fun ((body, ctx), side_eff) ->
- let body, ctx = match trust with
- | Pure -> body, ctx
- | SideEffects handle ->
- let body, ctx', _ = handle env body side_eff in
- body, Univ.ContextSet.union ctx ctx'
- in
+ let SideEffects handle = trust in
+ let body, ctx', _ = handle env body side_eff in
+ let ctx = Univ.ContextSet.union ctx ctx' in
(** [ctx] must contain local universes, such that it has no impact
on the rest of the graph (up to transitivity). *)
let env = push_subgraph ctx env in
@@ -195,10 +184,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
| DefinitionEntry c ->
let { const_entry_type = typ; _ } = c in
let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in
- let () = match trust with
- | Pure -> ()
- | SideEffects _ -> assert false
- in
+ let Pure = trust in
let env, usubst, univs = match c.const_entry_universes with
| Monomorphic_entry ctx ->
let env = push_context_set ~strict:true ctx env in
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 225abd60f8..ef01ece185 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -24,7 +24,7 @@ type 'a effect_handler =
type _ trust =
| Pure : unit trust
-| SideEffects : 'a effect_handler -> 'a trust
+| SideEffects : 'a effect_handler -> 'a Entries.seff_wrap trust
val translate_local_def : env -> Id.t -> section_def_entry ->
constr * Sorts.relevance * types
diff --git a/tactics/declare.ml b/tactics/declare.ml
index c0eae7503c..b8ba62a5e5 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -205,7 +205,7 @@ let cast_proof_entry e =
const_entry_inline_code = e.proof_entry_inline_code;
}
-let cast_opaque_proof_entry (type a) (pure : a Safe_typing.effect_entry) (e : a Proof_global.proof_entry) =
+let cast_opaque_proof_entry e =
let open Proof_global in
let typ = match e.proof_entry_type with
| None -> assert false
@@ -220,14 +220,8 @@ let cast_opaque_proof_entry (type a) (pure : a Safe_typing.effect_entry) (e : a
Id.Set.empty, Id.Set.empty
else
let ids_typ = global_vars_set env typ in
- let pf, env = match pure with
- | PureEntry ->
- let (pf, _), () = Future.force e.proof_entry_body in
- pf, env
- | EffectEntry ->
- let (pf, _), eff = Future.force e.proof_entry_body in
- pf, Safe_typing.push_private_constants env eff
- in
+ let (pf, _), eff = Future.force e.proof_entry_body in
+ let env = Safe_typing.push_private_constants env eff in
let vars = global_vars_set env pf in
ids_typ, vars
in
@@ -253,37 +247,28 @@ let get_roles export eff =
let define_constant ~side_effect ~name cd =
let open Proof_global in
(* Logically define the constant and its subproofs, no libobject tampering *)
- let is_poly de = match de.proof_entry_universes with
- | Monomorphic_entry _ -> false
- | Polymorphic_entry _ -> true
- in
let in_section = Lib.sections_are_opened () in
- let export, decl = (* We deal with side effects *)
- match cd with
- | DefinitionEntry de when
- not de.proof_entry_opaque ||
- is_poly de ->
+ let export, decl = match cd with
+ | DefinitionEntry de ->
+ (* We deal with side effects *)
+ if not de.proof_entry_opaque then
(* This globally defines the side-effects in the environment. *)
let body, eff = Future.force de.proof_entry_body in
let body, export = Global.export_private_constants ~in_section (body, eff.Evd.seff_private) in
let export = get_roles export eff in
let de = { de with proof_entry_body = Future.from_val (body, ()) } in
- let cd = match de.proof_entry_opaque with
- | true -> Entries.OpaqueEntry (cast_opaque_proof_entry PureEntry de)
- | false -> Entries.DefinitionEntry (cast_proof_entry de)
- in
+ let cd = Entries.DefinitionEntry (cast_proof_entry de) in
export, ConstantEntry (PureEntry, cd)
- | DefinitionEntry de ->
- let () = assert (de.proof_entry_opaque) in
+ else
let map (body, eff) = body, eff.Evd.seff_private in
let body = Future.chain de.proof_entry_body map in
let de = { de with proof_entry_body = body } in
- let de = cast_opaque_proof_entry EffectEntry de in
+ let de = cast_opaque_proof_entry de in
[], ConstantEntry (EffectEntry, Entries.OpaqueEntry de)
- | ParameterEntry e ->
- [], ConstantEntry (PureEntry, Entries.ParameterEntry e)
- | PrimitiveEntry e ->
- [], ConstantEntry (PureEntry, Entries.PrimitiveEntry e)
+ | ParameterEntry e ->
+ [], ConstantEntry (PureEntry, Entries.ParameterEntry e)
+ | PrimitiveEntry e ->
+ [], ConstantEntry (PureEntry, Entries.PrimitiveEntry e)
in
let kn, eff = Global.add_constant ~side_effect ~in_section name decl in
kn, eff, export
@@ -304,7 +289,7 @@ let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind
| None -> Cmap.empty
| Some r -> Cmap.singleton kn r
in
- let eff = { Evd.seff_private = eff; Evd.seff_roles; } in
+ let eff = { Evd.seff_private = eff.Entries.seff_wrap; Evd.seff_roles; } in
kn, eff
(** Declaration of section variables and local definitions *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:11:04 +0000