aboutsummaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/globnames.ml7
-rw-r--r--library/globnames.mli7
-rw-r--r--library/goptions.ml4
-rw-r--r--library/lib.ml2
-rw-r--r--library/lib.mli3
-rw-r--r--library/libobject.ml37
-rw-r--r--library/libobject.mli18
-rw-r--r--library/nametab.ml14
8 files changed, 71 insertions, 21 deletions
diff --git a/library/globnames.ml b/library/globnames.ml
index 9126a467bf..bc24fbf096 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -117,3 +117,10 @@ module ExtRefOrdered = struct
| SynDef kn -> combinesmall 2 (KerName.hash kn)
end
+
+module ExtRefMap = HMap.Make(ExtRefOrdered)
+module ExtRefSet = ExtRefMap.Set
+
+let subst_extended_reference sub = function
+ | SynDef kn -> SynDef (subst_kn sub kn)
+ | TrueGlobal gr -> TrueGlobal (subst_global_reference sub gr)
diff --git a/library/globnames.mli b/library/globnames.mli
index fb1583e16c..8acea5ef28 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -61,3 +61,10 @@ module ExtRefOrdered : sig
val equal : t -> t -> bool
val hash : t -> int
end
+
+module ExtRefSet : CSig.SetS with type elt = extended_global_reference
+module ExtRefMap : CMap.ExtS
+ with type key = extended_global_reference
+ and module Set := ExtRefSet
+
+val subst_extended_reference : substitution -> extended_global_reference -> extended_global_reference
diff --git a/library/goptions.ml b/library/goptions.ml
index 73132868d7..1418407533 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -90,7 +90,7 @@ module MakeTable =
let inGo : option_mark * A.t -> obj =
Libobject.declare_object {(Libobject.default_object nick) with
Libobject.load_function = load_options;
- Libobject.open_function = load_options;
+ Libobject.open_function = simple_open load_options;
Libobject.cache_function = cache_options;
Libobject.subst_function = subst_options;
Libobject.classify_function = (fun x -> Substitute x)}
@@ -262,7 +262,7 @@ let declare_option cast uncast append ?(preprocess = fun x -> x)
declare_object
{ (default_object (nickname key)) with
load_function = load_options;
- open_function = open_options;
+ open_function = simple_open open_options;
cache_function = cache_options;
subst_function = subst_options;
discharge_function = discharge_options;
diff --git a/library/lib.ml b/library/lib.ml
index e7e6dc640a..830777003b 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -46,7 +46,7 @@ let iter_objects f i prefix =
List.iter (fun (id,obj) -> f i (make_oname prefix id, obj))
let load_atomic_objects i pr = iter_objects load_object i pr
-let open_atomic_objects i pr = iter_objects open_object i pr
+let open_atomic_objects f i pr = iter_objects (open_object f) i pr
let subst_atomic_objects subst seg =
let subst_one = fun (id,obj as node) ->
diff --git a/library/lib.mli b/library/lib.mli
index 949b5e26c2..56ea35ec60 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -35,7 +35,8 @@ type lib_objects = (Id.t * Libobject.t) list
(** {6 Object iteration functions. } *)
-val open_atomic_objects : int -> Nametab.object_prefix -> lib_atomic_objects -> unit
+val open_atomic_objects : Libobject.open_filter
+ -> int -> Nametab.object_prefix -> lib_atomic_objects -> unit
val load_atomic_objects : int -> Nametab.object_prefix -> lib_atomic_objects -> unit
val subst_atomic_objects : Mod_subst.substitution -> lib_atomic_objects -> lib_atomic_objects
(*val load_and_subst_objects : int -> Libnames.Nametab.object_prefix -> Mod_subst.substitution -> lib_objects -> lib_objects*)
diff --git a/library/libobject.ml b/library/libobject.ml
index 0681e12449..c38e0d891b 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -18,11 +18,36 @@ type 'a substitutivity =
type object_name = Libnames.full_path * Names.KerName.t
+module NSet = Globnames.ExtRefSet
+
+type open_filter =
+ | Unfiltered
+ | Names of NSet.t
+
+let simple_open f filter i o = match filter with
+ | Unfiltered -> f i o
+ | Names _ -> ()
+
+let filter_and f1 f2 = match f1, f2 with
+ | Unfiltered, f | f, Unfiltered -> Some f
+ | Names n1, Names n2 ->
+ let n = NSet.inter n1 n2 in
+ if NSet.is_empty n then None
+ else Some (Names n)
+
+let filter_or f1 f2 = match f1, f2 with
+ | Unfiltered, f | f, Unfiltered -> Unfiltered
+ | Names n1, Names n2 -> Names (NSet.union n1 n2)
+
+let in_filter_ref gr = function
+ | Unfiltered -> true
+ | Names ns -> NSet.mem (Globnames.TrueGlobal gr) ns
+
type 'a object_declaration = {
object_name : string;
cache_function : object_name * 'a -> unit;
load_function : int -> object_name * 'a -> unit;
- open_function : int -> object_name * 'a -> unit;
+ open_function : open_filter -> int -> object_name * 'a -> unit;
classify_function : 'a -> 'a substitutivity;
subst_function : Mod_subst.substitution * 'a -> 'a;
discharge_function : object_name * 'a -> 'a option;
@@ -32,7 +57,7 @@ let default_object s = {
object_name = s;
cache_function = (fun _ -> ());
load_function = (fun _ _ -> ());
- open_function = (fun _ _ -> ());
+ open_function = (fun _ _ _ -> ());
subst_function = (fun _ ->
CErrors.anomaly (str "The object " ++ str s ++ str " does not know how to substitute!"));
classify_function = (fun atomic_obj -> Keep atomic_obj);
@@ -75,7 +100,7 @@ and t =
| ModuleTypeObject of substitutive_objects
| IncludeObject of algebraic_objects
| KeepObject of objects
- | ExportObject of { mpl : ModPath.t list }
+ | ExportObject of { mpl : (open_filter * ModPath.t) list }
| AtomicObject of obj
and objects = (Names.Id.t * t) list
@@ -105,9 +130,9 @@ let load_object i (sp, Dyn.Dyn (tag, v)) =
let decl = DynMap.find tag !cache_tab in
decl.load_function i (sp, v)
-let open_object i (sp, Dyn.Dyn (tag, v)) =
+let open_object f i (sp, Dyn.Dyn (tag, v)) =
let decl = DynMap.find tag !cache_tab in
- decl.open_function i (sp, v)
+ decl.open_function f i (sp, v)
let subst_object (subs, Dyn.Dyn (tag, v)) =
let decl = DynMap.find tag !cache_tab in
@@ -147,7 +172,7 @@ let global_object_nodischarge s ~cache ~subst =
let import i o = if Int.equal i 1 then cache o in
{ (default_object s) with
cache_function = cache;
- open_function = import;
+ open_function = simple_open import;
subst_function = (match subst with
| None -> fun _ -> CErrors.anomaly (str "The object " ++ str s ++ str " does not know how to substitute!")
| Some subst -> subst;
diff --git a/library/libobject.mli b/library/libobject.mli
index 24cadc2223..1c82349bb6 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -72,16 +72,28 @@ type 'a substitutivity =
type object_name = full_path * Names.KerName.t
+type open_filter = Unfiltered | Names of Globnames.ExtRefSet.t
+
type 'a object_declaration = {
object_name : string;
cache_function : object_name * 'a -> unit;
load_function : int -> object_name * 'a -> unit;
- open_function : int -> object_name * 'a -> unit;
+ open_function : open_filter -> int -> object_name * 'a -> unit;
classify_function : 'a -> 'a substitutivity;
subst_function : substitution * 'a -> 'a;
discharge_function : object_name * 'a -> 'a option;
rebuild_function : 'a -> 'a }
+val simple_open : (int -> object_name * 'a -> unit) -> open_filter -> int -> object_name * 'a -> unit
+(** Combinator for making objects which are only opened by unfiltered Import *)
+
+val filter_and : open_filter -> open_filter -> open_filter option
+(** Returns [None] when the intersection is empty. *)
+
+val filter_or : open_filter -> open_filter -> open_filter
+
+val in_filter_ref : Names.GlobRef.t -> open_filter -> bool
+
(** The default object is a "Keep" object with empty methods.
Object creators are advised to use the construction
[{(default_object "MY_OBJECT") with
@@ -114,7 +126,7 @@ and t =
| ModuleTypeObject of substitutive_objects
| IncludeObject of algebraic_objects
| KeepObject of objects
- | ExportObject of { mpl : Names.ModPath.t list }
+ | ExportObject of { mpl : (open_filter * Names.ModPath.t) list }
| AtomicObject of obj
and objects = (Names.Id.t * t) list
@@ -129,7 +141,7 @@ val declare_object :
val cache_object : object_name * obj -> unit
val load_object : int -> object_name * obj -> unit
-val open_object : int -> object_name * obj -> unit
+val open_object : open_filter -> int -> object_name * obj -> unit
val subst_object : substitution * obj -> obj
val classify_object : obj -> obj substitutivity
val discharge_object : object_name * obj -> obj option
diff --git a/library/nametab.ml b/library/nametab.ml
index 523fe8af50..d9b4dc9122 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -352,10 +352,8 @@ let the_univtab = Summary.ref ~name:"univtab" (UnivTab.empty : univtab)
(* Reversed name tables ***************************************************)
(* This table translates extended_global_references back to section paths *)
-module Globrevtab = HMap.Make(ExtRefOrdered)
-
-type globrevtab = full_path Globrevtab.t
-let the_globrevtab = Summary.ref ~name:"globrevtab" (Globrevtab.empty : globrevtab)
+type globrevtab = full_path ExtRefMap.t
+let the_globrevtab = Summary.ref ~name:"globrevtab" (ExtRefMap.empty : globrevtab)
type mprevtab = DirPath.t MPmap.t
@@ -386,7 +384,7 @@ let push_xref visibility sp xref =
match visibility with
| Until _ ->
the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab;
- the_globrevtab := Globrevtab.add xref sp !the_globrevtab
+ the_globrevtab := ExtRefMap.add xref sp !the_globrevtab
| _ ->
begin
if ExtRefTab.exists sp !the_ccitab then
@@ -520,7 +518,7 @@ let path_of_global ref =
let open GlobRef in
match ref with
| VarRef id -> make_path DirPath.empty id
- | _ -> Globrevtab.find (TrueGlobal ref) !the_globrevtab
+ | _ -> ExtRefMap.find (TrueGlobal ref) !the_globrevtab
let dirpath_of_global ref =
fst (repr_path (path_of_global ref))
@@ -529,7 +527,7 @@ let basename_of_global ref =
snd (repr_path (path_of_global ref))
let path_of_syndef kn =
- Globrevtab.find (SynDef kn) !the_globrevtab
+ ExtRefMap.find (SynDef kn) !the_globrevtab
let dirpath_of_module mp =
MPmap.find mp !the_modrevtab
@@ -547,7 +545,7 @@ let shortest_qualid_of_global ?loc ctx ref =
match ref with
| VarRef id -> make_qualid ?loc DirPath.empty id
| _ ->
- let sp = Globrevtab.find (TrueGlobal ref) !the_globrevtab in
+ let sp = ExtRefMap.find (TrueGlobal ref) !the_globrevtab in
ExtRefTab.shortest_qualid ?loc ctx sp !the_ccitab
let shortest_qualid_of_syndef ?loc ctx kn =
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 03:56:00 +0000