[coq] Implement (modules :standard) for .mlg coqpp preprocessor

Fixes ocaml#2414

doc/dune-files.rst

@@ -1627,13 +1627,21 @@ writers avoid boilerplate we provide a `(coqpp ...)` stanza:
 
 which for each ``g_mod`` in ``<mlg_list>`` is equivalent to:
 
-.. code:: lisp
+.. code:: scheme
 
     (rule
      (targets g_mod.ml)
      (deps (:mlg-file g_mod.mlg))
      (action (run coqpp %{mlg-file})))
 
+``<mlg_list>`` is an :ref:`ordered-set-language` expression, thus you can write:
+
+.. code:: scheme
+
+    (coq.pp (modules :standard \ mod1))
+
+as is usual in the OCaml / Coq ``modules`` field.
+
 .. _dune-workspace:
 
 mdx (since 2.4)

src/dune/coq_rules.ml

@@ -362,12 +362,16 @@ let install_rules ~sctx ~dir s =
                  vofile) ))
     |> List.rev_append coq_plugins_install_rules
 
-let coqpp_rules ~sctx ~build_dir ~dir (s : Dune_file.Coqpp.t) =
+let coqpp_rules ~sctx ~build_dir ~dir ~dir_contents (s : Dune_file.Coqpp.t) =
   let cc = create_ccoq sctx ~dir in
   let mlg_rule m =
     let source = Path.build (Path.Build.relative dir (m ^ ".mlg")) in
     let target = Path.Build.relative dir (m ^ ".ml") in
     let args = [ Command.Args.Dep source; Hidden_targets [ target ] ] in
     Command.run ~dir:(Path.build build_dir) cc.coqpp args
   in
-  List.map ~f:mlg_rule s.modules
+  let parse ~loc:_ m = m in
+  let eq = String.equal in
+  let standard = Coq_sources.mlg (Dir_contents.coq dir_contents) in
+  let modules = Ordered_set_lang.eval s.modules ~parse ~eq ~standard in
+  List.map ~f:mlg_rule modules

src/dune/coq_rules.mli

@@ -24,5 +24,6 @@ val coqpp_rules :
      sctx:Super_context.t
   -> build_dir:Path.Build.t
   -> dir:Path.Build.t
+  -> dir_contents:Dir_contents.t
   -> Dune_file.Coqpp.t
   -> Action.t Build.With_targets.t list

src/dune/coq_sources.ml

@@ -4,9 +4,12 @@ open Stdune
    harmful?
 
    In Coq all libs are "wrapped" so including a module twice is not so bad. *)
-type t = { libraries : Coq_module.t list Coq_lib_name.Map.t }
+type t =
+  { libraries : Coq_module.t list Coq_lib_name.Map.t
+  ; mlgs : string list
+  }
 
-let empty = { libraries = Coq_lib_name.Map.empty }
+let empty = { libraries = Coq_lib_name.Map.empty; mlgs = [] }
 
 let coq_modules_of_files ~dirs =
   let filter_v_files (dir, local, files) =
@@ -34,6 +37,8 @@ let build_coq_modules_map (d : _ Dir_with_dune.t) ~dir ~modules =
 
 let library t ~name = Coq_lib_name.Map.find_exn t.libraries name
 
+let mlg t = t.mlgs
+
 let check_no_unqualified (loc, (qualif_mode : Dune_file.Include_subdirs.t)) =
   if qualif_mode = Include Unqualified then
     User_error.raise ~loc
@@ -44,4 +49,5 @@ let of_dir d ~include_subdirs ~dirs =
   { libraries =
       build_coq_modules_map d ~dir:d.ctx_dir
         ~modules:(coq_modules_of_files ~dirs)
+  ; mlgs = []
   }

src/dune/coq_sources.mli

@@ -8,6 +8,8 @@ val empty : t
 (** Coq modules of library [name] is the Coq library name. *)
 val library : t -> name:Coq_lib_name.t -> Coq_module.t list
 
+val mlg : t -> string list
+
 val of_dir :
      Stanza.t list Dir_with_dune.t
   -> include_subdirs:Loc.t * Dune_file.Include_subdirs.t

src/dune/dir_contents.ml

@@ -129,8 +129,9 @@ end = struct
     let generated_files =
       List.concat_map stanzas ~f:(fun stanza ->
           match (stanza : Stanza.t) with
-          (* XXX What about mli files? *)
-          | Coqpp.T { modules; _ } -> List.map modules ~f:(fun m -> m ^ ".ml")
+          (* XXX What about mli files? EJGA: no mli files are generated by coqpp *)
+          | Coqpp.T { modules = _; _ } ->
+            [] (* List.map modules ~f:(fun m -> m ^ ".ml") *)
           | Menhir.T menhir -> Menhir_rules.targets menhir
           | Rule rule ->
             Simple_rules.user_rule sctx rule ~dir ~expander

src/dune/dune_file.ml

@@ -1962,13 +1962,13 @@ end
 
 module Coqpp = struct
   type t =
-    { modules : string list
+    { modules : Ordered_set_lang.t
     ; loc : Loc.t
     }
 
   let decode =
     fields
-      (let+ modules = field "modules" (repeat string)
+      (let+ modules = modules_field "modules"
        and+ loc = loc in
        { modules; loc })
 

src/dune/dune_file.mli

@@ -371,7 +371,7 @@ end
 
 module Coqpp : sig
   type t =
-    { modules : string list
+    { modules : Ordered_set_lang.t
     ; loc : Loc.t
     }
 

src/dune/gen_rules.ml

@@ -283,7 +283,7 @@ let gen_rules sctx dir_contents cctxs
         Coq_rules.setup_rules ~sctx ~build_dir ~dir:ctx_dir ~dir_contents m
         |> Super_context.add_rules ~dir:ctx_dir sctx
       | Coqpp.T m ->
-        Coq_rules.coqpp_rules ~sctx ~build_dir ~dir:ctx_dir m
+        Coq_rules.coqpp_rules ~sctx ~build_dir ~dir:ctx_dir ~dir_contents m
         |> Super_context.add_rules ~dir:ctx_dir sctx
       | _ -> ());
   define_all_alias ~dir:ctx_dir ~scope ~js_targets;