refactor: Lake.Build.Topological tweaks + docs

Author: tydeu

Diff for: Lake/Build/Context.lean

@@ -31,6 +31,9 @@ abbrev BuildM := BuildT <| MonadLogT BaseIO OptionIO
 /-- A transformer to equip a monad with a Lake build store. -/
 abbrev BuildStoreT := StateT BuildStore
 
+/-- A Lake build cycle. -/
+abbrev BuildCycle := Cycle BuildKey
+
 /-- A transformer for monads that may encounter a build cycle. -/
 abbrev BuildCycleT := CycleT BuildKey
 

Diff for: Lake/Build/Index.lean

@@ -70,7 +70,7 @@ Recursively build the given info using the Lake build index
 and a topological / suspending scheduler.
 -/
 def buildIndexTop' (info : BuildInfo) : RecBuildM (BuildData info.key) :=
-  buildDTop BuildData BuildInfo.key recBuildWithIndex info
+  buildDTop BuildData BuildInfo.key info recBuildWithIndex
 
 /--
 Recursively build the given info using the Lake build index

Diff for: Lake/Build/Monad.lean

@@ -36,7 +36,7 @@ Run the recursive build in the given build store.
 If a cycle is encountered, log it and then fail.
 -/
 @[inline] def RecBuildM.runIn (store : BuildStore) (build : RecBuildM α) : BuildM (α × BuildStore) := do
-  let (res, store) ← EStateT.run store build
+  let (res, store) ← EStateT.run store <| ReaderT.run build []
   return (← failOnBuildCycle res, store)
 
 /--

Diff for: Lake/Build/Topological.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+import Lake.Util.Cycle
 import Lake.Util.Store
 import Lake.Util.EquipT
 
@@ -19,53 +20,116 @@ This is called a suspending scheduler in *Build systems à la carte*.
 open Std
 namespace Lake
 
-/-! ## Abstractions -/
-
-/-- A dependently typed object builder. -/
-abbrev DBuildFn.{u,v,w} (ι : Type u) (β : ι → Type v) (m : Type v → Type w) :=
-  (i : ι) → m (β i)
-
-/-- A dependently typed recursive object builder. -/
-abbrev DRecBuildFn.{u,v,w} (ι : Type u) (β : ι → Type v) (m : Type v → Type w) :=
-  (i : ι) → EquipT (DBuildFn ι β m)  m (β i)
-
-/-- A recursive object builder. -/
-abbrev RecBuildFn ι α m := DRecBuildFn ι (fun _ => α) m
-
-/-- `ExceptT` for build cycles. -/
-abbrev CycleT (κ) :=
-  ExceptT (List κ)
-
-/-! ## Algorithm -/
-
-/-- Auxiliary function for `buildTop`. -/
-@[specialize] partial def buildTopCore [BEq κ] [Monad m] [MonadDStore κ β m]
-(parents : List κ) (keyOf : ι → κ) (build : DRecBuildFn ι (β ∘ keyOf) (CycleT κ m))
-(info : ι) : CycleT κ m (β (keyOf info)) := do
-  let key := keyOf info
-  -- return previous output if already built
-  if let some output ← fetch? key then
-    return output
-  -- detect cyclic builds
-  if parents.contains key then
-    throw <| key :: (parents.partition (· != key)).1 ++ [key]
-  -- build the key recursively
-  let output ← build info <| buildTopCore (key :: parents) keyOf build
-  -- save the output (to prevent repeated builds of the same key)
-  store key output
-  return output
+/-!
+## Recursive Fetching
+
+In this section, we define the primitives that make up a builder.
+-/
+
+/--
+A dependently typed monadic *fetch* function.
+
+That is, a function within the monad `m` and takes an input `a : α`
+describing what to fetch and and produces some output `b : β a` (dependently
+typed) or `b : B` (not) describing what was fetched. All build functions are
+fetch functions, but not all fetch functions need build something.
+-/
+abbrev DFetchFn (α : Type u) (β : α → Type v) (m : Type v → Type w) :=
+  (a : α) → m (β a)
+
+/-!
+In order to nest builds / fetches within one another,
+we equip the monad `m` with a fetch function of its own.
+-/
+
+/-- A transformer that equips a monad with a `DFetchFn`. -/
+abbrev DFetchT (α : Type u) (β : α → Type v) (m : Type v → Type w) :=
+  EquipT (DFetchFn α β m) m
+
+/-- A `DFetchT` that is not dependently typed. -/
+abbrev FetchT (α : Type u) (β : Type v) (m : Type v → Type w) :=
+  DFetchT α (fun _ => β) m
+
+/-!
+We can then use the such a monad as the basis for a fetch function itself.
+-/
+
+/-
+A `DFetchFn` that utilizes another `DFetchFn` equipped to the monad to
+fetch values. It is thus usually implemented recursively via some variation
+of the `recFetch` function below, hence the "rec" in both names.
+-/
+abbrev DRecFetchFn (α : Type u) (β : α → Type v) (m : Type v → Type w) :=
+  DFetchFn α β (DFetchT α β m)
+
+/-- A `DRecFetchFn` that is not dependently typed. -/
+abbrev RecFetchFn (α : Type u) (β : Type v) (m : Type v → Type w) :=
+  α → FetchT α β m β
+
+/-- A `DFetchFn` that provides its base `DRecFetchFn` with itself. -/
+@[specialize] partial def recFetch
+[(α : Type u) → Nonempty (m α)] (fetch : DRecFetchFn α β m) : DFetchFn α β m :=
+  fun a => fetch a (recFetch fetch)
+
+/-!
+The basic `recFetch` can fail to terminate in a variety of ways,
+it can even cycle (i.e., `a` fetches `b` which fetches `a`). Thus, we
+define the `acyclicRecFetch` below to guard against such cases.
+-/
+
+/--
+A `recFetch` augmented by a `CycleT` to guard against recursive cycles.
+If the set of visited keys is finite, this function should provably terminate.
+
+We use `keyOf` to the derive the unique key of a fetch from its descriptor
+`a : α`. We do this because descriptors may not be comparable and/or contain
+more information than necessary to determine uniqueness.
+-/
+@[inline] partial def acyclicRecFetch [BEq κ] [Monad m]
+(keyOf : α → κ) (fetch : DRecFetchFn α β (CycleT κ m)) : DFetchFn α β (CycleT κ m) :=
+  recFetch fun a recurse =>
+    /-
+    NOTE: We provide the stack directly to `recurse` rather than
+    get it through `ReaderT` to prevent it being overridden by the `fetch`
+    function (and thereby potentially produce a cycle).
+    -/
+    guardCycle (keyOf a) fun stack => fetch a (recurse · stack) stack
+
+/-!
+When building, we usually do not want to build the same thing twice during
+a single build pass. At the same time, separate builds may both wish to fetch
+the same thing. Thus, we need to keep track of past builds and make there
+results avoid to future fetches. This is what `memoizedRecFetch` below does.
+-/
+
+/--
+An `acyclicRecFetch` augmented with a `MonadDStore` to
+memoize fetch results and thus avoid computing the same result twice.
+-/
+@[inline] def memoizedRecFetch [BEq κ] [Monad m] [MonadDStore κ β m]
+(keyOf : α → κ) (fetch : DRecFetchFn α (fun a => β (keyOf a)) (CycleT κ m))
+: DFetchFn α (fun a => β (keyOf a)) (CycleT κ m) :=
+  acyclicRecFetch keyOf fun a recurse =>
+    fetchOrCreate (keyOf a) do fetch a recurse
+
+/-!
+## Building
+
+In this section, we use the abstractions we have just created to define
+the desired topological recursive build function (a.k.a. a suspending scheduler).
+-/
 
 /-- Dependently typed version of `buildTop`. -/
