[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.

4 files changed, 124 insertions, 128 deletions

diff --git a/dev/ci/user-overlays/09895-ejgallego-require+upper.sh b/dev/ci/user-overlays/09895-ejgallego-require+upper.sh
new file mode 100644
index 0000000000..9a42c829ce
--- /dev/null
+++ b/dev/ci/user-overlays/09895-ejgallego-require+upper.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "9895" ] || [ "$CI_BRANCH" = "require+upper" ]; then
+
+    quickchick_CI_REF=require+upper
+    quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick
+
+fi
diff --git a/vernac/loadpath.ml b/vernac/loadpath.ml
index cd5ccd856b..b164a2e37a 100644
--- a/vernac/loadpath.ml
+++ b/vernac/loadpath.ml
@@ -8,30 +8,31 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Pp
 open Util
-open CErrors
-open Names
-open Libnames
+module DP = Names.DirPath
 
 (** Load paths. Mapping from physical to logical paths. *)
 
 type t = {
   path_physical : CUnix.physical_path;
-  path_logical : DirPath.t;
+  path_logical : DP.t;
   path_implicit : bool;
 }
 
 let load_paths = Summary.ref ([] : t list) ~name:"LOADPATHS"
 
 let logical p = p.path_logical
-
 let physical p = p.path_physical
 
+let pp p =
+  let dir = DP.print p.path_logical in
+  let path = Pp.str (CUnix.escaped_string_of_physical_path p.path_physical) in
+  Pp.(hov 2 (dir ++ spc () ++ path))
+
 let get_load_paths () = !load_paths
 
 let anomaly_too_many_paths path =
-  anomaly (str "Several logical paths are associated to" ++ spc () ++ str path ++ str ".")
+  CErrors.anomaly Pp.(str "Several logical paths are associated to" ++ spc () ++ str path ++ str ".")
 
 let find_load_path phys_dir =
   let phys_dir = CUnix.canonical_path_name phys_dir in
@@ -42,22 +43,16 @@ let find_load_path phys_dir =
   | [p] -> p
   | _ -> anomaly_too_many_paths phys_dir
 
-let is_in_load_paths phys_dir =
-  let dir = CUnix.canonical_path_name phys_dir in
-  let lp = get_load_paths () in
-  let check_p p = String.equal dir p.path_physical in
-  List.exists check_p lp
-
 let remove_load_path dir =
   let filter p = not (String.equal p.path_physical dir) in
   load_paths := List.filter filter !load_paths
 
 let warn_overriding_logical_loadpath =
   CWarnings.create ~name:"overriding-logical-loadpath" ~category:"loadpath"
-         (fun (phys_path, old_path, coq_path) ->
-          str phys_path ++ strbrk " was previously bound to " ++
-            DirPath.print old_path ++ strbrk "; it is remapped to " ++
-            DirPath.print coq_path)
+    (fun (phys_path, old_path, coq_path) ->
+       Pp.(seq [str phys_path; strbrk " was previously bound to "
+               ; DP.print old_path; strbrk "; it is remapped to "
+               ; DP.print coq_path]))
 
 let add_load_path phys_path coq_path ~implicit =
   let phys_path = CUnix.canonical_path_name phys_path in
@@ -72,12 +67,12 @@ let add_load_path phys_path coq_path ~implicit =
     load_paths := binding :: !load_paths
   | [{ path_logical = old_path; path_implicit = old_implicit }] ->
     let replace =
-      if DirPath.equal coq_path old_path then
+      if DP.equal coq_path old_path then
         implicit <> old_implicit
       else
         let () =
           (* Do not warn when overriding the default "-I ." path *)
-          if not (DirPath.equal old_path Libnames.default_root_prefix) then
+          if not (DP.equal old_path Libnames.default_root_prefix) then
           warn_overriding_logical_loadpath (phys_path, old_path, coq_path)
         in
         true in
