[scope] [coq] Refactoring towards a Coq scope

Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>
ocaml · Feb 21, 2023 · bdf038d · bdf038d
1 parent a8b89bf
commit bdf038d
Showing 1 changed file with 31 additions and 29 deletions.
diff --git a/src/dune_rules/scope.ml b/src/dune_rules/scope.ml
@@ -219,6 +219,33 @@ module DB = struct
 
   module Path_source_map_traversals = Memo.Make_map_traversals (Path.Source.Map)
 
+  let coq_scopes_by_dir db_by_project_dir projects_by_dir public_theories
+      coq_stanzas =
+    let coq_stanzas_by_project_dir =
+      List.map coq_stanzas ~f:(fun (dir, (stanza : Coq_stanza.Theory.t)) ->
+          let project = stanza.project in
+          (Dune_project.root project, (dir, stanza)))
+      |> Path.Source.Map.of_list_multi
+    in
+
+    let public_theories = Lazy.force public_theories in
+    let parent = Some public_theories in
+    let find_db dir = snd (find_by_dir_in_map db_by_project_dir dir) in
+
+    Path.Source.Map.merge projects_by_dir coq_stanzas_by_project_dir
+      ~f:(fun _dir project coq_stanzas ->
+        assert (Option.is_some project);
+        let coq_stanzas = Option.value coq_stanzas ~default:[] in
+        List.map coq_stanzas ~f:(fun (dir, (stanza : Coq_stanza.Theory.t)) ->
+            let entry =
+              match stanza.package with
+              | None -> Coq_lib.DB.Theory dir
+              | Some _ -> Redirect public_theories
+            in
+            (stanza, entry))
+        |> Coq_lib.DB.create_from_coqlib_stanzas ~parent ~find_db
+        |> Option.some)
+
   let scopes_by_dir ~build_dir ~lib_config ~projects ~public_libs
       ~public_theories stanzas coq_stanzas =
     let open Memo.O in
@@ -238,13 +265,6 @@ module DB = struct
           (Dune_project.root project, stanza))
       |> Path.Source.Map.of_list_multi
     in
-    let coq_stanzas_by_project_dir =
-      lazy
-        (List.map coq_stanzas ~f:(fun (dir, (stanza : Coq_stanza.Theory.t)) ->
-             let project = stanza.project in
-             (Dune_project.root project, (dir, stanza)))
-        |> Path.Source.Map.of_list_multi)
-    in
     let+ db_by_project_dir =
       Path.Source.Map.merge projects_by_dir stanzas_by_project_dir
         ~f:(fun _dir project stanzas ->
@@ -259,33 +279,15 @@ module DB = struct
              (project, db))
     in
 
-    let coq_db_by_project_dir =
+    let coq_scopes_by_dir =
       lazy
-        (let public_theories = Lazy.force public_theories in
-         let find_db dir = snd (find_by_dir_in_map db_by_project_dir dir) in
-         Path.Source.Map.merge projects_by_dir
-           (Lazy.force coq_stanzas_by_project_dir)
-           ~f:(fun _dir project coq_stanzas ->
-             assert (Option.is_some project);
-             let stanzas = Option.value coq_stanzas ~default:[] in
-             let entries =
-               List.map stanzas ~f:(fun (dir, (stanza : Coq_stanza.Theory.t)) ->
-                   let entry =
-                     match stanza.package with
-                     | None -> Coq_lib.DB.Theory dir
-                     | Some _ -> Redirect public_theories
-                   in
-                   (stanza, entry))
-             in
-             Some entries)
-         |> Path.Source.Map.map ~f:(fun stanzas ->
-                Coq_lib.DB.create_from_coqlib_stanzas
-                  ~parent:(Some public_theories) ~find_db stanzas))
+        (coq_scopes_by_dir db_by_project_dir projects_by_dir public_theories
+           coq_stanzas)
     in
 
     let coq_db_find dir =
       lazy
-        (let map = Lazy.force coq_db_by_project_dir in
+        (let map = Lazy.force coq_scopes_by_dir in
          Path.Source.Map.find_exn map dir)
     in