refactor: simplify FacetConifg and build monads ala #107

closes #107

Author: tydeu

Diff for: Lake/Build.lean

@@ -6,4 +6,6 @@ Authors: Mac Malone
 import Lake.Build.Monad
 import Lake.Build.Actions
 import Lake.Build.IndexTargets
+import Lake.Build.Module
+import Lake.Build.Package
 import Lake.Build.Imports

Diff for: Lake/Build/Context.lean

@@ -9,6 +9,8 @@ import Lake.Util.Error
 import Lake.Util.OptionIO
 import Lake.Config.Context
 import Lake.Build.Trace
+import Lake.Build.Store
+import Lake.Build.Topological
 
 open System
 namespace Lake
@@ -29,9 +31,18 @@ abbrev BuildT := ReaderT BuildContext
 /-- The monad for the Lake build manager. -/
 abbrev SchedulerM := BuildT <| LogT BaseIO
 
-/-- The monad for Lake builds. -/
+/-- The core monad for Lake builds. -/
 abbrev BuildM := BuildT <| MonadLogT BaseIO OptionIO
 
+/-- A transformer to equip a monad with a Lake build store. -/
+abbrev BuildStoreT := StateT BuildStore
+
+/-- A transformer for monads that may encounter a build cycle. -/
+abbrev BuildCycleT := CycleT BuildKey
+
+/-- A recursive build of a Lake build store that may encounter a cycle. -/
+abbrev RecBuildM := BuildCycleT <| BuildStoreT BuildM
+
 instance : MonadError BuildM := ⟨MonadLog.error⟩
 instance : MonadLift IO BuildM := ⟨MonadError.runIO⟩
 

Diff for: Lake/Build/Facets.lean

@@ -11,7 +11,7 @@ import Lake.Build.TargetTypes
 
 This module declares most of the builtin facets an targets and
 their build data builtin facets and targets. Some of these definitions
-are needed for  configurations, so we define them here before we need to
+are needed for configurations, so we define them here before we need to
 import said configurations for `BuildInfo`.
 -/
 
@@ -33,62 +33,59 @@ instance (facet : ModuleFacet α) : FamilyDef ModuleData facet.name α :=
 instance [FamilyDef ModuleData facet α] : CoeDep Name facet (ModuleFacet α) :=
   ⟨facet, family_key_eq_type⟩
 
-namespace Module
-abbrev leanBinFacet  := `lean.bin
-abbrev oleanFacet    := `olean
-abbrev ileanFacet    := `ilean
-abbrev cFacet        := `lean.c
-abbrev oFacet        := `lean.o
-abbrev dynlibFacet   := `dynlib
-end Module
-
 /--
 The core compilation / elaboration of the Lean file via `lean`,
 which produce the Lean binaries of the module (i.e., `olean` and `ilean`).
 It is thus the facet used by default for building imports of a module.
 Also, if the module is not lean-only, it produces `c` files as well.
 -/
+abbrev Module.leanBinFacet  := `lean.bin
 module_data lean.bin : ActiveOpaqueTarget
 
 /-- The `olean` file produced by `lean`  -/
+abbrev Module.oleanFacet  := `olean
 module_data olean : ActiveFileTarget
 
 /-- The `ilean` file produced by `lean` -/
+abbrev Module.ileanFacet := `ilean
 module_data ilean : ActiveFileTarget
 
 /-- The C file built from the Lean file via `lean` -/
+abbrev Module.cFacet := `lean.c
 module_data lean.c : ActiveFileTarget
 
 /-- The object file built from `lean.c` -/
+abbrev Module.oFacet := `lean.o
 module_data lean.o : ActiveFileTarget
 
 /-- Shared library for `--load-dynlib` -/
+abbrev Module.dynlibFacet := `dynlib
 module_data dynlib : ActiveFileTarget
 
 /-! ## Package Facets -/
 