@@ -104,11 +99,11 @@ let expand_path ?root dir =
     let success =
       match root with
       | None ->
-        if implicit then is_dirpath_suffix_of dir lg
-        else DirPath.equal dir lg
+        if implicit then Libnames.is_dirpath_suffix_of dir lg
+        else DP.equal dir lg
       | Some root ->
-        is_dirpath_prefix_of root lg &&
-          is_dirpath_suffix_of dir (drop_dirpath_prefix root lg) in
+        Libnames.(is_dirpath_prefix_of root lg &&
+                  is_dirpath_suffix_of dir (drop_dirpath_prefix root lg)) in
     if success then (ph, lg) :: aux l else aux l in
   aux !load_paths
 
@@ -121,9 +116,9 @@ let locate_file fname =
 (************************************************************************)
 (*s Locate absolute or partially qualified library names in the path *)
 
-exception LibUnmappedDir
-exception LibNotFound
 type library_location = LibLoaded | LibInPath
+type locate_error = LibUnmappedDir | LibNotFound
+type 'a locate_result = ('a, locate_error) result
 
 let warn_several_object_files =
   CWarnings.create ~name:"several-object-files" ~category:"require"
@@ -133,62 +128,76 @@ let warn_several_object_files =
             ; strbrk " because it is more recent"
             ])
 
-let locate_absolute_library dir =
+let locate_absolute_library dir : CUnix.physical_path locate_result =
   (* Search in loadpath *)
   let pref, base = Libnames.split_dirpath dir in
-  let 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
-      let _, file = System.where_in_path ~warn:false loadpath name in
-      Some file
-    with Not_found -> None in
-  match find ".vo", find ".vio" with
-  | None, None -> raise LibNotFound
-  | Some file, None | None, Some file -> file
-  | Some vo, Some vi when Unix.((stat vo).st_mtime < (stat vi).st_mtime) ->
-    warn_several_object_files (vi, vo);
-    vi
-  | Some vo, Some _ -> vo
-
-let locate_qualified_library ?root ?(warn = true) qid =
+  let loadpath = filter_path (fun dir -> DP.equal dir pref) in
+  match loadpath with
+  | [] -> Error LibUnmappedDir
+  | _ ->
+    let loadpath = List.map fst loadpath in
+    let find ext =
+      try
+        let name = Names.Id.to_string base ^ ext in
+        let _, file = System.where_in_path ~warn:false loadpath name in
+        Some file
+      with Not_found -> None in
+    match find ".vo", find ".vio" with
+    | None, None ->
+      Error LibNotFound
+    | Some file, None | None, Some file ->
+      Ok file
+    | Some vo, Some vi when Unix.((stat vo).st_mtime < (stat vi).st_mtime) ->
+      warn_several_object_files (vi, vo);
+      Ok vi
+    | Some vo, Some _ ->
+      Ok vo
+
+let locate_qualified_library ?root ?(warn = true) qid :
+  (library_location * DP.t * CUnix.physical_path) locate_result =
   (* Search library in loadpath *)
   let dir, base = Libnames.repr_qualid qid in
   let loadpath = expand_path ?root dir in
