Merge branch 'v8.5' into trunk

6 files changed, 64 insertions, 77 deletions

diff --git a/library/libnames.ml b/library/libnames.ml
index f2a9d041d1..cdaec6a3de 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -32,6 +32,11 @@ let is_dirpath_prefix_of d1 d2 =
   List.prefix_of Id.equal
     (List.rev (DirPath.repr d1)) (List.rev (DirPath.repr d2))
 
+let is_dirpath_suffix_of dir1 dir2 =
+  let dir1 = DirPath.repr dir1 in
+  let dir2 = DirPath.repr dir2 in
+  List.prefix_of Id.equal dir1 dir2
+
 let chop_dirpath n d =
   let d1,d2 = List.chop n (List.rev (DirPath.repr d)) in
   DirPath.make (List.rev d1), DirPath.make (List.rev d2)
diff --git a/library/libnames.mli b/library/libnames.mli
index 3b5feb94e8..b95c088715 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -37,6 +37,8 @@ val append_dirpath : DirPath.t -> DirPath.t -> DirPath.t
 val drop_dirpath_prefix : DirPath.t -> DirPath.t -> DirPath.t
 val is_dirpath_prefix_of : DirPath.t -> DirPath.t -> bool
 
+val is_dirpath_suffix_of : DirPath.t -> DirPath.t -> bool
+
 module Dirset : Set.S with type elt = DirPath.t
 module Dirmap : Map.ExtS with type key = DirPath.t and module Set := Dirset
 
diff --git a/library/library.ml b/library/library.ml
index 2b607e1a38..9d0ccb972a 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -268,8 +268,9 @@ type library_location = LibLoaded | LibInPath
 let locate_absolute_library dir =
   (* Search in loadpath *)
   let pref, base = split_dirpath dir in
-  let loadpath = Loadpath.expand_root_path pref in
+  let loadpath = Loadpath.filter_path (fun dir -> DirPath.equal dir pref) in
   let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in
+  let loadpath = List.map fst loadpath in
   let find ext =
     try
       let name = Id.to_string base ^ ext in
@@ -286,10 +287,20 @@ let locate_absolute_library dir =
   | [vo;vi] -> dir, vo
   | _ -> assert false
 
-let locate_qualified_library warn qid =
+let locate_qualified_library ?root ?(warn = true) qid =
   (* Search library in loadpath *)
   let dir, base = repr_qualid qid in
-  let loadpath = Loadpath.expand_path dir in
+  let loadpath = match root with
+  | None -> Loadpath.expand_path dir
+  | Some root ->
+    let filter path =
+      if is_dirpath_prefix_of root path then
+        let path = drop_dirpath_prefix root path in
+        is_dirpath_suffix_of dir path
+      else false
+    in
+    Loadpath.filter_path filter
+  in
   let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in
   let find ext =
     try
@@ -333,14 +344,6 @@ let try_locate_absolute_library dir =
     | LibUnmappedDir -> error_unmapped_dir (qualid_of_dirpath dir)
     | LibNotFound -> error_lib_not_found (qualid_of_dirpath dir)
 
-let try_locate_qualified_library (loc,qid) =
-  try
-    let (_,dir,f) = locate_qualified_library (Flags.is_verbose()) qid in
-    dir,f
-  with
-    | LibUnmappedDir -> error_unmapped_dir qid
-    | LibNotFound -> error_lib_not_found qid
-
 (************************************************************************)
 (** {6 Tables of opaque proof terms} *)
 
@@ -592,10 +595,6 @@ let require_library_from_dirpath modrefl export =
       add_anonymous_leaf (in_require (needed,modrefl,export));
   add_frozen_state ()
 
-let require_library qidl export =
-  let modrefl = List.map try_locate_qualified_library qidl in
-    require_library_from_dirpath modrefl export
-
 let require_library_from_file idopt file export =
   let modref,needed = rec_intern_library_from_file idopt file in
   let needed = List.rev_map snd needed in
diff --git a/library/library.mli b/library/library.mli
index 75b256258f..3506706809 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -21,7 +21,6 @@ open Libnames
 (** {6 ... } *)
 (** Require = load in the environment + open (if the optional boolean
     is not [None]); mark also for export if the boolean is [Some true] *)
-val require_library : qualid located list -> bool option -> unit
 val require_library_from_dirpath : (DirPath.t * string) list -> bool option -> unit
 val require_library_from_file :
   Id.t option -> CUnix.physical_path -> bool option -> unit
@@ -73,8 +72,14 @@ exception LibNotFound
 type library_location = LibLoaded | LibInPath
 
 val locate_qualified_library :
-  bool -> qualid -> library_location * DirPath.t * CUnix.physical_path
-val try_locate_qualified_library : qualid located -> DirPath.t * string
+  ?root:DirPath.t -> ?warn:bool -> qualid ->
+  library_location * DirPath.t * CUnix.physical_path
+(** Locates a library by implicit name.
+
+  @raise LibUnmappedDir if the library is not in the path
+  @raise LibNotFound if there is no corresponding file in the path
+
+*)
 
 (** {6 Statistics: display the memory use of a library. } *)
 val mem : DirPath.t -> Pp.std_ppcmds
