[coq] Introduce Coq_scope

This PR is a RFC, as I'm not convinced at all this should be the way
to go before we introduce handling of public Coq theories as to allow
their inter-scope composition.

The current approach to handling Coq theories ─ introduced in ocaml#2053 ─
modified `Scope` and `Lib` adding a new library-like stanza type,
`Coq_theory`.

However, handling of libraries and theories is quite different so the
above approach led to a few spurious code cases.

There are two choices to improve this situation before we introduce
`coq_public_libs`:

- refactor `Scope` a bit more so we don't have to mess with
  `Lib.library_related_stanza`

  That's one option but still seems a bit invasive and messy for `scope.ml`.

- split all Coq-related scope code to `Coq_scope` and handle things
  there. This is what this PR does.

This approach does introduce some code duplication, so it is not clear
if it is indeed a gain w.r.t. current status-quo.

Code duplication could be solved by using some programming
abstractions.

Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>

src/dune/coq_rules.ml

@@ -240,8 +240,9 @@ let setup_rules ~sctx ~build_dir ~dir ~dir_contents (s : Dune_file.Coq.t) =
   let cc = create_ccoq sctx ~dir in
   let name = snd s.name in
   let scope = SC.find_scope_by_dir sctx dir in
+  let coq_scope = SC.find_coq_scope_by_dir sctx dir in
   let lib_db = Scope.libs scope in
-  let coq_lib_db = Scope.coq_libs scope in
+  let coq_lib_db = Coq_scope.libs coq_scope in
   let expander = SC.expander sctx ~dir in
 
   let theory = Coq_lib.DB.resolve coq_lib_db s.name |> Result.ok_exn in

src/dune/coq_scope.ml

@@ -0,0 +1,59 @@
+(* This file is licensed under The MIT License *)
+(* (c) MINES ParisTech 2019                    *)
+(* (c) INRIA 2020                              *)
+(* Written by: Emilio Jesús Gallego Arias *)
+
+open! Stdune
+
+type t = { db : Coq_lib.DB.t }
+
+let libs { db; _ } = db
+
+module DB = struct
+  type scope = t
+
+  type t =
+    { by_dir : scope Path.Source.Map.t
+    ; context : Context_name.t
+    }
+
+  let find_by_dir t (dir : Path.Source.t) =
+    let rec loop d =
+      match Path.Source.Map.find t.by_dir d with
+      | Some s -> s
+      | None -> (
+        match Path.Source.parent d with
+        | Some d -> loop d
+        | None ->
+          Code_error.raise "find_by_dir: invalid directory"
+            [ ("d", Path.Source.to_dyn d); ("dir", Path.Source.to_dyn dir) ] )
+    in
+    loop dir
+
+  let find_by_project t project =
+    Path.Source.Map.find_exn t.by_dir (Dune_project.root project)
+
+  let scopes_by_dir stanzas =
+    let stanzas_by_project_dir =
+      List.map stanzas
+        ~f:(fun ((dir, stanza) : Path.Build.t * Dune_file.Coq.t) ->
+          let project = stanza.project in
+          (Dune_project.root project, (dir, stanza)))
+      |> Path.Source.Map.of_list_multi
+    in
+    Path.Source.Map.map stanzas_by_project_dir ~f:(fun stanza ->
+        let db = Coq_lib.DB.create_from_coqlib_stanzas stanza in
+        { db })
+
+  let create ~context stanzas =
+    let by_dir = scopes_by_dir stanzas in
+    { by_dir; context }
+
+  let find_by_dir t dir =
+    if Path.Build.is_root dir then
+      Code_error.raise "Scope.DB.find_by_dir got an invalid path"
+        [ ("dir", Path.Build.to_dyn dir)
+        ; ("context", Context_name.to_dyn t.context)
+        ];
+    find_by_dir t (Path.Build.drop_build_context_exn dir)
+end

src/dune/coq_scope.mli

@@ -0,0 +1,25 @@
+(* This file is licensed under The MIT License *)
+(* (c) MINES ParisTech 2019                    *)
+(* (c) INRIA 2020                              *)
+(* Written by: Emilio Jesús Gallego Arias *)
+
+open! Stdune
+
+type t
+
+(** Return the library database associated to this scope *)
+val libs : t -> Coq_lib.DB.t
+
+module DB : sig
+  type scope = t
+
+  type t
+
+  val create :
+    context:Context_name.t -> (Path.Build.t * Dune_file.Coq.t) list -> t
+
+  val find_by_dir : t -> Path.Build.t -> scope
+
+  val find_by_project : t -> Dune_project.t -> scope
+end
+with type scope := t

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

