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

A state monad that uses an actual mutable reference cell (i.e. an ST.Ref ω σ).

The macro StateRefT σ m α infers ω from m. It should normally be used instead.

Equations

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

Instances For

• Lake.instMonadDStoreStateRefT'DRBMapOfMonadLiftTSTOfMonadOfEqOfCmpWrt
• Lake.instMonadStoreNameStateRefT'NameMapOfMonadLiftTSTOfMonad
• Lake.instMonadStoreStateRefT'RBArrayOfMonadLiftTSTOfMonad
• Lake.instMonadStoreStateRefT'RBMapOfMonadLiftTSTOfMonad
• Lean.Compiler.LCNF.instMonadCodeBindStateRefT'OfSTWorld
• Lean.instMonadAlwaysExceptStateRefT'
• Lean.instMonadMCtxStateRefT'MetavarContextST
• Lean.instMonadRecDepthStateRefT'OfMonad
• Lean.instMonadRuntimeExceptionStateRefT'
• StateRefT'.instAlternativeOfMonad
• StateRefT'.instMonad
• StateRefT'.instMonadExceptOf
• StateRefT'.instMonadFunctor
• StateRefT'.instMonadLift
• StateRefT'.instMonadStateOfOfMonadLiftTST
• instLawfulMonadStateRefT'
• instMonadControlStateRefT'
• instMonadFinallyStateRefT'

Recall that StateRefT is a macro that infers ω from the m.

@[inline]

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

Executes an action from a monad with added state in the underlying monad m. Given an initial state, it returns a value paired with the final state.

The monad m must support ST effects in order to create and mutate reference cells.

Equations

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

@[inline]

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

Executes an action from a monad with added state in the underlying monad m. Given an initial state, it returns a value, discarding the final state.

The monad m must support ST effects in order to create and mutate reference cells.

Equations

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

@[inline]

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

Runs an action from the underlying monad in the monad with state. The state is not modified.

This function is typically implicitly accessed via a MonadLiftT instance as part of automatic lifting.

Equations

• StateRefT'.lift x x✝ = x

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

Equations

• StateRefT'.instMonad = inferInstanceAs (Monad (ReaderT (ST.Ref ω σ) m))

instance StateRefT'.instMonadLift {ω σ : Type} {m : Type → Type} : MonadLift m (StateRefT' ω σ m)

Equations

• StateRefT'.instMonadLift = { monadLift := fun {α : Type} => StateRefT'.lift }

instance StateRefT'.instMonadFunctor {ω : Type} (σ : Type) (m : Type → Type) : MonadFunctor m (StateRefT' ω σ m)

Equations

• StateRefT'.instMonadFunctor σ m = inferInstanceAs (MonadFunctor m (ReaderT (ST.Ref ω σ) m))

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

Equations

• StateRefT'.instAlternativeOfMonad = inferInstanceAs (Alternative (ReaderT (ST.Ref ω σ) m))

@[inline]

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

Retrieves the current value of the monad's mutable state.

This increments the reference count of the state, which may inhibit in-place updates.

Equations

• StateRefT'.get ref = ref.get

@[inline]

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

Replaces the mutable state with a new value.

Equations

• StateRefT'.set s ref = ref.set s

@[inline]

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

Applies a function to the current state that both computes a new state and a value. The new state replaces the current state, and the value is returned.

It is equivalent to a get followed by a set. However, using modifyGet may lead to higher performance because it doesn't add a new reference to the state value. Additional references can inhibit in-place updates of data.

Equations

• StateRefT'.modifyGet f ref = ref.modifyGet f

instance StateRefT'.instMonadStateOfOfMonadLiftTST {ω σ : Type} {m : Type → Type} [MonadLiftT (ST ω) m] : MonadStateOf σ (StateRefT' ω σ m)

Equations

• StateRefT'.instMonadStateOfOfMonadLiftTST = { get := StateRefT'.get, set := StateRefT'.set, modifyGet := fun {α : Type} => StateRefT'.modifyGet }

@[always_inline]

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

Equations

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

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

Equations

• instMonadControlStateRefT' ω σ m = inferInstanceAs (MonadControl m (ReaderT (ST.Ref ω σ) m))

instance instMonadFinallyStateRefT' {m : Type → Type} {ω σ : Type} [MonadFinally m] : MonadFinally (StateRefT' ω σ m)

Equations

• instMonadFinallyStateRefT' = inferInstanceAs (MonadFinally (ReaderT (ST.Ref ω σ) m))