Init.Control.StateRef

def StateRefT' (ω : Type) (σ : Type) (m : Type → Type) (α : Type) :

Type

Equations

StateRefT' ω σ m α = ReaderT (ST.Ref ω σ) m α

@[inline]

def StateRefT'.run {ω : Type} {σ : Type} {m : Type → Type} [inst : Monad m] [inst : MonadLiftT (ST ω) m] {α : Type} (x : StateRefT' ω σ m α) (s : σ) :

m (α × σ)

Equations

StateRefT'.run x s = do let ref ← ST.mkRef s let a ← x ref let s ← ST.Ref.get ref pure (a, s)

source

@[inline]

def StateRefT'.run' {ω : Type} {σ : Type} {m : Type → Type} [inst : Monad m] [inst : MonadLiftT (ST ω) m] {α : Type} (x : StateRefT' ω σ m α) (s : σ) :

m α

Equations

StateRefT'.run' x s = do let discr ← StateRefT'.run x s match discr with | (a, snd) => pure a

source

@[inline]

def StateRefT'.lift {ω : Type} {σ : Type} {m : Type → Type} {α : Type} (x : m α) :

StateRefT' ω σ m α

Equations

StateRefT'.lift x x = x

source

instance StateRefT'.instMonadStateRefT' {ω : Type} {σ : Type} {m : Type → Type} [inst : Monad m] :

Monad (StateRefT' ω σ m)

Equations

StateRefT'.instMonadStateRefT' = inferInstanceAs (Monad (ReaderT (ST.Ref ω σ) fun α => m α))

source

instance StateRefT'.instMonadLiftStateRefT' {ω : Type} {σ : Type} {m : Type → Type} :

MonadLift m (StateRefT' ω σ m)

Equations

StateRefT'.instMonadLiftStateRefT' = { monadLift := fun {α} => StateRefT'.lift }

source

instance StateRefT'.instMonadFunctorStateRefT' {ω : Type} (σ : Type) (m : Type → Type) [inst : Monad m] :

MonadFunctor m (StateRefT' ω σ m)

Equations

StateRefT'.instMonadFunctorStateRefT' σ m = inferInstanceAs (MonadFunctor m (ReaderT (ST.Ref ω σ) fun α => m α))

source

instance StateRefT'.instAlternativeStateRefT' {ω : Type} {σ : Type} {m : Type → Type} [inst : Alternative m] [inst : Monad m] :

Alternative (StateRefT' ω σ m)

Equations

StateRefT'.instAlternativeStateRefT' = inferInstanceAs (Alternative (ReaderT (ST.Ref ω σ) fun α => m α))

source

@[inline]

def StateRefT'.get {ω : Type} {σ : Type} {m : Type → Type} [inst : Monad m] [inst : MonadLiftT (ST ω) m] :

StateRefT' ω σ m σ

Equations

StateRefT'.get ref = ST.Ref.get ref

source

@[inline]

def StateRefT'.set {ω : Type} {σ : Type} {m : Type → Type} [inst : Monad m] [inst : MonadLiftT (ST ω) m] (s : σ) :

StateRefT' ω σ m PUnit

Equations

StateRefT'.set s ref = ST.Ref.set ref s

source

@[inline]

def StateRefT'.modifyGet {ω : Type} {σ : Type} {m : Type → Type} {α : Type} [inst : Monad m] [inst : MonadLiftT (ST ω) m] (f : σ → α × σ) :

StateRefT' ω σ m α

Equations

StateRefT'.modifyGet f ref = ST.Ref.modifyGet ref f

source

instance StateRefT'.instMonadStateOfStateRefT' {ω : Type} {σ : Type} {m : Type → Type} [inst : MonadLiftT (ST ω) m] [inst : Monad m] :

MonadStateOf σ (StateRefT' ω σ m)

Equations

StateRefT'.instMonadStateOfStateRefT' = { get := StateRefT'.get, set := StateRefT'.set, modifyGet := fun {α} => StateRefT'.modifyGet }

source

instance StateRefT'.instMonadExceptOfStateRefT' {ω : Type} {σ : Type} {m : Type → Type} (ε : Type u_1) [inst : MonadExceptOf ε m] :

MonadExceptOf ε (StateRefT' ω σ m)

Equations

StateRefT'.instMonadExceptOfStateRefT' ε = { throw := fun {α} => StateRefT'.lift ∘ throwThe ε, tryCatch := fun {α} x c s => tryCatchThe ε (x s) fun e => c e s }

source

instance instMonadControlStateRefT' (ω : Type) (σ : Type) (m : Type → Type) :

MonadControl m (StateRefT' ω σ m)

Equations

instMonadControlStateRefT' ω σ m = inferInstanceAs (MonadControl m (ReaderT (ST.Ref ω σ) fun α => m α))

source

instance instMonadFinallyStateRefT' {m : Type → Type} {ω : Type} {σ : Type} [inst : MonadFinally m] [inst : Monad m] :

MonadFinally (StateRefT' ω σ m)

Equations

instMonadFinallyStateRefT' = inferInstanceAs (MonadFinally (ReaderT (ST.Ref ω σ) fun α => m α))