[coq] Add coqpp preprocessing stanza.

CHANGES.md

@@ -1,3 +1,9 @@
+unreleased
+----------
+
+- [coq] Add `coq.pp` stanza to help with pre-processing of grammar
+  files (#2054, @ejgallego, review by @rgrinberg)
+
 1.9.1 (11/04/2019)
 ------------------
 

doc/coq.rst

@@ -49,6 +49,26 @@ The stanza will build all `.v` files on the given directory. The semantics of fi
   ``coqdep`` and ``coqc`` using Coq's ``-I`` flag; this allows for a Coq
   library to depend on a ML plugin.
 
+Preprocessing with ``coqpp``
+============================
+
+Coq plugin writers usually need to write ``.mlg`` files to extend Coq
+grammar. Such files are pre-processed with `coqpp`; to help plugin
+writers avoid boilerplate we provide a `(coqpp ...)` stanza:
+
+.. code:: scheme
+
+    (coq.pp (modules <mlg_list>))
+
+which for each ``g_mod`` in ``<mlg_list>```is equivalent to:
+
+.. code:: scheme
+
+    (rule
+     (targets g_mod.ml)
+     (deps (:mlg-file g_mod.mlg))
+     (action (run coqpp %{mlg-file})))
+
 Recursive Qualification of Modules
 ==================================
 

src/coq_rules.ml

@@ -211,3 +211,17 @@ let install_rules ~sctx ~dir s =
       let dst = Path.to_string dst in
       None, Install.(Entry.make Section.Lib_root ~dst vofile))
     |> List.rev_append (coq_plugins_install_rules ~scope ~package ~dst_dir s)
+
+let coqpp_rules ~sctx ~dir (s : Dune_file.Coqpp.t) =
+
+  let scope = SC.find_scope_by_dir sctx dir in
+  let base_dir = Scope.root scope in
+  let cc = create_ccoq sctx ~dir in
+
+  let mlg_rule m =
+    let source = Path.relative dir (m ^ ".mlg") in
+    let target = Path.relative dir (m ^ ".ml") in
+    let args = Arg_spec.[Dep source; Hidden_targets [target]] in
+    Build.run ~dir:base_dir cc.coqpp args in
+
+  List.map ~f:mlg_rule s.modules

src/coq_rules.mli

@@ -18,3 +18,9 @@ val install_rules
   -> dir:Path.t
   -> Dune_file.Coq.t
   -> (Loc.t option * Install.Entry.t) list
+
+val coqpp_rules
+  :  sctx:Super_context.t
+  -> dir:Path.t
+  -> Dune_file.Coqpp.t
+  -> (unit, Action.t) Build.t list

src/dir_contents.ml

@@ -266,10 +266,8 @@ let load_text_files sctx ft_dir
   let generated_files =
     List.concat_map stanzas ~f:(fun stanza ->
       match (stanza : Stanza.t) with
-      | Coq.T _coq ->
-        (* Format.eprintf "[coq] generated_files called at sctx: %a@\n%!" Path.pp (File_tree.Dir.path ft_dir); *)
-        (* FIXME: Need to generate ml files from mlg ? *)
-        []
+      | Coqpp.T { modules; _ } ->
+        List.map modules ~f:(fun m -> m ^ ".ml")
       | Menhir.T menhir ->
         Menhir_rules.targets menhir
       | Rule rule ->

src/dune_file.ml

@@ -1812,6 +1812,25 @@ module Menhir = struct
        })
 end
 
+module Coqpp = struct
+
+  type t =
+    { modules    : string list
+    ; loc        : Loc.t
+    }
+
+  let decode =
+    record
+      (let+ modules = field "modules" (list string)
+       and+ loc = loc in
+       { modules
+       ; loc
+       })
+
+  type Stanza.t += T of t
+
+end
+
 module Coq = struct
 
   type t =
@@ -1867,8 +1886,11 @@ module Coq = struct
 
   let unit_to_sexp () = Sexp.List []
 
+  let coqlib_p = "coqlib", decode >>| fun x -> [T x]
+  let coqpp_p = "coq.pp", Coqpp.(decode >>| fun x -> [T x])
+
   let unit_stanzas =
-    let+ r = return ["coqlib", decode >>| fun x -> [T x]] in
+    let+ r = return [coqlib_p; coqpp_p] in
     ((), r)
 
   let key =

src/dune_file.mli

@@ -372,6 +372,16 @@ module Coq : sig
   type Stanza.t += T of t
 end
 
+module Coqpp : sig
+
+  type t =
+    { modules    : string list
+    ; loc        : Loc.t
+    }
+
+  type Stanza.t += T of t
+end
+
 module Alias_conf : sig
   type t =
     { name    : string

src/gen_rules.ml

@@ -188,6 +188,10 @@ module Gen(P : sig val sctx : Super_context.t end) = struct
         let dir = ctx_dir in
         let coq_rules = Coq_rules.setup_rules ~sctx ~dir ~dir_contents m in
         SC.add_rules ~dir:ctx_dir sctx coq_rules
+      | Coqpp.T m ->
+        let dir = ctx_dir in
+        let coqpp_rules = Coq_rules.coqpp_rules ~sctx ~dir m in
+        SC.add_rules ~dir:ctx_dir sctx coqpp_rules
       | _ -> ());
     let dyn_deps =
       let pred =

src/stdune/path.ml

@@ -873,8 +873,8 @@ let readdir_unsorted =
       Exn.protect
         ~f:(fun () ->
           match loop dh [] with
-          | exception (Unix.Unix_error (e, _, _)) -> Error e 
-          | s -> Ok s)
+          | exception (Unix.Unix_error (e, _, _)) -> Error e
+          | s -> Result.Ok s)
         ~finally:(fun () -> Unix.closedir dh)
     with
       Unix.Unix_error (e, _, _) -> Error e

test/blackbox-tests/test-cases/coq/ml_lib/src/dune

@@ -1,4 +1,7 @@
 (library
  (public_name ml_lib.ml_plugin)
  (name ml_plugin)
+ (flags :standard -rectypes)
  (libraries coq.plugins.ltac))
+
+(coq.pp (modules gram))

test/blackbox-tests/test-cases/coq/ml_lib/src/gram.mlg

@@ -0,0 +1,9 @@
+DECLARE PLUGIN "gram"
+
+{
+
+(* We don't use any coqpp specific macros as to make the test more
+   resilient on different Coq versions *)
+let foo = 3
+
+}

test/blackbox-tests/test-cases/coq/ml_lib/src/gram.mli

@@ -0,0 +1 @@
+val foo : int

test/blackbox-tests/test-cases/coq/run.t

@@ -18,12 +18,18 @@
 
   $ dune build --root ml_lib --display short --debug-dependency-path @all
   Entering directory 'ml_lib'
+         coqpp src/gram.ml
+      ocamldep src/.ml_plugin.objs/gram.ml.d
         ocamlc src/.ml_plugin.objs/byte/ml_plugin.{cmi,cmo,cmt}
       ocamlopt src/.ml_plugin.objs/native/ml_plugin.{cmx,o}
+      ocamldep src/.ml_plugin.objs/gram.mli.d
+        ocamlc src/.ml_plugin.objs/byte/ml_plugin__Gram.{cmi,cmti}
+        ocamlc src/.ml_plugin.objs/byte/ml_plugin__Gram.{cmo,cmt}
       ocamldep src/.ml_plugin.objs/simple.ml.d
         ocamlc src/.ml_plugin.objs/byte/ml_plugin__Simple.{cmi,cmo,cmt}
         ocamlc src/ml_plugin.cma
         coqdep theories/a.v.d
+      ocamlopt src/.ml_plugin.objs/native/ml_plugin__Gram.{cmx,o}
       ocamlopt src/.ml_plugin.objs/native/ml_plugin__Simple.{cmx,o}
       ocamlopt src/ml_plugin.{a,cmxa}
       ocamlopt src/ml_plugin.cmxs