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

3 files changed, 72 insertions, 49 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