Merge branch 'v8.5'

6 files changed, 60 insertions, 55 deletions

diff --git a/library/globnames.ml b/library/globnames.ml
index 5eb091af4c..3befaa9a94 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Util
 open Errors
 open Names
 open Term
diff --git a/library/library.ml b/library/library.ml
index b078e2c478..e4169d66e0 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -172,28 +172,32 @@ let open_libraries export modl =
 
 
 (**********************************************************************)
-(* import and export  -  synchronous operations*)
+(* 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 i (_,(dir,export)) =
+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 [try_find_library dir]
+      open_libraries export (List.map try_find_library modl)
 
-let cache_import obj =
-  open_import 1 obj
+let cache_import_library obj =
+  open_import_library 1 obj
 
-let subst_import (_,o) = o
+let subst_import_library (_,o) = o
 
-let classify_import (_,export as obj) =
+let classify_import_library (_,export as obj) =
   if export then Substitute obj else Dispose
 
-let in_import : DirPath.t * bool -> obj =
+let in_import_library : DirPath.t list * bool -> obj =
   declare_object {(default_object "IMPORT LIBRARY") with
-       cache_function = cache_import;
-       open_function = open_import;
-       subst_function = subst_import;
-       classify_function = classify_import }
+       cache_function = cache_import_library;
+       open_function = open_import_library;
+       subst_function = subst_import_library;
+       classify_function = classify_import_library }
 
 
 (************************************************************************)
@@ -310,7 +314,7 @@ let fetch_table what dp (f,pos,digest) =
     if not (String.equal (System.digest_in f ch) digest) then raise Faulty;
     let table, pos', digest' = System.marshal_in_segment f ch in
     let () = close_in ch in
-    let ch' = open_in f in
+    let ch' = open_in_bin f in
     if not (String.equal (Digest.channel ch' pos') digest') then raise Faulty;
     let () = close_in ch' in
     table
@@ -402,9 +406,6 @@ let intern_from_file f =
 
 module DPMap = Map.Make(DirPath)
 
-let deps_to_string deps =
-  Array.fold_left (fun s (n, _) -> s^"\n  - "^(DirPath.to_string n)) "" deps
-
 let rec intern_library (needed, contents) (dir, f) from =
   Pp.feedback(Feedback.FileDependency (from, f));
   (* Look if in the current logical environment *)
@@ -543,7 +544,7 @@ let require_library_from_dirpath modrefl export =
       begin
 	add_anonymous_leaf (in_require (needed,modrefl,None));
 	Option.iter (fun exp ->
-	  List.iter (fun dir -> add_anonymous_leaf (in_import(dir,exp))) modrefl)
+	  add_anonymous_leaf (in_import_library (modrefl,exp)))
 	  export
       end
     else
@@ -559,7 +560,7 @@ let require_library_from_file idopt file export =
   let needed = List.rev_map snd needed in
   if Lib.is_module_or_modtype () then begin
     add_anonymous_leaf (in_require (needed,[modref],None));
-    Option.iter (fun exp -> add_anonymous_leaf (in_import (modref,exp)))
+    Option.iter (fun exp -> add_anonymous_leaf (in_import_library ([modref],exp)))
       export
   end
   else
@@ -568,21 +569,30 @@ let require_library_from_file idopt file export =
 
 (* the function called by Vernacentries.vernac_import *)
 
