@[reducible, inline]

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

A sequence of calls donated by the key type κ.

@[reducible, inline]

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

A CallStack ending in a cycle.

def Lake.formatCycle {κ : Type u_1} [ToString κ] (cycle : Cycle κ) : String

class Lake.MonadCallStackOf (κ : semiOutParam (Type u)) (m : Type u → Type v) : Type (max (u + 1) v)

A monad equipped with a call stack.

• getCallStack : m (CallStack κ)
• withCallStack {α : Type u} (stack : CallStack κ) (x : m α) : m α

class Lake.MonadCallStack (κ : outParam (Type u)) (m : Type u → Type v) : Type (max (u + 1) v)

Similar to MonadCallStackOf, but κ is an outParam for convenience.

• getCallStack : m (CallStack κ)
• withCallStack {α : Type u} (stack : CallStack κ) (x : m α) : m α

instance Lake.instMonadCallStackOfMonadCallStackOf {κ : Type u_1} {m : Type u_1 → Type u_2} [MonadCallStackOf κ m] : MonadCallStack κ m

instance Lake.instMonadCallStackOfOfMonadLiftOfMonadFunctor {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {κ : Type u_1} [MonadLift m n] [MonadFunctor m n] [MonadCallStackOf κ m] : MonadCallStackOf κ n

class Lake.MonadCycleOf (κ : semiOutParam (Type u)) (m : Type u → Type v) extends Lake.MonadCallStackOf κ m : Type (max (u + 1) v)

A monad equipped with a call stack and the ability to error on a cycle.

• getCallStack : m (CallStack κ)
• withCallStack {α : Type u} (stack : CallStack κ) (x : m α) : m α
• throwCycle {α : Type u} (cycle : Cycle κ) : m α

class Lake.MonadCycle (κ : outParam (Type u)) (m : Type u → Type v) extends Lake.MonadCallStack κ m : Type (max (u + 1) v)

Similar to MonadCycle, but κ is an outParam for convenience.

• getCallStack : m (CallStack κ)
• withCallStack {α : Type u} (stack : CallStack κ) (x : m α) : m α
• throwCycle {α : Type u} (cycle : Cycle κ) : m α

instance Lake.instMonadCycleOfMonadCycleOf {κ : Type u_1} {m : Type u_1 → Type u_2} [MonadCycleOf κ m] : MonadCycle κ m

instance Lake.instMonadCycleOfOfMonadLiftOfMonadFunctor {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {κ : Type u_1} [MonadLift m n] [MonadFunctor m n] [MonadCycleOf κ m] : MonadCycleOf κ n

instance Lake.inhabitedOfMonadCycle {κ : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_1} [MonadCycle κ m] : Inhabited (m α)

@[reducible, inline]

abbrev Lake.CallStackT (κ : 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.

instance Lake.instMonadCallStackOfCallStackTOfMonad {m : Type u_1 → Type u_2} {κ : Type u_1} [Monad m] : MonadCallStackOf κ (CallStackT κ m)

@[reducible, inline]

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.

instance Lake.instMonadCycleOfCycleTOfMonad {m : Type u_1 → Type u_2} {κ : Type u_1} [Monad m] : MonadCycleOf κ (CycleT κ m)

@[inline]

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

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