-  let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in
-  let find ext =
-    try
-      let name = Id.to_string base ^ ext in
-      let lpath, file =
-        System.where_in_path ~warn (List.map fst loadpath) name in
-      Some (lpath, file)
-    with Not_found -> None in
-  let lpath, file =
-    match find ".vo", find ".vio" with
-    | None, None -> raise LibNotFound
-    | Some res, None | None, Some res -> res
-    | Some (_, vo), Some (_, vi as resvi)
-      when Unix.((stat vo).st_mtime < (stat vi).st_mtime) ->
-      warn_several_object_files (vi, vo);
-       resvi
-    | Some resvo, Some _ -> resvo
-  in
-  let dir = Libnames.add_dirpath_suffix
-      (CString.List.assoc lpath loadpath) base in
-  (* Look if loaded *)
-  if Library.library_is_loaded dir
-  then (LibLoaded, dir, Library.library_full_filename dir)
-  (* Otherwise, look for it in the file system *)
-  else (LibInPath, dir, file)
+  match loadpath with
+  | [] -> Error LibUnmappedDir
+  | _ ->
+    let find ext =
+      try
+        let name = Names.Id.to_string base ^ ext in
+        let lpath, file =
+          System.where_in_path ~warn (List.map fst loadpath) name in
+        Some (lpath, file)
+      with Not_found -> None in
+    let vores =
+      match find ".vo", find ".vio" with
+      | None, None ->
+        Error LibNotFound
+      | Some res, None | None, Some res ->
+        Ok res
+      | Some (_, vo), Some (_, vi as resvi)
+        when Unix.((stat vo).st_mtime < (stat vi).st_mtime) ->
+        warn_several_object_files (vi, vo);
+        Ok resvi
+      | Some resvo, Some _ ->
+        Ok resvo
+    in
+    match vores with
+    | Ok (lpath, file) ->
+      let dir = Libnames.add_dirpath_suffix
+          (CString.List.assoc lpath loadpath) base in
+      (* Look if loaded *)
+      if Library.library_is_loaded dir
+      then Ok (LibLoaded, dir, Library.library_full_filename dir)
+      (* Otherwise, look for it in the file system *)
+      else Ok (LibInPath, dir, file)
+    | Error fail -> Error fail
 
 let error_unmapped_dir qid =
   let prefix, _ = Libnames.repr_qualid qid in
   CErrors.user_err ~hdr:"load_absolute_library_from"
     Pp.(seq [ str "Cannot load "; Libnames.pr_qualid qid; str ":"; spc ()
             ; str "no physical path bound to"; spc ()
-            ; DirPath.print prefix; fnl ()
+            ; DP.print prefix; fnl ()
             ])
 
 let error_lib_not_found qid =
@@ -196,12 +205,12 @@ let error_lib_not_found qid =
     Pp.(seq [ str "Cannot find library "; Libnames.pr_qualid qid; str" in loadpath"])
 
 let try_locate_absolute_library dir =
-  try
-    locate_absolute_library dir
-  with
-    | LibUnmappedDir -> error_unmapped_dir (Libnames.qualid_of_dirpath dir)
-    | LibNotFound -> error_lib_not_found (Libnames.qualid_of_dirpath dir)
-
+  match locate_absolute_library dir with
+  | Ok res -> res
+  | Error LibUnmappedDir ->
+    error_unmapped_dir (Libnames.qualid_of_dirpath dir)
+  | Error LibNotFound ->
+    error_lib_not_found (Libnames.qualid_of_dirpath dir)
 
 (** { 5 Extending the load path } *)
 
@@ -209,10 +218,10 @@ let try_locate_absolute_library dir =
 type add_ml = AddNoML | AddTopML | AddRecML
 
 type vo_path_spec = {
-  unix_path : string;           (* Filesystem path contaning vo/ml files *)
-  coq_path  : Names.DirPath.t;  (* Coq prefix for the path *)
-  implicit  : bool;             (* [implicit = true] avoids having to qualify with [coq_path] *)
-  has_ml    : add_ml;           (* If [has_ml] is true, the directory will also be search for plugins *)
+  unix_path : string;  (* Filesystem path contaning vo/ml files *)
+  coq_path  : DP.t;    (* Coq prefix for the path *)
+  implicit  : bool;    (* [implicit = true] avoids having to qualify with [coq_path] *)
+  has_ml    : add_ml;  (* If [has_ml] is true, the directory will also be search for plugins *)
 }
 
 type coq_path_spec =
