[toplevel] Refactor load path handling.

We refactor top-level load path handling. This is in preparation to
make load paths become local to a particular document.

To this effect, we introduce a new data type `coq_path` that includes
the full specification of a load path:

```
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 *)
}

type coq_path_spec =
  | VoPath of vo_path_spec
  | MlPath of string

type coq_path = {
  path_spec: coq_path_spec;
  recursive: bool;
}
```

Then, initialization of load paths is split into building a list of
load paths and actually making them effective. A future commit will
make thus the list of load paths a parameter for document creation.

This API is necessarily internal [for now] thus I don't think a
changes entry is needed.

6 files changed, 124 insertions, 62 deletions

diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 176dfb3c9..b3b5375bf 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -59,13 +59,23 @@ let load_rcfile ~time doc sid =
      doc, sid)
 
 (* Recursively puts dir in the LoadPath if -nois was not passed *)
-let add_stdlib_path ~load_init ~unix_path ~coq_root ~with_ml =
-  let add_ml = if with_ml then Mltop.AddRecML else Mltop.AddNoML in
-  Mltop.add_rec_path add_ml ~unix_path ~coq_root ~implicit:load_init
+let build_stdlib_path ~load_init ~unix_path ~coq_path ~with_ml =
+  let open Mltop in
+  let add_ml = if with_ml then AddRecML else AddNoML in
+  { recursive = true;
+    path_spec = VoPath { unix_path; coq_path ; has_ml = add_ml; implicit = load_init }
+  }
 
-let add_userlib_path ~unix_path =
-  Mltop.add_rec_path Mltop.AddRecML ~unix_path
-    ~coq_root:Libnames.default_root_prefix ~implicit:false
+let build_userlib_path ~unix_path =
+  let open Mltop in
+  { recursive = true;
+    path_spec = VoPath {
+        unix_path;
+        coq_path = Libnames.default_root_prefix;
+        has_ml = Mltop.AddRecML;
+        implicit = false;
+      }
+  }
 
 (* Options -I, -I-as, and -R of the command line *)
 let includes = ref []
@@ -74,51 +84,65 @@ let push_include s alias implicit =
 let ml_includes = ref []
 let push_ml_include s = ml_includes := s :: !ml_includes
 
+let ml_path_if c p =
+  let open Mltop in
+  let f x = { recursive = false; path_spec = MlPath x } in
+  if c then List.map f p else []
+
 (* Initializes the LoadPath *)
 let init_load_path ~load_init =
+  let open Mltop in
   let coqlib = Envars.coqlib () in
   let user_contrib = coqlib/"user-contrib" in
   let xdg_dirs = Envars.xdg_dirs ~warn:(fun x -> Feedback.msg_warning (str x)) in
   let coqpath = Envars.coqpath in
