Merge PR #11618: [loadpath] Rework and simplify ML loadpath handling

Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: herbelin
Reviewed-by: maximedenes

8 files changed, 59 insertions, 91 deletions

diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 8486de3aed..37b584f8d9 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -912,10 +912,11 @@ GRAMMAR EXTEND Gram
       | IDENT "Locate"; l = locatable -> { VernacLocate l }
 
       (* Managing load paths *)
-      | IDENT "Add"; IDENT "LoadPath"; dir = ne_string; alias = as_dirpath ->
-          { VernacAddLoadPath (false, dir, alias) }
-      | IDENT "Add"; IDENT "Rec"; IDENT "LoadPath"; dir = ne_string;
-          alias = as_dirpath -> { VernacAddLoadPath (true, dir, alias) }
+      | IDENT "Add"; IDENT "LoadPath"; physical_path = ne_string; "as"; logical_path = dirpath ->
+          { VernacAddLoadPath { implicit = false; logical_path; physical_path } }
+      | IDENT "Add"; IDENT "Rec"; IDENT "LoadPath"; physical_path = ne_string; "as"; logical_path = dirpath ->
+          { VernacAddLoadPath { implicit = true; logical_path; physical_path } }
+
       | IDENT "Remove"; IDENT "LoadPath"; dir = ne_string ->
           { VernacRemoveLoadPath dir }
 
@@ -934,9 +935,7 @@ GRAMMAR EXTEND Gram
       | IDENT "Inspect"; n = natural -> { VernacPrint (PrintInspect n) }
 
       | IDENT "Add"; IDENT "ML"; IDENT "Path"; dir = ne_string ->
-          { VernacAddMLPath (false, dir) }
-      | IDENT "Add"; IDENT "Rec"; IDENT "ML"; IDENT "Path"; dir = ne_string ->
-          { VernacAddMLPath (true, dir) }
+          { VernacAddMLPath dir }
 
       (* For acting on parameter tables *)
       | "Set"; table = option_table; v = option_setting ->
@@ -1070,9 +1069,6 @@ GRAMMAR EXTEND Gram
   option_table:
     [ [ fl = LIST1 [ x = IDENT -> { x } ] -> { fl } ]]
   ;
-  as_dirpath:
-    [ [ d = OPT [ "as"; d = dirpath -> { d } ] -> { d } ] ]
-  ;
   ne_in_or_out_modules:
     [ [ IDENT "inside"; l = LIST1 global -> { SearchInside l }
       | IDENT "outside"; l = LIST1 global -> { SearchOutside l } ] ]
diff --git a/vernac/loadpath.ml b/vernac/loadpath.ml
index 506b3bc505..38aa42c349 100644
--- a/vernac/loadpath.ml
+++ b/vernac/loadpath.ml
@@ -218,24 +218,18 @@ let try_locate_absolute_library dir =
 
 (** { 5 Extending the load path } *)
 