diff --git a/library/loadpath.ml b/library/loadpath.ml
index ab8b0a3078..26af809e78 100644
--- a/library/loadpath.ml
+++ b/library/loadpath.ml
@@ -17,7 +17,6 @@ open Libnames
 type t = {
   path_physical : CUnix.physical_path;
   path_logical : DirPath.t;
-  path_root : bool;
   path_implicit : bool;
 }
 
@@ -53,33 +52,35 @@ 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 coq_path ~root ~implicit =
+let add_load_path phys_path coq_path ~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_root = root;
     path_implicit = implicit;
   } in
   match List.filter filter !load_paths with
   | [] ->
     load_paths := binding :: !load_paths
-  | [p] ->
-    let dir = p.path_logical in
-    if not (DirPath.equal coq_path dir)
-      (* If this is not the default -I . to coqtop *)
-      && not
-      (String.equal phys_path (CUnix.canonical_path_name Filename.current_dir_name)
-          && DirPath.equal coq_path (Nameops.default_root_prefix))
-    then
+  | [{ path_logical = old_path; path_implicit = old_implicit }] ->
+    let replace =
+      if DirPath.equal coq_path old_path then
+        implicit <> old_implicit
+      else if DirPath.equal coq_path (Nameops.default_root_prefix)
+              && String.equal phys_path (CUnix.canonical_path_name Filename.current_dir_name) then
+        false (* This is the default "-I ." path, don't override the old path *)
+      else
+        let () =
+          (* Do not warn when overriding the default "-I ." path *)
+          if not (DirPath.equal old_path Nameops.default_root_prefix) then
+            msg_warning
+              (str phys_path ++ strbrk " was previously bound to " ++
+                 pr_dirpath old_path ++ strbrk "; it is remapped to " ++
+                 pr_dirpath coq_path) in
+        true in
+    if replace then
       begin
-        (* Assume the user is concerned by library naming *)
-        if not (DirPath.equal dir Nameops.default_root_prefix) then
-          msg_warning
-            (str phys_path ++ strbrk " was previously bound to " ++
-              pr_dirpath dir ++ strbrk "; it is remapped to " ++
-              pr_dirpath coq_path);
         remove_load_path phys_path;
         load_paths := binding :: !load_paths;
       end
@@ -89,51 +90,25 @@ let extend_path_with_dirpath p dir =
   List.fold_left Filename.concat p
     (List.rev_map Id.to_string (DirPath.repr dir))
 
-let expand_root_path dir =
+let filter_path f =
   let rec aux = function
   | [] -> []
   | p :: l ->
-    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
+    if f p.path_logical then (p.path_physical, p.path_logical) :: aux l
     else aux l
   in
   aux !load_paths
 
-(* Root p is bound to A.B.C.D and we require file C.D.E.F *)
-(* We may mean A.B.C.D.E.F, or A.B.C.D.C.D.E.F *)
-
-(* Root p is bound to A.B.C.C and we require file C.C.E.F *)
-(* We may mean A.B.C.C.E.F, or A.B.C.C.C.E.F, or A.B.C.C.C.C.E.F *)
-
-let intersections d1 d2 =
-  let rec aux d1 =
-    if DirPath.is_empty d1 then [d2] else
-      let rest = aux (snd (chop_dirpath 1 d1)) in
-      if is_dirpath_prefix_of d1 d2 then drop_dirpath_prefix d1 d2 :: rest
-      else rest in
-  aux d1
-
-let expand p dir =
-  let ph = extend_path_with_dirpath p.path_physical dir in
-  let log = append_dirpath p.path_logical dir in
-  (ph, log)
-
 let expand_path dir =
   let rec aux = function
   | [] -> []
-  | p :: l ->
-    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
-    | 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
-    | 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
+  | { path_physical = ph; path_logical = lg; path_implicit = implicit }  :: l ->
+    match implicit with
+    | true ->
+      (** The path is implicit, so that we only want match the logical suffix *)
+      if is_dirpath_suffix_of dir lg then (ph, lg) :: aux l else aux l
+    | false ->
+      (** Otherwise we must match exactly *)
+      if DirPath.equal dir lg then (ph, lg) :: aux l else aux l
+  in
   aux !load_paths
diff --git a/library/loadpath.mli b/library/loadpath.mli
index d4029303d2..3251b8c60c 100644
--- a/library/loadpath.mli
+++ b/library/loadpath.mli
@@ -30,8 +30,8 @@ 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 -> DirPath.t -> root:bool -> implicit:bool -> unit
-(** [add_load_path phys type log] adds the binding [phys := log] to the current
+val add_load_path : CUnix.physical_path -> DirPath.t -> implicit:bool -> unit
+(** [add_load_path phys log type] adds the binding [phys := log] to the current
     loadpaths. *)
 
 val remove_load_path : CUnix.physical_path -> unit
@@ -47,7 +47,8 @@ val is_in_load_paths : CUnix.physical_path -> bool
 
 val expand_path : DirPath.t -> (CUnix.physical_path * DirPath.t) list
 (** Given a relative logical path, associate the list of absolute physical and
-    logical paths which are possible expansions of it. *)
+    logical paths which are possible matches of it. *)
 
-val expand_root_path : DirPath.t -> CUnix.physical_path list
-(** As [expand_path] but restricts to root loadpaths. *)
+val filter_path : (DirPath.t -> bool) -> (CUnix.physical_path * DirPath.t) list
+(** As {!expand_path} but uses a filter function instead, and ignores the
+    implicit status of loadpaths. *)