[toplevel] Move command line path processing to Coqargs

We move the processing of path-related arguments to `Coqargs`, and
following experience from `SerAPI` we stored already-processed
`coq_paths` in the `opts` record.

This has proven to be very convenient as to avoid duplication of code
in the presence of several clients of the `Coqargs` parsing
functionality.

3 files changed, 30 insertions, 33 deletions

diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 15411d55d0..e3b15d1988 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -40,8 +40,8 @@ type coq_cmdopts = {
   load_rcfile : bool;
   rcfile      : string option;
 
-  ml_includes : string list;
-  vo_includes : (string * Names.DirPath.t * bool) list;
+  ml_includes : Mltop.coq_path list;
+  vo_includes : Mltop.coq_path list;
   vo_requires : (string * string option * bool option) list;
   (* None = No Import; Some false = Import; Some true = Export *)
 
@@ -145,11 +145,14 @@ let init_args = {
 (* Functional arguments                                                       *)
 (******************************************************************************)
 let add_ml_include opts s =
-  { opts with ml_includes = s :: opts.ml_includes }
+  Mltop.{ opts with ml_includes = {recursive = false; path_spec = MlPath s} :: opts.ml_includes }
 
-let add_vo_include opts d p implicit =
-  let p = Libnames.dirpath_of_string p in
-  { opts with vo_includes = (d, p, implicit) :: opts.vo_includes }
+let add_vo_include opts unix_path coq_path implicit =
+  let open Mltop in
+  let coq_path = Libnames.dirpath_of_string coq_path in
+  { opts with vo_includes = {
+        recursive = true;
+        path_spec = VoPath { unix_path; coq_path; has_ml = AddNoML; implicit } } :: opts.vo_includes }
 
 let add_vo_require opts d p export =
   { opts with vo_requires = (d, p, export) :: opts.vo_requires }
@@ -597,3 +600,19 @@ let parse_args arglist : coq_cmdopts * string list =
   try
     parse init_args
   with any -> fatal_error any
+
+(******************************************************************************)
+(* Startup LoadPath and Modules                                               *)
+(******************************************************************************)
+(* prelude_data == From Coq Require Export Prelude. *)
+let prelude_data = "Prelude", Some "Coq", Some false
+
+let require_libs opts =
+  if opts.load_init then prelude_data :: opts.vo_requires else opts.vo_requires
+
+let cmdline_load_path opts =
+  List.rev opts.vo_includes @ List.(rev opts.ml_includes)
+
+let build_load_path opts =
+  Coqinit.libs_init_load_path ~load_init:opts.load_init @
+  cmdline_load_path opts
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index b709788dde..a18da9c1e3 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -19,8 +19,8 @@ type coq_cmdopts = {
   load_rcfile : bool;
   rcfile      : string option;
 
-  ml_includes : string list;
-  vo_includes : (string * Names.DirPath.t * bool) list;
+  ml_includes : Mltop.coq_path list;
+  vo_includes : Mltop.coq_path list;
   vo_requires : (string * string option * bool option) list;
 
   (* Fuse these two? Currently, [batch_mode] is only used to
@@ -69,3 +69,6 @@ type coq_cmdopts = {
 
 val parse_args : string list -> coq_cmdopts * string list
 val exitcode : coq_cmdopts -> int
+
+val require_libs : coq_cmdopts -> (string * string option * bool option) list
+val build_load_path : coq_cmdopts -> Mltop.coq_path list
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 66af7f7cdf..2552ca4bf5 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -90,31 +90,6 @@ let load_init_vernaculars opts ~state =
   load_vernacular opts ~state
 
 (******************************************************************************)
-(* Startup LoadPath and Modules                                               *)
-(******************************************************************************)
-(* prelude_data == From Coq Require Export Prelude. *)
-let prelude_data = "Prelude", Some "Coq", Some false
-
-let require_libs opts =
-  if opts.load_init then prelude_data :: opts.vo_requires else opts.vo_requires
-
-let cmdline_load_path opts =
-  let open Mltop in
-  (* loadpaths given by 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 opts.vo_includes) @
-
-  (* additional ml directories, given with option -I *)
-  List.map (fun s -> {recursive = false; path_spec = MlPath s}) (List.rev opts.ml_includes)
-
-let build_load_path opts =
-  Coqinit.libs_init_load_path ~load_init:opts.load_init @
-  cmdline_load_path opts
-
-(******************************************************************************)
 (* Fatal Errors                                                               *)
 (******************************************************************************)