[coqtop] also handle extraction [.v] files.

Signed-off-by: Rodolphe Lepigre <rodolphe@bedrocksystems.com>

bin/coqtop.ml

@@ -78,17 +78,22 @@ let term =
                 in
                 Action_builder.run deps Eager
               in
-              let theory =
+              let stanza =
                 let name = Dune_rules.Coq_module.name coq_module in
                 Dune_rules.Coq_sources.lookup_module coq_src name
               in
               let* args =
-                match theory with
+                match stanza with
                 | None -> Memo.Build.return [] (* FIXME? *)
-                | Some(theory) ->
+                | Some(stanza) ->
                     let dir = Dune_rules.Coq_module.source coq_module in
-                    Dune_rules.Coq_rules.coqtop_args ~sctx ~dir
-                      ~dir_contents:dc theory coq_module
+                    match stanza with
+                    | `Theory theory ->
+                        Dune_rules.Coq_rules.coqtop_args_theory ~sctx ~dir
+                          ~dir_contents:dc theory coq_module
+                    | `Extraction extr ->
+                        Dune_rules.Coq_rules.coqtop_args_extraction ~sctx ~dir
+                          ~dir_contents:dc extr
               in
               let* (args, _) : string list * Dep.Fact.t Dep.Map.t =
                 let args =

src/dune_rules/coq_rules.ml

@@ -447,7 +447,7 @@ let setup_rules ~sctx ~dir ~dir_contents (s : Theory.t) =
       let { Module_rule.coqc; coqdep } = setup_rule cctx ~source_rule m in
       [ coqc; coqdep ])
 
-let coqtop_args ~sctx ~dir ~dir_contents (s : Theory.t) coq_module =
+let coqtop_args_theory ~sctx ~dir ~dir_contents (s : Theory.t) coq_module =
   let name = snd s.name in
   let scope = SC.find_scope_by_dir sctx dir in
   let coq_lib_db = Scope.coq_libs scope in
@@ -591,3 +591,23 @@ let extraction_rules ~sctx ~dir ~dir_contents (s : Extraction.t) =
   let { Module_rule.coqc; coqdep } = setup_rule cctx ~source_rule coq_module in
   let coqc = Action_builder.With_targets.add coqc ~file_targets:ml_targets in
   [ coqdep; coqc ]
+
+let coqtop_args_extraction ~sctx ~dir ~dir_contents (s : Extraction.t) =
+  let* cctx =
+    let wrapper_name = "DuneExtraction" in
+    let theories_deps =
+      let scope = SC.find_scope_by_dir sctx dir in
+      let coq_lib_db = Scope.coq_libs scope in
+      Resolve.of_result
+        (Coq_lib.DB.requires_for_user_written coq_lib_db s.buildable.theories)
+    in
+    let theory_dirs = Path.Build.Set.empty in
+    Context.create sctx ~coqc_dir:dir ~dir ~wrapper_name ~theories_deps
+      ~theory_dirs s.buildable
+  in
+  let+ coq_module =
+    let+ coq = Dir_contents.coq dir_contents in
+    Coq_sources.extract coq s
+  in
+  let cctx = Context.for_module cctx coq_module in
+  Context.coqc_file_flags cctx

src/dune_rules/coq_rules.mli

@@ -52,11 +52,17 @@ val deps_of :
     Coq_module.t ->
     unit Dune_engine.Action_builder.t
 
-val coqtop_args :
+val coqtop_args_theory :
      sctx:Super_context.t
   -> dir:Path.Build.t
   -> dir_contents:Dir_contents.t
   -> Theory.t
   -> Coq_module.t
   -> 'a Command.Args.t list Memo.Build.t
 
+val coqtop_args_extraction :
+     sctx:Super_context.t
+  -> dir:Path.Build.t
+  -> dir_contents:Dir_contents.t
+  -> Extraction.t
+  -> 'a Command.Args.t list Memo.Build.t

src/dune_rules/coq_sources.ml

@@ -12,7 +12,8 @@ type t =
         (* [directories] is used to compute the include paths for Coq's native
            mode *)
   ; extract : Coq_module.t Loc.Map.t
-  ; rev_map : Coq_stanza.Theory.t Coq_module.Map.t
+  ; rev_map : [ `Theory of Theory.t
+              | `Extraction of Extraction.t ] Coq_module.Map.t
   }
 
 let find_module ~source t =
@@ -60,7 +61,7 @@ let of_dir (d : _ Dir_with_dune.t) ~include_subdirs ~dirs =
   check_no_unqualified include_subdirs;
   let modules = coq_modules_of_files ~dirs in
   List.fold_left d.data ~init:empty ~f:(fun acc -> function
-    | Coq_stanza.Theory.T coq ->
+    | Theory.T coq ->
       let modules =
         Coq_module.eval ~dir:d.ctx_dir coq.modules ~standard:modules
       in
@@ -73,11 +74,11 @@ let of_dir (d : _ Dir_with_dune.t) ~include_subdirs ~dirs =
       in
       let rev_map =
         List.fold_left modules ~init:acc.rev_map ~f:(fun acc m ->
-          Coq_module.Map.add_exn acc (Coq_module.name m) coq)
+          Coq_module.Map.add_exn acc (Coq_module.name m) (`Theory coq))
       in
       { acc with directories; libraries; rev_map }
-    | Coq_stanza.Extraction.T extract ->
-      let loc, prelude = extract.prelude in
+    | Extraction.T extr ->
+      let loc, prelude = extr.prelude in
       let m =
         match
           List.find modules ~f:(fun m ->
@@ -88,8 +89,12 @@ let of_dir (d : _ Dir_with_dune.t) ~include_subdirs ~dirs =
           User_error.raise ~loc
             [ Pp.text "no coq source corresponding to prelude field" ]
       in
-      let extract = Loc.Map.add_exn acc.extract extract.buildable.loc m in
-      { acc with extract }
+      let extract = Loc.Map.add_exn acc.extract extr.buildable.loc m in
+      let rev_map =
+        let name = Coq_module.name m in
+        Coq_module.Map.add_exn acc.rev_map name (`Extraction extr)
+      in
+      { acc with extract; rev_map }
     | _ -> acc)
 
 let lookup_module t name =

src/dune_rules/coq_sources.mli

@@ -2,6 +2,7 @@
 open! Dune_engine
 
 open Stdune
+open Coq_stanza
 
 type t
 
@@ -12,7 +13,7 @@ val library : t -> name:Coq_lib_name.t -> Coq_module.t list
 
 val directories : t -> name:Coq_lib_name.t -> Path.Build.t list
 
-val extract : t -> Coq_stanza.Extraction.t -> Coq_module.t
+val extract : t -> Extraction.t -> Coq_module.t
 
 val of_dir :
      Stanza.t list Dir_with_dune.t
@@ -28,4 +29,4 @@ val find_module :
 val lookup_module :
      t
   -> Coq_module.Name.t
-  -> Coq_stanza.Theory.t option
+  -> [ `Theory of Theory.t | `Extraction of Extraction.t ] option