diff options
| -rw-r--r-- | library/libnames.ml | 5 | ||||
| -rw-r--r-- | library/libnames.mli | 2 | ||||
| -rw-r--r-- | library/library.ml | 25 | ||||
| -rw-r--r-- | library/library.mli | 10 | ||||
| -rw-r--r-- | library/loadpath.ml | 11 | ||||
| -rw-r--r-- | library/loadpath.mli | 5 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 24 |
7 files changed, 53 insertions, 29 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. *) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 62e5f0a32..7d29a3f8e 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -392,7 +392,7 @@ let err_notfound_library loc qid = let print_located_library r = let (loc,qid) = qualid_of_reference r in - try msg_found_library (Library.locate_qualified_library false qid) + try msg_found_library (Library.locate_qualified_library ~warn:false qid) with | Library.LibUnmappedDir -> err_unmapped_library loc qid | Library.LibNotFound -> err_notfound_library loc qid @@ -750,12 +750,24 @@ let vernac_end_segment (_,id as lid) = (* Libraries *) let vernac_require from import qidl = - let qidl = match from with - | None -> qidl - | Some ns -> List.map (Libnames.join_reference ns) qidl - in let qidl = List.map qualid_of_reference qidl in - let modrefl = List.map Library.try_locate_qualified_library qidl in + let root = match from with + | None -> None + | Some from -> + let (_, qid) = Libnames.qualid_of_reference from in + let (hd, tl) = Libnames.repr_qualid qid in + Some (Libnames.add_dirpath_suffix hd tl) + in + let locate (loc, qid) = + try + let warn = Flags.is_verbose () in + let (_, dir, f) = Library.locate_qualified_library ?root ~warn qid in + (dir, f) + with + | Library.LibUnmappedDir -> err_unmapped_library loc qid + | Library.LibNotFound -> err_unmapped_library loc qid + in + let modrefl = List.map locate qidl in if Dumpglob.dump () then List.iter2 (fun (loc, _) dp -> Dumpglob.dump_libref loc dp "lib") qidl (List.map fst modrefl); Library.require_library_from_dirpath modrefl import |