@[inline, reducible]

abbrev Lake.CallStack (κ : Type u_1) : Type u_1

A sequence of calls donated by the key type κ.

Equations

• Lake.CallStack κ = List κ

@[inline, reducible]

abbrev Lake.Cycle (κ : Type u_1) : Type u_1

A CallStack ending in a cycle.

Equations

• Lake.Cycle κ = Lake.CallStack κ

@[inline, reducible]

abbrev Lake.CycleT (κ : Type u_1) (m : Type u_1 → Type u_2) (α : Type u_1) : Type (max u_1 u_2)

A transformer that equips a monad with a CallStack to detect cycles.

Equations

• Lake.CycleT κ m = ReaderT (Lake.CallStack κ) (ExceptT (Lake.Cycle κ) m)

def Lake.CycleT.readCallStack {m : Type u_1 → Type u_2} {κ : Type u_1} [Pure m] : Lake.CycleT κ m (Lake.CallStack κ)

Read the call stack from a CycleT. this specialized version exists to be used in e.g. BuildM.

Equations

• Lake.CycleT.readCallStack callStack = ExceptT.mk (pure (Except.ok callStack))

@[inline]

def Lake.guardCycle {κ : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_1} [BEq κ] [Monad m] (key : κ) (act : Lake.CycleT κ m α) : Lake.CycleT κ m α

Add key to the monad's CallStack before invoking act. If adding key produces a cycle, the cyclic call stack is thrown.

Equations

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