Recursive Building

This module defines Lake's top-level build monad, FetchM, used for performing recursive builds. A recursive build is a build function which can fetch the results of other (recursive) builds. This is done using the fetch function defined in this module.

@[reducible, inline]

abbrev Lake.RecBuildM (α : Type) : Type

A recursive build of a Lake build store that may encounter a cycle.

Equations

• Lake.RecBuildM = Lake.CallStackT Lake.BuildKey (StateT Lake.BuildStore Lake.CoreBuildM)

@[inline]

def Lake.RecBuildM.run {α : Type} (stack : Lake.CallStack Lake.BuildKey) (store : Lake.BuildStore) (build : Lake.RecBuildM α) : Lake.CoreBuildM (α × Lake.BuildStore)

Run a recursive build.

Equations

• Lake.RecBuildM.run stack store build = build stack store

@[inline]

def Lake.RecBuildM.run' {α : Type} (build : Lake.RecBuildM α) : Lake.CoreBuildM α

Run a recursive build in a fresh build store.

Equations

• build.run' = (fun (x : α × Lake.BuildStore) => x.fst) <$> Lake.RecBuildM.run ∅ ∅ build

@[specialize #[]]

def Lake.buildCycleError {m : Type u_1 → Type u_2} {α : Type u_1} [Lake.MonadError m] (cycle : Lake.Cycle Lake.BuildKey) : m α

Log build cycle and error.

Equations

• One or more equations did not get rendered due to their size.

instance Lake.instMonadCycleOfBuildKeyRecBuildM : Lake.MonadCycleOf Lake.BuildKey Lake.RecBuildM

Equations

• Lake.instMonadCycleOfBuildKeyRecBuildM = Lake.MonadCycleOf.mk fun {α : Type} => Lake.buildCycleError

@[reducible, inline]

abbrev Lake.IndexBuildFn (m : Type → Type v) : Type v

A build function for any element of the Lake build index.

Equations

• Lake.IndexBuildFn m = ((info : Lake.BuildInfo) → m (Lake.BuildData info.key))

@[reducible, inline]

abbrev Lake.IndexT (m : Type → Type v) (α : Type) : Type v

A transformer to equip a monad with a build function for the Lake index.

Equations

• Lake.IndexT m = Lake.EquipT (Lake.IndexBuildFn m) m

@[reducible, inline]

abbrev Lake.FetchM (α : Type) : Type

The top-level monad for Lake build functions.

Equations

• Lake.FetchM = Lake.IndexT Lake.RecBuildM

@[reducible, inline, deprecated Lake.FetchM]

abbrev Lake.IndexBuildM (α : Type) : Type

The top-level monad for Lake build functions. Renamed FetchM.

Equations

• Lake.IndexBuildM = Lake.FetchM

@[reducible, inline, deprecated Lake.FetchM]

abbrev Lake.BuildM (α : Type) : Type

The old build monad. Uses should generally be replaced by FetchM.

Equations

• Lake.BuildM = Lake.CoreBuildM

@[inline]

def Lake.BuildInfo.fetch {α : Type} (self : Lake.BuildInfo) [Lake.FamilyOut Lake.BuildData self.key α] : Lake.FetchM α

Fetch the result associated with the info using the Lake build index.

Equations

• self.fetch build = cast ⋯ (build self)