-let import_module export (loc,qid) =
-  try
-    match Nametab.locate_module qid with
-      | MPfile dir ->
-	  if Lib.is_module_or_modtype () || not export then
-	    add_anonymous_leaf (in_import (dir, export))
-	  else
-	    add_anonymous_leaf (in_import (dir, export))
-      | mp ->
-	  Declaremods.import_module export mp
-  with
-      Not_found ->
-	user_err_loc
-          (loc,"import_library",
-	  str ((string_of_qualid qid)^" is not a module"))
+let safe_locate_module (loc,qid) =
+  try Nametab.locate_module qid
+  with Not_found ->
+    user_err_loc
+      (loc,"import_library", str (string_of_qualid qid ^ " 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
+    | m :: l ->
+        (match safe_locate_module m with
+        | MPfile dir -> aux (dir::acc) l
+        | mp -> flush acc; Declaremods.import_module export mp; aux [] l)
+    | [] -> flush acc
+  in aux [] modl
 
 (************************************************************************)
 (*s Initializing the compilation of a library. *)
diff --git a/library/library.mli b/library/library.mli
index 13d83a5c02..77d78207da 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -37,7 +37,7 @@ type seg_proofs = Term.constr Future.computation 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 located -> unit
+val import_module : bool -> qualid located list -> unit
 
 (** {6 Start the compilation of a library } *)
 val start_library : string -> DirPath.t * string
diff --git a/library/loadpath.ml b/library/loadpath.ml
index 5876eedd2a..ab8b0a3078 100644
--- a/library/loadpath.ml
+++ b/library/loadpath.ml
@@ -12,14 +12,13 @@ open Errors
 open Names
 open Libnames
 
-type path_type = ImplicitPath | ImplicitRootPath | RootPath
-
 (** Load paths. Mapping from physical to logical paths. *)
 
 type t = {
   path_physical : CUnix.physical_path;
   path_logical : DirPath.t;
-  path_type : path_type;
+  path_root : bool;
+  path_implicit : bool;
 }
 
 let load_paths = Summary.ref ([] : t list) ~name:"LOADPATHS"
@@ -54,13 +53,14 @@ let remove_load_path dir =
   let filter p = not (String.equal p.path_physical dir) in
   load_paths := List.filter filter !load_paths
 
-let add_load_path phys_path path_type coq_path =
+let add_load_path phys_path coq_path ~root ~implicit =
   let phys_path = CUnix.canonical_path_name phys_path in
   let filter p = String.equal p.path_physical phys_path in
   let binding = {
     path_logical = coq_path;
     path_physical = phys_path;
-    path_type = path_type;
+    path_root = root;
+    path_implicit = implicit;
   } in
   match List.filter filter !load_paths with
   | [] ->
@@ -93,7 +93,7 @@ let expand_root_path dir =
   let rec aux = function
   | [] -> []
   | p :: l ->
-    if p.path_type <> ImplicitPath && is_dirpath_prefix_of p.path_logical dir then
+    if p.path_root && is_dirpath_prefix_of p.path_logical dir then
       let suffix = drop_dirpath_prefix p.path_logical dir in
       extend_path_with_dirpath p.path_physical suffix :: aux l
     else aux l
@@ -123,13 +123,17 @@ let expand_path dir =
   let rec aux = function
   | [] -> []
   | p :: l ->
-    match p.path_type with
-    | ImplicitPath -> expand p dir :: aux l
-    | ImplicitRootPath ->
+    match p.path_implicit, p.path_root with
+    | true, false -> expand p dir :: aux l
+    | true, true ->
       let inters = intersections p.path_logical dir in
       List.map (expand p) inters @ aux l
-    | RootPath ->
+    | false, true ->
       if is_dirpath_prefix_of p.path_logical dir then
 	expand p (drop_dirpath_prefix p.path_logical dir) :: aux l
-      else aux l in
+      else aux l
+    | false, false ->
+      (* nothing to do, an explicit root path should also match above
+         if [is_dirpath_prefix_of p.path_logical dir] were true here *)
+      aux l in
   aux !load_paths
diff --git a/library/loadpath.mli b/library/loadpath.mli
index 62dc5d5912..d4029303d2 100644
--- a/library/loadpath.mli
+++ b/library/loadpath.mli
@@ -15,11 +15,6 @@ open Names
 
 *)
 
-type path_type =
-  | ImplicitPath     (** Can be implicitly appended to a logical path. *)
-  | ImplicitRootPath (** Can be implicitly appended to the suffix of a logical path. *)
-  | RootPath         (** Can only be a prefix of a logical path. *)
-
 type t
 (** Type of loadpath bindings. *)
 
@@ -35,7 +30,7 @@ val get_load_paths : unit -> t list
 val get_paths : unit -> CUnix.physical_path list
 (** Same as [get_load_paths] but only get the physical part. *)
 
-val add_load_path : CUnix.physical_path -> path_type -> DirPath.t -> unit
+val add_load_path : CUnix.physical_path -> DirPath.t -> root:bool -> implicit:bool -> unit
 (** [add_load_path phys type log] adds the binding [phys := log] to the current
     loadpaths. *)
 
diff --git a/library/universes.mli b/library/universes.mli
index f2f68d329c..252648d7dc 100644
--- a/library/universes.mli
+++ b/library/universes.mli
@@ -7,12 +7,9 @@
 (************************************************************************)
 
 open Util
-open Pp
 open Names
 open Term
-open Context
 open Environ
-open Locus
 open Univ
 
 (** Universes *)