pass filters around

7 files changed, 55 insertions, 13 deletions

diff --git a/library/globnames.ml b/library/globnames.ml
index 5dbc8db647..bc24fbf096 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -120,3 +120,7 @@ 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 f5ed3a3ec7..8acea5ef28 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -66,3 +66,5 @@ 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..392a64e5d0 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -18,11 +18,34 @@ 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 todo_filter = simple_open
+
+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)
+
 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 +55,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 +98,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 +128,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 +170,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..27b47264a6 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 todo_filter : (int -> object_name * 'a -> unit) -> open_filter -> int -> object_name * 'a -> unit
+
 (** 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