[coq] Rework Coq_lib.DB handling as not to interfere with Lib

We make the handling of Coq theories to be independent of `Lib`, which
deals with OCaml libs. This is in preparation for the introduction of
composition with inter-scope public Coq theories.

This is softer alternative to ocaml#3280, at the cost of introducing some
uglier code in `Scope`.

Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>

src/dune/lib.ml

@@ -1683,7 +1683,6 @@ module DB = struct
       | Library of Path.Build.t * Dune_file.Library.t
       | External_variant of Dune_file.External_variant.t
       | Deprecated_library_name of Dune_file.Deprecated_library_name.t
-      | Coq_theory of Path.Build.t * Dune_file.Coq.t
   end
 
   module Found_or_redirect = struct
@@ -1697,8 +1696,7 @@ module DB = struct
     List.iter stanzas ~f:(fun (stanza : Library_related_stanza.t) ->
         match stanza with
         | Library _
-        | Deprecated_library_name _
-        | Coq_theory _ ->
+        | Deprecated_library_name _ ->
           ()
         | External_variant ev -> (
           let loc, virtual_lib = ev.virtual_lib in
@@ -1816,10 +1814,7 @@ module DB = struct
               else
                 [ (name, Found info)
                 ; (Lib_name.of_local conf.name, Redirect p.name)
-                ] )
-          | Coq_theory _ ->
-            (* As of today Coq theories do live in a separate namespace *)
-            [])
+                ] ))
       |> Lib_name.Map.of_list_reducei
            ~f:(fun name (v1 : Found_or_redirect.t) v2 ->
              let res =

src/dune/lib.mli

@@ -185,7 +185,6 @@ module DB : sig
       | Library of Path.Build.t * Dune_file.Library.t
       | External_variant of Dune_file.External_variant.t
       | Deprecated_library_name of Dune_file.Deprecated_library_name.t
-      | Coq_theory of Path.Build.t * Dune_file.Coq.t
   end
 
   (** Create a database from a list of library/variants stanzas *)

src/dune/scope.ml

@@ -71,11 +71,7 @@ module DB = struct
               ; _
               } ->
             Some
-              (Dune_file.Public_lib.name old_public_name, Name new_public_name)
-          | Coq_theory _ ->
-            (* All libraries in Coq are private to a scope for now, we will lift
-               this restriction soon *)
-            None)
+              (Dune_file.Public_lib.name old_public_name, Name new_public_name))
       |> Lib_name.Map.of_list
       |> function
       | Ok x -> x
@@ -105,7 +101,8 @@ module DB = struct
       ~all:(fun () -> Lib_name.Map.keys public_libs)
       ()
 
-  let scopes_by_dir context ~projects ~lib_config ~public_libs stanzas =
+  let scopes_by_dir context ~projects ~lib_config ~public_libs stanzas
+      coq_stanzas =
     let build_context_dir = Context_name.build_dir context in
     let projects_by_dir =
       List.map projects ~f:(fun (project : Dune_project.t) ->
@@ -119,38 +116,47 @@ module DB = struct
             | Library (_, lib) -> lib.project
             | External_variant ev -> ev.project
             | Deprecated_library_name x -> x.project
-            | Coq_theory (_, thr) -> thr.project
           in
           (Dune_project.root project, stanza))
       |> Path.Source.Map.of_list_multi
+      (* val of_list_multi : (key * 'a) list -> 'a list t *)
+    in
+    let coq_stanzas_by_project_dir =
+      List.map coq_stanzas ~f:(fun (dir, t) ->
+          let project = t.Dune_file.Coq.project in
+          (Dune_project.root project, (dir, t)))
+      |> Path.Source.Map.of_list_multi
+    in
+    let stanzas_by_project_dir =
+      Path.Source.Map.merge stanzas_by_project_dir coq_stanzas_by_project_dir
+        ~f:(fun _dir stanzas coq_stanzas ->
+          let stanza = Option.value stanzas ~default:[] in
+          let coq_stanzas = Option.value coq_stanzas ~default:[] in
+          Some (stanza, coq_stanzas))
     in
     Path.Source.Map.merge projects_by_dir stanzas_by_project_dir
       ~f:(fun _dir project stanzas ->
         let project = Option.value_exn project in
-        let stanzas = Option.value stanzas ~default:[] in
+        let stanzas, coq_stanzas = Option.value stanzas ~default:([], []) in
         let db =
           Lib.DB.create_from_stanzas stanzas ~parent:public_libs ~lib_config
         in
-        let coq_stanzas =
-          List.filter_map stanzas ~f:(function
-            | Coq_theory (p, l) -> Some (p, l)
-            | _ -> None)
-        in
         let coq_db = Coq_lib.DB.create_from_coqlib_stanzas coq_stanzas in
         let root =
           Path.Build.append_source build_context_dir (Dune_project.root project)
         in
         Some { project; db; coq_db; root })
 
-  let create ~projects ~context ~installed_libs ~lib_config stanzas =
+  let create ~projects ~context ~installed_libs ~lib_config stanzas coq_stanzas
+      =
     let t = Fdecl.create Dyn.Encoder.opaque in
     let public_libs =
       public_libs t ~stdlib_dir:lib_config.Lib_config.stdlib_dir ~installed_libs
         stanzas
     in
     let by_dir =
       scopes_by_dir context ~projects ~lib_config
-        ~public_libs:(Some public_libs) stanzas
+        ~public_libs:(Some public_libs) stanzas coq_stanzas
     in
     let value = { by_dir; context } in
     Fdecl.set t value;

src/dune/scope.mli

@@ -30,6 +30,7 @@ module DB : sig
     -> installed_libs:Lib.DB.t
     -> lib_config:Lib_config.t
     -> Lib.DB.Library_related_stanza.t list
+    -> (Path.Build.t * Dune_file.Coq.t) list
     -> t * Lib.DB.t
 
   val find_by_dir : t -> Path.Build.t -> scope

src/dune/super_context.ml

@@ -437,19 +437,20 @@ let create ~(context : Context.t) ?host ~projects ~packages ~stanzas
             let ctx_dir =
               Path.Build.append_source context.build_dir dune_file.dir
             in
-            Lib.DB.Library_related_stanza.Library (ctx_dir, lib) :: acc
-          | Dune_file.External_variant ev -> External_variant ev :: acc
+            Left (Lib.DB.Library_related_stanza.Library (ctx_dir, lib)) :: acc
+          | Dune_file.External_variant ev -> Left (External_variant ev) :: acc
           | Dune_file.Deprecated_library_name d ->
-            Deprecated_library_name d :: acc
+            Left (Deprecated_library_name d) :: acc
           | Dune_file.Coq.T coq_lib ->
             let ctx_dir =
               Path.Build.append_source context.build_dir dune_file.dir
             in
-            Coq_theory (ctx_dir, coq_lib) :: acc
+            Right (ctx_dir, coq_lib) :: acc
           | _ -> acc)
     in
+    let stanzas, coq_stanzas = List.partition_map stanzas ~f:Fun.id in
     Scope.DB.create ~projects ~context:context.name ~installed_libs ~lib_config
-      stanzas
+      stanzas coq_stanzas
   in
   let stanzas =
     List.map stanzas ~f:(fun { Dune_load.Dune_file.dir; project; stanzas } ->