-(* Adds a path to the Coq and ML paths *)
-type add_ml = AddNoML | AddTopML | AddRecML
-
-type vo_path_spec = {
-  unix_path : string;  (* Filesystem path containing 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 =
-  | VoPath of vo_path_spec
-  | MlPath of string
-
-type coq_path = {
-  path_spec: coq_path_spec;
-  recursive: bool;
-}
+type vo_path =
+  { unix_path : string
+  (** Filesystem path containing 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    : bool
+  (** If [has_ml] is true, the directory will also be added to the ml include path *)
+  ; recursive : bool
+  (** [recursive] will determine whether we explore sub-directories  *)
+  }
 
 let warn_cannot_open_path =
   CWarnings.create ~name:"cannot-open-path" ~category:"filesystem"
@@ -255,9 +249,10 @@ let convert_string d =
     warn_cannot_use_directory d;
     raise Exit
 
-let add_vo_path ~recursive lp =
+let add_vo_path lp =
   let unix_path = lp.unix_path in
   let implicit = lp.implicit in
+  let recursive = lp.recursive in
   if System.exists_dir unix_path then
     let dirs = if recursive then System.all_subdirs ~unix_path else [] in
     let prefix = DP.repr lp.coq_path in
@@ -268,22 +263,17 @@ let add_vo_path ~recursive lp =
       with Exit -> None
     in
     let dirs = List.map_filter convert_dirs dirs in
-    let add_ml_dir = Mltop.add_ml_dir ~recursive:false in
-    let () = match lp.has_ml with
-      | AddNoML -> ()
-      | AddTopML ->
-        Mltop.add_ml_dir ~recursive:false unix_path
-      | AddRecML ->
-        List.iter (fun (lp,_) -> add_ml_dir lp) dirs;
-        add_ml_dir unix_path in
+    let () =
+      if lp.has_ml && not lp.recursive then
+        Mltop.add_ml_dir unix_path
+      else if lp.has_ml && lp.recursive then
+        (List.iter (fun (lp,_) -> Mltop.add_ml_dir lp) dirs;
+         Mltop.add_ml_dir unix_path)
+      else
+        ()
+    in
     let add (path, dir) = add_load_path path ~implicit dir in
     let () = List.iter add dirs in
     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 ->
-    Mltop.add_ml_dir ~recursive dir
diff --git a/vernac/loadpath.mli b/vernac/loadpath.mli
index 47d2d34125..68212b9a47 100644
--- a/vernac/loadpath.mli
+++ b/vernac/loadpath.mli
@@ -64,26 +64,17 @@ val try_locate_absolute_library : DirPath.t -> string
 (** {6 Extending the Load Path } *)
 
 (** Adds a path to the Coq and ML paths *)
-type add_ml = AddNoML | AddTopML | AddRecML
-
-type vo_path_spec = {
-  unix_path : string;
+type vo_path =
+  { unix_path : string
   (** Filesystem path containing vo/ml files *)
-  coq_path  : Names.DirPath.t;
+  ; coq_path  : DirPath.t
   (** Coq prefix for the path *)
-  implicit  : bool;
+  ; 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;
-}
+  ; has_ml    : bool
+  (** If [has_ml] is true, the directory will also be added to the ml include path *)
+  ; recursive : bool
+  (** [recursive] will determine whether we explore sub-directories  *)
+  }
 
-val add_coq_path : coq_path -> unit
+val add_vo_path : vo_path -> unit
diff --git a/vernac/mltop.ml b/vernac/mltop.ml
index 5046248e11..671dae7876 100644
--- a/vernac/mltop.ml
+++ b/vernac/mltop.ml
@@ -128,11 +128,6 @@ let add_ml_dir s =
     | WithoutTop when has_dynlink -> keep_copy_mlpath s
     | _ -> ()
 
-(* For Rec Add ML Path (-R) *)
-let add_ml_dir ~recursive unix_path =
-  let dirs = if recursive then (all_subdirs ~unix_path) else [unix_path,[]] in
-  List.iter (fun (lp,_) -> add_ml_dir lp) dirs
-
 (* 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 271772d7ba..633a5c241d 100644
--- a/vernac/mltop.mli
+++ b/vernac/mltop.mli
@@ -32,7 +32,7 @@ val ocaml_toploop : unit -> unit
 (** {5 ML Dynlink} *)
 
 (** Adds a dir to the plugin search path *)
-val add_ml_dir : recursive:bool -> string -> unit
+val add_ml_dir : string -> unit
 
 (** Tests if we can load ML files *)
 val has_dynlink : bool
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 314c423f65..33d9e3d98a 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -1016,22 +1016,18 @@ let string_of_definition_object_kind = let open Decls in function
         return (keyword "Existential" ++ spc () ++ int i ++ pr_lconstrarg c)
 
       (* Auxiliary file and library management *)
-      | VernacAddLoadPath (fl,s,d) ->
+      | VernacAddLoadPath { implicit; physical_path; logical_path } ->
         return (
           hov 2
             (keyword "Add" ++
-               (if fl then spc () ++ keyword "Rec" ++ spc () else spc()) ++
-               keyword "LoadPath" ++ spc() ++ qs s ++
-               (match d with
-                 | None -> mt()
-                 | Some dir -> spc() ++ keyword "as" ++ spc() ++ DirPath.print dir))
-        )
+             (if implicit then spc () ++ keyword "Rec" ++ spc () else spc()) ++
+             keyword "LoadPath" ++ spc() ++ qs physical_path ++
+             spc() ++ keyword "as" ++ spc() ++ DirPath.print logical_path))
       | VernacRemoveLoadPath s ->
         return (keyword "Remove LoadPath" ++ qs s)
-      | VernacAddMLPath (fl,s) ->
+      | VernacAddMLPath (s) ->
         return (
           keyword "Add"
-          ++ (if fl then spc () ++ keyword "Rec" ++ spc () else spc())
           ++ keyword "ML Path"
           ++ qs s
         )
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 2eb1aa39b0..3cf4b4a89d 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1120,20 +1120,17 @@ let vernac_set_used_variables ~pstate e : Proof_global.t =
 let expand filename =
   Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) filename
 
-let vernac_add_loadpath implicit pdir ldiropt =
+let vernac_add_loadpath ~implicit pdir coq_path =
   let open Loadpath in
   let pdir = expand pdir in
-  let alias = Option.default Libnames.default_root_prefix ldiropt in
-  add_coq_path { recursive = true;
-                 path_spec = VoPath { unix_path = pdir; coq_path = alias; has_ml = AddTopML; implicit } }
+  add_vo_path { unix_path = pdir; coq_path; has_ml = true; implicit; recursive = true }
 
 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 =
-  let open Loadpath in
-  add_coq_path { recursive = isrec; path_spec = MlPath (expand path) }
+let vernac_add_ml_path path =
+  Mltop.add_ml_dir (expand path)
 
 let vernac_declare_ml_module ~local l =
   let local = Option.default false local in
@@ -2106,18 +2103,18 @@ let translate_vernac ~atts v = let open Vernacextend in match v with
         unsupported_attributes atts;
         vernac_solve_existential ~pstate n c)
   (* Auxiliary file and library management *)
