[loadpath] Further cleanup after merge with MlTop.

We cleanup a bit the implementation of LoadPath which is not possible
as now all the loadpath logic is in the same place.

In particular, we remove exceptions in favor a `locate_result` monad.

More cleanup should still be possible, in particular
`locate_absolute_library` and `locate_qualified_library` should be
merged.

1 files changed, 11 insertions, 23 deletions

diff --git a/vernac/loadpath.mli b/vernac/loadpath.mli
index fe4dc55c21..d393fc35b5 100644
--- a/vernac/loadpath.mli
+++ b/vernac/loadpath.mli
@@ -20,19 +20,15 @@ open Names
 type t
 (** Type of loadpath bindings. *)
 
-val physical : t -> CUnix.physical_path
-(** Get the physical path (filesystem location) of a loadpath. *)
-
 val logical : t -> DirPath.t
 (** Get the logical path (Coq module hierarchy) of a loadpath. *)
 
+val pp : t -> Pp.t
+(** Print a load path *)
+
 val get_load_paths : unit -> t list
 (** Get the current loadpath association. *)
 
-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
 (** Remove the current logical path binding associated to a given physical path,
     if any. *)
@@ -41,29 +37,21 @@ val find_load_path : CUnix.physical_path -> t
 (** Get the binding associated to a physical path. Raises [Not_found] if there
     is none. *)
 
-val is_in_load_paths : CUnix.physical_path -> bool
-(** Whether a physical path is currently bound. *)
-
-val expand_path : ?root:DirPath.t -> 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 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. *)
-
 val locate_file : string -> string
 (** Locate a file among the registered paths. Do not use this function, as
     it does not respect the visibility of paths. *)
 
 (** {6 Locate a library in the load path } *)
-exception LibUnmappedDir
-exception LibNotFound
 type library_location = LibLoaded | LibInPath
+type locate_error = LibUnmappedDir | LibNotFound
+type 'a locate_result = ('a, locate_error) result
+
+val locate_qualified_library
+  :  ?root:DirPath.t
+  -> ?warn:bool
+  -> Libnames.qualid
+  -> (library_location * DirPath.t * CUnix.physical_path) locate_result
 
-val locate_qualified_library :
-  ?root:DirPath.t -> ?warn:bool -> Libnames.qualid ->
-  library_location * DirPath.t * CUnix.physical_path
 (** Locates a library by implicit name.
 
   @raise LibUnmappedDir if the library is not in the path