-@[inline] def buildDTop (β) [BEq κ] [Monad m] [MonadDStore κ β m]
-(keyOf : ι → κ) (build : DRecBuildFn ι (β ∘ keyOf) (CycleT κ m))
-(info : ι) : CycleT κ m (β (keyOf info)) :=
-  buildTopCore [] keyOf build info
+@[specialize] def buildDTop (β) [BEq κ] [Monad m] [MonadDStore κ β m]
+(keyOf : α → κ) (a : α) (build : DRecFetchFn α (fun a => β (keyOf a)) (CycleT κ m))
+: ExceptT (Cycle κ) m (β (keyOf a)) :=
+  memoizedRecFetch keyOf build a []
 
 /--
 Recursively fills a `MonadStore` of key-object pairs by
 building objects topologically (ι.e., via a depth-first search with memoization).
 If a cycle is detected, the list of keys traversed is thrown.
 -/
-@[inline] def buildTop [BEq κ] [Monad m] [MonadStore κ α m]
-(keyOf : ι → κ) (build : RecBuildFn ι α (CycleT κ m)) (info : ι) : CycleT κ m α :=
-  buildDTop (fun _ => α) keyOf build info
+@[specialize] def buildTop [BEq κ] [Monad m] [MonadStore κ β m]
+(keyOf : α → κ) (a : α) (build : RecFetchFn α β (CycleT κ m)) : ExceptT (Cycle κ) m β :=
+  memoizedRecFetch (β := fun _ => β) keyOf build a []

Diff for: Lake/Load/Main.lean

@@ -44,7 +44,7 @@ def resolveDeps (ws : Workspace) (pkg : Package) (leanOpts : Options)
     store := fun _ pkg => modify (·.addPackage pkg)
   }
   let (res, ws) ← EStateT.run ws <| deps.mapM fun dep =>
-    buildTop (·.2.name) recResolveDep (pkg, dep)
+    buildTop (·.2.name) (pkg, dep) recResolveDep
   match res with
   | Except.ok deps => return (ws, deps)
   | Except.error cycle => do

Diff for: Lake/Util/Cycle.lean

@@ -0,0 +1,28 @@
+/-
+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 sequence of calls donated by the key type `κ`. -/
+abbrev CallStack κ := List κ
+
+/-- A `CallStack` ending in a cycle. -/
+abbrev Cycle κ := CallStack κ
+
+/-- A transformer that equips a monad with a `CallStack` to detect cycles. -/
+abbrev CycleT κ m := ReaderT (CallStack κ) <| ExceptT (Cycle κ) m
+
+/--
+Add `key` to the monad's `CallStack` before invoking `act`.
+If adding `key` produces a cycle, the cyclic call stack is thrown.
+-/
+@[inline] def guardCycle [BEq κ] [Monad m]
+(key : κ) (act : CycleT κ m α) : CycleT κ m α := do
+  let parents ← read
+  if parents.contains key then
+    throw <| key :: (parents.partition (· != key)).1 ++ [key]
+  else
+    act (key :: parents)

Diff for: Lake/Util/Store.lean

@@ -27,3 +27,12 @@ abbrev MonadStore κ α m := MonadDStore κ (fun _ => α) m
 instance [MonadLift m n] [MonadDStore κ β m] : MonadDStore κ β n where
   fetch? k := liftM (m := m) <| fetch? k
   store k a := liftM (m := m) <| store k a
+
+@[inline] def fetchOrCreate [Monad m]
+(key : κ) [MonadStore1 key α m] (create : m α) : m α := do
+  if let some val ← fetch? key then
+    return val
+  else
+    let val ← create
+    store key val
+    return val