-  | VernacAddLoadPath (isrec,s,alias) ->
+  | VernacAddLoadPath { implicit; physical_path; logical_path } ->
     VtDefault(fun () ->
         unsupported_attributes atts;
-        vernac_add_loadpath isrec s alias)
+        vernac_add_loadpath ~implicit physical_path logical_path)
   | VernacRemoveLoadPath s ->
     VtDefault(fun () ->
         unsupported_attributes atts;
         vernac_remove_loadpath s)
-  | VernacAddMLPath (isrec,s) ->
+  | VernacAddMLPath (s) ->
     VtDefault(fun () ->
         unsupported_attributes atts;
-        vernac_add_ml_path isrec s)
+        vernac_add_ml_path s)
   | VernacDeclareMLModule l ->
     VtDefault(fun () -> with_locality ~atts vernac_declare_ml_module l)
   | VernacChdir s ->
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 45018a246c..22aaab2a68 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -98,7 +98,6 @@ type search_restriction =
   | SearchInside of qualid list
   | SearchOutside of qualid list
 
-type rec_flag       = bool (* true = Rec;           false = NoRec          *)
 type verbose_flag   = bool (* true = Verbose;       false = Silent         *)
 type coercion_flag  = bool (* true = AddCoercion    false = NoCoercion     *)
 type instance_flag  = bool option
@@ -363,9 +362,13 @@ type nonrec vernac_expr =
   | VernacSolveExistential of int * constr_expr
 
   (* Auxiliary file and library management *)
-  | VernacAddLoadPath of rec_flag * string * DirPath.t option
+  | VernacAddLoadPath of { implicit : bool
+                         ; physical_path : CUnix.physical_path
+                         ; logical_path : DirPath.t
+                         }
+
   | VernacRemoveLoadPath of string
-  | VernacAddMLPath of rec_flag * string
+  | VernacAddMLPath of string
   | VernacDeclareMLModule of string list
   | VernacChdir of string option