@[reducible, inline]

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

A sequence of calls donated by the key type κ.

Equations

• Lake.CallStack κ = List κ

@[reducible, inline]

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

A CallStack ending in a cycle.

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 (Lake.CallStack κ)
• withCallStack : {α : Type u} → Lake.CallStack κ → 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 (Lake.CallStack κ)
• withCallStack : {α : Type u} → Lake.CallStack κ → m α → m α

instance Lake.instMonadCallStackOfMonadCallStackOf {κ : Type u_1} {m : Type u_1 → Type u_2} [Lake.MonadCallStackOf κ m] : Lake.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] [Lake.MonadCallStackOf κ m] : Lake.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 (Lake.CallStack κ)
• withCallStack : {α : Type u} → Lake.CallStack κ → m α → m α
• throwCycle : {α : Type u} → Lake.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 (Lake.CallStack κ)
• withCallStack : {α : Type u} → Lake.CallStack κ → m α → m α
• throwCycle : {α : Type u} → Lake.Cycle κ → m α

instance Lake.instMonadCycleOfMonadCycleOf {κ : Type u_1} {m : Type u_1 → Type u_2} [Lake.MonadCycleOf κ m] : Lake.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] [Lake.MonadCycleOf κ m] : Lake.MonadCycleOf κ n

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

Equations

• Lake.inhabitedOfMonadCycle = { default := Lake.throwCycle [] }

@[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.

Equations

• Lake.CallStackT κ m = ReaderT (Lake.CallStack κ) m

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

Equations

• Lake.instMonadCallStackOfCallStackTOfMonad = { getCallStack := read, withCallStack := fun {α : Type ?u.30} (s : Lake.CallStack κ) (x : Lake.CallStackT κ m α) => liftM (x s) }

@[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] : Lake.MonadCycleOf κ (Lake.CycleT κ m)

@[inline]

def Lake.guardCycle {κ : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_1} [BEq κ] [Monad m] [Lake.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.