pass filters around

10 files changed, 114 insertions, 75 deletions

diff --git a/vernac/canonical.ml b/vernac/canonical.ml
index 390ed62bee..eaa6c84791 100644
--- a/vernac/canonical.ml
+++ b/vernac/canonical.ml
@@ -28,7 +28,7 @@ let discharge_canonical_structure (_,((gref, _ as x), local)) =
 
 let inCanonStruc : (GlobRef.t * inductive) * bool -> obj =
   declare_object {(default_object "CANONICAL-STRUCTURE") with
-                  open_function = open_canonical_structure;
+                  open_function = simple_open open_canonical_structure;
                   cache_function = cache_canonical_structure;
                   subst_function = (fun (subst,(c,local)) -> subst_canonical_structure subst c, local);
                   classify_function = (fun x -> Substitute x);
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 3d38713e09..a9425b15d2 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -116,7 +116,7 @@ let instance_input : instance -> obj =
     { (default_object "type classes instances state") with
       cache_function = cache_instance;
       load_function = (fun _ x -> cache_instance x);
-      open_function = (fun _ x -> cache_instance x);
+      open_function = simple_open (fun _ x -> cache_instance x);
       classify_function = classify_instance;
       discharge_function = discharge_instance;
       rebuild_function = rebuild_instance;
@@ -237,7 +237,7 @@ let class_input : typeclass -> obj =
     { (default_object "type classes state") with
       cache_function = cache_class;
       load_function = (fun _ -> cache_class);
-      open_function = (fun _ -> cache_class);
+      open_function = simple_open (fun _ -> cache_class);
       classify_function = (fun x -> Substitute x);
       discharge_function = (fun a -> Some (discharge_class a));
       rebuild_function = rebuild_class;
diff --git a/vernac/comCoercion.ml b/vernac/comCoercion.ml
index c339c53a9b..4a8e217fc1 100644
--- a/vernac/comCoercion.ml
+++ b/vernac/comCoercion.ml
@@ -256,7 +256,7 @@ let classify_coercion obj =
 
 let inCoercion : coercion -> obj =
   declare_object {(default_object "COERCION") with
-    open_function = open_coercion;
+    open_function = simple_open open_coercion;
     cache_function = cache_coercion;
     subst_function = (fun (subst,c) -> subst_coercion subst c);
     classify_function = classify_coercion;
diff --git a/vernac/declareInd.ml b/vernac/declareInd.ml
index 2610f16d92..203e11d6ab 100644
--- a/vernac/declareInd.ml
+++ b/vernac/declareInd.ml
@@ -65,7 +65,7 @@ let objInductive : inductive_obj Libobject.Dyn.tag =
   declare_object_full {(default_object "INDUCTIVE") with
     cache_function = cache_inductive;
     load_function = load_inductive;
-    open_function = open_inductive;
+    open_function = todo_filter open_inductive;
     classify_function = (fun a -> Substitute a);
     subst_function = ident_subst_function;
     discharge_function = discharge_inductive;
diff --git a/vernac/declareUniv.ml b/vernac/declareUniv.ml
index 300dfe6c35..20fa43c8e7 100644
--- a/vernac/declareUniv.ml
+++ b/vernac/declareUniv.ml
@@ -56,7 +56,7 @@ let input_univ_names : universe_name_decl -> Libobject.obj =
     { (default_object "Global universe name state") with
       cache_function = cache_univ_names;
       load_function = load_univ_names;
-      open_function = open_univ_names;
+      open_function = simple_open open_univ_names;
       discharge_function = discharge_univ_names;
       subst_function = (fun (subst, a) -> (* Actually the name is generated once and for all. *) a);
       classify_function = (fun a -> Substitute a) }
diff --git a/vernac/declaremods.ml b/vernac/declaremods.ml
index 4f527b73d0..b87d3c5681 100644
--- a/vernac/declaremods.ml
+++ b/vernac/declaremods.ml
@@ -81,6 +81,19 @@ module ModSubstObjs :
 
 let sobjs_no_functor (mbids,_) = List.is_empty mbids
 
+let subst_filtered sub (f,mp) =
+  let f = match f with
+    | Unfiltered -> Unfiltered
+    | Names ns ->
+      let module NSet = Globnames.ExtRefSet in
+      let ns =
+        NSet.fold (fun n ns -> NSet.add (Globnames.subst_extended_reference sub n) ns)
+          ns NSet.empty
+      in
+      Names ns
+  in
+  f, subst_mp sub mp
+
 let rec subst_aobjs sub = function
   | Objs o as objs ->
     let o' = subst_objects sub o in
@@ -109,7 +122,7 @@ and subst_objects subst seg =
       let aobjs' = subst_aobjs subst aobjs in
       if aobjs' == aobjs then node else (id, IncludeObject aobjs')
     | ExportObject { mpl } ->
-      let mpl' = List.map (subst_mp subst) mpl in
+      let mpl' = List.Smart.map (subst_filtered subst) mpl in
       if mpl'==mpl then node else (id, ExportObject { mpl = mpl' })
     | KeepObject _ -> assert false
   in
@@ -285,86 +298,104 @@ and load_keep i ((sp,kn),kobjs) =
 
 (** {6 Implementation of Import and Export commands} *)
 
-let mark_object obj (exports,acc) =
-  (exports, obj::acc)
+let mark_object f obj (exports,acc) =
+  (exports, (f,obj)::acc)
 
-let rec collect_module_objects mp acc =
+let rec collect_module_objects (f,mp) acc =
   (* May raise Not_found for unknown module and for functors *)
   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
+  let acc = collect_objects f 1 prefix modobjs.module_keep_objects acc in
+  collect_objects f 1 prefix modobjs.module_substituted_objects acc
 
-and collect_object i (name, obj as o) acc =
+and collect_object f i (name, obj as o) acc =
   match obj with
-  | ExportObject { mpl; _ } -> collect_export i mpl acc
+  | ExportObject { mpl } -> collect_export f i mpl acc
   | AtomicObject _ | IncludeObject _ | KeepObject _
-  | ModuleObject _ | ModuleTypeObject _ -> mark_object o acc
+  | ModuleObject _ | ModuleTypeObject _ -> mark_object f o acc
+
+and collect_objects f i prefix objs acc =
+  List.fold_right (fun (id, obj) acc -> collect_object f i (Lib.make_oname prefix id, obj) acc) objs acc
+
+and collect_one_export f (f',mp) (exports,objs as acc) =
+  match filter_and f f' with
+  | None -> acc
+  | Some f ->
+    let exports' = MPmap.update mp (function
+        | None -> Some f
+        | Some f0 -> Some (filter_or f f0))
+        exports
+    in
+    (* If the map doesn't change there is nothing new to export.
 
-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
+       It's possible that [filter_and] or [filter_or] mangled precise
+       filters such that we repeat uselessly, but the important
+       [Unfiltered] case is handled correctly.
+    *)
+    if exports == exports' then acc
+    else
+      collect_module_objects (f,mp) (exports', objs)
 
-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 =
+and collect_export f i mpl acc =
   if Int.equal i 1 then
-    List.fold_right collect_one_export mpl acc
+    List.fold_right (collect_one_export f) mpl acc
   else acc
 
-let rec open_object i (name, obj) =
+let open_modtype i ((sp,kn),_) =
+  let mp = mp_of_kn kn in
+  let mp' =
+    try Nametab.locate_modtype (qualid_of_path sp)
+    with Not_found ->
+      anomaly (pr_path sp ++ str " should already exist!");
+  in
+  assert (ModPath.equal mp mp');
+  Nametab.push_modtype (Nametab.Exactly i) sp mp
+
+let rec open_object f i (name, obj) =
   match obj with
-  | AtomicObject o -> Libobject.open_object i (name, o)
+  | AtomicObject o -> Libobject.open_object f i (name, o)
   | ModuleObject sobjs ->
     let dir = dir_of_sp (fst name) in
     let mp = mp_of_kn (snd name) in
-    open_module i dir mp sobjs
+    open_module f i dir mp sobjs
   | ModuleTypeObject sobjs -> open_modtype i (name, sobjs)
-  | IncludeObject aobjs -> open_include i (name, aobjs)
-  | ExportObject { mpl; _ } -> open_export i mpl
-  | KeepObject objs -> open_keep i (name, objs)
+  | IncludeObject aobjs -> open_include f i (name, aobjs)
+  | ExportObject { mpl } -> open_export f i mpl
+  | KeepObject objs -> open_keep f i (name, objs)
 
-and open_module i obj_dir obj_mp sobjs =
+and open_module f i obj_dir obj_mp sobjs =
   let prefix = Nametab.{ obj_dir ; obj_mp; } in
   let dirinfo = Nametab.GlobDirRef.DirModule prefix in
   consistency_checks true obj_dir dirinfo;
-  Nametab.push_dir (Nametab.Exactly i) obj_dir dirinfo;
+  (match f with
+   | Unfiltered -> Nametab.push_dir (Nametab.Exactly i) obj_dir dirinfo
+   | Names _ -> ());
   (* 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
+    open_objects f (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
-
-and open_modtype i ((sp,kn),_) =
-  let mp = mp_of_kn kn in
-  let mp' =
-    try Nametab.locate_modtype (qualid_of_path sp)
-    with Not_found ->
-      anomaly (pr_path sp ++ str " should already exist!");
-  in
-  assert (ModPath.equal mp mp');
-  Nametab.push_modtype (Nametab.Exactly i) sp mp
+and open_objects f i prefix objs =
+  List.iter (fun (id, obj) -> open_object f i (Lib.make_oname prefix id, obj)) objs
 
-and open_include i ((sp,kn), aobjs) =
+and open_include f i ((sp,kn), aobjs) =
   let obj_dir = Libnames.dirpath sp in
   let obj_mp = KerName.modpath kn in
   let prefix = Nametab.{ obj_dir; obj_mp; } in
   let o = expand_aobjs aobjs in
-  open_objects i prefix o
+  open_objects f i prefix o
 
-and open_export i mpl =
-  let _,objs = collect_export i mpl (MPset.empty, []) in
-  List.iter (open_object 1) objs
+and open_export f i mpl =
+  let _ = todo_filter in (* exports will have their own filters! *)
+  let _,objs = collect_export f i mpl (MPmap.empty, []) in
+  List.iter (fun (f,o) -> open_object f 1 o) objs
 
-and open_keep i ((sp,kn),kobjs) =
+and open_keep f i ((sp,kn),kobjs) =
   let obj_dir = dir_of_sp sp and obj_mp = mp_of_kn kn in
   let prefix = Nametab.{ obj_dir; obj_mp; } in
-  open_objects i prefix kobjs
+  open_objects f i prefix kobjs
 
 let rec cache_object (name, obj) =
   match obj with
@@ -383,7 +414,7 @@ and cache_include ((sp,kn), aobjs) =
   let prefix = Nametab.{ obj_dir; obj_mp; } in
   let o = expand_aobjs aobjs in
   load_objects 1 prefix o;
-  open_objects 1 prefix o
+  open_objects Unfiltered 1 prefix o
 
 and cache_keep ((sp,kn),kobjs) =
   anomaly (Pp.str "This module should not be cached!")
@@ -1023,12 +1054,12 @@ let end_library ?except ~output_native_objects dir =
   cenv,(substitute,keep),ast
 
 let import_modules ~export mpl =
-  let _,objs = List.fold_right collect_module_objects mpl (MPset.empty, []) in
-  List.iter (open_object 1) objs;
+  let _,objs = List.fold_right collect_module_objects mpl (MPmap.empty, []) in
+  List.iter (fun (f,o) -> open_object f 1 o) objs;
   if export then Lib.add_anonymous_entry (Lib.Leaf (ExportObject { mpl }))
 
-let import_module ~export mp =
-  import_modules ~export [mp]
+let import_module f ~export mp =
+  import_modules ~export [f,mp]
 
 (** {6 Iterators} *)
 
@@ -1073,6 +1104,6 @@ let debug_print_modtab _ =
 
 
 let mod_ops = {
-  Printmod.import_module = import_module;
+  Printmod.import_module = import_module Unfiltered;
   process_module_binding = process_module_binding;
 }
diff --git a/vernac/declaremods.mli b/vernac/declaremods.mli
index e37299aad6..5e45957e83 100644
--- a/vernac/declaremods.mli
+++ b/vernac/declaremods.mli
@@ -97,11 +97,11 @@ val append_end_library_hook : (unit -> unit) -> unit
    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 : export:bool -> ModPath.t -> unit
+val import_module : Libobject.open_filter -> 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
+val import_modules : export:bool -> (Libobject.open_filter * ModPath.t) list -> unit
 
 (** Include  *)
 
diff --git a/vernac/library.ml b/vernac/library.ml
index 1b0bd4c0f7..01f5101764 100644
--- a/vernac/library.ml
+++ b/vernac/library.ml
@@ -335,7 +335,11 @@ let load_require _ (_,(needed,modl,_)) =
   List.iter register_library needed
 
 let open_require i (_,(_,modl,export)) =
-  Option.iter (fun export -> Declaremods.import_modules ~export @@ List.map (fun m -> MPfile m) modl) export
+  Option.iter (fun export ->
+      let mpl = List.map (fun m -> Unfiltered, MPfile m) modl in
+      (* TODO support filters in Require *)
+      Declaremods.import_modules ~export mpl)
+    export
 
   (* [needed] is the ordered list of libraries not already loaded *)
 let cache_require o =
@@ -370,16 +374,17 @@ 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 export ->
-          List.iter (fun m -> Declaremods.import_module ~export (MPfile m)) modrefl)
-                export
-      end
-    else
-      add_anonymous_leaf (in_require (needed,modrefl,export));
+  if Lib.is_module_or_modtype () then
+    begin
+      warn_require_in_module ();
+      add_anonymous_leaf (in_require (needed,modrefl,None));
+      Option.iter (fun export ->
+          (* TODO import filters *)
+          List.iter (fun m -> Declaremods.import_module Unfiltered ~export (MPfile m)) modrefl)
+        export
+    end
+  else
+    add_anonymous_leaf (in_require (needed,modrefl,export));
   ()
 
 (************************************************************************)
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 475d5c31f7..3b9c771b93 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -877,9 +877,12 @@ let subst_syntax_extension (subst, (local, (pa_sy,pp_sy))) =
 let classify_syntax_definition (local, _ as o) =
   if local then Dispose else Substitute o
 
+let open_syntax_extension i o =
+  if Int.equal i 1 then cache_syntax_extension o
+
 let inSyntaxExtension : syntax_extension_obj -> obj =
   declare_object {(default_object "SYNTAX-EXTENSION") with
-       open_function = (fun i o -> if Int.equal i 1 then cache_syntax_extension o);
+       open_function = simple_open open_syntax_extension;
        cache_function = cache_syntax_extension;
        subst_function = subst_syntax_extension;
        classify_function = classify_syntax_definition}
@@ -1454,7 +1457,7 @@ let classify_notation nobj =
 
 let inNotation : notation_obj -> obj =
   declare_object {(default_object "NOTATION") with
-       open_function = open_notation;
+       open_function = simple_open open_notation;
        cache_function = cache_notation;
        subst_function = subst_notation;
        load_function = load_notation;
@@ -1765,7 +1768,7 @@ let classify_scope_command (local, _, _ as o) =
 let inScopeCommand : locality_flag * scope_name * scope_command -> obj =
   declare_object {(default_object "DELIMITERS") with
       cache_function = cache_scope_command;
-      open_function = open_scope_command;
+      open_function = simple_open open_scope_command;
       load_function = load_scope_command;
       subst_function = subst_scope_command;
       classify_function = classify_scope_command}
@@ -1831,7 +1834,7 @@ let classify_custom_entry (local,s as o) =
 let inCustomEntry : locality_flag * string -> obj =
   declare_object {(default_object "CUSTOM-ENTRIES") with
       cache_function = cache_custom_entry;
-      open_function = open_custom_entry;
+      open_function = simple_open open_custom_entry;
       load_function = load_custom_entry;
       subst_function = subst_custom_entry;
       classify_function = classify_custom_entry}
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 3195f339b6..de781109ef 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -874,7 +874,7 @@ let vernac_constraint ~poly l =
 
 let vernac_import export refl =
   let import_mod qid =
-    try Declaremods.import_module ~export @@ Nametab.locate_module qid
+    try Declaremods.import_module Libobject.Unfiltered ~export @@ Nametab.locate_module qid
     with Not_found ->
       CErrors.user_err Pp.(str "Cannot find module " ++ pr_qualid qid)
    in