Clean up coq obj handling

All the obj related functions are basically the same. One function + enum is enough to handle everything. Signed-off-by: Rudi Grinberg <me@rgrinberg.com>
ocaml · Aug 21, 2020 · e0b5678 · e0b5678
1 parent fff62cf
commit e0b5678
Show file tree

Hide file tree

Showing 3 changed files with 29 additions and 27 deletions.
diff --git a/src/dune/coq_module.ml b/src/dune/coq_module.ml
@@ -37,21 +37,23 @@ let name x = x.name
 let build_vo_dir ~obj_dir x =
   List.fold_left x.prefix ~init:obj_dir ~f:Path.Build.relative
 
-let dep_file x ~obj_dir =
-  let vo_dir = build_vo_dir ~obj_dir x in
-  Path.Build.relative vo_dir (x.name ^ ".v.d")
-
-let aux_file x ~obj_dir =
-  let vo_dir = build_vo_dir ~obj_dir x in
-  Path.Build.relative vo_dir ("." ^ x.name ^ ".aux")
-
-let glob_file x ~obj_dir =
-  let vo_dir = build_vo_dir ~obj_dir x in
-  Path.Build.relative vo_dir (x.name ^ ".glob")
-
-let obj_file x ~obj_dir =
-  let vo_dir = build_vo_dir ~obj_dir x in
-  Path.Build.relative vo_dir (x.name ^ ".vo")
+type obj =
+  | Dep
+  | Aux
+  | Glob
+  | Obj
+
+let fname_of_obj t obj =
+  match obj with
+  | Dep -> t.name ^ ".v.d"
+  | Aux -> "." ^ t.name ^ ".aux"
+  | Glob -> t.name ^ ".glob"
+  | Obj -> t.name ^ ".vo"
+
+let obj_file t obj ~obj_dir =
+  let vo_dir = build_vo_dir ~obj_dir t in
+  let fname = fname_of_obj t obj in
+  Path.Build.relative vo_dir fname
 
 let to_dyn { source; prefix; name } =
   let open Dyn.Encoder in

diff --git a/src/dune/coq_module.mli b/src/dune/coq_module.mli
@@ -36,13 +36,13 @@ val prefix : t -> string list
 
 val name : t -> Name.t
 
-val dep_file : t -> obj_dir:Path.Build.t -> Path.Build.t
+type obj =
+  | Dep
+  | Aux
+  | Glob
+  | Obj
 
-val aux_file : t -> obj_dir:Path.Build.t -> Path.Build.t
-
-val glob_file : t -> obj_dir:Path.Build.t -> Path.Build.t
-
-val obj_file : t -> obj_dir:Path.Build.t -> Path.Build.t
+val obj_file : t -> obj -> obj_dir:Path.Build.t -> Path.Build.t
 
 val to_dyn : t -> Dyn.t
 

diff --git a/src/dune/coq_rules.ml b/src/dune/coq_rules.ml
@@ -239,7 +239,7 @@ let parse_coqdep ~dir ~(boot_type : Bootstrap.t) ~coq_module
       :: deps )
 
 let deps_of ~dir ~boot_type coq_module =
-  let stdout_to = Coq_module.dep_file ~obj_dir:dir coq_module in
+  let stdout_to = Coq_module.obj_file ~obj_dir:dir coq_module Dep in
   Build.dyn_paths_unit
     (Build.map
        (Build.lines_of (Path.build stdout_to))
@@ -254,7 +254,7 @@ let coqdep_rule (cctx : _ Context.t) ~source_rule ~file_flags coq_module =
     ; Dep (Path.build source)
     ]
   in
-  let stdout_to = Coq_module.dep_file ~obj_dir:cctx.dir coq_module in
+  let stdout_to = Coq_module.obj_file ~obj_dir:cctx.dir coq_module Dep in
   (* Coqdep has to be called in the stanza's directory *)
   let open Build.With_targets.O in
   Build.with_no_targets cctx.mlpack_rule
@@ -264,9 +264,9 @@ let coqdep_rule (cctx : _ Context.t) ~source_rule ~file_flags coq_module =
 let coqc_rule (cctx : _ Context.t) ~file_flags coq_module =
   let source = Coq_module.source coq_module in
   let file_flags =
-    let object_to = Coq_module.obj_file ~obj_dir:cctx.dir coq_module in
-    let aux = Coq_module.aux_file ~obj_dir:cctx.dir coq_module in
-    let glob = Coq_module.glob_file ~obj_dir:cctx.dir coq_module in
+    let object_to = Coq_module.obj_file ~obj_dir:cctx.dir coq_module Obj in
+    let aux = Coq_module.obj_file ~obj_dir:cctx.dir coq_module Aux in
+    let glob = Coq_module.obj_file ~obj_dir:cctx.dir coq_module Glob in
     [ Command.Args.Hidden_targets [ object_to; aux; glob ]
     ; S file_flags
     ; Command.Args.Dep (Path.build source)
@@ -423,7 +423,7 @@ let install_rules ~sctx ~dir s =
            let to_dst f =
              Path.Local.to_string @@ Path.Local.relative dst_dir f
            in
-           let vofile = Coq_module.obj_file ~obj_dir:dir vfile in
+           let vofile = Coq_module.obj_file ~obj_dir:dir vfile Obj in
            let vfile = Coq_module.source vfile in
            let make_entry file =
              ( Some loc