Optimize multiple imports

6 files changed, 29 insertions, 19 deletions

diff --git a/checker/values.ml b/checker/values.ml
index 1590097731..6b340635d7 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -357,7 +357,7 @@ and v_libobjt = Sum("Libobject.t",0,
      [| v_substobjs |];
      [| v_aobjs |];
      [| v_libobjs |];
-     [| v_mp |];
+     [| List v_mp |];
      [| v_obj |]
   |])
 
diff --git a/library/declaremods.ml b/library/declaremods.ml
index cca3bfa3b7..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')
-    | ExportObject { mp } ->
-      let mp' = subst_mp subst mp in
-      if mp'==mp then node else (id, ExportObject { 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
@@ -299,18 +299,23 @@ let rec collect_module_objects mp acc =
 
 and collect_object i (name, obj as o) acc =
   match obj with
-  | ExportObject { mp; _ } -> collect_export i mp acc
+  | 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_export i mp (exports,objs as acc) =
-  if Int.equal i 1 && not (MPset.mem mp exports) then
+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
+
 let rec open_object i (name, obj) =
   match obj with
   | AtomicObject o -> Libobject.open_object i (name, o)
@@ -320,7 +325,7 @@ let rec open_object i (name, obj) =
     open_module i dir mp sobjs
   | ModuleTypeObject sobjs -> open_modtype i (name, sobjs)
   | IncludeObject aobjs -> open_include i (name, aobjs)
-  | ExportObject { mp; _ } -> open_export i mp
+  | ExportObject { mpl; _ } -> open_export i mpl
   | KeepObject objs -> open_keep i (name, objs)
 
 and open_module i obj_dir obj_mp sobjs =
@@ -354,9 +359,8 @@ and open_include i ((sp,kn), aobjs) =
   let o = expand_aobjs aobjs in
   open_objects i prefix o
 
-and open_export i mp =
-  if Int.equal i 1 then
-  let _,objs = collect_module_objects mp (MPset.empty, []) in
+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) =
@@ -372,7 +376,7 @@ let rec cache_object (name, obj) =
     let (sp,kn) = name in
     load_modtype 0 sp (mp_of_kn kn) sobjs
   | IncludeObject aobjs -> cache_include (name, aobjs)
-  | ExportObject { mp } -> anomaly Pp.(str "Export should not be cached")
+  | ExportObject { mpl } -> anomaly Pp.(str "Export should not be cached")
   | KeepObject objs -> cache_keep (name, objs)
 
 and cache_include ((sp,kn), aobjs) =
@@ -1019,10 +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 =
-  let _,objs = collect_module_objects mp (MPset.empty, []) in
+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 { mp }))
+  if export then Lib.add_anonymous_entry (Lib.Leaf (ExportObject { mpl }))
+
+let import_module ~export mp =
+  import_modules ~export [mp]
 
 (** {6 Iterators} *)
 
diff --git a/library/declaremods.mli b/library/declaremods.mli
index c1d2de9783..b7c7cd1dba 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -111,6 +111,10 @@ val append_end_library_hook : (unit -> unit) -> 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  *)
 
 val declare_include :
diff --git a/library/libobject.ml b/library/libobject.ml
index 3d4a33c74e..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
-  | ExportObject of { 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 88d292ad03..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
-  | ExportObject of { mp : Names.ModPath.t }
+  | ExportObject of { mpl : Names.ModPath.t list }
   | AtomicObject of obj
 
 and objects = (Names.Id.t * t) list
diff --git a/vernac/library.ml b/vernac/library.ml
index 437ec7961e..8125c3de35 100644
--- a/vernac/library.ml
+++ b/vernac/library.ml
@@ -340,8 +340,7 @@ let load_require _ (_,(needed,modl,_)) =
   List.iter register_library needed
 
 let open_require i (_,(_,modl,export)) =
-  Option.iter (fun export -> List.iter (fun m -> Declaremods.import_module ~export (MPfile m)) modl)
-    export
+  Option.iter (fun export -> Declaremods.import_modules ~export @@ List.map (fun m -> MPfile m) modl) export
 
   (* [needed] is the ordered list of libraries not already loaded *)
 let cache_require o =