refactor: move recurse arg into the monad stack

Author: tydeu

Diff for: Lake/Build/Info.lean

@@ -5,6 +5,7 @@ Authors: Mac Malone
 -/
 import Lake.Build.Data
 import Lake.Config.Module
+import Lake.Util.EquipT
 
 namespace Lake
 
@@ -29,20 +30,21 @@ def BuildInfo.key : (self : BuildInfo) → BuildKey
 | package p f => ⟨p.name, none, f⟩
 | target p t f => ⟨p.name, t, f⟩
 
-/-- A build function for a single element of the Lake build index. -/
+/-- A build function for any element of the Lake build index. -/
 abbrev IndexBuildFn (m : Type → Type v) :=
   -- `DBuildFn BuildInfo (BuildData ·.key) m` with less imports
   (info : BuildInfo) → m (BuildData info.key)
 
-@[inline] def Module.recBuildFacet {m : Type → Type v}
-(mod : Module) (facet : WfName) [DynamicType ModuleData facet α]
-(build : (info : BuildInfo) → m (BuildData info.key)) : m α :=
+/-- A transformer to equip a monad with a build function for the Lake index. -/
+abbrev IndexT (m : Type → Type v) := EquipT (IndexBuildFn m) m
+
+@[inline] def Module.recBuildFacet (mod : Module) (facet : WfName)
+[DynamicType ModuleData facet α] : IndexT m α := fun build =>
   let to_data := by unfold BuildData, BuildInfo.key; simp [eq_dynamic_type]
   cast to_data <| build <| BuildInfo.module mod facet
 
-@[inline] def Package.recBuildFacet {m : Type → Type v}
-(pkg : Package) (facet : WfName) [DynamicType PackageData facet α]
-(build : (info : BuildInfo) → m (BuildData info.key)) : m α :=
+@[inline] def Package.recBuildFacet (pkg : Package) (facet : WfName)
+[DynamicType PackageData facet α] : IndexT m α := fun build =>
   let to_data := by unfold BuildData, BuildInfo.key; simp [eq_dynamic_type]
   cast to_data <| build <| BuildInfo.package pkg facet
 

Diff for: Lake/Build/Module1.lean

@@ -59,11 +59,11 @@ section
 variable [Monad m] [MonadLiftT BuildM m] [MonadBuildStore m]
 
 /-- Build the dynlibs of the imports that want precompilation. -/
-def recBuildPrecompileDynlibs (imports : Array Module)
-(recurse : IndexBuildFn m) : m (Array ActiveFileTarget) := do
+@[specialize] def recBuildPrecompileDynlibs (imports : Array Module)
+: IndexT m (Array ActiveFileTarget) := do
   imports.filterMapM fun imp => do
     if imp.shouldPrecompile then
-      return some <| ← imp.recBuildFacet &`lean.dynlib recurse
+      return some <| ← imp.recBuildFacet &`lean.dynlib
     else
       return none
 
@@ -72,19 +72,19 @@ Recursively build a module and its (transitive, local) imports,
 optionally outputting a `.c` file as well if `c` is set to `true`.
 -/
 @[specialize] def Module.recBuildLean (mod : Module) (c : Bool)
-(recurse : IndexBuildFn m) : m ActiveOpaqueTarget := do
+: IndexT m ActiveOpaqueTarget := do
   have : MonadLift BuildM m := ⟨liftM⟩
-  let extraDepTarget ← mod.pkg.recBuildFacet &`extraDep recurse
-  let (imports, transImports) ← mod.recBuildFacet &`lean.imports recurse
+  let extraDepTarget ← mod.pkg.recBuildFacet &`extraDep
+  let (imports, transImports) ← mod.recBuildFacet &`lean.imports
   let dynlibsTarget ← ActiveTarget.collectArray
-    <| ← recBuildPrecompileDynlibs transImports recurse
+    <| ← recBuildPrecompileDynlibs transImports
   let importTarget ←
     if c then
       ActiveTarget.collectOpaqueArray
-        <| ← imports.mapM (·.recBuildFacet &`lean.c recurse)
+        <| ← imports.mapM (·.recBuildFacet &`lean.c)
     else
       ActiveTarget.collectOpaqueArray
-        <| ← imports.mapM (·.recBuildFacet &`lean recurse)
+        <| ← imports.mapM (·.recBuildFacet &`lean)
   let depTarget := Target.active <| ← extraDepTarget.mixOpaqueAsync
     <| ← dynlibsTarget.mixOpaqueAsync importTarget
   let modTarget ← mod.soloTarget dynlibsTarget.info depTarget c |>.activate
@@ -103,7 +103,7 @@ Recursively parse the Lean files of a module and its imports
 building an `Array` product of its direct and transitive local imports.
 -/
 @[specialize] def Module.recParseImports (mod : Module)
-(recurse : IndexBuildFn m) : m (Array Module × Array Module) := do
+: IndexT m (Array Module × Array Module) := do
   have : MonadLift BuildM m := ⟨liftM⟩
   let contents ← IO.FS.readFile mod.leanFile
   let (imports, _, _) ← Elab.parseImports contents mod.leanFile.toString
@@ -112,7 +112,7 @@ building an `Array` product of its direct and transitive local imports.
   let mut imports := #[]
   let mut transImports := ModuleSet.empty
   for imp in importSet do
-    let (_, impTransImports) ← imp.recBuildFacet &`lean.imports recurse
+    let (_, impTransImports) ← imp.recBuildFacet &`lean.imports
     for imp in impTransImports do
       transImports := transImports.insert imp
     transImports := transImports.insert imp
@@ -123,11 +123,11 @@ building an `Array` product of its direct and transitive local imports.
 Recursively build the shared library of a module (e.g., for `--load-dynlib`).
 -/
 @[specialize] def Module.recBuildDynLib (mod : Module)