@@ -4,7 +4,6 @@ open Import
 type t =
   { project : Dune_project.t
   ; db : Lib.DB.t
-  ; coq_db : Coq_lib.DB.t
   ; root : Path.Build.t
   }
 
@@ -16,8 +15,6 @@ let project t = t.project
 
 let libs t = t.db
 
-let coq_libs t = t.coq_db
-
 module DB = struct
   type scope = t
 
@@ -71,11 +68,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
@@ -119,7 +112,6 @@ 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
@@ -131,16 +123,10 @@ module DB = struct
         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 })
+        Some { project; db; root })
 
   let create ~projects ~context ~installed_libs ~lib_config stanzas =
     let t = Fdecl.create Dyn.Encoder.opaque in

src/dune/scope.mli

@@ -15,8 +15,6 @@ val project : t -> Dune_project.t
 (** Return the library database associated to this scope *)
 val libs : t -> Lib.DB.t
 
-val coq_libs : t -> Coq_lib.DB.t
-
 (** Scope databases *)
 module DB : sig
   type scope = t

src/dune/super_context.ml

@@ -175,6 +175,7 @@ end
 type t =
   { context : Context.t
   ; scopes : Scope.DB.t
+  ; coq_scopes : Coq_scope.DB.t
   ; public_libs : Lib.DB.t
   ; installed_libs : Lib.DB.t
   ; stanzas : Dune_file.Stanzas.t Dir_with_dune.t list
@@ -242,6 +243,8 @@ let installed_libs t = t.installed_libs
 
 let find_scope_by_dir t dir = Scope.DB.find_by_dir t.scopes dir
 
+let find_coq_scope_by_dir t dir = Coq_scope.DB.find_by_dir t.coq_scopes dir
+
 let find_scope_by_project t = Scope.DB.find_by_project t.scopes
 
 let find_project_by_key t = Dune_project.File_key.Map.find_exn t.projects_by_key
@@ -441,15 +444,24 @@ let create ~(context : Context.t) ?host ~projects ~packages ~stanzas
           | Dune_file.External_variant ev -> External_variant ev :: acc
           | Dune_file.Deprecated_library_name d ->
             Deprecated_library_name d :: acc
-          | Dune_file.Coq.T coq_lib ->
+          | _ -> acc)
+    in
+    Scope.DB.create ~projects ~context:context.name ~installed_libs ~lib_config
+      stanzas
+  in
+  let coq_scopes =
+    let stanzas =
+      Dune_load.Dune_file.fold_stanzas stanzas ~init:[]
+        ~f:(fun dune_file stanza acc ->
+          match stanza with
+          | Dune_file.Coq.T theory ->
             let ctx_dir =
               Path.Build.append_source context.build_dir dune_file.dir
             in
-            Coq_theory (ctx_dir, coq_lib) :: acc
+            (ctx_dir, theory) :: acc
           | _ -> acc)
     in
-    Scope.DB.create ~projects ~context:context.name ~installed_libs ~lib_config
-      stanzas
+    Coq_scope.DB.create ~context:context.name stanzas
   in
   let stanzas =
     List.map stanzas ~f:(fun { Dune_load.Dune_file.dir; project; stanzas } ->
@@ -524,6 +536,7 @@ let create ~(context : Context.t) ?host ~projects ~packages ~stanzas
   ; root_expander
   ; host
   ; scopes
+  ; coq_scopes
   ; public_libs
   ; installed_libs
   ; stanzas

src/dune/super_context.mli

@@ -87,6 +87,8 @@ val dump_env : t -> dir:Path.Build.t -> Dune_lang.t list Build.t
 
 val find_scope_by_dir : t -> Path.Build.t -> Scope.t
 
+val find_coq_scope_by_dir : t -> Path.Build.t -> Coq_scope.t
+
 val find_scope_by_project : t -> Dune_project.t -> Scope.t
 
 val find_project_by_key : t -> Dune_project.File_key.t -> Dune_project.t