aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cooking.ml9
-rw-r--r--kernel/declareops.ml21
-rw-r--r--kernel/declareops.mli14
-rw-r--r--kernel/environ.ml2
-rw-r--r--kernel/environ.mli3
-rw-r--r--kernel/mod_typing.ml2
-rw-r--r--kernel/modops.ml29
-rw-r--r--kernel/modops.mli3
-rw-r--r--kernel/opaqueproof.ml121
-rw-r--r--kernel/opaqueproof.mli33
-rw-r--r--kernel/pre_env.ml11
-rw-r--r--kernel/pre_env.mli4
-rw-r--r--kernel/safe_typing.ml45
-rw-r--r--kernel/subtyping.ml6
-rw-r--r--kernel/term_typing.ml8
15 files changed, 191 insertions, 120 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 5f6aebc4e0..4127426116 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -161,10 +161,10 @@ let on_body ml hy f = function
OpaqueDef (Opaqueproof.discharge_direct_opaque ~cook_constr:f
{ Opaqueproof.modlist = ml; abstract = hy } o)
-let constr_of_def = function
+let constr_of_def otab = function
| Undef _ -> assert false
| Def cs -> Mod_subst.force_constr cs
- | OpaqueDef lc -> Opaqueproof.force_proof lc
+ | OpaqueDef lc -> Opaqueproof.force_proof otab lc
let expmod_constr_subst cache modlist subst c =
let c = expmod_constr cache modlist c in
@@ -189,7 +189,8 @@ let lift_univs cb subst =
subst, Univ.UContext.make (inst,cstrs')
else subst, cb.const_universes
-let cook_constant env { from = cb; info = { Opaqueproof.modlist; abstract } } =
+let cook_constant env { from = cb; info } =
+ let { Opaqueproof.modlist; abstract } = info in
let cache = RefTable.create 13 in
let abstract, usubst, abs_ctx = abstract in
let usubst, univs = lift_univs cb usubst in
@@ -211,7 +212,7 @@ let cook_constant env { from = cb; info = { Opaqueproof.modlist; abstract } } =
| TemplateArity (ctx,s) ->
let t = mkArity (ctx,Type s.template_level) in
let typ = abstract_constant_type (expmod t) hyps in
- let j = make_judge (constr_of_def body) typ in
+ let j = make_judge (constr_of_def (opaque_tables env) body) typ in
Typeops.make_polymorphic_if_constant_for_ind env j
in
let projection pb =
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 51e435d796..d993821293 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -42,10 +42,10 @@ let instantiate cb c =
Vars.subst_instance_constr (Univ.UContext.instance cb.const_universes) c
else c
-let body_of_constant cb = match cb.const_body with
+let body_of_constant otab cb = match cb.const_body with
| Undef _ -> None
| Def c -> Some (instantiate cb (force_constr c))
- | OpaqueDef o -> Some (instantiate cb (Opaqueproof.force_proof o))
+ | OpaqueDef o -> Some (instantiate cb (Opaqueproof.force_proof otab o))
let type_of_constant cb =
match cb.const_type with
@@ -54,23 +54,24 @@ let type_of_constant cb =
if t' == t then x else RegularArity t'
| TemplateArity _ as x -> x
-let constraints_of_constant cb = Univ.Constraint.union
+let constraints_of_constant otab cb = Univ.Constraint.union
(Univ.UContext.constraints cb.const_universes)
(match cb.const_body with
| Undef _ -> Univ.empty_constraint
| Def c -> Univ.empty_constraint
- | OpaqueDef o -> Univ.ContextSet.constraints (Opaqueproof.force_constraints o))
+ | OpaqueDef o ->
+ Univ.ContextSet.constraints (Opaqueproof.force_constraints otab o))
-let universes_of_constant cb =
+let universes_of_constant otab cb =
match cb.const_body with
| Undef _ | Def _ -> cb.const_universes
| OpaqueDef o ->
Univ.UContext.union cb.const_universes
- (Univ.ContextSet.to_context (Opaqueproof.force_constraints o))
+ (Univ.ContextSet.to_context (Opaqueproof.force_constraints otab o))
-let universes_of_polymorphic_constant cb =
+let universes_of_polymorphic_constant otab cb =
if cb.const_polymorphic then
- let univs = universes_of_constant cb in
+ let univs = universes_of_constant otab cb in
Univ.instantiate_univ_context univs
else Univ.UContext.empty
@@ -291,9 +292,9 @@ let hcons_mind mib =
(** {6 Stm machinery } *)
-let join_constant_body cb =
+let join_constant_body otab cb =
match cb.const_body with
- | OpaqueDef o -> Opaqueproof.join_opaque o
+ | OpaqueDef o -> Opaqueproof.join_opaque otab o
| _ -> ()
let string_of_side_effect = function
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index 04a067aff0..4978566765 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -28,15 +28,19 @@ val constant_has_body : constant_body -> bool
(** Accessing const_body, forcing access to opaque proof term if needed.
Only use this function if you know what you're doing. *)
-val body_of_constant : constant_body -> Term.constr option
+val body_of_constant :
+ Opaqueproof.opaquetab -> constant_body -> Term.constr option
val type_of_constant : constant_body -> constant_type
-val constraints_of_constant : constant_body -> Univ.constraints
-val universes_of_constant : constant_body -> Univ.universe_context
+val constraints_of_constant :
+ Opaqueproof.opaquetab -> constant_body -> Univ.constraints
+val universes_of_constant :
+ Opaqueproof.opaquetab -> constant_body -> Univ.universe_context
(** Return the universe context, in case the definition is polymorphic, otherwise
the context is empty. *)
-val universes_of_polymorphic_constant : constant_body -> Univ.universe_context
+val universes_of_polymorphic_constant :
+ Opaqueproof.opaquetab -> constant_body -> Univ.universe_context
val is_opaque : constant_body -> bool
@@ -71,7 +75,7 @@ val subst_wf_paths : substitution -> wf_paths -> wf_paths
val subst_mind_body : substitution -> mutual_inductive_body -> mutual_inductive_body
-val join_constant_body : constant_body -> unit
+val join_constant_body : Opaqueproof.opaquetab -> constant_body -> unit
(** {6 Hash-consing} *)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index b331d8da7a..c3e59487cb 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -57,6 +57,8 @@ let universes env = env.env_stratification.env_universes
let named_context env = env.env_named_context
let named_context_val env = env.env_named_context,env.env_named_vals
let rel_context env = env.env_rel_context
+let opaque_tables env = env.indirect_pterms
+let set_opaque_tables env indirect_pterms = { env with indirect_pterms }
let empty_context env =
match env.env_rel_context, env.env_named_context with
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 5e9e5264d9..a20944758b 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -46,6 +46,9 @@ val rel_context : env -> rel_context
val named_context : env -> named_context
val named_context_val : env -> named_context_val
+val opaque_tables : env -> Opaqueproof.opaquetab
+val set_opaque_tables : env -> Opaqueproof.opaquetab -> env
+
val engagement : env -> engagement option
val is_impredicative_set : env -> bool
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index cab3276c39..7a9b12c430 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -72,7 +72,7 @@ let rec check_with_def env struc (idl,c) mp equiv =
(* In the spirit of subtyping.check_constant, we accept
any implementations of parameters and opaques terms,
as long as they have the right type *)
- let ccst = Declareops.constraints_of_constant cb in
+ let ccst = Declareops.constraints_of_constant (opaque_tables env) cb in
let env' = Environ.add_constraints ccst env' in
let c',cst = match cb.const_body with
| Undef _ | OpaqueDef _ ->
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 859f83e052..585b38a081 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -612,19 +612,20 @@ let clean_bounded_mod_expr sign =
(** {6 Stm machinery } *)
-let rec join_module mb =
- implem_iter join_signature join_expression mb.mod_expr;
- Option.iter join_expression mb.mod_type_alg;
- join_signature mb.mod_type
-and join_modtype mt =
- Option.iter join_expression mt.typ_expr_alg;
- join_signature mt.typ_expr
-and join_field (l,body) = match body with
- |SFBconst sb -> join_constant_body sb
+let rec join_module otab mb =
+ implem_iter (join_signature otab) (join_expression otab) mb.mod_expr;
+ Option.iter (join_expression otab) mb.mod_type_alg;
+ join_signature otab mb.mod_type
+and join_modtype otab mt =
+ Option.iter (join_expression otab) mt.typ_expr_alg;
+ join_signature otab mt.typ_expr
+and join_field otab (l,body) = match body with
+ |SFBconst sb -> join_constant_body otab sb
|SFBmind _ -> ()
- |SFBmodule m -> join_module m
- |SFBmodtype m -> join_modtype m
-and join_structure struc = List.iter join_field struc
-and join_signature sign = functor_iter join_modtype join_structure sign
-and join_expression me = functor_iter join_modtype (fun _ -> ()) me
+ |SFBmodule m -> join_module otab m
+ |SFBmodtype m -> join_modtype otab m
+and join_structure otab struc = List.iter (join_field otab) struc
+and join_signature otab sign =
+ functor_iter (join_modtype otab) (join_structure otab) sign
+and join_expression otab me = functor_iter (join_modtype otab) (fun _ -> ()) me
diff --git a/kernel/modops.mli b/kernel/modops.mli
index 63d71a5669..0009b859ce 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -80,8 +80,7 @@ val clean_bounded_mod_expr : module_signature -> module_signature
(** {6 Stm machinery } *)
-val join_module : module_body -> unit
-val join_structure : structure_body -> unit
+val join_structure : Opaqueproof.opaquetab -> structure_body -> unit
(** {6 Errors } *)
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index a5def3dc8f..52e6eb95d8 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -21,7 +21,8 @@ type proofterm = (constr * Univ.universe_context_set) Future.computation
type opaque =
| Indirect of substitution list * DirPath.t * int (* subst, lib, index *)
| Direct of cooking_info list * proofterm
- | NoIndirect of substitution list * proofterm
+type opaquetab = (cooking_info list * proofterm) Int.Map.t * DirPath.t
+let empty_opaquetab = Int.Map.empty, DirPath.initial
(* hooks *)
let default_get_opaque dp _ =
@@ -31,87 +32,113 @@ let default_get_univ dp _ =
Errors.error
("Cannot access universe constraints of opaque proofs in library " ^
DirPath.to_string dp)
-let default_mk_indirect _ = None
-let default_join_indirect_local_opaque _ _ = ()
-let default_join_indirect_local_univ _ _ = ()
let get_opaque = ref default_get_opaque
let get_univ = ref default_get_univ
-let join_indirect_local_opaque = ref default_join_indirect_local_opaque
-let join_indirect_local_univ = ref default_join_indirect_local_univ
-let mk_indirect = ref default_mk_indirect
let set_indirect_opaque_accessor f = (get_opaque := f)
let set_indirect_univ_accessor f = (get_univ := f)
-let set_indirect_creator f = (mk_indirect := f)
-let set_join_indirect_local_opaque f = join_indirect_local_opaque := f
-let set_join_indirect_local_univ f = join_indirect_local_univ := f
-let reset_indirect_creator () = mk_indirect := default_mk_indirect
(* /hooks *)
let create cu = Direct ([],cu)
-let turn_indirect o = match o with
- | Indirect _
- | NoIndirect _ -> Errors.anomaly (Pp.str "Already an indirect opaque")
+let turn_indirect dp o (prfs,odp) = match o with
+ | Indirect _ -> Errors.anomaly (Pp.str "Already an indirect opaque")
| Direct (d,cu) ->
let cu = Future.chain ~pure:true cu (fun (c, u) -> hcons_constr c, u) in
- match !mk_indirect (d,cu) with
- | None -> Future.sink cu; NoIndirect([],cu)
- | Some (dp,i) -> Indirect ([],dp,i)
+ let id = Int.Map.cardinal prfs in
+ let prfs = Int.Map.add id (d,cu) prfs in
+ let ndp =
+ if DirPath.equal dp odp then odp
+ else if DirPath.equal odp DirPath.initial then dp
+ else Errors.anomaly
+ (Pp.str "Using the same opaque table for multiple dirpaths") in
+ Indirect ([],dp,id), (prfs, ndp)
let subst_opaque sub = function
| Indirect (s,dp,i) -> Indirect (sub::s,dp,i)
- | NoIndirect (s,uc) -> NoIndirect (sub::s,uc)
| Direct _ -> Errors.anomaly (Pp.str "Substituting a Direct opaque")
let iter_direct_opaque f = function
- | Indirect _
- | NoIndirect _ -> Errors.anomaly (Pp.str "Not a direct opaque")
+ | Indirect _ -> Errors.anomaly (Pp.str "Not a direct opaque")
| Direct (d,cu) ->
Direct (d,Future.chain ~pure:true cu (fun (c, u) -> f c; c, u))
let discharge_direct_opaque ~cook_constr ci = function
- | Indirect _
- | NoIndirect _ -> Errors.anomaly (Pp.str "Not a direct opaque")
+ | Indirect _ -> Errors.anomaly (Pp.str "Not a direct opaque")
| Direct (d,cu) ->
Direct (ci::d,Future.chain ~pure:true cu (fun (c, u) -> cook_constr c, u))
-let join_opaque = function
+let join_opaque (prfs,odp) = function
| Direct (_,cu) -> ignore(Future.join cu)
- | NoIndirect (_,cu) -> ignore(Future.join cu)
| Indirect (_,dp,i) ->
- !join_indirect_local_opaque dp i;
- !join_indirect_local_univ dp i
+ if DirPath.equal dp odp then
+ let fp = snd (Int.Map.find i prfs) in
+ ignore(Future.join fp)
-let force_proof = function
+let uuid_opaque (prfs,odp) = function
+ | Direct (_,cu) -> Some (Future.uuid cu)
+ | Indirect (_,dp,i) ->
+ if DirPath.equal dp odp
+ then Some (Future.uuid (snd (Int.Map.find i prfs)))
+ else None
+
+let force_proof (prfs,odp) = function
| Direct (_,cu) ->
fst(Future.force cu)
- | NoIndirect (l,cu) ->
- let c, _ = Future.force cu in
- force_constr (List.fold_right subst_substituted l (from_val c))
| Indirect (l,dp,i) ->
- let c = Future.force (!get_opaque dp i) in
+ let pt =
+ if DirPath.equal dp odp
+ then Future.chain ~pure:true (snd (Int.Map.find i prfs)) fst
+ else !get_opaque dp i in
+ let c = Future.force pt in
force_constr (List.fold_right subst_substituted l (from_val c))
-let force_constraints = function
- | Direct (_,cu)
- | NoIndirect(_,cu) -> snd(Future.force cu)
+let force_constraints (prfs,odp) = function
+ | Direct (_,cu) -> snd(Future.force cu)
| Indirect (_,dp,i) ->
- match !get_univ dp i with
- | None -> Univ.ContextSet.empty
- | Some u -> Future.force u
-
-let get_constraints = function
- | Direct (_,cu)
- | NoIndirect(_,cu) -> Some(Future.chain ~pure:true cu snd)
- | Indirect (_,dp,i) -> !get_univ dp i
+ if DirPath.equal dp odp
+ then snd (Future.force (snd (Int.Map.find i prfs)))
+ else match !get_univ dp i with
+ | None -> Univ.ContextSet.empty
+ | Some u -> Future.force u
+
+let get_constraints (prfs,odp) = function
+ | Direct (_,cu) -> Some(Future.chain ~pure:true cu snd)
+ | Indirect (_,dp,i) ->
+ if DirPath.equal dp odp
+ then Some(Future.chain ~pure:true (snd (Int.Map.find i prfs)) snd)
+ else !get_univ dp i
-let get_proof = function
+let get_proof (prfs,odp) = function
| Direct (_,cu) -> Future.chain ~pure:true cu fst
- | NoIndirect(l,cu) ->
- Future.chain ~pure:true cu (fun (c,_) ->
- force_constr (List.fold_right subst_substituted l (from_val c)))
| Indirect (l,dp,i) ->
- Future.chain ~pure:true (!get_opaque dp i) (fun c ->
+ let pt =
+ if DirPath.equal dp odp
+ then Future.chain ~pure:true (snd (Int.Map.find i prfs)) fst
+ else !get_opaque dp i in
+ Future.chain ~pure:true pt (fun c ->
force_constr (List.fold_right subst_substituted l (from_val c)))
+
+module FMap = Future.UUIDMap
+
+let a_constr = Future.from_val (Term.mkRel 1)
+let a_univ = Future.from_val Univ.ContextSet.empty
+let a_discharge : cooking_info list = []
+
+let dump (otab,_) =
+ let n = Int.Map.cardinal otab in
+ let opaque_table = Array.make n a_constr in
+ let univ_table = Array.make n a_univ in
+ let disch_table = Array.make n a_discharge in
+ let f2t_map = ref FMap.empty in
+ Int.Map.iter (fun n (d,cu) ->
+ let c, u = Future.split2 ~greedy:true cu in
+ Future.sink u;
+ Future.sink c;
+ opaque_table.(n) <- c;
+ univ_table.(n) <- u;
+ disch_table.(n) <- d;
+ f2t_map := FMap.add (Future.uuid cu) n !f2t_map)
+ otab;
+ opaque_table, univ_table, disch_table, !f2t_map
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 092f0aeb17..5f1c282925 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -9,6 +9,7 @@
open Names
open Term
open Mod_subst
+open Int
(** This module implements the handling of opaque proof terms.
Opauqe proof terms are special since:
@@ -20,20 +21,25 @@ open Mod_subst
and the [opaque] is turned into an index. *)
type proofterm = (constr * Univ.universe_context_set) Future.computation
+type opaquetab
type opaque
+val empty_opaquetab : opaquetab
+
(** From a [proofterm] to some [opaque]. *)
val create : proofterm -> opaque
-(** Turn a direct [opaque] into an indirect one, also hashconses constr *)
-val turn_indirect : opaque -> opaque
+(** Turn a direct [opaque] into an indirect one, also hashconses constr.
+ * The integer is an hint of the maximum id used so far *)
+val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab
(** From a [opaque] back to a [constr]. This might use the
indirect opaque accessor configured below. *)
-val force_proof : opaque -> constr
-val force_constraints : opaque -> Univ.universe_context_set
-val get_proof : opaque -> Term.constr Future.computation
-val get_constraints : opaque -> Univ.universe_context_set Future.computation option
+val force_proof : opaquetab -> opaque -> constr
+val force_constraints : opaquetab -> opaque -> Univ.universe_context_set
+val get_proof : opaquetab -> opaque -> Term.constr Future.computation
+val get_constraints :
+ opaquetab -> opaque -> Univ.universe_context_set Future.computation option
val subst_opaque : substitution -> opaque -> opaque
val iter_direct_opaque : (constr -> unit) -> opaque -> opaque
@@ -52,7 +58,14 @@ type cooking_info = {
val discharge_direct_opaque :
cook_constr:(constr -> constr) -> cooking_info -> opaque -> opaque
-val join_opaque : opaque -> unit
+val uuid_opaque : opaquetab -> opaque -> Future.UUID.t option
+val join_opaque : opaquetab -> opaque -> unit
+
+val dump : opaquetab ->
+ Constr.t Future.computation array *
+ Univ.universe_context_set Future.computation array *
+ cooking_info list array *
+ int Future.UUIDMap.t
(** When stored indirectly, opaque terms are indexed by their library
dirpath and an integer index. The following two functions activate
@@ -61,12 +74,8 @@ val join_opaque : opaque -> unit
any indirect link, and default accessor always raises an error.
*)
-val set_indirect_creator :
- (cooking_info list * proofterm -> (DirPath.t * int) option) -> unit
val set_indirect_opaque_accessor :
(DirPath.t -> int -> Term.constr Future.computation) -> unit
val set_indirect_univ_accessor :
(DirPath.t -> int -> Univ.universe_context_set Future.computation option) -> unit
-val set_join_indirect_local_opaque : (DirPath.t -> int -> unit) -> unit
-val set_join_indirect_local_univ : (DirPath.t -> int -> unit) -> unit
-val reset_indirect_creator : unit -> unit
+
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index a5221c7794..48043f116f 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -74,7 +74,9 @@ type env = {
env_nb_rel : int;
env_stratification : stratification;
env_conv_oracle : Conv_oracle.oracle;
- retroknowledge : Retroknowledge.retroknowledge }
+ retroknowledge : Retroknowledge.retroknowledge;
+ indirect_pterms : Opaqueproof.opaquetab;
+}
type named_context_val = named_context * named_vals
@@ -96,7 +98,8 @@ let empty_env = {
env_engagement = None;
env_type_in_type = false};
env_conv_oracle = Conv_oracle.empty;
- retroknowledge = Retroknowledge.initial_retroknowledge }
+ retroknowledge = Retroknowledge.initial_retroknowledge;
+ indirect_pterms = Opaqueproof.empty_opaquetab }
(* Rel context *)
@@ -141,7 +144,9 @@ let push_named d env =
env_nb_rel = env.env_nb_rel;
env_stratification = env.env_stratification;
env_conv_oracle = env.env_conv_oracle;
- retroknowledge = env.retroknowledge; }
+ retroknowledge = env.retroknowledge;
+ indirect_pterms = env.indirect_pterms;
+ }
let lookup_named_val id env =
snd(List.find (fun (id',_) -> Id.equal id id') env.env_named_vals)
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index 9561333c8d..7ef2ab0098 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -54,7 +54,9 @@ type env = {
env_nb_rel : int;
env_stratification : stratification;
env_conv_oracle : Conv_oracle.oracle;
- retroknowledge : Retroknowledge.retroknowledge }
+ retroknowledge : Retroknowledge.retroknowledge;
+ indirect_pterms : Opaqueproof.opaquetab;
+}
type named_context_val = named_context * named_vals
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index f7464013fd..9aca7727b1 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -125,7 +125,7 @@ type safe_environment =
type_in_type : bool;
imports : vodigest DPMap.t;
loads : (module_path * module_body) list;
- local_retroknowledge : Retroknowledge.action list}
+ local_retroknowledge : Retroknowledge.action list }
and modvariant =
| NONE
@@ -133,6 +133,12 @@ and modvariant =
| SIG of module_parameters * safe_environment (** saved env *)
| STRUCT of module_parameters * safe_environment (** saved env *)
+let rec library_dp_of_senv senv =
+ match senv.modvariant with
+ | NONE | LIBRARY -> ModPath.dp senv.modpath
+ | SIG(_,senv) -> library_dp_of_senv senv
+ | STRUCT(_,senv) -> library_dp_of_senv senv
+
let empty_environment =
{ env = Environ.empty_env;
modpath = initial_path;
@@ -219,7 +225,7 @@ let is_curmod_library senv =
match senv.modvariant with LIBRARY -> true | _ -> false
let join_safe_environment e =
- Modops.join_structure e.revstruct;
+ Modops.join_structure (Environ.opaque_tables e.env) e.revstruct;
List.fold_left
(fun e fc -> add_constraints (Now (Future.join fc)) e)
{e with future_cst = []} e.future_cst
@@ -312,9 +318,12 @@ let push_named_def (id,de) senv =
let c,typ,univs = Term_typing.translate_local_def senv.env id de in
let senv' = push_context univs senv in
let c, senv' = match c with
- | Def c -> Mod_subst.force_constr c, senv'
- | OpaqueDef o -> Opaqueproof.force_proof o,
- push_context_set (Opaqueproof.force_constraints o) senv'
+ | Def c -> Mod_subst.force_constr c, senv'
+ | OpaqueDef o ->
+ Opaqueproof.force_proof (Environ.opaque_tables senv'.env) o,
+ push_context_set
+ (Opaqueproof.force_constraints (Environ.opaque_tables senv'.env) o)
+ senv'
| _ -> assert false in
let env'' = safe_push_named (id,Some c,typ) senv'.env in
{senv' with env=env''}
@@ -341,7 +350,7 @@ let labels_of_mib mib =
Array.iter visit_mip mib.mind_packets;
get ()
-let globalize_constant_universes cb =
+let globalize_constant_universes env cb =
if cb.const_polymorphic then
[Now Univ.Constraint.empty]
else
@@ -350,7 +359,7 @@ let globalize_constant_universes cb =
(match cb.const_body with
| (Undef _ | Def _) -> []
| OpaqueDef lc ->
- match Opaqueproof.get_constraints lc with
+ match Opaqueproof.get_constraints (Environ.opaque_tables env) lc with
| None -> []
| Some fc ->
match Future.peek_val fc with
@@ -363,9 +372,9 @@ let globalize_mind_universes mb =
else
[Now (Univ.UContext.constraints mb.mind_universes)]
-let constraints_of_sfb sfb =
+let constraints_of_sfb env sfb =
match sfb with
- | SFBconst cb -> globalize_constant_universes cb
+ | SFBconst cb -> globalize_constant_universes env cb
| SFBmind mib -> globalize_mind_universes mib
| SFBmodtype mtb -> [Now mtb.typ_constraints]
| SFBmodule mb -> [Now mb.mod_constraints]
@@ -389,7 +398,7 @@ let add_field ((l,sfb) as field) gn senv =
| SFBmodule _ | SFBmodtype _ ->
check_modlabel l senv; (Label.Set.singleton l, Label.Set.empty)
in
- let cst = constraints_of_sfb sfb in
+ let cst = constraints_of_sfb senv.env sfb in
let senv = add_constraints_list cst senv in
let env' = match sfb, gn with
| SFBconst cb, C con -> Environ.add_constant con cb senv.env
@@ -421,13 +430,17 @@ let add_constant dir l decl senv =
let cb = Term_typing.translate_recipe senv.env kn r in
if DirPath.is_empty dir then Declareops.hcons_const_body cb else cb
in
- let cb = match cb.const_body with
+ let cb, otab = match cb.const_body with
| OpaqueDef lc when DirPath.is_empty dir ->
(* In coqc, opaque constants outside sections will be stored
indirectly in a specific table *)
- { cb with const_body = OpaqueDef (Opaqueproof.turn_indirect lc) }
- | _ -> cb
+ let od, otab =
+ Opaqueproof.turn_indirect
+ (library_dp_of_senv senv) lc (Environ.opaque_tables senv.env) in
+ { cb with const_body = OpaqueDef od }, otab
+ | _ -> cb, (Environ.opaque_tables senv.env)
in
+ let senv = { senv with env = Environ.set_opaque_tables senv.env otab } in
let senv' = add_field (l,SFBconst cb) (C kn) senv in
let senv'' = match cb.const_body with
| Undef (Some lev) ->
@@ -588,7 +601,7 @@ let propagate_senv newdef newenv newresolver senv oldsenv =
imports = senv.imports;
loads = senv.loads@oldsenv.loads;
local_retroknowledge =
- senv.local_retroknowledge@oldsenv.local_retroknowledge }
+ senv.local_retroknowledge@oldsenv.local_retroknowledge }
let end_module l restype senv =
let mp = senv.modpath in
@@ -597,7 +610,7 @@ let end_module l restype senv =
let () = check_empty_context senv in
let mbids = List.rev_map fst params in
let mb = build_module_body params restype senv in
- let newenv = oldsenv.env in
+ let newenv = Environ.set_opaque_tables oldsenv.env (Environ.opaque_tables senv.env) in
let newenv = set_engagement_opt newenv senv.engagement in
let senv'=
propagate_loads { senv with
@@ -619,7 +632,7 @@ let end_modtype l senv =
let () = check_empty_context senv in
let mbids = List.rev_map fst params in
let auto_tb = NoFunctor (List.rev senv.revstruct) in
- let newenv = oldsenv.env in
+ let newenv = Environ.set_opaque_tables oldsenv.env (Environ.opaque_tables senv.env) in
let newenv = Environ.add_constraints senv.univ newenv in
let newenv = set_engagement_opt newenv senv.engagement in
let senv' = propagate_loads {senv with env=newenv} in
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 4f54220e72..857f577a81 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -352,7 +352,8 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
let u1 = inductive_instance mind1 in
let arity1,cst1 = constrained_type_of_inductive env
((mind1,mind1.mind_packets.(i)),u1) in
- let cst2 = Declareops.constraints_of_constant cb2 in
+ let cst2 =
+ Declareops.constraints_of_constant (Environ.opaque_tables env) cb2 in
let typ2 = Typeops.type_of_constant_type env cb2.const_type in
let cst = Constraint.union cst (Constraint.union cst1 cst2) in
let error = NotConvertibleTypeField (env, arity1, typ2) in
@@ -367,7 +368,8 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
if Declareops.constant_has_body cb2 then error DefinitionFieldExpected;
let u1 = inductive_instance mind1 in
let ty1,cst1 = constrained_type_of_constructor (cstr,u1) (mind1,mind1.mind_packets.(i)) in
- let cst2 = Declareops.constraints_of_constant cb2 in
+ let cst2 =
+ Declareops.constraints_of_constant (Environ.opaque_tables env) cb2 in
let ty2 = Typeops.type_of_constant_type env cb2.const_type in
let cst = Constraint.union cst (Constraint.union cst1 cst2) in
let error = NotConvertibleTypeField (env, ty1, ty2) in
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 232508bc82..415e91f706 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -86,7 +86,7 @@ let handle_side_effects env body side_eff =
let univs = cb.const_universes in
sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t)
| OpaqueDef b ->
- let b = Opaqueproof.force_proof b in
+ let b = Opaqueproof.force_proof (opaque_tables env) b in
let poly = cb.const_polymorphic in
if not poly then
let b_ty = Typeops.type_of_constant_type env cb.const_type in
@@ -217,9 +217,11 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
| Undef _ -> Idset.empty
| Def cs -> global_vars_set env (Mod_subst.force_constr cs)
| OpaqueDef lc ->
- let vars = global_vars_set env (Opaqueproof.force_proof lc) in
+ 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 lc);
+ ignore(Opaqueproof.force_constraints (opaque_tables env) lc);
!suggest_proof_using kn env vars ids_typ context_ids;
if !Flags.compilation_mode = Flags.BuildVo then
record_aux env ids_typ vars;
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 03:56:14 +0000