Documentation

Init.Control.StateCps

The State monad transformer using CPS style.

def StateCpsT (σ : Type u) (m : Type u → Type v) (α : Type u) :
Type (max (u + 1) v)
Equations
  • StateCpsT σ m α = ((δ : Type u) → σ(ασm δ) → m δ)
Instances For
    @[inline]
    def StateCpsT.runK {β : Type u} {α : Type u} {σ : Type u} {m : Type u → Type v} (x : StateCpsT σ m α) (s : σ) (k : ασm β) :
    m β
    Equations
    Instances For
      @[inline]
      def StateCpsT.run {α : Type u} {σ : Type u} {m : Type u → Type v} [Monad m] (x : StateCpsT σ m α) (s : σ) :
      m (α × σ)
      Equations
      Instances For
        @[inline]
        def StateCpsT.run' {α : Type u} {σ : Type u} {m : Type u → Type v} [Monad m] (x : StateCpsT σ m α) (s : σ) :
        m α
        Equations
        Instances For
          @[always_inline]
          instance StateCpsT.instMonadStateCpsT {σ : Type u_1} {m : Type u_1 → Type u_2} :
          Equations
          • StateCpsT.instMonadStateCpsT = Monad.mk
          @[always_inline]
          instance StateCpsT.instMonadStateOfStateCpsT {σ : Type u_1} {m : Type u_1 → Type u_2} :
          Equations
          • StateCpsT.instMonadStateOfStateCpsT = { get := fun x s k => k s s, set := fun s x x_1 k => k PUnit.unit s, modifyGet := fun {α} f x s k => match f s with | (a, s) => k a s }
          @[inline]
          def StateCpsT.lift {m : Type u_1 → Type u_2} {α : Type u_1} {σ : Type u_1} [Monad m] (x : m α) :
          StateCpsT σ m α
          Equations
          Instances For
            instance StateCpsT.instMonadLiftStateCpsT {m : Type u_1 → Type u_2} {σ : Type u_1} [Monad m] :
            Equations
            • StateCpsT.instMonadLiftStateCpsT = { monadLift := fun {α} => StateCpsT.lift }
            @[simp]
            theorem StateCpsT.runK_pure {α : Type u} {σ : Type u} {β : Type u} {m : Type u → Type v} (a : α) (s : σ) (k : ασm β) :
            StateCpsT.runK (pure a) s k = k a s
            @[simp]
            theorem StateCpsT.runK_get {σ : Type u} {β : Type u} {m : Type u → Type v} (s : σ) (k : σσm β) :
            StateCpsT.runK get s k = k s s
            @[simp]
            theorem StateCpsT.runK_set {σ : Type u} {β : Type u} {m : Type u → Type v} (s : σ) (s' : σ) (k : PUnitσm β) :
            @[simp]
            theorem StateCpsT.runK_modify {σ : Type u} {β : Type u} {m : Type u → Type v} (f : σσ) (s : σ) (k : PUnitσm β) :
            @[simp]
            theorem StateCpsT.runK_lift {m : Type u → Type u_1} {β : Type u} {α : Type u} {σ : Type u} [Monad m] (x : m α) (s : σ) (k : ασm β) :
            StateCpsT.runK (StateCpsT.lift x) s k = do let x ← x k x s
            @[simp]
            theorem StateCpsT.runK_monadLift {m : Type u → Type u_1} {n : Type u → Type u_2} {α : Type u} {β : Type u} {σ : Type u} [Monad m] [MonadLiftT n m] (x : n α) (s : σ) (k : ασm β) :
            StateCpsT.runK (monadLift x) s k = do let x ← monadLift x k x s
            @[simp]
            theorem StateCpsT.runK_bind_pure {m : Type u → Type u_1} {β : Type u} {γ : Type u} {α : Type u} {σ : Type u} [Monad m] (a : α) (f : αStateCpsT σ m β) (s : σ) (k : βσm γ) :
            StateCpsT.runK (pure a >>= f) s k = StateCpsT.runK (f a) s k
            @[simp]
            theorem StateCpsT.runK_bind_lift {m : Type u → Type u_1} {β : Type u} {γ : Type u} {α : Type u} {σ : Type u} [Monad m] (x : m α) (f : αStateCpsT σ m β) (s : σ) (k : βσm γ) :
            StateCpsT.runK (StateCpsT.lift x >>= f) s k = do let a ← x StateCpsT.runK (f a) s k
            @[simp]
            theorem StateCpsT.runK_bind_get {m : Type u → Type u_1} {β : Type u} {γ : Type u} {σ : Type u} [Monad m] (f : σStateCpsT σ m β) (s : σ) (k : βσm γ) :
            StateCpsT.runK (get >>= f) s k = StateCpsT.runK (f s) s k
            @[simp]
            theorem StateCpsT.runK_bind_set {m : Type u → Type u_1} {β : Type u} {γ : Type u} {σ : Type u} [Monad m] (f : PUnitStateCpsT σ m β) (s : σ) (s' : σ) (k : βσm γ) :
            @[simp]
            theorem StateCpsT.runK_bind_modify {m : Type u → Type u_1} {β : Type u} {γ : Type u} {σ : Type u} [Monad m] (f : σσ) (g : PUnitStateCpsT σ m β) (s : σ) (k : βσm γ) :
            @[simp]
            theorem StateCpsT.run_eq {m : Type (max u_1 u_2) → Type u_3} {σ : Type (max u_1 u_2)} {α : Type (max u_1 u_2)} [Monad m] (x : StateCpsT σ m α) (s : σ) :
            StateCpsT.run x s = StateCpsT.runK x s fun a s => pure (a, s)
            @[simp]
            theorem StateCpsT.run'_eq {m : Type u_1 → Type u_2} {σ : Type u_1} {α : Type u_1} [Monad m] (x : StateCpsT σ m α) (s : σ) :
            StateCpsT.run' x s = StateCpsT.runK x s fun a x => pure a