aboutsummaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/coqlib.ml6
-rw-r--r--library/decl_kinds.ml11
-rw-r--r--library/declaremods.ml116
-rw-r--r--library/declaremods.mli15
-rw-r--r--library/global.ml13
-rw-r--r--library/global.mli13
-rw-r--r--library/goptions.ml4
-rw-r--r--library/lib.ml182
-rw-r--r--library/lib.mli7
-rw-r--r--library/libobject.ml2
-rw-r--r--library/libobject.mli2
-rw-r--r--library/library.ml642
-rw-r--r--library/library.mli77
-rw-r--r--library/library.mllib2
-rw-r--r--library/states.ml8
-rw-r--r--library/states.mli3
16 files changed, 150 insertions, 953 deletions
diff --git a/library/coqlib.ml b/library/coqlib.ml
index b1e4ef2b00..11d053624c 100644
--- a/library/coqlib.ml
+++ b/library/coqlib.ml
@@ -104,8 +104,10 @@ let gen_reference_in_modules locstr dirs s =
let check_required_library d =
let dir = make_dir d in
- if Library.library_is_loaded dir then ()
- else
+ try
+ let _ : Declarations.module_body = Global.lookup_module (ModPath.MPfile dir) in
+ ()
+ with Not_found ->
let in_current_dir = match Lib.current_mp () with
| MPfile dp -> DirPath.equal dir dp
| _ -> false
diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
deleted file mode 100644
index 17746645ee..0000000000
--- a/library/decl_kinds.ml
+++ /dev/null
@@ -1,11 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-type binding_kind = Explicit | Implicit
diff --git a/library/declaremods.ml b/library/declaremods.ml
index eea129eae7..b4dc42bdfe 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -110,9 +110,9 @@ and subst_objects subst seg =
| IncludeObject aobjs ->
let aobjs' = subst_aobjs subst aobjs in
if aobjs' == aobjs then node else (id, IncludeObject aobjs')
- | ImportObject { export; mp } ->
- let mp' = subst_mp subst mp in
- if mp'==mp then node else (id, ImportObject { export; mp = mp' })
+ | ExportObject { mpl } ->
+ let mpl' = List.map (subst_mp subst) mpl in
+ if mpl'==mpl then node else (id, ExportObject { mpl = mpl' })
| KeepObject _ -> assert false
in
List.Smart.map subst_one seg
@@ -151,7 +151,11 @@ let expand_sobjs (_,aobjs) = expand_aobjs aobjs
Module M:SIG. ... End M. have the keep list empty.
*)
-type module_objects = Nametab.object_prefix * Lib.lib_objects * Lib.lib_objects
+type module_objects =
+ { module_prefix : Nametab.object_prefix;
+ module_substituted_objects : Lib.lib_objects;
+ module_keep_objects : Lib.lib_objects;
+ }
module ModObjs :
sig
@@ -217,7 +221,13 @@ let do_module exists iter_objects i obj_dir obj_mp sobjs kobjs =
(* If we're not a functor, let's iter on the internal components *)
if sobjs_no_functor sobjs then begin
let objs = expand_sobjs sobjs in
- ModObjs.set obj_mp (prefix,objs,kobjs);
+ let module_objects =
+ { module_prefix = prefix;
+ module_substituted_objects = objs;
+ module_keep_objects = kobjs;
+ }
+ in
+ ModObjs.set obj_mp module_objects;
iter_objects (i+1) prefix objs;
iter_objects (i+1) prefix kobjs
end
@@ -233,7 +243,7 @@ let do_module' exists iter_objects i ((sp,kn),sobjs) =
(** Nota: Interactive modules and module types cannot be recached!
This used to be checked more properly here. *)
-let do_modtype i sp mp sobjs =
+let load_modtype i sp mp sobjs =
if Nametab.exists_modtype sp then
anomaly (pr_path sp ++ str " already exists.");
Nametab.push_modtype (Nametab.Until i) sp mp;
@@ -247,9 +257,9 @@ let rec load_object i (name, obj) =
| ModuleObject sobjs -> do_module' false load_objects i (name, sobjs)
| ModuleTypeObject sobjs ->
let (sp,kn) = name in
- do_modtype i sp (mp_of_kn kn) sobjs
+ load_modtype i sp (mp_of_kn kn) sobjs
| IncludeObject aobjs -> load_include i (name, aobjs)
- | ImportObject _ -> ()
+ | ExportObject _ -> ()
| KeepObject objs -> load_keep i (name, objs)
and load_objects i prefix objs =
@@ -266,32 +276,69 @@ and load_keep i ((sp,kn),kobjs) =
(* Invariant : seg isn't empty *)
let obj_dir = dir_of_sp sp and obj_mp = mp_of_kn kn in
let prefix = Nametab.{ obj_dir ; obj_mp; obj_sec = DirPath.empty } in
- let prefix',sobjs,kobjs0 =
+ let modobjs =
try ModObjs.get obj_mp
with Not_found -> assert false (* a substobjs should already be loaded *)
in
- assert Nametab.(eq_op prefix' prefix);
- assert (List.is_empty kobjs0);
- ModObjs.set obj_mp (prefix,sobjs,kobjs);
+ assert Nametab.(eq_op modobjs.module_prefix prefix);
+ assert (List.is_empty modobjs.module_keep_objects);
+ ModObjs.set obj_mp { modobjs with module_keep_objects = kobjs };
load_objects i prefix kobjs
(** {6 Implementation of Import and Export commands} *)
-let rec really_import_module mp =
+let mark_object obj (exports,acc) =
+ (exports, obj::acc)
+
+let rec collect_module_objects mp acc =
(* May raise Not_found for unknown module and for functors *)
- let prefix,sobjs,keepobjs = ModObjs.get mp in
- open_objects 1 prefix sobjs;
- open_objects 1 prefix keepobjs
+ let modobjs = ModObjs.get mp in
+ let prefix = modobjs.module_prefix in
+ let acc = collect_objects 1 prefix modobjs.module_keep_objects acc in
+ collect_objects 1 prefix modobjs.module_substituted_objects acc
+
+and collect_object i (name, obj as o) acc =
+ match obj with
+ | ExportObject { mpl; _ } -> collect_export i mpl acc
+ | AtomicObject _ | IncludeObject _ | KeepObject _
+ | ModuleObject _ | ModuleTypeObject _ -> mark_object o acc
+
+and collect_objects i prefix objs acc =
+ List.fold_right (fun (id, obj) acc -> collect_object i (Lib.make_oname prefix id, obj) acc) objs acc
+
+and collect_one_export mp (exports,objs as acc) =
+ if not (MPset.mem mp exports) then
+ collect_module_objects mp (MPset.add mp exports, objs)
+ else acc
+
+and collect_export i mpl acc =
+ if Int.equal i 1 then
+ List.fold_right collect_one_export mpl acc
+ else acc
-and open_object i (name, obj) =
+let rec open_object i (name, obj) =
match obj with
| AtomicObject o -> Libobject.open_object i (name, o)
- | ModuleObject sobjs -> do_module' true open_objects i (name, sobjs)
+ | ModuleObject sobjs ->
+ let dir = dir_of_sp (fst name) in
+ let mp = mp_of_kn (snd name) in
+ open_module i dir mp sobjs
| ModuleTypeObject sobjs -> open_modtype i (name, sobjs)
| IncludeObject aobjs -> open_include i (name, aobjs)
- | ImportObject { mp; _ } -> open_import i mp
+ | ExportObject { mpl; _ } -> open_export i mpl
| KeepObject objs -> open_keep i (name, objs)
+and open_module i obj_dir obj_mp sobjs =
+ let prefix = Nametab.{ obj_dir ; obj_mp; obj_sec = DirPath.empty } in
+ let dirinfo = Nametab.GlobDirRef.DirModule prefix in
+ consistency_checks true obj_dir dirinfo;
+ Nametab.push_dir (Nametab.Exactly i) obj_dir dirinfo;
+ (* If we're not a functor, let's iter on the internal components *)
+ if sobjs_no_functor sobjs then begin
+ let modobjs = ModObjs.get obj_mp in
+ open_objects (i+1) modobjs.module_prefix modobjs.module_substituted_objects
+ end
+
and open_objects i prefix objs =
List.iter (fun (id, obj) -> open_object i (Lib.make_oname prefix id, obj)) objs
@@ -312,8 +359,9 @@ and open_include i ((sp,kn), aobjs) =
let o = expand_aobjs aobjs in
open_objects i prefix o
-and open_import i mp =
- if Int.equal i 1 then really_import_module mp
+and open_export i mpl =
+ let _,objs = collect_export i mpl (MPset.empty, []) in
+ List.iter (open_object 1) objs
and open_keep i ((sp,kn),kobjs) =
let obj_dir = dir_of_sp sp and obj_mp = mp_of_kn kn in
@@ -326,9 +374,9 @@ let rec cache_object (name, obj) =
| ModuleObject sobjs -> do_module' false load_objects 1 (name, sobjs)
| ModuleTypeObject sobjs ->
let (sp,kn) = name in
- do_modtype 1 sp (mp_of_kn kn) sobjs
+ load_modtype 0 sp (mp_of_kn kn) sobjs
| IncludeObject aobjs -> cache_include (name, aobjs)
- | ImportObject { mp } -> really_import_module mp
+ | ExportObject { mpl } -> anomaly Pp.(str "Export should not be cached")
| KeepObject objs -> cache_keep (name, objs)
and cache_include ((sp,kn), aobjs) =
@@ -975,9 +1023,13 @@ let end_library ?except ~output_native_objects dir =
let substitute, keep, _ = Lib.classify_segment lib_stack in
cenv,(substitute,keep),ast
-let import_module export mp =
- really_import_module mp;
- Lib.add_anonymous_entry (Lib.Leaf (ImportObject { export; mp }))
+let import_modules ~export mpl =
+ let _,objs = List.fold_right collect_module_objects mpl (MPset.empty, []) in
+ List.iter (open_object 1) objs;
+ if export then Lib.add_anonymous_entry (Lib.Leaf (ExportObject { mpl }))
+
+let import_module ~export mp =
+ import_modules ~export [mp]
(** {6 Iterators} *)
@@ -988,9 +1040,10 @@ let iter_all_segments f =
List.iter (apply_obj prefix) objs
| _ -> f (Lib.make_oname prefix id) obj
in
- let apply_mod_obj _ (prefix,substobjs,keepobjs) =
- List.iter (apply_obj prefix) substobjs;
- List.iter (apply_obj prefix) keepobjs
+ let apply_mod_obj _ modobjs =
+ let prefix = modobjs.module_prefix in
+ List.iter (apply_obj prefix) modobjs.module_substituted_objects;
+ List.iter (apply_obj prefix) modobjs.module_keep_objects
in
let apply_node = function
| sp, Lib.Leaf o -> f sp o
@@ -1016,9 +1069,10 @@ let debug_print_modtab _ =
| [] -> str "[]"
| l -> str "[." ++ int (List.length l) ++ str ".]"
in
- let pr_modinfo mp (prefix,substobjs,keepobjs) s =
+ let pr_modinfo mp modobjs s =
+ let objs = modobjs.module_substituted_objects @ modobjs.module_keep_objects in
s ++ str (ModPath.to_string mp) ++ (spc ())
- ++ (pr_seg (Lib.segment_of_objects prefix (substobjs@keepobjs)))
+ ++ (pr_seg (Lib.segment_of_objects modobjs.module_prefix objs))
in
let modules = MPmap.fold pr_modinfo (ModObjs.all ()) (mt ()) in
hov 0 modules
diff --git a/library/declaremods.mli b/library/declaremods.mli
index ada53dbff0..b7c7cd1dba 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -103,18 +103,17 @@ val end_library :
(** append a function to be executed at end_library *)
val append_end_library_hook : (unit -> unit) -> unit
-(** [really_import_module mp] opens the module [mp] (in a Caml sense).
+(** [import_module export mp] imports the module [mp].
It modifies Nametab and performs the [open_object] function for
every object of the module. Raises [Not_found] when [mp] is unknown
- or when [mp] corresponds to a functor. *)
-
-val really_import_module : ModPath.t -> unit
-
-(** [import_module export mp] is a synchronous version of
- [really_import_module]. If [export] is [true], the module is also
+ or when [mp] corresponds to a functor. If [export] is [true], the module is also
opened every time the module containing it is. *)
-val import_module : bool -> ModPath.t -> unit
+val import_module : export:bool -> ModPath.t -> unit
+
+(** Same as [import_module] but for multiple modules, and more optimized than
+ iterating [import_module]. *)
+val import_modules : export:bool -> ModPath.t list -> unit
(** Include *)
diff --git a/library/global.ml b/library/global.ml
index 0fc9e11364..3d28178d7b 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -83,6 +83,7 @@ let i2l = Label.of_id
let push_named_assum a = globalize0 (Safe_typing.push_named_assum a)
let push_named_def d = globalize0 (Safe_typing.push_named_def d)
+let push_section_context c = globalize0 (Safe_typing.push_section_context c)
let add_constraints c = globalize0 (Safe_typing.add_constraints c)
let push_context_set b c = globalize0 (Safe_typing.push_context_set b c)
@@ -104,6 +105,13 @@ let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl)
let add_module id me inl = globalize (Safe_typing.add_module (i2l id) me inl)
let add_include me ismod inl = globalize (Safe_typing.add_include me ismod inl)
+let open_section ~poly = globalize0 (Safe_typing.open_section ~poly)
+let close_section fs =
+ (* TODO: use globalize0_with_summary *)
+ Summary.unfreeze_summaries fs;
+ let env = Safe_typing.close_section (safe_env ()) in
+ GlobalSafeEnv.set_safe_env env
+
let start_module id = globalize (Safe_typing.start_module (i2l id))
let start_modtype id = globalize (Safe_typing.start_modtype (i2l id))
@@ -119,6 +127,7 @@ let add_module_parameter mbid mte inl =
(** Queries on the global environment *)
let universes () = universes (env())
+let universes_lbound () = universes_lbound (env())
let named_context () = named_context (env())
let named_context_val () = named_context_val (env())
@@ -181,6 +190,10 @@ let is_polymorphic r = Environ.is_polymorphic (env()) r
let is_template_polymorphic r = is_template_polymorphic (env ()) r
+let is_template_checked r = is_template_checked (env ()) r
+
+let get_template_polymorphic_variables r = get_template_polymorphic_variables (env ()) r
+
let is_type_in_type r = is_type_in_type (env ()) r
let current_modpath () =
diff --git a/library/global.mli b/library/global.mli
index b089b7dd80..b809e9b241 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -22,6 +22,7 @@ val env : unit -> Environ.env
val env_is_initial : unit -> bool
val universes : unit -> UGraph.t
+val universes_lbound : unit -> Univ.Level.t
val named_context_val : unit -> Environ.named_context_val
val named_context : unit -> Constr.named_context
@@ -43,6 +44,7 @@ val sprop_allowed : unit -> bool
val push_named_assum : (Id.t * Constr.types) -> unit
val push_named_def : (Id.t * Entries.section_def_entry) -> unit
+val push_section_context : (Name.t array * Univ.UContext.t) -> unit
val export_private_constants : in_section:bool ->
Safe_typing.private_constants Entries.proof_output ->
@@ -70,6 +72,15 @@ val add_include :
Entries.module_struct_entry -> bool -> Declarations.inline ->
Mod_subst.delta_resolver
+(** Sections *)
+
+val open_section : poly:bool -> unit
+(** [poly] is true when the section should be universe polymorphic *)
+
+val close_section : Summary.frozen -> unit
+(** Close the section and reset the global state to the one at the time when
+ the section what opened. *)
+
(** Interactive modules and module types *)
val start_module : Id.t -> ModPath.t
@@ -136,6 +147,8 @@ val is_joined_environment : unit -> bool
val is_polymorphic : GlobRef.t -> bool
val is_template_polymorphic : GlobRef.t -> bool
+val is_template_checked : GlobRef.t -> bool
+val get_template_polymorphic_variables : GlobRef.t -> Univ.Level.t list
val is_type_in_type : GlobRef.t -> bool
(** {6 Retroknowledge } *)
diff --git a/library/goptions.ml b/library/goptions.ml
index c7024ca81d..0973944fb5 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -398,9 +398,9 @@ let print_option_value key =
let s = read () in
match s with
| BoolValue b ->
- Feedback.msg_info (str "The " ++ str name ++ str " mode is " ++ str (if b then "on" else "off"))
+ Feedback.msg_notice (str "The " ++ str name ++ str " mode is " ++ str (if b then "on" else "off"))
| _ ->
- Feedback.msg_info (str "Current value of " ++ str name ++ str " is " ++ msg_option_value (name, s))
+ Feedback.msg_notice (str "Current value of " ++ str name ++ str " is " ++ msg_option_value (name, s))
let get_tables () =
let tables = !value_tab in
diff --git a/library/lib.ml b/library/lib.ml
index 6b01eb07e9..1c6f82e8a6 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -73,11 +73,8 @@ let classify_segment seg =
clean ((id,o)::substl, keepl, anticipl) stk
| KeepObject _ ->
clean (substl, (id,o)::keepl, anticipl) stk
- | ImportObject { export } ->
- if export then
- clean ((id,o)::substl, keepl, anticipl) stk
- else
- clean acc stk
+ | ExportObject _ ->
+ clean ((id,o)::substl, keepl, anticipl) stk
| AtomicObject obj ->
begin match classify_object obj with
| Dispose -> clean acc stk
@@ -413,91 +410,11 @@ let find_opening_node id =
- the list of substitution to do at section closing
*)
-type abstr_info = {
+type abstr_info = Section.abstr_info = private {
abstr_ctx : Constr.named_context;
abstr_subst : Univ.Instance.t;
abstr_uctx : Univ.AUContext.t;
}
-type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t
-
-type secentry =
- | Variable of {
- id:Names.Id.t;
- }
- | Context of Univ.ContextSet.t
-
-type section_data = {
- sec_entry : secentry list;
- sec_abstr : abstr_list;
- sec_poly : bool;
-}
-
-let empty_section_data ~poly = {
- sec_entry = [];
- sec_abstr = (Names.Cmap.empty,Names.Mindmap.empty);
- sec_poly = poly;
-}
-
-let sectab =
- Summary.ref ([] : section_data list) ~name:"section-context"
-
-let sec_implicits =
- Summary.ref Id.Map.empty ~name:"section-implicits"
-
-let check_same_poly p sec =
- if p != sec.sec_poly then
- user_err Pp.(str "Cannot mix universe polymorphic and monomorphic declarations in sections.")
-
-let add_section ~poly () =
- List.iter (fun tab -> check_same_poly poly tab) !sectab;
- sectab := empty_section_data ~poly :: !sectab
-
-let add_section_variable ~name ~kind ~poly =
- match !sectab with
- | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
- | s :: sl ->
- List.iter (fun tab -> check_same_poly poly tab) !sectab;
- let s = { s with sec_entry = Variable {id=name} :: s.sec_entry } in
- sectab := s :: sl;
- sec_implicits := Id.Map.add name kind !sec_implicits
-
-let add_section_context ctx =
- match !sectab with
- | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
- | s :: sl ->
- check_same_poly true s;
- let s = { s with sec_entry = Context ctx :: s.sec_entry } in
- sectab := s :: sl
-
-exception PolyFound (* make this a let exception once possible *)
-let is_polymorphic_univ u =
- try
- let open Univ in
- List.iter (fun s ->
- let vars = s.sec_entry in
- List.iter (function
- | Variable _ -> ()
- | Context (univs,_) ->
- if LSet.mem u univs then raise PolyFound
- ) vars
- ) !sectab;
- false
- with PolyFound -> true
-
-let extract_hyps poly (secs,ohyps) =
- let rec aux = function
- | (Variable {id}::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) ->
- let l, r = aux (idl,hyps) in
- decl :: l, r
- | (Variable _::idl,hyps) ->
- let l, r = aux (idl,hyps) in
- l, r
- | (Context ctx :: idl, hyps) ->
- let () = assert poly in
- let l, r = aux (idl, hyps) in
- l, Univ.ContextSet.union r ctx
- | [], _ -> [],Univ.ContextSet.empty
- in aux (secs,ohyps)
let instance_from_variable_context =
List.rev %> List.filter is_local_assum %> List.map NamedDecl.get_id %> Array.of_list
@@ -506,66 +423,21 @@ let extract_worklist info =
let args = instance_from_variable_context info.abstr_ctx in
info.abstr_subst, args
-let make_worklist (cmap, mmap) =
- Cmap.map extract_worklist cmap, Mindmap.map extract_worklist mmap
-
-let name_instance inst =
- (* FIXME: this should probably be done at an upper level, by storing the
- name information in the section data structure. *)
- let map lvl = match Univ.Level.name lvl with
- | None -> (* Having Prop/Set/Var as section universes makes no sense *)
- assert false
- | Some na ->
- try
- let qid = Nametab.shortest_qualid_of_universe na in
- Name (Libnames.qualid_basename qid)
- with Not_found ->
- (* Best-effort naming from the string representation of the level.
- See univNames.ml for a similar hack. *)
- Name (Id.of_string_soft (Univ.Level.to_string lvl))
- in
- Array.map map (Univ.Instance.to_array inst)
-
-let add_section_replacement g poly hyps =
- match !sectab with
- | [] -> ()
- | s :: sl ->
- let () = check_same_poly poly s in
- let sechyps,ctx = extract_hyps s.sec_poly (s.sec_entry, hyps) in
- let ctx = Univ.ContextSet.to_context ctx in
- let nas = name_instance (Univ.UContext.instance ctx) in
- let subst, ctx = Univ.abstract_universes nas ctx in
- let info = {
- abstr_ctx = sechyps;
- abstr_subst = subst;
- abstr_uctx = ctx;
- } in
- let s = { s with
- sec_abstr = g info s.sec_abstr;
- } in
- sectab := s :: sl
-
-let add_section_kn ~poly kn =
- let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in
- add_section_replacement f poly
-
-let add_section_constant ~poly kn =
- let f x (l1,l2) = (Names.Cmap.add kn x l1,l2) in
- add_section_replacement f poly
-
-let replacement_context () = make_worklist (List.hd !sectab).sec_abstr
+let sections () = Safe_typing.sections_of_safe_env @@ Global.safe_env ()
+
+let is_polymorphic_univ u =
+ Section.is_polymorphic_univ u (sections ())
+
+let replacement_context () =
+ Section.replacement_context (Global.env ()) (sections ())
let section_segment_of_constant con =
- Names.Cmap.find con (fst (List.hd !sectab).sec_abstr)
+ Section.segment_of_constant (Global.env ()) con (sections ())
let section_segment_of_mutual_inductive kn =
- Names.Mindmap.find kn (snd (List.hd !sectab).sec_abstr)
+ Section.segment_of_inductive (Global.env ()) kn (sections ())
-let empty_segment = {
- abstr_ctx = [];
- abstr_subst = Univ.Instance.empty;
- abstr_uctx = Univ.AUContext.empty;
-}
+let empty_segment = Section.empty_segment
let section_segment_of_reference = let open GlobRef in function
| ConstRef c -> section_segment_of_constant c
@@ -576,30 +448,24 @@ let section_segment_of_reference = let open GlobRef in function
let variable_section_segment_of_reference gr =
(section_segment_of_reference gr).abstr_ctx
-let variable_section_kind id = Id.Map.get id !sec_implicits
+let is_in_section ref =
+ Section.is_in_section (Global.env ()) ref (sections ())
let section_instance = let open GlobRef in function
| VarRef id ->
- let eq = function
- | Variable {id=id'} -> Names.Id.equal id id'
- | Context _ -> false
- in
- if List.exists eq (List.hd !sectab).sec_entry
- then Univ.Instance.empty, [||]
- else raise Not_found
+ if is_in_section (VarRef id) then (Univ.Instance.empty, [||])
+ else raise Not_found
| ConstRef con ->
- let data = Names.Cmap.find con (fst (List.hd !sectab).sec_abstr) in
+ let data = section_segment_of_constant con in
extract_worklist data
| IndRef (kn,_) | ConstructRef ((kn,_),_) ->
- let data = Names.Mindmap.find kn (snd (List.hd !sectab).sec_abstr) in
+ let data = section_segment_of_mutual_inductive kn in
extract_worklist data
-let is_in_section ref =
- try ignore (section_instance ref); true with Not_found -> false
-
(*************)
(* Sections. *)
let open_section ~poly id =
+ let () = Global.open_section ~poly in
let opp = !lib_state.path_prefix in
let obj_dir = add_dirpath_suffix opp.Nametab.obj_dir id in
let prefix = Nametab.{ obj_dir; obj_mp = opp.obj_mp; obj_sec = add_dirpath_suffix opp.obj_sec id } in
@@ -609,9 +475,7 @@ let open_section ~poly id =
add_entry (make_foname id) (OpenedSection (prefix, fs));
(*Pushed for the lifetime of the section: removed by unfrozing the summary*)
Nametab.(push_dir (Until 1) obj_dir (GlobDirRef.DirOpenSection prefix));
- lib_state := { !lib_state with path_prefix = prefix };
- add_section ~poly ()
-
+ lib_state := { !lib_state with path_prefix = prefix }
(* Restore lib_stk and summaries as before the section opening, and
add a ClosedSection object. *)
@@ -621,7 +485,7 @@ let discharge_item ((sp,_ as oname),e) =
| Leaf lobj ->
begin match lobj with
| ModuleObject _ | ModuleTypeObject _ | IncludeObject _ | KeepObject _
- | ImportObject _ -> None
+ | ExportObject _ -> None
| AtomicObject obj ->
Option.map (fun o -> (basename sp,o)) (discharge_object (oname,obj))
end
@@ -640,7 +504,7 @@ let close_section () =
lib_state := { !lib_state with lib_stk = before };
pop_path_prefix ();
let newdecls = List.map discharge_item secdecls in
- Summary.unfreeze_summaries fs;
+ let () = Global.close_section fs in
List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls
(* State and initialization. *)
diff --git a/library/lib.mli b/library/lib.mli
index 7dc8b52282..5ce601f2d3 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -163,7 +163,7 @@ val drop_objects : frozen -> frozen
val init : unit -> unit
(** {6 Section management for discharge } *)
-type abstr_info = private {
+type abstr_info = Section.abstr_info = private {
abstr_ctx : Constr.named_context;
(** Section variables of this prefix *)
abstr_subst : Univ.Instance.t;
@@ -177,15 +177,10 @@ val section_segment_of_mutual_inductive: MutInd.t -> abstr_info
val section_segment_of_reference : GlobRef.t -> abstr_info
val variable_section_segment_of_reference : GlobRef.t -> Constr.named_context
-val variable_section_kind : Id.t -> Decl_kinds.binding_kind
val section_instance : GlobRef.t -> Univ.Instance.t * Id.t array
val is_in_section : GlobRef.t -> bool
-val add_section_variable : name:Id.t -> kind:Decl_kinds.binding_kind -> poly:bool -> unit
-val add_section_context : Univ.ContextSet.t -> unit
-val add_section_constant : poly:bool -> Constant.t -> Constr.named_context -> unit
-val add_section_kn : poly:bool -> MutInd.t -> Constr.named_context -> unit
val replacement_context : unit -> Opaqueproof.work_list
val is_polymorphic_univ : Univ.Level.t -> bool
diff --git a/library/libobject.ml b/library/libobject.ml
index 27e7810e6c..932f065f73 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -75,7 +75,7 @@ and t =
| ModuleTypeObject of substitutive_objects
| IncludeObject of algebraic_objects
| KeepObject of objects
- | ImportObject of { export : bool; mp : ModPath.t }
+ | ExportObject of { mpl : ModPath.t list }
| AtomicObject of obj
and objects = (Names.Id.t * t) list
diff --git a/library/libobject.mli b/library/libobject.mli
index 3b37db4a6f..146ccc293f 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -112,7 +112,7 @@ and t =
| ModuleTypeObject of substitutive_objects
| IncludeObject of algebraic_objects
| KeepObject of objects
- | ImportObject of { export : bool; mp : Names.ModPath.t }
+ | ExportObject of { mpl : Names.ModPath.t list }
| AtomicObject of obj
and objects = (Names.Id.t * t) list
diff --git a/library/library.ml b/library/library.ml
deleted file mode 100644
index 0faef7bf84..0000000000
--- a/library/library.ml
+++ /dev/null
@@ -1,642 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-open Pp
-open CErrors
-open Util
-
-open Names
-open Libnames
-open Lib
-open Libobject
-
-(************************************************************************)
-(*s Low-level interning/externing of libraries to files *)
-
-let raw_extern_library f =
- System.raw_extern_state Coq_config.vo_magic_number f
-
-let raw_intern_library f =
- System.with_magic_number_check
- (System.raw_intern_state Coq_config.vo_magic_number) f
-
-(************************************************************************)
-(** Serialized objects loaded on-the-fly *)
-
-exception Faulty of string
-
-module Delayed :
-sig
-
-type 'a delayed
-val in_delayed : string -> in_channel -> 'a delayed * Digest.t
-val fetch_delayed : 'a delayed -> 'a
-
-end =
-struct
-
-type 'a delayed = {
- del_file : string;
- del_off : int;
- del_digest : Digest.t;
-}
-
-let in_delayed f ch =
- let pos = pos_in ch in
- let _, digest = System.skip_in_segment f ch in
- ({ del_file = f; del_digest = digest; del_off = pos; }, digest)
-
-(** Fetching a table of opaque terms at position [pos] in file [f],
- expecting to find first a copy of [digest]. *)
-
-let fetch_delayed del =
- let { del_digest = digest; del_file = f; del_off = pos; } = del in
- try
- let ch = raw_intern_library f in
- let () = seek_in ch pos in
- let obj, _, digest' = System.marshal_in_segment f ch in
- let () = close_in ch in
- if not (String.equal digest digest') then raise (Faulty f);
- obj
- with e when CErrors.noncritical e -> raise (Faulty f)
-
-end
-
-open Delayed
-
-
-(************************************************************************)
-(*s Modules on disk contain the following informations (after the magic
- number, and before the digest). *)
-
-type compilation_unit_name = DirPath.t
-
-type library_disk = {
- md_compiled : Safe_typing.compiled_library;
- md_objects : Declaremods.library_objects;
-}
-
-type summary_disk = {
- md_name : compilation_unit_name;
- md_imports : compilation_unit_name array;
- md_deps : (compilation_unit_name * Safe_typing.vodigest) array;
-}
-
-(*s Modules loaded in memory contain the following informations. They are
- kept in the global table [libraries_table]. *)
-
-type library_t = {
- library_name : compilation_unit_name;
- library_data : library_disk delayed;
- library_deps : (compilation_unit_name * Safe_typing.vodigest) array;
- library_imports : compilation_unit_name array;
- library_digests : Safe_typing.vodigest;
- library_extra_univs : Univ.ContextSet.t;
-}
-
-type library_summary = {
- libsum_name : compilation_unit_name;
- libsum_digests : Safe_typing.vodigest;
- libsum_imports : compilation_unit_name array;
-}
-
-module LibraryOrdered = DirPath
-module LibraryMap = Map.Make(LibraryOrdered)
-module LibraryFilenameMap = Map.Make(LibraryOrdered)
-
-(* This is a map from names to loaded libraries *)
-let libraries_table : library_summary LibraryMap.t ref =
- Summary.ref LibraryMap.empty ~name:"LIBRARY"
-
-(* This is the map of loaded libraries filename *)
-(* (not synchronized so as not to be caught in the states on disk) *)
-let libraries_filename_table = ref LibraryFilenameMap.empty
-
-(* These are the _ordered_ sets of loaded, imported and exported libraries *)
-let libraries_loaded_list = Summary.ref [] ~name:"LIBRARY-LOAD"
-let libraries_imports_list = Summary.ref [] ~name:"LIBRARY-IMPORT"
-let libraries_exports_list = Summary.ref [] ~name:"LIBRARY-EXPORT"
-
-(* various requests to the tables *)
-
-let find_library dir =
- LibraryMap.find dir !libraries_table
-
-let try_find_library dir =
- try find_library dir
- with Not_found ->
- user_err ~hdr:"Library.find_library"
- (str "Unknown library " ++ DirPath.print dir)
-
-let register_library_filename dir f =
- (* Not synchronized: overwrite the previous binding if one existed *)
- (* from a previous play of the session *)
- libraries_filename_table :=
- LibraryFilenameMap.add dir f !libraries_filename_table
-
-let library_full_filename dir =
- try LibraryFilenameMap.find dir !libraries_filename_table
- with Not_found -> "<unavailable filename>"
-
-let overwrite_library_filenames f =
- let f =
- if Filename.is_relative f then Filename.concat (Sys.getcwd ()) f else f in
- LibraryMap.iter (fun dir _ -> register_library_filename dir f)
- !libraries_table
-
-let library_is_loaded dir =
- try let _ = find_library dir in true
- with Not_found -> false
-
-let library_is_opened dir =
- List.exists (fun name -> DirPath.equal name dir) !libraries_imports_list
-
-let loaded_libraries () = !libraries_loaded_list
-
-let opened_libraries () = !libraries_imports_list
-
- (* If a library is loaded several time, then the first occurrence must
- be performed first, thus the libraries_loaded_list ... *)
-
-let register_loaded_library m =
- let libname = m.libsum_name in
- let link () =
- let dirname = Filename.dirname (library_full_filename libname) in
- let prefix = Nativecode.mod_uid_of_dirpath libname ^ "." in
- let f = prefix ^ "cmo" in
- let f = Dynlink.adapt_filename f in
- if Coq_config.native_compiler then
- Nativelib.link_library (Global.env()) ~prefix ~dirname ~basename:f
- in
- let rec aux = function
- | [] -> link (); [libname]
- | m'::_ as l when DirPath.equal m' libname -> l
- | m'::l' -> m' :: aux l' in
- libraries_loaded_list := aux !libraries_loaded_list;
- libraries_table := LibraryMap.add libname m !libraries_table
-
- (* ... while if a library is imported/exported several time, then
- only the last occurrence is really needed - though the imported
- list may differ from the exported list (consider the sequence
- Export A; Export B; Import A which results in A;B for exports but
- in B;A for imports) *)
-
-let rec remember_last_of_each l m =
- match l with
- | [] -> [m]
- | m'::l' when DirPath.equal m' m -> remember_last_of_each l' m
- | m'::l' -> m' :: remember_last_of_each l' m
-
-let register_open_library export m =
- libraries_imports_list := remember_last_of_each !libraries_imports_list m;
- if export then
- libraries_exports_list := remember_last_of_each !libraries_exports_list m
-
-(************************************************************************)
-(*s Opening libraries *)
-
-(* [open_library export explicit m] opens library [m] if not already
- opened _or_ if explicitly asked to be (re)opened *)
-
-let open_library export explicit_libs m =
- if
- (* Only libraries indirectly to open are not reopen *)
- (* Libraries explicitly mentioned by the user are always reopen *)
- List.exists (fun m' -> DirPath.equal m m') explicit_libs
- || not (library_is_opened m)
- then begin
- register_open_library export m;
- Declaremods.really_import_module (MPfile m)
- end
- else
- if export then
- libraries_exports_list := remember_last_of_each !libraries_exports_list m
-
-(* open_libraries recursively open a list of libraries but opens only once
- a library that is re-exported many times *)
-
-let open_libraries export modl =
- let to_open_list =
- List.fold_left
- (fun l m ->
- let subimport =
- Array.fold_left
- (fun l m -> remember_last_of_each l m)
- l m.libsum_imports
- in remember_last_of_each subimport m.libsum_name)
- [] modl in
- let explicit = List.map (fun m -> m.libsum_name) modl in
- List.iter (open_library export explicit) to_open_list
-
-
-(**********************************************************************)
-(* import and export of libraries - synchronous operations *)
-(* at the end similar to import and export of modules except that it *)
-(* is optimized: when importing several libraries at the same time *)
-(* which themselves indirectly imports the very same modules, these *)
-(* ones are imported only ones *)
-
-let open_import_library i (_,(modl,export)) =
- if Int.equal i 1 then
- (* even if the library is already imported, we re-import it *)
- (* if not (library_is_opened dir) then *)
- open_libraries export (List.map try_find_library modl)
-
-let cache_import_library obj =
- open_import_library 1 obj
-
-let subst_import_library (_,o) = o
-
-let classify_import_library (_,export as obj) =
- if export then Substitute obj else Dispose
-
-let in_import_library : DirPath.t list * bool -> obj =
- declare_object {(default_object "IMPORT LIBRARY") with
- cache_function = cache_import_library;
- open_function = open_import_library;
- subst_function = subst_import_library;
- classify_function = classify_import_library }
-
-(************************************************************************)
-(** {6 Tables of opaque proof terms} *)
-
-(** We now store opaque proof terms apart from the rest of the environment.
- See the [Indirect] constructor in [Lazyconstr.lazy_constr]. This way,
- we can quickly load a first half of a .vo file without these opaque
- terms, and access them only when a specific command (e.g. Print or
- Print Assumptions) needs it. *)
-
-(** Delayed / available tables of opaque terms *)
-
-type 'a table_status =
- | ToFetch of 'a array delayed
- | Fetched of 'a array
-
-let opaque_tables =
- ref (LibraryMap.empty : (Opaqueproof.opaque_proofterm table_status) LibraryMap.t)
-
-let add_opaque_table dp st =
- opaque_tables := LibraryMap.add dp st !opaque_tables
-
-let access_table what tables dp i =
- let t = match LibraryMap.find dp !tables with
- | Fetched t -> t
- | ToFetch f ->
- let dir_path = Names.DirPath.to_string dp in
- Flags.if_verbose Feedback.msg_info (str"Fetching " ++ str what++str" from disk for " ++ str dir_path);
- let t =
- try fetch_delayed f
- with Faulty f ->
- user_err ~hdr:"Library.access_table"
- (str "The file " ++ str f ++ str " (bound to " ++ str dir_path ++
- str ") is inaccessible or corrupted,\ncannot load some " ++
- str what ++ str " in it.\n")
- in
- tables := LibraryMap.add dp (Fetched t) !tables;
- t
- in
- assert (i < Array.length t); t.(i)
-
-let access_opaque_table dp i =
- let what = "opaque proofs" in
- access_table what opaque_tables dp i
-
-let indirect_accessor = {
- Opaqueproof.access_proof = access_opaque_table;
- Opaqueproof.access_discharge = Cooking.cook_constr;
-}
-
-(************************************************************************)
-(* Internalise libraries *)
-
-type seg_sum = summary_disk
-type seg_lib = library_disk
-type seg_univ = (* true = vivo, false = vi *)
- Univ.ContextSet.t * bool
-type seg_proofs = Opaqueproof.opaque_proofterm array
-
-let mk_library sd md digests univs =
- {
- library_name = sd.md_name;
- library_data = md;
- library_deps = sd.md_deps;
- library_imports = sd.md_imports;
- library_digests = digests;
- library_extra_univs = univs;
- }
-
-let mk_summary m = {
- libsum_name = m.library_name;
- libsum_imports = m.library_imports;
- libsum_digests = m.library_digests;
-}
-
-let intern_from_file f =
- let ch = raw_intern_library f in
- let (lsd : seg_sum), _, digest_lsd = System.marshal_in_segment f ch in
- let ((lmd : seg_lib delayed), digest_lmd) = in_delayed f ch in
- let (univs : seg_univ option), _, digest_u = System.marshal_in_segment f ch in
- let _ = System.skip_in_segment f ch in
- let ((del_opaque : seg_proofs delayed),_) = in_delayed f ch in
- close_in ch;
- register_library_filename lsd.md_name f;
- add_opaque_table lsd.md_name (ToFetch del_opaque);
- let open Safe_typing in
- match univs with
- | None -> mk_library lsd lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty
- | Some (uall,true) ->
- mk_library lsd lmd (Dvivo (digest_lmd,digest_u)) uall
- | Some (_,false) ->
- mk_library lsd lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty
-
-module DPMap = Map.Make(DirPath)
-
-let rec intern_library ~lib_resolver (needed, contents) (dir, f) from =
- (* Look if in the current logical environment *)
- try (find_library dir).libsum_digests, (needed, contents)
- with Not_found ->
- (* Look if already listed and consequently its dependencies too *)
- try (DPMap.find dir contents).library_digests, (needed, contents)
- with Not_found ->
- Feedback.feedback(Feedback.FileDependency (from, DirPath.to_string dir));
- (* [dir] is an absolute name which matches [f] which must be in loadpath *)
- let f = match f with Some f -> f | None -> lib_resolver dir in
- let m = intern_from_file f in
- if not (DirPath.equal dir m.library_name) then
- user_err ~hdr:"load_physical_library"
- (str "The file " ++ str f ++ str " contains library" ++ spc () ++
- DirPath.print m.library_name ++ spc () ++ str "and not library" ++
- spc() ++ DirPath.print dir);
- Feedback.feedback (Feedback.FileLoaded(DirPath.to_string dir, f));
- m.library_digests, intern_library_deps ~lib_resolver (needed, contents) dir m f
-
-and intern_library_deps ~lib_resolver libs dir m from =
- let needed, contents =
- Array.fold_left (intern_mandatory_library ~lib_resolver dir from)
- libs m.library_deps in
- (dir :: needed, DPMap.add dir m contents )
-
-and intern_mandatory_library ~lib_resolver caller from libs (dir,d) =
- let digest, libs = intern_library ~lib_resolver libs (dir, None) (Some from) in
- if not (Safe_typing.digest_match ~actual:digest ~required:d) then
- user_err (str "Compiled library " ++ DirPath.print caller ++
- str " (in file " ++ str from ++ str ") makes inconsistent assumptions \
- over library " ++ DirPath.print dir);
- libs
-
-let rec_intern_library ~lib_resolver libs (dir, f) =
- let _, libs = intern_library ~lib_resolver libs (dir, Some f) None in
- libs
-
-let native_name_from_filename f =
- let ch = raw_intern_library f in
- let (lmd : seg_sum), pos, digest_lmd = System.marshal_in_segment f ch in
- Nativecode.mod_uid_of_dirpath lmd.md_name
-
-(**********************************************************************)
-(*s [require_library] loads and possibly opens a library. This is a
- synchronized operation. It is performed as follows:
-
- preparation phase: (functions require_library* ) the library and its
- dependencies are read from to disk (using intern_* )
- [they are read from disk to ensure that at section/module
- discharging time, the physical library referred to outside the
- section/module is the one that was used at type-checking time in
- the section/module]
-
- execution phase: (through add_leaf and cache_require)
- the library is loaded in the environment and Nametab, the objects are
- registered etc, using functions from Declaremods (via load_library,
- which recursively loads its dependencies)
-*)
-
-let register_library m =
- let l = fetch_delayed m.library_data in
- Declaremods.register_library
- m.library_name
- l.md_compiled
- l.md_objects
- m.library_digests
- m.library_extra_univs;
- register_loaded_library (mk_summary m)
-
-(* Follow the semantics of Anticipate object:
- - called at module or module type closing when a Require occurs in
- the module or module type
- - not called from a library (i.e. a module identified with a file) *)
-let load_require _ (_,(needed,modl,_)) =
- List.iter register_library needed
-
-let open_require i (_,(_,modl,export)) =
- Option.iter (fun exp -> open_libraries exp (List.map find_library modl))
- export
-
- (* [needed] is the ordered list of libraries not already loaded *)
-let cache_require o =
- load_require 1 o;
- open_require 1 o
-
-let discharge_require (_,o) = Some o
-
-(* open_function is never called from here because an Anticipate object *)
-
-type require_obj = library_t list * DirPath.t list * bool option
-
-let in_require : require_obj -> obj =
- declare_object {(default_object "REQUIRE") with
- cache_function = cache_require;
- load_function = load_require;
- open_function = (fun _ _ -> assert false);
- discharge_function = discharge_require;
- classify_function = (fun o -> Anticipate o) }
-
-(* Require libraries, import them if [export <> None], mark them for export
- if [export = Some true] *)
-
-let warn_require_in_module =
- CWarnings.create ~name:"require-in-module" ~category:"deprecated"
- (fun () -> strbrk "Require inside a module is" ++
- strbrk " deprecated and strongly discouraged. " ++
- strbrk "You can Require a module at toplevel " ++
- strbrk "and optionally Import it inside another one.")
-
-let require_library_from_dirpath ~lib_resolver modrefl export =
- let needed, contents = List.fold_left (rec_intern_library ~lib_resolver) ([], DPMap.empty) modrefl in
- let needed = List.rev_map (fun dir -> DPMap.find dir contents) needed in
- let modrefl = List.map fst modrefl in
- if Lib.is_module_or_modtype () then
- begin
- warn_require_in_module ();
- add_anonymous_leaf (in_require (needed,modrefl,None));
- Option.iter (fun exp ->
- add_anonymous_leaf (in_import_library (modrefl,exp)))
- export
- end
- else
- add_anonymous_leaf (in_require (needed,modrefl,export));
- ()
-
-(* the function called by Vernacentries.vernac_import *)
-
-let safe_locate_module qid =
- try Nametab.locate_module qid
- with Not_found ->
- user_err ?loc:qid.CAst.loc ~hdr:"safe_locate_module"
- (pr_qualid qid ++ str " is not a module")
-
-let import_module export modl =
- (* Optimization: libraries in a raw in the list are imported
- "globally". If there is non-library in the list; it breaks the
- optimization For instance: "Import Arith MyModule Zarith" will
- not be optimized (possibly resulting in redefinitions, but
- "Import MyModule Arith Zarith" and "Import Arith Zarith MyModule"
- will have the submodules imported by both Arith and ZArith
- imported only once *)
- let flush = function
- | [] -> ()
- | modl -> add_anonymous_leaf (in_import_library (List.rev modl, export)) in
- let rec aux acc = function
- | qid :: l ->
- let m,acc =
- try Nametab.locate_module qid, acc
- with Not_found-> flush acc; safe_locate_module qid, [] in
- (match m with
- | MPfile dir -> aux (dir::acc) l
- | mp ->
- flush acc;
- try Declaremods.import_module export mp; aux [] l
- with Not_found ->
- user_err ?loc:qid.CAst.loc ~hdr:"import_module"
- (pr_qualid qid ++ str " is not a module"))
- | [] -> flush acc
- in aux [] modl
-
-(************************************************************************)
-(*s Initializing the compilation of a library. *)
-
-let load_library_todo f =
- let ch = raw_intern_library f in
- let (s0 : seg_sum), _, _ = System.marshal_in_segment f ch in
- let (s1 : seg_lib), _, _ = System.marshal_in_segment f ch in
- let (s2 : seg_univ option), _, _ = System.marshal_in_segment f ch in
- let tasks, _, _ = System.marshal_in_segment f ch in
- let (s4 : seg_proofs), _, _ = System.marshal_in_segment f ch in
- close_in ch;
- if tasks = None then user_err ~hdr:"restart" (str"not a .vio file");
- if s2 = None then user_err ~hdr:"restart" (str"not a .vio file");
- if snd (Option.get s2) then user_err ~hdr:"restart" (str"not a .vio file");
- s0, s1, Option.get s2, Option.get tasks, s4
-
-(************************************************************************)
-(*s [save_library dir] ends library [dir] and save it to the disk. *)
-
-let current_deps () =
- let map name =
- let m = try_find_library name in
- (name, m.libsum_digests)
- in
- List.map map !libraries_loaded_list
-
-let current_reexports () = !libraries_exports_list
-
-let error_recursively_dependent_library dir =
- user_err
- (strbrk "Unable to use logical name " ++ DirPath.print dir ++
- strbrk " to save current library because" ++
- strbrk " it already depends on a library of this name.")
-
-(* We now use two different digests in a .vo file. The first one
- only covers half of the file, without the opaque table. It is
- used for identifying this version of this library : this digest
- is the one leading to "inconsistent assumptions" messages.
- The other digest comes at the very end, and covers everything
- before it. This one is used for integrity check of the whole
- file when loading the opaque table. *)
-
-(* Security weakness: file might have been changed on disk between
- writing the content and computing the checksum... *)
-
-let save_library_to ?todo ~output_native_objects dir f otab =
- let except = match todo with
- | None ->
- (* XXX *)
- (* assert(!Flags.compilation_mode = Flags.BuildVo); *)
- assert(Filename.check_suffix f ".vo");
- Future.UUIDSet.empty
- | Some (l,_) ->
- assert(Filename.check_suffix f ".vio");
- List.fold_left (fun e (r,_) -> Future.UUIDSet.add r.Stateid.uuid e)
- Future.UUIDSet.empty l in
- let cenv, seg, ast = Declaremods.end_library ~output_native_objects ~except dir in
- let opaque_table, f2t_map = Opaqueproof.dump ~except otab in
- let tasks, utab =
- match todo with
- | None -> None, None
- | Some (tasks, rcbackup) ->
- let tasks =
- List.map Stateid.(fun (r,b) ->
- try { r with uuid = Future.UUIDMap.find r.uuid f2t_map }, b
- with Not_found -> assert b; { r with uuid = -1 }, b)
- tasks in
- Some (tasks,rcbackup),
- Some (Univ.ContextSet.empty,false)
- in
- let sd = {
- md_name = dir;
- md_deps = Array.of_list (current_deps ());
- md_imports = Array.of_list (current_reexports ());
- } in
- let md = {
- md_compiled = cenv;
- md_objects = seg;
- } in
- if Array.exists (fun (d,_) -> DirPath.equal d dir) sd.md_deps then
- error_recursively_dependent_library dir;
- (* Open the vo file and write the magic number *)
- let f' = f in
- let ch = raw_extern_library f' in
- try
- (* Writing vo payload *)
- System.marshal_out_segment f' ch (sd : seg_sum);
- System.marshal_out_segment f' ch (md : seg_lib);
- System.marshal_out_segment f' ch (utab : seg_univ option);
- System.marshal_out_segment f' ch (tasks : 'tasks option);
- System.marshal_out_segment f' ch (opaque_table : seg_proofs);
- close_out ch;
- (* Writing native code files *)
- if output_native_objects then
- let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in
- Nativelib.compile_library dir ast fn
- with reraise ->
- let reraise = CErrors.push reraise in
- let () = Feedback.msg_warning (str "Removed file " ++ str f') in
- let () = close_out ch in
- let () = Sys.remove f' in
- iraise reraise
-
-let save_library_raw f sum lib univs proofs =
- let ch = raw_extern_library f in
- System.marshal_out_segment f ch (sum : seg_sum);
- System.marshal_out_segment f ch (lib : seg_lib);
- System.marshal_out_segment f ch (Some univs : seg_univ option);
- System.marshal_out_segment f ch (None : 'tasks option);
- System.marshal_out_segment f ch (proofs : seg_proofs);
- close_out ch
-
-module StringOrd = struct type t = string let compare = String.compare end
-module StringSet = Set.Make(StringOrd)
-
-let get_used_load_paths () =
- StringSet.elements
- (List.fold_left (fun acc m -> StringSet.add
- (Filename.dirname (library_full_filename m)) acc)
- StringSet.empty !libraries_loaded_list)
-
-let _ = Nativelib.get_load_paths := get_used_load_paths
diff --git a/library/library.mli b/library/library.mli
deleted file mode 100644
index bb6c42e393..0000000000
--- a/library/library.mli
+++ /dev/null
@@ -1,77 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-open Names
-open Libnames
-
-(** This module provides functions to load, open and save
- libraries. Libraries correspond to the subclass of modules that
- coincide with a file on disk (the ".vo" files). Libraries on the
- disk comes with checksums (obtained with the [Digest] module), which
- are checked at loading time to prevent inconsistencies between files
- written at various dates.
-*)
-
-(** {6 ... }
- Require = load in the environment + open (if the optional boolean
- is not [None]); mark also for export if the boolean is [Some true] *)
-val require_library_from_dirpath
- : lib_resolver:(DirPath.t -> CUnix.physical_path)
- -> (DirPath.t * string) list
- -> bool option
- -> unit
-
-(** {6 Start the compilation of a library } *)
-
-(** Segments of a library *)
-type seg_sum
-type seg_lib
-type seg_univ = (* all_cst, finished? *)
- Univ.ContextSet.t * bool
-type seg_proofs = Opaqueproof.opaque_proofterm array
-
-(** Open a module (or a library); if the boolean is true then it's also
- an export otherwise just a simple import *)
-val import_module : bool -> qualid list -> unit
-
-(** End the compilation of a library and save it to a ".vo" file.
- [output_native_objects]: when producing vo objects, also compile the native-code version. *)
-val save_library_to :
- ?todo:(((Future.UUID.t,'document) Stateid.request * bool) list * 'counters) ->
- output_native_objects:bool ->
- DirPath.t -> string -> Opaqueproof.opaquetab -> unit
-
-val load_library_todo
- : CUnix.physical_path
- -> seg_sum * seg_lib * seg_univ * 'tasks * seg_proofs
-
-val save_library_raw : string -> seg_sum -> seg_lib -> seg_univ -> seg_proofs -> unit
-
-(** {6 Interrogate the status of libraries } *)
-
- (** - Tell if a library is loaded or opened *)
-val library_is_loaded : DirPath.t -> bool
-val library_is_opened : DirPath.t -> bool
-
- (** - Tell which libraries are loaded or imported *)
-val loaded_libraries : unit -> DirPath.t list
-val opened_libraries : unit -> DirPath.t list
-
- (** - Return the full filename of a loaded library. *)
-val library_full_filename : DirPath.t -> string
-
- (** - Overwrite the filename of all libraries (used when restoring a state) *)
-val overwrite_library_filenames : string -> unit
-
-(** {6 Native compiler. } *)
-val native_name_from_filename : string -> string
-
-(** {6 Opaque accessors} *)
-val indirect_accessor : Opaqueproof.indirect_accessor
diff --git a/library/library.mllib b/library/library.mllib
index 84937ede93..c34d8911e8 100644
--- a/library/library.mllib
+++ b/library/library.mllib
@@ -1,4 +1,3 @@
-Decl_kinds
Libnames
Globnames
Libobject
@@ -7,7 +6,6 @@ Nametab
Global
Lib
Declaremods
-Library
States
Kindops
Goptions
diff --git a/library/states.ml b/library/states.ml
index a73f16957d..0be153d96a 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -9,7 +9,6 @@
(************************************************************************)
open Util
-open System
type state = Lib.frozen * Summary.frozen
@@ -25,13 +24,6 @@ let unfreeze (fl,fs) =
Lib.unfreeze fl;
Summary.unfreeze_summaries fs
-let extern_state s =
- System.extern_state Coq_config.state_magic_number s (freeze ~marshallable:true)
-
-let intern_state s =
- unfreeze (with_magic_number_check (System.intern_state Coq_config.state_magic_number) s);
- Library.overwrite_library_filenames s
-
(* Rollback. *)
let with_state_protection f x =
diff --git a/library/states.mli b/library/states.mli
index c4f3eae49d..4870f48fc3 100644
--- a/library/states.mli
+++ b/library/states.mli
@@ -15,9 +15,6 @@
freezing the states of both [Lib] and [Summary]. We provide functions
to write and restore state to and from a given file. *)
-val intern_state : string -> unit
-val extern_state : string -> unit
-
type state
val freeze : marshallable:bool -> state
val unfreeze : state -> unit
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 07:50:27 +0000