-/-- The package's `extraDepTarget`. -/
+/-- The package's `extraDepTarget` mixed with its transitive dependencies `extraDepTarget`. -/
+abbrev Package.extraDepFacet := `extraDep
 package_data extraDep : ActiveOpaqueTarget
 
 /-! ## Target Facets -/
 
-abbrev LeanLib.staticFacet := `leanLib.static
-abbrev LeanLib.sharedFacet := `leanLib.shared
-abbrev LeanExe.exeFacet := `leanExe
-abbrev ExternLib.staticFacet := `externLib.static
-abbrev ExternLib.sharedFacet := `externLib.shared
-
 /-- A Lean library's static binary. -/
+abbrev LeanLib.staticFacet := `leanLib.static
 target_data leanLib.static : ActiveFileTarget
 
 /-- A Lean library's shared binary. -/
+abbrev LeanLib.sharedFacet := `leanLib.shared
 target_data leanLib.shared : ActiveFileTarget
 
 /-- A Lean binary executable. -/
+abbrev LeanExe.exeFacet := `leanExe
 target_data leanExe : ActiveFileTarget
 
 /-- A external library's static binary. -/
+abbrev ExternLib.staticFacet := `externLib.static
 target_data externLib.static : ActiveFileTarget
 
 /-- A external library's shared binary. -/