-  let coq_root = Names.DirPath.make [Libnames.coq_root] in
-    (* NOTE: These directories are searched from last to first *)
-    (* first, developer specific directory to open *)
-    if Coq_config.local then
-      Mltop.add_ml_dir (coqlib/"dev");
-    (* main loops *)
-    if Coq_config.local || !Flags.boot then begin
-      Mltop.add_ml_dir (coqlib/"stm");
-      Mltop.add_ml_dir (coqlib/"ide")
-    end;
-    if System.exists_dir (coqlib/"toploop") then
-      Mltop.add_ml_dir (coqlib/"toploop");
-    (* then standard library *)
-    add_stdlib_path ~load_init ~unix_path:(coqlib/"theories") ~coq_root ~with_ml:false;
-    (* then plugins *)
-    add_stdlib_path ~load_init ~unix_path:(coqlib/"plugins") ~coq_root ~with_ml:true;
-    (* then user-contrib *)
-    if Sys.file_exists user_contrib then
-      add_userlib_path ~unix_path:user_contrib;
-    (* then directories in XDG_DATA_DIRS and XDG_DATA_HOME *)
-    List.iter (fun s -> add_userlib_path ~unix_path:s) xdg_dirs;
-    (* then directories in COQPATH *)
-    List.iter (fun s -> add_userlib_path ~unix_path:s) coqpath;
-    (* then current directory (not recursively!) *)
-    Mltop.add_ml_dir ".";
-    Loadpath.add_load_path "." Libnames.default_root_prefix ~implicit:false;
-    (* additional loadpath, given with options -Q and -R *)
-    List.iter
-      (fun (unix_path, coq_root, implicit) ->
-        Mltop.add_rec_path Mltop.AddNoML ~unix_path ~coq_root ~implicit)
-      (List.rev !includes);
-    (* additional ml directories, given with option -I *)
-    List.iter Mltop.add_ml_dir (List.rev !ml_includes)
+  let coq_path = Names.DirPath.make [Libnames.coq_root] in
+
+  (* NOTE: These directories are searched from last to first *)
+  (* first, developer specific directory to open *)
+  ml_path_if Coq_config.local [coqlib/"dev"] @
+
+  (* main loops *)
+  ml_path_if (Coq_config.local || !Flags.boot) [coqlib/"stm"; coqlib/"ide"] @
+  ml_path_if (System.exists_dir (coqlib/"toploop")) [coqlib/"toploop"] @
+
+  (* then standard library and plugins *)
+  [build_stdlib_path ~load_init ~unix_path:(coqlib/"theories") ~coq_path ~with_ml:false;
+   build_stdlib_path ~load_init ~unix_path:(coqlib/"plugins")  ~coq_path ~with_ml:true ] @
+
+  (* then user-contrib *)
+  (if Sys.file_exists user_contrib then
+     [build_userlib_path ~unix_path:user_contrib] else []
+  ) @
+
+  (* then directories in XDG_DATA_DIRS and XDG_DATA_HOME and COQPATH *)
+  List.map (fun s -> build_userlib_path ~unix_path:s) (xdg_dirs @ coqpath) @
+
+  (* then current directory (not recursively!) *)
+  [ { recursive = false;
+      path_spec = VoPath { unix_path = ".";
+                           coq_path = Libnames.default_root_prefix;
+                           implicit = false;
+                           has_ml = AddTopML }
+    } ] @
+
+  (* additional loadpaths, given with options -Q and -R *)
+  List.map
+    (fun (unix_path, coq_path, implicit) ->
+       { recursive = true;
+         path_spec = VoPath { unix_path; coq_path; has_ml = Mltop.AddNoML; implicit } })
+      (List.rev !includes) @
+
+  (* additional ml directories, given with option -I *)
+  List.map (fun s -> {recursive = false; path_spec = MlPath s}) (List.rev !ml_includes)
 
 (* Initialises the Ocaml toplevel before launching it, so that it can
    find the "include" file in the *source* directory *)
 let init_ocaml_path () =
+  let open Mltop in
+  let lp s = { recursive = false; path_spec = MlPath s } in
   let add_subdir dl =
-    Mltop.add_ml_dir (List.fold_left (/) Envars.coqroot [dl])
+    Mltop.add_coq_path (lp (List.fold_left (/) Envars.coqroot [dl]))
   in
-    Mltop.add_ml_dir (Envars.coqlib ());
+    Mltop.add_coq_path (lp (Envars.coqlib ()));
     List.iter add_subdir Coq_config.all_src_dirs
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index c3fd72754..089847f5d 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.mli
@@ -19,7 +19,5 @@ val push_include : string -> Names.DirPath.t -> bool -> unit
 (** [push_include phys_path log_path implicit] *)
 
 val push_ml_include : string -> unit
-
-val init_load_path : load_init:bool -> unit
-
+val init_load_path : load_init:bool -> Mltop.coq_path list
 val init_ocaml_path : unit -> unit
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index a3a4e20af..9719f60bb 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -489,11 +489,11 @@ exception NoCoqLib
 
 let usage batch =
   begin
-  try
-  Envars.set_coqlib ~fail:(fun x -> raise NoCoqLib);
-  Coqinit.init_load_path ~load_init:!load_init;
-  with NoCoqLib -> usage_no_coqlib ()
+    try Envars.set_coqlib ~fail:(fun x -> raise NoCoqLib)
+    with NoCoqLib -> usage_no_coqlib ()
   end;
+  let lp = Coqinit.init_load_path ~load_init:!load_init in
+  List.iter Mltop.add_coq_path lp;
   if batch then Usage.print_usage_coqc ()
   else begin
     Mltop.load_ml_objects_raw_rex
@@ -776,7 +776,8 @@ let init_toplevel arglist =
       if !print_config then (Envars.print_config stdout Coq_config.all_src_dirs; exit (exitcode ()));
       if !print_tags then (print_style_tags (); exit (exitcode ()));
       if !filter_opts then (print_string (String.concat "\n" extras); exit 0);
-      Coqinit.init_load_path ~load_init:!load_init;
+      let lp = Coqinit.init_load_path ~load_init:!load_init in
+      List.iter Mltop.add_coq_path lp;
       Option.iter Mltop.load_ml_object_raw !toploop;
       let extras = !toploop_init extras in
       if not (CList.is_empty extras) then begin
