aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cClosure.ml2
-rw-r--r--kernel/cClosure.mli2
-rw-r--r--kernel/cbytegen.mli2
-rw-r--r--kernel/cooking.ml6
-rw-r--r--kernel/cooking.mli8
-rw-r--r--kernel/declarations.ml10
-rw-r--r--kernel/declareops.mli12
-rw-r--r--kernel/environ.ml2
-rw-r--r--kernel/environ.mli12
-rw-r--r--kernel/nativecode.mli2
-rw-r--r--kernel/opaqueproof.ml5
-rw-r--r--kernel/opaqueproof.mli1
-rw-r--r--kernel/safe_typing.ml152
-rw-r--r--kernel/safe_typing.mli11
-rw-r--r--kernel/subtyping.ml2
-rw-r--r--kernel/term_typing.ml54
-rw-r--r--kernel/term_typing.mli8
17 files changed, 142 insertions, 149 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 412637c4b6..95f88c0306 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -389,7 +389,7 @@ type clos_infos = {
i_flags : reds;
i_cache : infos_cache }
-type clos_tab = fconstr constant_def KeyTable.t
+type clos_tab = (fconstr, Empty.t) constant_def KeyTable.t
let info_flags info = info.i_flags
let info_env info = info.i_cache.i_env
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index b1b69dded8..1a790eaed6 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -215,7 +215,7 @@ val eta_expand_ind_stack : env -> inductive -> fconstr -> stack ->
(** Conversion auxiliary functions to do step by step normalisation *)
(** [unfold_reference] unfolds references in a [fconstr] *)
-val unfold_reference : clos_infos -> clos_tab -> table_key -> fconstr constant_def
+val unfold_reference : clos_infos -> clos_tab -> table_key -> (fconstr, Util.Empty.t) constant_def
(***********************************************************************
i This is for lazy debug *)
diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
index 6a9550342c..bdaf5fe422 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/cbytegen.mli
@@ -20,7 +20,7 @@ val compile : fail_on_error:bool ->
(** init, fun, fv *)
val compile_constant_body : fail_on_error:bool ->
- env -> universes -> Constr.t Mod_subst.substituted constant_def ->
+ env -> universes -> (Constr.t Mod_subst.substituted, 'opaque) constant_def ->
body_code option
(** Shortcut of the previous function used during module strengthening *)
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 9b974c4ecc..9b6e37251f 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -152,11 +152,11 @@ let abstract_constant_body c (hyps, subst) =
let c = Vars.subst_vars subst c in
it_mkLambda_or_LetIn c hyps
-type recipe = { from : constant_body; info : Opaqueproof.cooking_info }
+type recipe = { from : Opaqueproof.opaque constant_body; info : Opaqueproof.cooking_info }
type inline = bool
-type result = {
- cook_body : constr Mod_subst.substituted constant_def;
+type 'opaque result = {
+ cook_body : (constr Mod_subst.substituted, 'opaque) constant_def;
cook_type : types;
cook_universes : universes;
cook_private_univs : Univ.ContextSet.t option;
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index b0f143c47d..b022e2ac09 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -13,12 +13,12 @@ open Declarations
(** {6 Cooking the constants. } *)
-type recipe = { from : constant_body; info : Opaqueproof.cooking_info }
+type recipe = { from : Opaqueproof.opaque constant_body; info : Opaqueproof.cooking_info }
type inline = bool
-type result = {
- cook_body : constr Mod_subst.substituted constant_def;
+type 'opaque result = {
+ cook_body : (constr Mod_subst.substituted, 'opaque) constant_def;
cook_type : types;
cook_universes : universes;
cook_private_univs : Univ.ContextSet.t option;
@@ -27,7 +27,7 @@ type result = {
cook_context : Constr.named_context option;
}
-val cook_constant : hcons:bool -> recipe -> result
+val cook_constant : hcons:bool -> recipe -> Opaqueproof.opaque result
val cook_constr : Opaqueproof.cooking_info -> constr -> constr
(** {6 Utility functions used in module [Discharge]. } *)
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 5551742c02..36ee952099 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -47,10 +47,10 @@ type inline = int option
transparent body, or an opaque one *)
(* Global declarations (i.e. constants) can be either: *)
-type 'a constant_def =
+type ('a, 'opaque) constant_def =
| Undef of inline (** a global assumption *)
| Def of 'a (** or a transparent global definition *)
- | OpaqueDef of Opaqueproof.opaque (** or an opaque global definition *)
+ | OpaqueDef of 'opaque (** or an opaque global definition *)
| Primitive of CPrimitives.t (** or a primitive operation *)
type universes =
@@ -87,9 +87,9 @@ type typing_flags = {
(* some contraints are in constant_constraints, some other may be in
* the OpaqueDef *)
-type constant_body = {
+type 'opaque constant_body = {
const_hyps : Constr.named_context; (** New: younger hyp at top *)
- const_body : Constr.t Mod_subst.substituted constant_def;
+ const_body : (Constr.t Mod_subst.substituted, 'opaque) constant_def;
const_type : types;
const_relevance : Sorts.relevance;
const_body_code : Cemitcodes.to_patch_substituted option;
@@ -246,7 +246,7 @@ type module_alg_expr =
(** A component of a module structure *)
type structure_field_body =
- | SFBconst of constant_body
+ | SFBconst of Opaqueproof.opaque constant_body
| SFBmind of mutual_inductive_body
| SFBmodule of module_body
| SFBmodtype of module_type_body
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index 54a853fc81..fb02c6a029 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -26,21 +26,21 @@ val map_decl_arity : ('a -> 'c) -> ('b -> 'd) ->
(** {6 Constants} *)
-val subst_const_body : substitution -> constant_body -> constant_body
+val subst_const_body : substitution -> Opaqueproof.opaque constant_body -> Opaqueproof.opaque constant_body
(** Is there a actual body in const_body ? *)
-val constant_has_body : constant_body -> bool
+val constant_has_body : 'a constant_body -> bool
-val constant_polymorphic_context : constant_body -> AUContext.t
+val constant_polymorphic_context : 'a constant_body -> AUContext.t
(** Is the constant polymorphic? *)
-val constant_is_polymorphic : constant_body -> bool
+val constant_is_polymorphic : 'a constant_body -> bool
(** Return the universe context, in case the definition is polymorphic, otherwise
the context is empty. *)
-val is_opaque : constant_body -> bool
+val is_opaque : 'a constant_body -> bool
(** {6 Inductive types} *)
@@ -83,7 +83,7 @@ val safe_flags : Conv_oracle.oracle -> typing_flags
of the structure, but simply hash-cons all inner constr
and other known elements *)
-val hcons_const_body : constant_body -> constant_body
+val hcons_const_body : 'a constant_body -> 'a constant_body
val hcons_mind : mutual_inductive_body -> mutual_inductive_body
val hcons_module_body : module_body -> module_body
val hcons_module_type : module_type_body -> module_type_body
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 617519a038..05f342a82a 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -46,7 +46,7 @@ type link_info =
| LinkedInteractive of string
| NotLinked
-type constant_key = constant_body * (link_info ref * key)
+type constant_key = Opaqueproof.opaque constant_body * (link_info ref * key)
type mind_key = mutual_inductive_body * link_info ref
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 4e6dbbe206..f6cd41861e 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -42,7 +42,7 @@ type link_info =
type key = int CEphemeron.key option ref
-type constant_key = constant_body * (link_info ref * key)
+type constant_key = Opaqueproof.opaque constant_body * (link_info ref * key)
type mind_key = mutual_inductive_body * link_info ref
@@ -174,19 +174,19 @@ val reset_with_named_context : named_context_val -> env -> env
val pop_rel_context : int -> env -> env
(** Useful for printing *)
-val fold_constants : (Constant.t -> constant_body -> 'a -> 'a) -> env -> 'a -> 'a
+val fold_constants : (Constant.t -> Opaqueproof.opaque constant_body -> 'a -> 'a) -> env -> 'a -> 'a
(** {5 Global constants }
{6 Add entries to global environment } *)
-val add_constant : Constant.t -> constant_body -> env -> env
-val add_constant_key : Constant.t -> constant_body -> link_info ->
+val add_constant : Constant.t -> Opaqueproof.opaque constant_body -> env -> env
+val add_constant_key : Constant.t -> Opaqueproof.opaque constant_body -> link_info ->
env -> env
val lookup_constant_key : Constant.t -> env -> constant_key
(** Looks up in the context of global constant names
raises [Not_found] if the required path is not found *)
-val lookup_constant : Constant.t -> env -> constant_body
+val lookup_constant : Constant.t -> env -> Opaqueproof.opaque constant_body
val evaluable_constant : Constant.t -> env -> bool
(** New-style polymorphism *)
@@ -219,7 +219,7 @@ val constant_context : env -> Constant.t -> Univ.AUContext.t
it lives in. For monomorphic constant, the latter is empty, and for
polymorphic constants, the term contains De Bruijn universe variables that
need to be instantiated. *)
-val body_of_constant_body : env -> constant_body -> (Constr.constr * Univ.AUContext.t) option
+val body_of_constant_body : env -> Opaqueproof.opaque constant_body -> (Constr.constr * Univ.AUContext.t) option
(* These functions should be called under the invariant that [env]
already contains the constraints corresponding to the constant
diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli
index 96efa7faa5..b5c03b6ca3 100644
--- a/kernel/nativecode.mli
+++ b/kernel/nativecode.mli
@@ -65,7 +65,7 @@ val empty_updates : code_location_updates
val register_native_file : string -> unit
val compile_constant_field : env -> string -> Constant.t ->
- global list -> constant_body -> global list
+ global list -> 'a constant_body -> global list
val compile_mind_field : ModPath.t -> Label.t ->
global list -> mutual_inductive_body -> global list
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 57059300b8..18c1bcc0f8 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -77,11 +77,6 @@ let subst_opaque sub = function
| Indirect (s,dp,i) -> Indirect (sub::s,dp,i)
| Direct _ -> CErrors.anomaly (Pp.str "Substituting a Direct opaque.")
-let iter_direct_opaque f = function
- | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
- | Direct (d,cu) ->
- Direct (d,Future.chain cu (fun (c, u) -> f c; c, u))
-
let discharge_direct_opaque ~cook_constr ci = function
| Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
| Direct (d,cu) ->
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index d47c0bbb3c..4e8956af06 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -43,7 +43,6 @@ val get_constraints :
opaquetab -> opaque -> Univ.ContextSet.t Future.computation option
val subst_opaque : substitution -> opaque -> opaque
-val iter_direct_opaque : (constr -> unit) -> opaque -> opaque
type work_list = (Univ.Instance.t * Id.t array) Cmap.t *
(Univ.Instance.t * Id.t array) Mindmap.t
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 75375812c0..a5d8a480ee 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -228,27 +228,10 @@ let check_engagement env expected_impredicative_set =
(** {6 Stm machinery } *)
-type seff_env =
- [ `Nothing
- (* The proof term and its universes.
- Same as the constant_body's but not in an ephemeron *)
- | `Opaque of Constr.t * Univ.ContextSet.t ]
-
-let get_opaque_body env cbo =
- match cbo.const_body with
- | Undef _ -> assert false
- | Primitive _ -> assert false
- | Def _ -> `Nothing
- | OpaqueDef opaque ->
- `Opaque
- (Opaqueproof.force_proof (Environ.opaque_tables env) opaque,
- Opaqueproof.force_constraints (Environ.opaque_tables env) opaque)
-
type side_effect = {
from_env : Declarations.structure_body CEphemeron.key;
seff_constant : Constant.t;
- seff_body : Declarations.constant_body;
- seff_env : seff_env;
+ seff_body : (Constr.t * Univ.ContextSet.t) Declarations.constant_body;
seff_role : Entries.side_effect_role;
}
@@ -288,39 +271,38 @@ type private_constants = SideEffects.t
let side_effects_of_private_constants l =
List.rev (SideEffects.repr l)
+(* Only used to push in an Environ.env. *)
+let lift_constant c =
+ let body = match c.const_body with
+ | OpaqueDef _ -> Undef None
+ | Def _ | Undef _ | Primitive _ as body -> body
+ in
+ { c with const_body = body }
+
+let map_constant f c =
+ let body = match c.const_body with
+ | OpaqueDef o -> OpaqueDef (f o)
+ | Def _ | Undef _ | Primitive _ as body -> body
+ in
+ { c with const_body = body }
+
let push_private_constants env eff =
let eff = side_effects_of_private_constants eff in
let add_if_undefined env eff =
try ignore(Environ.lookup_constant eff.seff_constant env); env
- with Not_found -> Environ.add_constant eff.seff_constant eff.seff_body env
+ with Not_found -> Environ.add_constant eff.seff_constant (lift_constant eff.seff_body) env
in
List.fold_left add_if_undefined env eff
let empty_private_constants = SideEffects.empty
let concat_private = SideEffects.concat
-let private_constant env role cst =
- (** The constant must be the last entry of the safe environment *)
- let () = match env.revstruct with
- | (lbl, SFBconst _) :: _ -> assert (Label.equal lbl (Constant.label cst))
- | _ -> assert false
- in
- let from_env = CEphemeron.create env.revstruct in
- let cbo = Environ.lookup_constant cst env.env in
- let eff = {
- from_env = from_env;
- seff_constant = cst;
- seff_body = cbo;
- seff_env = get_opaque_body env.env cbo;
- seff_role = role;
- } in
- SideEffects.add eff empty_private_constants
-
let universes_of_private eff =
let fold acc eff =
- let acc = match eff.seff_env with
- | `Nothing -> acc
- | `Opaque (_, ctx) -> ctx :: acc
+ 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
@@ -565,7 +547,6 @@ type 'a effect_entry =
type global_declaration =
| ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration
- | GlobalRecipe of Cooking.recipe
type exported_private_constant =
Constant.t * Entries.side_effect_role
@@ -598,7 +579,7 @@ let inline_side_effects env body side_eff =
let open Constr in
(** First step: remove the constants that are still in the environment *)
let filter e =
- let cb = (e.seff_constant, e.seff_body, e.seff_env) in
+ let cb = (e.seff_constant, e.seff_body) in
try ignore (Environ.lookup_constant e.seff_constant env); None
with Not_found -> Some (cb, e.from_env)
in
@@ -612,10 +593,10 @@ let inline_side_effects env body side_eff =
else
(** Second step: compute the lifts and substitutions to apply *)
let cname c r = Context.make_annot (Name (Label.to_id (Constant.label c))) r in
- let fold (subst, var, ctx, args) (c, cb, b) =
- let (b, opaque) = match cb.const_body, b with
- | Def b, _ -> (Mod_subst.force_constr b, false)
- | OpaqueDef _, `Opaque (b,_) -> (b, true)
+ 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)
| _ -> assert false
in
match cb.const_universes with
@@ -701,7 +682,8 @@ let check_signatures curmb sl =
| Some (n, _) -> n
-let constant_entry_of_side_effect cb u =
+let constant_entry_of_side_effect eff =
+ let cb = eff.seff_body in
let open Entries in
let univs =
match cb.const_universes with
@@ -711,9 +693,9 @@ let constant_entry_of_side_effect cb u =
Polymorphic_entry (Univ.AUContext.names auctx, Univ.AUContext.repr auctx)
in
let pt =
- match cb.const_body, u with
- | OpaqueDef _, `Opaque (b, c) -> b, c
- | Def b, `Nothing -> Mod_subst.force_constr b, Univ.ContextSet.empty
+ match cb.const_body with
+ | OpaqueDef (b, c) -> b, c
+ | Def b -> Mod_subst.force_constr b, Univ.ContextSet.empty
| _ -> assert false in
DefinitionEntry {
const_entry_body = Future.from_val (pt, ());
@@ -724,18 +706,6 @@ let constant_entry_of_side_effect cb u =
const_entry_opaque = Declareops.is_opaque cb;
const_entry_inline_code = cb.const_inline_code }
-let turn_direct orig =
- let cb = orig.seff_body in
- if Declareops.is_opaque cb then
- let p = match orig.seff_env with
- | `Opaque (b, c) -> (b, c)
- | _ -> assert false
- in
- let const_body = OpaqueDef (Opaqueproof.create (Future.from_val p)) in
- let cb = { cb with const_body } in
- { orig with seff_body = cb }
- else orig
-
let export_eff eff =
(eff.seff_constant, eff.seff_body, eff.seff_role)
@@ -756,13 +726,14 @@ let export_side_effects mb env c =
let trusted = check_signatures mb signatures in
let push_seff env eff =
let { seff_constant = kn; seff_body = cb ; _ } = eff in
- let env = Environ.add_constant kn cb env in
+ let env = Environ.add_constant kn (lift_constant cb) env in
match cb.const_universes with
| Polymorphic _ -> env
| Monomorphic ctx ->
- let ctx = match eff.seff_env with
- | `Nothing -> ctx
- | `Opaque(_, ctx') -> Univ.ContextSet.union ctx' 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
@@ -771,35 +742,39 @@ let export_side_effects mb env c =
| [] -> List.rev acc, ce
| eff :: rest ->
if Int.equal sl 0 then
- let env, cb =
- let { seff_constant = kn; seff_body = ocb; seff_env = u ; _ } = eff in
- let ce = constant_entry_of_side_effect ocb u in
+ 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 eff = { eff with
- seff_body = cb;
- seff_env = `Nothing;
- } in
+ let cb = map_constant Future.force cb in
+ let eff = { eff with seff_body = cb } in
(push_seff env eff, export_eff eff)
in
translate_seff 0 rest (cb :: acc) env
else
- let cb = turn_direct eff in
- let env = push_seff env cb in
- let ecb = export_eff cb in
+ let env = push_seff env eff in
+ let ecb = export_eff eff in
translate_seff (sl - 1) rest (ecb :: acc) env
in
translate_seff trusted seff [] env
let export_private_constants ~in_section ce senv =
let exported, ce = export_side_effects senv.revstruct senv.env ce in
- let bodies = List.map (fun (kn, cb, _) -> (kn, cb)) exported in
+ let map (kn, cb, _) = (kn, map_constant (fun p -> Opaqueproof.create (Future.from_val p)) cb) in
+ let bodies = List.map map exported in
let exported = List.map (fun (kn, _, r) -> (kn, r)) exported in
let senv = List.fold_left (add_constant_aux ~in_section) senv bodies in
(ce, exported), senv
-let add_constant ~in_section l decl senv =
+let add_recipe ~in_section l r senv =
+ let kn = Constant.make2 senv.modpath l in
+ let cb = Term_typing.translate_recipe ~hcons:(not in_section) senv.env kn r in
+ let cb = if in_section then cb else Declareops.hcons_const_body cb in
+ let senv = add_constant_aux ~in_section senv (kn, cb) in
+ kn, senv
+
+let add_constant ?role ~in_section l decl senv =
let kn = Constant.make2 senv.modpath l in
- let senv =
let cb =
match decl with
| ConstantEntry (EffectEntry, ce) ->
@@ -811,9 +786,9 @@ let add_constant ~in_section l decl senv =
Term_typing.translate_constant (Term_typing.SideEffects handle) senv.env kn ce
| ConstantEntry (PureEntry, ce) ->
Term_typing.translate_constant Term_typing.Pure senv.env kn ce
- | GlobalRecipe r ->
- let cb = Term_typing.translate_recipe ~hcons:(not in_section) senv.env kn r in
- if in_section then cb else Declareops.hcons_const_body cb in
+ in
+ let senv =
+ let cb = map_constant Opaqueproof.create cb in
add_constant_aux ~in_section senv (kn, cb) in
let senv =
match decl with
@@ -822,7 +797,20 @@ let add_constant ~in_section l decl senv =
add_retroknowledge (Retroknowledge.Register_type(t,kn)) senv
| _ -> senv
in
- kn, senv
+ let eff = match role with
+ | None -> empty_private_constants
+ | Some role ->
+ let cb = map_constant Future.force cb 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
+ (kn, eff), senv
(** Insertion of inductive types *)
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index d6c7022cf5..36ca3d8c47 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -48,9 +48,6 @@ val concat_private : private_constants -> private_constants -> private_constants
(** [concat_private e1 e2] adds the constants of [e1] to [e2], i.e. constants in
[e1] must be more recent than those of [e2]. *)
-val private_constant : safe_environment -> Entries.side_effect_role -> Constant.t -> private_constants
-(** Constant must be the last definition of the safe_environment. *)
-
val mk_pure_proof : Constr.constr -> private_constants Entries.proof_output
val inline_private_constants_in_constr :
Environ.env -> Constr.constr -> private_constants -> Constr.constr
@@ -91,7 +88,6 @@ type 'a effect_entry =
type global_declaration =
| ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration
- | GlobalRecipe of Cooking.recipe
type exported_private_constant =
Constant.t * Entries.side_effect_role
@@ -103,8 +99,11 @@ val export_private_constants : in_section:bool ->
(** returns the main constant plus a list of auxiliary constants (empty
unless one requires the side effects to be exported) *)
val add_constant :
- in_section:bool -> Label.t -> global_declaration ->
- Constant.t safe_transformer
+ ?role:Entries.side_effect_role -> in_section:bool -> Label.t -> global_declaration ->
+ (Constant.t * private_constants) safe_transformer
+
+val add_recipe :
+ in_section:bool -> Label.t -> Cooking.recipe -> Constant.t safe_transformer
(** Adding an inductive type *)
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 1857ea3329..24845ce459 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -31,7 +31,7 @@ open Mod_subst
an inductive type. It can also be useful to allow reorderings in
inductive types *)
type namedobject =
- | Constant of constant_body
+ | Constant of Opaqueproof.opaque constant_body
| IndType of inductive * mutual_inductive_body
| IndConstr of constructor * mutual_inductive_body
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index faa4411e92..74c6189a65 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -154,7 +154,7 @@ the polymorphic case
let c = Constr.hcons j.uj_val in
feedback_completion_typecheck feedback_id;
c, uctx) in
- let def = OpaqueDef (Opaqueproof.create proofterm) in
+ let def = OpaqueDef proofterm in
{
Cooking.cook_body = def;
cook_type = tyj.utj_val;
@@ -207,7 +207,7 @@ the polymorphic case
in
let def = Constr.hcons (Vars.subst_univs_level_constr usubst j.uj_val) in
let def =
- if opaque then OpaqueDef (Opaqueproof.create (Future.from_val (def, Univ.ContextSet.empty)))
+ if opaque then OpaqueDef (Future.from_val (def, Univ.ContextSet.empty))
else Def (Mod_subst.from_val def)
in
feedback_completion_typecheck feedback_id;
@@ -232,7 +232,7 @@ let record_aux env s_ty s_bo =
(keep_hyps env s_bo)) in
Aux_file.record_in_aux "context_used" v
-let build_constant_declaration _kn env result =
+let build_constant_declaration env result =
let open Cooking in
let typ = result.cook_type in
let check declared inferred =
@@ -271,11 +271,8 @@ let build_constant_declaration _kn env result =
| Undef _ | Primitive _ -> Id.Set.empty
| Def cs -> global_vars_set env (Mod_subst.force_constr cs)
| OpaqueDef lc ->
- let vars =
- global_vars_set env
- (Opaqueproof.force_proof (opaque_tables env) lc) in
- (* we force so that cst are added to the env immediately after *)
- ignore(Opaqueproof.force_constraints (opaque_tables env) lc);
+ let (lc, _) = Future.force lc in
+ let vars = global_vars_set env lc in
if !Flags.record_aux_file then record_aux env ids_typ vars;
vars
in
@@ -296,11 +293,15 @@ let build_constant_declaration _kn env result =
check declared inferred;
x
| OpaqueDef lc -> (* In this case we can postpone the check *)
- OpaqueDef (Opaqueproof.iter_direct_opaque (fun c ->
- let ids_typ = global_vars_set env typ in
- let ids_def = global_vars_set env c in
- let inferred = keep_hyps env (Id.Set.union ids_typ ids_def) in
- check declared inferred) lc) in
+ let iter k cu = Future.chain cu (fun (c, _ as p) -> k c; p) in
+ let kont c =
+ let ids_typ = global_vars_set env typ in
+ let ids_def = global_vars_set env c in
+ let inferred = keep_hyps env (Id.Set.union ids_typ ids_def) in
+ check declared inferred
+ in
+ OpaqueDef (iter kont lc)
+ in
let univs = result.cook_universes in
let tps =
let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs def in
@@ -318,8 +319,8 @@ let build_constant_declaration _kn env result =
(*s Global and local constant declaration. *)
-let translate_constant mb env kn ce =
- build_constant_declaration kn env
+let translate_constant mb env _kn ce =
+ build_constant_declaration env
(infer_declaration ~trust:mb env ce)
let translate_local_assum env t =
@@ -327,8 +328,21 @@ let translate_local_assum env t =
let t = Typeops.assumption_of_judgment env j in
j.uj_val, t
-let translate_recipe ~hcons env kn r =
- build_constant_declaration kn env (Cooking.cook_constant ~hcons r)
+let translate_recipe ~hcons env _kn r =
+ let open Cooking in
+ let result = Cooking.cook_constant ~hcons r in
+ let univs = result.cook_universes in
+ let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs result.cook_body in
+ let tps = Option.map Cemitcodes.from_val res in
+ { const_hyps = Option.get result.cook_context;
+ const_body = result.cook_body;
+ const_type = result.cook_type;
+ const_body_code = tps;
+ const_universes = univs;
+ const_private_poly_univs = result.cook_private_univs;
+ const_relevance = result.cook_relevance;
+ const_inline_code = result.cook_inline;
+ const_typing_flags = Environ.typing_flags env }
let translate_local_def env _id centry =
let open Cooking in
@@ -351,8 +365,7 @@ let translate_local_def env _id centry =
| Def _ -> ()
| OpaqueDef lc ->
let ids_typ = global_vars_set env typ in
- let ids_def = global_vars_set env
- (Opaqueproof.force_proof (opaque_tables env) lc) in
+ let ids_def = global_vars_set env (fst (Future.force lc)) in
record_aux env ids_typ ids_def
end;
let () = match decl.cook_universes with
@@ -362,8 +375,7 @@ let translate_local_def env _id centry =
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 (p, cst) = Future.force 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
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 1fa5eca2e3..592a97e132 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -33,14 +33,14 @@ val translate_local_assum : env -> types -> types * Sorts.relevance
val translate_constant :
'a trust -> env -> Constant.t -> 'a constant_entry ->
- constant_body
+ Opaqueproof.proofterm constant_body
-val translate_recipe : hcons:bool -> env -> Constant.t -> Cooking.recipe -> constant_body
+val translate_recipe : hcons:bool -> env -> Constant.t -> Cooking.recipe -> Opaqueproof.opaque constant_body
(** Internal functions, mentioned here for debug purpose only *)
val infer_declaration : trust:'a trust -> env ->
- 'a constant_entry -> Cooking.result
+ 'a constant_entry -> Opaqueproof.proofterm Cooking.result
val build_constant_declaration :
- Constant.t -> env -> Cooking.result -> constant_body
+ env -> Opaqueproof.proofterm Cooking.result -> Opaqueproof.proofterm constant_body
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:55:38 +0000