aboutsummaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/assumptions.ml2
-rw-r--r--library/declare.ml5
-rw-r--r--library/global.ml19
-rw-r--r--library/global.mli8
-rw-r--r--library/heads.ml2
-rw-r--r--library/library.ml94
-rw-r--r--library/library.mli4
-rw-r--r--library/universes.ml10
8 files changed, 47 insertions, 97 deletions
diff --git a/library/assumptions.ml b/library/assumptions.ml
index e4638f5e42..b01e24196c 100644
--- a/library/assumptions.ml
+++ b/library/assumptions.ml
@@ -236,7 +236,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st (* t *) =
else (s, acc)
else (s, acc)
in
- match Declareops.body_of_constant cb with
+ match Global.body_of_constant_body cb with
| None -> do_type (Axiom kn)
| Some body -> do_constr body s acc
diff --git a/library/declare.ml b/library/declare.ml
index 1c9e10a190..4ec81c49fc 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -116,7 +116,7 @@ let open_constant i ((sp,kn), obj) =
match (Global.lookup_constant con).const_body with
| (Def _ | Undef _) -> ()
| OpaqueDef lc ->
- match Opaqueproof.get_constraints lc with
+ match Opaqueproof.get_constraints (Global.opaque_tables ())lc with
| Some f when Future.is_val f -> Global.push_context_set (Future.force f)
| _ -> ()
@@ -208,7 +208,8 @@ let declare_sideff env fix_exn se =
match cb with
| { const_body = Def sc } -> (Mod_subst.force_constr sc, Univ.ContextSet.empty), false
| { const_body = OpaqueDef fc } ->
- (Opaqueproof.force_proof fc, Opaqueproof.force_constraints fc), true
+ (Opaqueproof.force_proof (Environ.opaque_tables env) fc,
+ Opaqueproof.force_constraints (Environ.opaque_tables env) fc), true
| { const_body = Undef _ } -> anomaly(str"Undefined side effect")
in
let ty_of cb =
diff --git a/library/global.ml b/library/global.ml
index 80238d8e2d..49f78e4955 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -113,6 +113,14 @@ let lookup_modtype kn = lookup_modtype kn (env())
let exists_objlabel id = Safe_typing.exists_objlabel id (safe_env ())
+let opaque_tables () = Environ.opaque_tables (env ())
+let body_of_constant_body cb = Declareops.body_of_constant (opaque_tables ()) cb
+let body_of_constant cst = body_of_constant_body (lookup_constant cst)
+let constraints_of_constant_body cb =
+ Declareops.constraints_of_constant (opaque_tables ()) cb
+let universes_of_constant_body cb =
+ Declareops.universes_of_constant (opaque_tables ()) cb
+
(** Operations on kernel names *)
let constant_of_delta_kn kn =
@@ -153,7 +161,9 @@ let type_of_global_unsafe r =
| VarRef id -> Environ.named_type id env
| ConstRef c ->
let cb = Environ.lookup_constant c env in
- let univs = Declareops.universes_of_polymorphic_constant cb in
+ let univs =
+ Declareops.universes_of_polymorphic_constant
+ (Environ.opaque_tables env) cb in
let ty = Typeops.type_of_constant_type env cb.Declarations.const_type in
Vars.subst_instance_constr (Univ.UContext.instance univs) ty
| IndRef ind ->
@@ -175,7 +185,9 @@ let type_of_global_in_context env r =
| VarRef id -> Environ.named_type id env, Univ.UContext.empty
| ConstRef c ->
let cb = Environ.lookup_constant c env in
- let univs = Declareops.universes_of_polymorphic_constant cb in
+ let univs =
+ Declareops.universes_of_polymorphic_constant
+ (Environ.opaque_tables env) cb in
Typeops.type_of_constant_type env cb.Declarations.const_type, univs
| IndRef ind ->
let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
@@ -198,7 +210,8 @@ let universes_of_global env r =
| VarRef id -> Univ.UContext.empty
| ConstRef c ->
let cb = Environ.lookup_constant c env in
- Declareops.universes_of_polymorphic_constant cb
+ Declareops.universes_of_polymorphic_constant
+ (Environ.opaque_tables env) cb
| IndRef ind ->
let (mib, oib) = Inductive.lookup_mind_specif env ind in
Univ.instantiate_univ_context mib.mind_universes
diff --git a/library/global.mli b/library/global.mli
index 7dcfdbd3a0..8ae77a9e4c 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -87,6 +87,14 @@ val exists_objlabel : Label.t -> bool
val constant_of_delta_kn : kernel_name -> constant
val mind_of_delta_kn : kernel_name -> mutual_inductive
+val opaque_tables : unit -> Opaqueproof.opaquetab
+val body_of_constant : constant -> Term.constr option
+val body_of_constant_body : Declarations.constant_body -> Term.constr option
+val constraints_of_constant_body :
+ Declarations.constant_body -> Univ.constraints
+val universes_of_constant_body :
+ Declarations.constant_body -> Univ.universe_context
+
(** {6 Compiled libraries } *)
val start_library : DirPath.t -> module_path
diff --git a/library/heads.ml b/library/heads.ml
index 8b28f05003..94ce117317 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -123,7 +123,7 @@ let compute_head = function
let is_Def = function Declarations.Def _ -> true | _ -> false in
let body =
if cb.Declarations.const_proj = None && is_Def cb.Declarations.const_body
- then Declareops.body_of_constant cb else None
+ then Declareops.body_of_constant (Environ.opaque_tables env) cb else None
in
(match body with
| None -> RigidHead (RigidParameter cst)
diff --git a/library/library.ml b/library/library.ml
index 7bff05cda2..7f5ca5af63 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -351,87 +351,15 @@ let access_opaque_table dp i =
(fetch_table "opaque proofs")
add_opaque_table !opaque_tables dp i
let access_univ_table dp i =
- access_table
- (fetch_table "universe contexts of opaque proofs")
- add_univ_table !univ_tables dp i
-
-(** Table of opaque terms from the library currently being compiled *)
-
-module OpaqueTables = struct
-
- let a_constr = Future.from_val (Term.mkRel 1)
- let a_univ = Future.from_val Univ.ContextSet.empty
- let a_discharge : Opaqueproof.cooking_info list = []
-
- let local_opaque_table = ref (Array.make 100 a_constr)
- let local_univ_table = ref (Array.make 100 a_univ)
- let local_discharge_table = ref (Array.make 100 a_discharge)
- let local_index = ref 0
-
- module FMap = Map.Make(Future.UUID)
- let f2t = ref FMap.empty
-
- let get_opaque dp i =
- if DirPath.equal dp (Lib.library_dp ())
- then (!local_opaque_table).(i)
- else access_opaque_table dp i
-
- let join_local_opaque dp i =
- if DirPath.equal dp (Lib.library_dp ()) then
- ignore(Future.force (!local_opaque_table).(i))
-
- let join_local_univ dp i =
- if DirPath.equal dp (Lib.library_dp ()) then
- ignore(Future.join (!local_univ_table).(i))
-
- let get_univ dp i =
- if DirPath.equal dp (Lib.library_dp ())
- then Some (!local_univ_table).(i)
- else try Some (access_univ_table dp i) with Not_found -> None
-
- let store (d,cu) =
- let n = !local_index in
- incr local_index;
- if Int.equal n (Array.length !local_opaque_table) then begin
- let t = Array.make (2*n) a_constr in
- Array.blit !local_opaque_table 0 t 0 n;
- local_opaque_table := t;
- let t = Array.make (2*n) a_univ in
- Array.blit !local_univ_table 0 t 0 n;
- local_univ_table := t;
- let t = Array.make (2*n) a_discharge in
- Array.blit !local_discharge_table 0 t 0 n;
- local_discharge_table := t
- end;
- let c, u = Future.split2 ~greedy:true cu in
- Future.sink u;
- Future.sink c;
- (!local_opaque_table).(n) <- c;
- (!local_univ_table).(n) <- u;
- (!local_discharge_table).(n) <- d;
- f2t := FMap.add (Future.uuid cu) n !f2t;
- Some (Lib.library_dp (), n)
-
- let dump () =
- Array.sub !local_opaque_table 0 !local_index,
- Array.sub !local_univ_table 0 !local_index,
- Array.sub !local_discharge_table 0 !local_index,
- FMap.bindings !f2t
-
- let reset () =
- local_discharge_table := Array.make 100 a_discharge;
- local_univ_table := Array.make 100 a_univ;
- local_opaque_table := Array.make 100 a_constr;
- f2t := FMap.empty;
- local_index := 0
-
-end
+ try
+ Some (access_table
+ (fetch_table "universe contexts of opaque proofs")
+ add_univ_table !univ_tables dp i)
+ with Not_found -> None
let () =
- Opaqueproof.set_indirect_opaque_accessor OpaqueTables.get_opaque;
- Opaqueproof.set_indirect_univ_accessor OpaqueTables.get_univ;
- Opaqueproof.set_join_indirect_local_opaque OpaqueTables.join_local_opaque;
- Opaqueproof.set_join_indirect_local_univ OpaqueTables.join_local_univ
+ Opaqueproof.set_indirect_opaque_accessor access_opaque_table;
+ Opaqueproof.set_indirect_univ_accessor access_univ_table
(************************************************************************)
(* Internalise libraries *)
@@ -694,8 +622,6 @@ let start_library f =
check_module_name file;
check_coq_overwriting ldir0 id;
let ldir = add_dirpath_suffix ldir0 id in
- OpaqueTables.reset ();
- Opaqueproof.set_indirect_creator OpaqueTables.store;
Declaremods.start_library ldir;
ldir,longf
@@ -743,7 +669,7 @@ let error_recursively_dependent_library dir =
(* Security weakness: file might have been changed on disk between
writing the content and computing the checksum... *)
-let save_library_to ?todo dir f =
+let save_library_to ?todo dir f otab =
let f, todo, utab, dtab =
match todo with
| None ->
@@ -753,10 +679,8 @@ let save_library_to ?todo dir f =
assert(!Flags.compilation_mode = Flags.BuildVi);
f ^ "i", (fun x -> Some (d x)),
(fun x -> Some (x,Univ.ContextSet.empty,false)), (fun x -> Some x) in
- Opaqueproof.reset_indirect_creator ();
let cenv, seg, ast = Declaremods.end_library dir in
- let opaque_table, univ_table, disch_table, f2t_map =
- OpaqueTables.dump () in
+ let opaque_table, univ_table, disch_table, f2t_map = Opaqueproof.dump otab in
assert(!Flags.compilation_mode = Flags.BuildVi ||
Array.for_all Future.is_val opaque_table);
let md = {
diff --git a/library/library.mli b/library/library.mli
index 5154c25e41..c92b9d623c 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -43,8 +43,8 @@ val import_module : bool -> qualid located -> unit
val start_library : string -> DirPath.t * string
(** {6 End the compilation of a library and save it to a ".vo" file } *)
-val save_library_to : ?todo:((Future.UUID.t * int) list -> 'tasks) ->
- DirPath.t -> string -> unit
+val save_library_to : ?todo:(int Future.UUIDMap.t -> 'tasks) ->
+ DirPath.t -> string -> Opaqueproof.opaquetab -> unit
val load_library_todo :
string -> string * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs
diff --git a/library/universes.ml b/library/universes.ml
index cc0153311b..708324aede 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -310,7 +310,10 @@ let unsafe_instance_from ctx =
let fresh_constant_instance env c inst =
let cb = lookup_constant c env in
if cb.Declarations.const_polymorphic then
- let inst, ctx = fresh_instance_from (Declareops.universes_of_constant cb) inst in
+ let inst, ctx =
+ fresh_instance_from
+ (Declareops.universes_of_constant (Environ.opaque_tables env) cb) inst
+ in
((c, inst), ctx)
else ((c,Instance.empty), ContextSet.empty)
@@ -331,7 +334,8 @@ let fresh_constructor_instance env (ind,i) inst =
let unsafe_constant_instance env c =
let cb = lookup_constant c env in
if cb.Declarations.const_polymorphic then
- let inst, ctx = unsafe_instance_from (Declareops.universes_of_constant cb) in
+ let inst, ctx = unsafe_instance_from
+ (Declareops.universes_of_constant (Environ.opaque_tables env) cb) in
((c, inst), ctx)
else ((c,Instance.empty), UContext.empty)
@@ -441,7 +445,7 @@ let type_of_reference env r =
let cb = Environ.lookup_constant c env in
let ty = Typeops.type_of_constant_type env cb.const_type in
if cb.const_polymorphic then
- let inst, ctx = fresh_instance_from (Declareops.universes_of_constant cb) None in
+ let inst, ctx = fresh_instance_from (Declareops.universes_of_constant (Environ.opaque_tables env) cb) None in
Vars.subst_instance_constr inst ty, ctx
else ty, ContextSet.empty
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 19:39:26 +0000