+abbrev ExternLib.sharedFacet := `externLib.shared
 target_data externLib.shared : ActiveFileTarget

Diff for: Lake/Build/Imports.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
 import Lake.Build.Index
-import Lake.Config.Workspace
 
 /-!
 Definitions to support `lake print-paths` builds.

Diff for: Lake/Build/Index.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
 import Lake.Build.Roots
-import Lake.Build.Module
 import Lake.Build.Topological
 import Lake.Util.EStateT
 
@@ -14,146 +13,35 @@ import Lake.Util.EStateT
 The Lake build index is the complete map of Lake build keys to
 Lake build functions, which is used by Lake to build any Lake build info.
 
-This module contains the definitions used to formalize this concept,
-and it leverages the index to perform topologically-based recursive builds.
+This module leverages the index to perform topologically-based recursive builds.
 -/
 
 open Std Lean
 namespace Lake
 
-/-!
-## Facet Build Maps
--/
-
-/-- A map from module facet names to build functions. -/
-abbrev ModuleBuildMap (m : Type → Type v) :=
-  DRBMap Name (cmp := Name.quickCmp) fun k =>
-    Module → IndexBuildFn m → m (ModuleData k)
-
-@[inline] def ModuleBuildMap.empty : ModuleBuildMap m := DRBMap.empty
-
-/-- A map from package facet names to build functions. -/
-abbrev PackageBuildMap (m : Type → Type v) :=
-  DRBMap Name (cmp := Name.quickCmp) fun k =>
-    Package → IndexBuildFn m → m (PackageData k)
-
-@[inline] def PackageBuildMap.empty : PackageBuildMap m := DRBMap.empty
-
-/-- A map from target facet names to build functions. -/
-abbrev TargetBuildMap (m : Type → Type v) :=
-  DRBMap Name (cmp := Name.quickCmp) fun k =>
-    Package → IndexBuildFn m → m (PackageData k)
-
-@[inline] def TargetBuildMap.empty : PackageBuildMap m := DRBMap.empty
-
-/-!
-## Build Function Constructor Helpers
--/
-
-/--
-Converts a conveniently typed module facet build function into its
-dynamically typed equivalent.
--/
-@[inline] def mkModuleFacetBuild {facet : Name} (build : Module → IndexT m α)
-[h : FamilyDef ModuleData facet α] : Module → IndexT m (ModuleData facet) :=
-  cast (by rw [← h.family_key_eq_type]) build
-
-/--
-Converts a conveniently typed package facet build function into its
-dynamically typed equivalent.
--/
-@[inline] def mkPackageFacetBuild {facet : Name} (build : Package → IndexT m α)
-[h : FamilyDef PackageData facet α] : Package → IndexT m (PackageData facet) :=
-  cast (by rw [← h.family_key_eq_type]) build
-
 /--
 Converts a conveniently typed target facet build function into its
 dynamically typed equivalent.
 -/
-@[inline] def mkTargetFacetBuild (facet : Name) (build : IndexT m α)
-[h : FamilyDef TargetData facet α] : IndexT m (TargetData facet) :=
+@[macroInline] def mkTargetFacetBuild (facet : Name) (build : IndexBuildM α)
+[h : FamilyDef TargetData facet α] : IndexBuildM (TargetData facet) :=
   cast (by rw [← h.family_key_eq_type]) build
 
-section
-variable [Monad m] [MonadLiftT BuildM m] [MonadBuildStore m]
-
-/-!
-## Initial Facet Maps
--/
-
-open Module in
-/--
-A module facet name to build function map that contains builders for
-the initial set of Lake module facets (e.g., `lean.{imports, c, o, dynlib]`).
--/
-@[specialize] def moduleBuildMap : ModuleBuildMap m :=
-  have : MonadLift BuildM m := ⟨liftM⟩
-  ModuleBuildMap.empty (m := m)
-  -- Compute unique imports (direct × transitive)
-  |>.insert importFacet (mkModuleFacetBuild (·.recParseImports))
-  -- Build module (`.olean`, `.ilean`, and possibly `.c`)
-  |>.insert leanBinFacet (mkModuleFacetBuild (·.recBuildLean .leanBin))
-  |>.insert oleanFacet (mkModuleFacetBuild (·.recBuildLean .olean))
-  |>.insert ileanFacet (mkModuleFacetBuild (·.recBuildLean .ilean))
-  |>.insert cFacet (mkModuleFacetBuild (·.recBuildLean .c))
-  -- Build module `.o`
-  |>.insert oFacet (mkModuleFacetBuild <| fun mod => do
-    mod.mkOTarget (Target.active (← mod.c.recBuild)) |>.activate
-  )
-  -- Build shared library for `--load-dynlb`
-  |>.insert dynlibFacet (mkModuleFacetBuild (·.recBuildDynlib))
-
-/--
-A package facet name to build function map that contains builders for
-the initial set of Lake package facets (e.g., `extraDep`).
--/
-@[specialize] def packageBuildMap : PackageBuildMap m :=
-  have : MonadLift BuildM m := ⟨liftM⟩
-  PackageBuildMap.empty (m := m)
-  -- Compute the package's transitive dependencies
-  |>.insert `deps (mkPackageFacetBuild <| fun pkg => do
-    let mut deps := #[]
-    let mut depSet := PackageSet.empty
-    for dep in pkg.deps do
-      for depDep in (← recBuild <| dep.facet `deps) do
-        unless depSet.contains depDep do
-          deps := deps.push depDep
-          depSet := depSet.insert depDep
-      unless depSet.contains dep do
-        deps := deps.push dep
-        depSet := depSet.insert dep
-    return deps
-  )
-  -- Build the `extraDepTarget` for the package and its transitive dependencies
-  |>.insert `extraDep (mkPackageFacetBuild <| fun pkg => do
-    let mut target := ActiveTarget.nil
-    for dep in pkg.deps do
-      target ← target.mixOpaqueAsync (← dep.extraDep.recBuild)
-    target.mixOpaqueAsync <| ← pkg.extraDepTarget.activate
-  )
-
 /-!
 ## Topologically-based Recursive Build Using the Index
 -/
 
 /-- Recursive build function for anything in the Lake build index. -/
-@[specialize] def recBuildIndex (info : BuildInfo) : IndexT m (BuildData info.key) := do
-  have : MonadLift BuildM m := ⟨liftM⟩
+def recBuildWithIndex (info : BuildInfo) : IndexBuildM (BuildData info.key) := do
   match info with
   | .moduleFacet mod facet =>
-    if let some build := moduleBuildMap.find? facet then
-      build mod
-    else if let some config := (← getWorkspace).findModuleFacetConfig? facet then
-      have := config.familyDef
-      mkModuleFacetBuild config.build mod
+    if let some config := (← getWorkspace).findModuleFacetConfig? facet then
+      config.build mod
     else
       error s!"do not know how to build module facet `{facet}`"
   | .packageFacet pkg facet =>
-    if let some build := packageBuildMap.find? facet then
-      build pkg
-    else if let some config := (← getWorkspace).findPackageFacetConfig? facet then
-      have := config.familyDef
-      mkPackageFacetBuild config.build pkg
+    if let some config := (← getWorkspace).findPackageFacetConfig? facet then
+      config.build pkg
     else
       error s!"do not know how to build package facet `{facet}`"
   | .customTarget pkg target =>
@@ -170,7 +58,7 @@ the initial set of Lake package facets (e.g., `extraDep`).
   | .sharedLeanLib lib =>
     mkTargetFacetBuild LeanLib.sharedFacet lib.recBuildShared
   | .leanExe exe =>
-    mkTargetFacetBuild LeanExe.exeFacet exe.recBuild
+    mkTargetFacetBuild LeanExe.exeFacet exe.recBuildExe
   | .staticExternLib lib =>
     mkTargetFacetBuild ExternLib.staticFacet lib.target.activate
   | .sharedExternLib lib =>
@@ -182,31 +70,41 @@ the initial set of Lake package facets (e.g., `extraDep`).
 Recursively build the given info using the Lake build index
 and a topological / suspending scheduler.
 -/
-@[specialize] def buildIndexTop' (info : BuildInfo) : CycleT BuildKey m (BuildData info.key) :=
-  buildDTop BuildData BuildInfo.key recBuildIndex info
+def buildIndexTop' (info : BuildInfo) : RecBuildM (BuildData info.key) :=
+  buildDTop BuildData BuildInfo.key recBuildWithIndex info
 
 /--
 Recursively build the given info using the Lake build index
 and a topological / suspending scheduler and return the dynamic result.
 -/
-@[inline] def buildIndexTop (info : BuildInfo)
-[FamilyDef BuildData info.key α] : CycleT BuildKey m α := do
-  cast (by simp) <| buildIndexTop' (m := m) info
-
-end
+@[macroInline] def buildIndexTop (info : BuildInfo)
+[FamilyDef BuildData info.key α] : RecBuildM α := do
+  cast (by simp) <| buildIndexTop' info
 
 /-- Build the given Lake target using the given Lake build store. -/
-@[inline] def BuildInfo.buildIn (store : BuildStore) (self : BuildInfo)
-[FamilyDef BuildData self.key α] : BuildM α := do
-  failOnBuildCycle <| ← EStateT.run' (m := BuildM) store <| buildIndexTop self
+@[inline] def BuildInfo.buildIn
+(store : BuildStore) (self : BuildInfo) [FamilyDef BuildData self.key α] : BuildM α := do
+  failOnBuildCycle <| ← EStateT.run' store <| buildIndexTop self
 
 /-- Build the given Lake target in a fresh build store. -/
-@[inline] def BuildInfo.build (self : BuildInfo) [FamilyDef BuildData self.key α] : BuildM α :=
+@[macroInline] def BuildInfo.build
+(self : BuildInfo) [FamilyDef BuildData self.key α] : BuildM α :=
   buildIn BuildStore.empty self
 
 export BuildInfo (build buildIn)
 
-/-- An opaque target that builds the Lake target in a fresh build store. -/
+/-! ## Targets Using the Build Index -/
+
+/-- An opaque target that builds the info in a fresh build store. -/
 @[inline] def BuildInfo.target (self : BuildInfo)
 [FamilyDef BuildData self.key (ActiveBuildTarget α)] : OpaqueTarget :=
   BuildTarget.mk' () <| self.build <&> (·.task)
+
+/-- A smart constructor for facet configurations that generate targets. -/
+@[inline] def mkFacetTargetConfig (build : ι → IndexBuildM (ActiveBuildTarget α))
+[h : FamilyDef Fam facet (ActiveBuildTarget α)] : FacetConfig Fam ι facet where
+  build := cast (by rw [← h.family_key_eq_type]) build
+  toTarget? := fun info key_eq_type =>
+    have : FamilyDef BuildData info.key (ActiveBuildTarget α) :=
+      ⟨h.family_key_eq_type ▸ key_eq_type⟩
+    info.target