@@ -226,17 +235,18 @@ type coq_path = {
 
 let warn_cannot_open_path =
   CWarnings.create ~name:"cannot-open-path" ~category:"filesystem"
-      (fun unix_path -> str "Cannot open " ++ str unix_path)
+    (fun unix_path -> Pp.(str "Cannot open " ++ str unix_path))
 
 let warn_cannot_use_directory =
   CWarnings.create ~name:"cannot-use-directory" ~category:"filesystem"
-         (fun d ->
-          str "Directory " ++ str d ++
-            strbrk " cannot be used as a Coq identifier (skipped)")
+    (fun d ->
+       Pp.(str "Directory " ++ str d ++
+           strbrk " cannot be used as a Coq identifier (skipped)"))
 
 let convert_string d =
   try Names.Id.of_string d
-  with UserError _ ->
+  with
+  | CErrors.UserError _ ->
     let d = Unicode.escaped_if_non_utf8 d in
     warn_cannot_use_directory d;
     raise Exit
@@ -246,11 +256,11 @@ let add_vo_path ~recursive lp =
   let implicit = lp.implicit in
   if System.exists_dir unix_path then
     let dirs = if recursive then System.all_subdirs ~unix_path else [] in
-    let prefix = Names.DirPath.repr lp.coq_path in
+    let prefix = DP.repr lp.coq_path in
     let convert_dirs (lp, cp) =
       try
         let path = List.rev_map convert_string cp @ prefix in
-        Some (lp, Names.DirPath.make path)
+        Some (lp, DP.make path)
       with Exit -> None
     in
     let dirs = List.map_filter convert_dirs dirs in
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
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 4fd9c713b9..29b78a5195 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -201,11 +201,6 @@ let show_match id =
 
 (* "Print" commands *)
 
-let print_path_entry p =
-  let dir = DirPath.print (Loadpath.logical p) in
-  let path = str (CUnix.escaped_string_of_physical_path (Loadpath.physical p)) in
-  Pp.hov 2 (dir ++ spc () ++ path)
-
 let print_loadpath dir =
   let l = Loadpath.get_load_paths () in
   let l = match dir with
@@ -215,7 +210,7 @@ let print_loadpath dir =
     List.filter filter l
   in
   str "Logical Path / Physical path:" ++ fnl () ++
-    prlist_with_sep fnl print_path_entry l
+    prlist_with_sep fnl Loadpath.pp l
 
 let print_modules () =
   let opened = Library.opened_libraries ()
@@ -472,10 +467,10 @@ let err_notfound_library ?from qid =
 
 let print_located_library qid =
   let open Loadpath in
-  try msg_found_library (locate_qualified_library ~warn:false qid)
-  with
-    | LibUnmappedDir -> err_unmapped_library qid
-    | LibNotFound -> err_notfound_library qid
+  match locate_qualified_library ~warn:false qid with
+  | Ok lib -> msg_found_library lib
+  | Error LibUnmappedDir -> err_unmapped_library qid
+  | Error LibNotFound -> err_notfound_library qid
 
 let smart_global r =
   let gr = Smartlocate.smart_global r in
@@ -1028,13 +1023,11 @@ let vernac_require from import qidl =
   in
   let locate qid =
     let open Loadpath in
-    try
-      let warn = not !Flags.quiet in
-      let (_, dir, f) = locate_qualified_library ?root ~warn qid in
-      (dir, f)
-    with
-      | LibUnmappedDir -> err_unmapped_library ?from:root qid
-      | LibNotFound -> err_notfound_library ?from:root qid
+    let warn = not !Flags.quiet in
+    match locate_qualified_library ?root ~warn qid with
+    | Ok (_,dir,f) -> dir, f
+    | Error LibUnmappedDir -> err_unmapped_library ?from:root qid
+    | Error LibNotFound -> err_notfound_library ?from:root qid
   in
   let modrefl = List.map locate qidl in
   if Dumpglob.dump () then
@@ -1144,7 +1137,6 @@ let vernac_add_loadpath implicit pdir ldiropt =
 
 let vernac_remove_loadpath path =
   Loadpath.remove_load_path (expand path)
-
   (* Coq syntax for ML or system commands *)
 
 let vernac_add_ml_path isrec path =