Documentation

Lake.Util.Cycle

@[reducible, inline]
abbrev Lake.CallStack (κ : Type u_1) :
Type u_1

A sequence of calls donated by the key type κ.

Equations
Instances For
    @[reducible, inline]
    abbrev Lake.Cycle (κ : Type u_1) :
    Type u_1

    A CallStack ending in a cycle.

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

      A monad equipped with a call stack.

      Instances
        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.

        Instances
          Equations
          • Lake.instMonadCallStackOfMonadCallStackOf = { getCallStack := Lake.MonadCallStackOf.getCallStack, withCallStack := fun {α : Type ?u.27} => Lake.MonadCallStackOf.withCallStack }
          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] :
          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 :
          Type (max (u + 1) v)

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

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

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

            Instances
              instance Lake.instMonadCycleOfMonadCycleOf {κ : Type u_1} {m : Type u_1 → Type u_2} [Lake.MonadCycleOf κ m] :
              Equations
              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] :
              Equations
              instance Lake.inhabitedOfMonadCycle {κ : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_1} [Lake.MonadCycle κ m] :
              Inhabited (m α)
              Equations
              @[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
              Instances For
                Equations
                @[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
                Instances For
                  instance Lake.instMonadCycleOfCycleTOfMonad {m : Type u_1 → Type u_2} {κ : Type u_1} [Monad m] :
                  Equations
                  @[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.

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