From X Require Y looks for X with absolute path, disregarding -R.

6 files changed, 35 insertions, 23 deletions

diff --git a/library/libnames.ml b/library/libnames.ml
index f2a9d041d..cdaec6a3d 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 3b5feb94e..b95c08871 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 2ebf4e5c3..9d0ccb972 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} *)
 
diff --git a/library/library.mli b/library/library.mli
index 150896783..350670680 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -72,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 ca2280102..54ea0be4f 100644
--- a/library/loadpath.ml
+++ b/library/loadpath.ml
@@ -87,20 +87,15 @@ 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 DirPath.equal p.path_logical dir then p.path_physical :: aux l
+    if f p.path_logical then (p.path_physical, p.path_logical) :: aux l
     else aux l
   in
   aux !load_paths
 
-let is_suffix dir1 dir2 =
-  let dir1 = DirPath.repr dir1 in
-  let dir2 = DirPath.repr dir2 in
-  List.prefix_of Id.equal dir1 dir2
-
 let expand_path dir =
   let rec aux = function
   | [] -> []
@@ -109,7 +104,7 @@ let expand_path dir =
     match p.path_implicit with
     | true ->
       (** The path is implicit, so that we only want match the logical suffix *)
-      if is_suffix dir lg then (ph, lg) :: aux l else aux l
+      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
diff --git a/library/loadpath.mli b/library/loadpath.mli
index ae54b3183..3251b8c60 100644
--- a/library/loadpath.mli
+++ b/library/loadpath.mli
@@ -49,5 +49,6 @@ 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 matches of it. *)
 
-val expand_root_path : DirPath.t -> CUnix.physical_path list
-(** As [expand_path] but ignores the implicit status. *)
+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. *)