-(recurse : IndexBuildFn m) : m ActiveFileTarget := do
+: IndexT m ActiveFileTarget := do
   have : MonadLift BuildM m := ⟨liftM⟩
-  let oTarget ← mod.recBuildFacet &`lean.o recurse
-  let (_, transImports) ← mod.recBuildFacet &`lean.imports recurse
-  let dynlibTargets ← recBuildPrecompileDynlibs transImports recurse
+  let oTarget ← mod.recBuildFacet &`lean.o
+  let (_, transImports) ← mod.recBuildFacet &`lean.imports
+  let dynlibTargets ← recBuildPrecompileDynlibs transImports
   -- TODO: Link in external libraries
   -- let externLibTargets ← mod.pkg.externLibTargets.mapM (·.activate)
   -- let linkTargets := #[oTarget] ++ sharedLibTargets ++ externLibTargets |>.map Target.active

Diff for: Lake/Build/Store.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
 import Lake.Build.Data
-import Lake.Build.Topological
 import Lake.Util.StoreInsts
 
 /-!

Diff for: Lake/Build/Topological.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
 import Lake.Util.Store
+import Lake.Util.EquipT
 
 /-!
 # Topological / Suspending Recursive Builder
@@ -26,7 +27,7 @@ abbrev DBuildFn.{u,v,w} (ι : Type u) (β : ι → Type v) (m : Type v → Type
 
 /-- A dependently typed recursive object builder. -/
 abbrev DRecBuildFn.{u,v,w} (ι : Type u) (β : ι → Type v) (m : Type v → Type w) :=
-  (i : ι) → DBuildFn ι β m → m (β i)
+  (i : ι) → EquipT (DBuildFn ι β m)  m (β i)
 
 /-- A recursive object builder. -/
 abbrev RecBuildFn ι α m := DRecBuildFn ι (fun _ => α) m

Diff for: Lake/Util/EquipT.lean

@@ -0,0 +1,92 @@
+/-
+Copyright (c) 2022 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+namespace Lake
+
+/--
+A monad transformer that equips a monad with a value.
+This is a generalization of `ReaderT` where the value is not
+necessarily directly readable through the monad.
+-/
+def EquipT (ρ : Type u) (m : Type v → Type w) (α : Type v) :=
+  ρ → m α
+
+variable {ρ : Type u} {m : Type v → Type w}
+
+instance {α : Type v} [Inhabited (m α)] : Inhabited (EquipT ρ m α) where
+  default := fun _ => default
+
+namespace EquipT
+
+@[inline] protected
+def run {α : Type v} (self : EquipT ρ m α) (r : ρ) : m α :=
+  self r
+
+@[inline] protected
+def map [Functor m] {α β : Type v} (f : α → β) (self : EquipT ρ m α) : EquipT ρ m β :=
+  fun fetch => Functor.map f (self fetch)
+
+instance [Functor m] : Functor (EquipT ρ m) where
+  map := EquipT.map
+
+@[inline] protected
+def pure [Pure m] {α : Type v} (a : α) : EquipT ρ m α :=
+  fun _ => pure a
+
+instance [Pure m] : Pure (EquipT ρ m) where
+  pure := EquipT.pure
+
+@[inline] protected
+def compose {α₁ α₂ β : Type v} (f : m α₁ → (Unit → m α₂) → m β) (x₁ : EquipT ρ m α₁) (x₂ : Unit → EquipT ρ m α₂) : EquipT ρ m β :=
+  fun fetch => f (x₁ fetch) (fun _ => x₂ () fetch)
+
+@[inline] protected
+def seq [Seq m] {α β : Type v} : EquipT ρ m (α → β) → (Unit → EquipT ρ m α) → EquipT ρ m β :=
+  EquipT.compose Seq.seq
+
+instance [Seq m] : Seq (EquipT ρ m) where
+  seq  := EquipT.seq
+
+instance [Applicative m] : Applicative (EquipT ρ m)  := {}
+
+@[inline] protected
+def bind [Bind m] {α β : Type v} (self : EquipT ρ m α) (f : α → EquipT ρ m β) : EquipT ρ m β :=
+  fun fetch => bind (self fetch) fun a => f a fetch
+
+instance [Bind m] : Bind (EquipT ρ m) where
+  bind := EquipT.bind
+
+instance [Monad m] : Monad (EquipT ρ m) := {}
+
+@[inline] protected
+def lift {α : Type v} (t : m α) : EquipT ρ m α :=
+  fun _ => t
+
+instance : MonadLift m (EquipT ρ m) where
+  monadLift := EquipT.lift
+
+@[inline] protected
+def failure [Alternative m] {α : Type v} : EquipT ρ m α :=
+  fun _ => failure
+
+@[inline] protected
+def orElse [Alternative m] {α : Type v} : EquipT ρ m α → (Unit → EquipT ρ m α) → EquipT ρ m α :=
+  EquipT.compose Alternative.orElse
+
+instance [Alternative m] : Alternative (EquipT ρ m) where
+  failure := EquipT.failure
+  orElse  := EquipT.orElse
+
+@[inline] protected
+def throw {ε : Type v} [MonadExceptOf ε m] {α : Type v} (e : ε) : EquipT ρ m α  :=
+  fun _ => throw e
+
+@[inline] protected
+def tryCatch {ε : Type v} [MonadExceptOf ε m] {α : Type v} (self : EquipT ρ m α) (c : ε → EquipT ρ m α) : EquipT ρ m α :=
+  fun f => tryCatchThe ε (self f) fun e => (c e) f
+
+instance (ε) [MonadExceptOf ε m] : MonadExceptOf ε (EquipT ρ m) where
+  throw    := EquipT.throw
+  tryCatch := EquipT.tryCatch