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

Equations

• Lake.Cycle κ = Lake.CallStack κ

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

Equations

• Lake.formatCycle cycle = "\n".intercalate (List.map (fun (x : κ) => toString " " ++ toString x) 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 (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_reducible]

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

Equations

• Lake.instMonadCallStackOfMonadCallStackOf = { getCallStack := Lake.MonadCallStackOf.getCallStack, withCallStack := fun {α : Type ?u.2} => Lake.MonadCallStackOf.withCallStack }

@[instance_reducible]

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

Equations

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

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_reducible]

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

Equations

• Lake.instMonadCycleOfMonadCycleOf = { toMonadCallStack := Lake.instMonadCallStackOfMonadCallStackOf, throwCycle := fun {α : Type ?u.2} => Lake.MonadCycleOf.throwCycle }

@[instance_reducible]

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

Equations

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

@[instance_reducible]

instance Lake.inhabitedOfMonadCycle {κ : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_1} [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_reducible]

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

Equations

• Lake.instMonadCallStackOfCallStackTOfMonad = { getCallStack := read, withCallStack := fun {α : Type ?u.2} (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.

Equations

• Lake.CycleT κ m = Lake.CallStackT κ (ExceptT (Lake.Cycle κ) m)

@[instance_reducible]

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

Equations

• Lake.instMonadCycleOfCycleTOfMonad = { toMonadCallStackOf := Lake.instMonadCallStackOfCallStackTOfMonad, throwCycle := fun {α : Type ?u.2} => throw }

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

Equations

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