diff --git a/vernac/mltop.ml b/vernac/mltop.ml
index 00554e3ba..053b9d070 100644
--- a/vernac/mltop.ml
+++ b/vernac/mltop.ml
@@ -184,10 +184,28 @@ let warn_cannot_open_path =
 
 type add_ml = AddNoML | AddTopML | AddRecML
 
-let add_rec_path add_ml ~unix_path ~coq_root ~implicit =
+type vo_path_spec = {
+  unix_path : string;
+  coq_path  : Names.DirPath.t;
+  implicit  : bool;
+  has_ml    : add_ml;
+}
+
+type coq_path_spec =
+  | VoPath of vo_path_spec
+  | MlPath of string
+
+type coq_path = {
+  path_spec: coq_path_spec;
+  recursive: bool;
+}
+
+let add_vo_path ~recursive lp =
+  let unix_path = lp.unix_path in
+  let implicit = lp.implicit in
   if exists_dir unix_path then
-    let dirs = all_subdirs ~unix_path in
-    let prefix = Names.DirPath.repr coq_root in
+    let dirs = if recursive then all_subdirs ~unix_path else [] in
+    let prefix = Names.DirPath.repr lp.coq_path in
     let convert_dirs (lp, cp) =
       try
         let path = List.rev_map convert_string cp @ prefix in
@@ -195,17 +213,23 @@ let add_rec_path add_ml ~unix_path ~coq_root ~implicit =
       with Exit -> None
     in
     let dirs = List.map_filter convert_dirs dirs in
-    let () = match add_ml with
+    let () = match lp.has_ml with
       | AddNoML -> ()
       | AddTopML -> add_ml_dir unix_path
       | AddRecML -> List.iter (fun (lp,_) -> add_ml_dir lp) dirs in
     let add (path, dir) =
       Loadpath.add_load_path path ~implicit dir in
     let () = List.iter add dirs in
-    Loadpath.add_load_path unix_path ~implicit coq_root
+    Loadpath.add_load_path unix_path ~implicit lp.coq_path
   else
     warn_cannot_open_path unix_path
 
+let add_coq_path { recursive; path_spec } = match path_spec with
+  | VoPath lp ->
+    add_vo_path ~recursive lp
+  | MlPath dir ->
+    if recursive then add_rec_ml_dir dir else add_ml_dir dir
+
 (* convertit un nom quelconque en nom de fichier ou de module *)
 let mod_of_name name =
     if Filename.check_suffix name ".cmo" then
diff --git a/vernac/mltop.mli b/vernac/mltop.mli
index 324a66d38..e44a7c243 100644
--- a/vernac/mltop.mli
+++ b/vernac/mltop.mli
@@ -42,14 +42,26 @@ val dir_ml_load : string -> unit
 (** Dynamic interpretation of .ml *)
 val dir_ml_use : string -> unit
 
-(** Adds a path to the ML paths *)
-val add_ml_dir : string -> unit
-val add_rec_ml_dir : string -> unit
-
+(** Adds a path to the Coq and ML paths *)
 type add_ml = AddNoML | AddTopML | AddRecML
 
-(** Adds a path to the Coq and ML paths *)
-val add_rec_path : add_ml -> unix_path:string -> coq_root:Names.DirPath.t -> implicit:bool -> unit
+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 *)
+}
+
+type coq_path_spec =
+  | VoPath of vo_path_spec
+  | MlPath of string
+
+type coq_path = {
+  path_spec: coq_path_spec;
+  recursive: bool;
+}
+
+val add_coq_path : coq_path -> unit
 
 (** List of modules linked to the toplevel *)
 val add_known_module : string -> unit
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 3358951f4..1a02a22a5 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -905,9 +905,11 @@ let expand filename =
   Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) filename
 
 let vernac_add_loadpath implicit pdir ldiropt =
+  let open Mltop in
   let pdir = expand pdir in
   let alias = Option.default Libnames.default_root_prefix ldiropt in
-  Mltop.add_rec_path Mltop.AddTopML ~unix_path:pdir ~coq_root:alias ~implicit
+  add_coq_path { recursive = true;
+                 path_spec = VoPath { unix_path = pdir; coq_path = alias; has_ml = AddTopML; implicit } }
 
 let vernac_remove_loadpath path =
   Loadpath.remove_load_path (expand path)
@@ -915,7 +917,8 @@ let vernac_remove_loadpath path =
   (* Coq syntax for ML or system commands *)
 
 let vernac_add_ml_path isrec path =
-  (if isrec then Mltop.add_rec_ml_dir else Mltop.add_ml_dir) (expand path)
+  let open Mltop in
+  add_coq_path { recursive = isrec; path_spec = MlPath (expand path) }
 
 let vernac_declare_ml_module ~atts l =
   let local = make_locality atts.locality in