source
def EST (ε σ : Type) :
Type → Type

A restricted version of `IO` in which mutable state and exceptions are the only side effects.

It is possible to run `EST` computations in a non-monadic context using `runEST`.

Equations

- EST ε σ = EStateM ε σ

Instances For

source
@[reducible, inline]
abbrev ST (σ : Type) :
Type → Type

A restricted version of `IO` in which mutable state is the only side effect.

It is possible to run `ST` computations in a non-monadic context using `runST`.

Equations

- ST σ = EST Empty σ

Instances For

source
instance instMonadEST (ε σ : Type) :
Monad (EST ε σ)
Equations

- instMonadEST ε σ = inferInstanceAs (Monad (EStateM ε σ))

source
instance instMonadExceptOfEST (ε σ : Type) :
MonadExceptOf ε (EST ε σ)
Equations

- instMonadExceptOfEST ε σ = inferInstanceAs (MonadExceptOf ε (EStateM ε σ))

source
instance instInhabitedEST {ε σ α : Type} [Inhabited ε] :
Inhabited (EST ε σ α)
Equations

- instInhabitedEST = inferInstanceAs (Inhabited (EStateM ε σ α))

source
instance instMonadST (σ : Type) :
Monad (ST σ)
Equations

- instMonadST σ = inferInstanceAs (Monad (EST Empty σ))

source
class STWorld (σ : outParam Type) (m : Type → Type) :
Type

An auxiliary class used to infer the “state” of `EST` and `ST` monads.

Instances

source
instance instSTWorldOfMonadLift {σ : Type} {m n : Type → Type} [MonadLift m n] [STWorld σ m] :
STWorld σ n
Equations

- instSTWorldOfMonadLift = { }

source
instance instSTWorldEST {ε σ : Type} :
STWorld σ (EST ε σ)
Equations

- instSTWorldEST = { }

source
@[noinline]
def runEST {ε α : Type} (x : (σ : Type) → EST ε σ α) :
Except ε α

Runs an `EST` computation, in which mutable state and exceptions are the only side effects.

Equations

- runEST x = match x Unit () with | EStateM.Result.ok a a_1 => Except.ok a | EStateM.Result.error ex a => Except.error ex

Instances For

source
@[noinline]
def runST {α : Type} (x : (σ : Type) → ST σ α) :
α

Runs an `ST` computation, in which mutable state via `ST.Ref` is the only side effect.

Equations

- runST x = match x Unit () with | EStateM.Result.ok a a_1 => a | EStateM.Result.error ex a => nomatch ex

Instances For

source
@[always_inline]
instance instMonadLiftSTEST {ε σ : Type} :
MonadLift (ST σ) (EST ε σ)
Equations

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

source
opaque ST.RefPointed :
NonemptyType

References

source
structure ST.Ref (σ α : Type) :
Type

Mutable reference cells that contain values of type `α`. These cells can read from and mutated in the `ST σ` monad.

- ref : RefPointed.type
- h : Nonempty α

Instances For

source
instance ST.instNonemptyRef {σ α : Type} [s : Nonempty α] :
Nonempty (Ref σ α)
source
@[extern lean_st_mk_ref]
opaque ST.Prim.mkRef {σ α : Type} (a : α) :
ST σ (Ref σ α)
source
@[extern lean_st_ref_get]
opaque ST.Prim.Ref.get {σ α : Type} (r : Ref σ α) :
ST σ α
source
@[extern lean_st_ref_set]
opaque ST.Prim.Ref.set {σ α : Type} (r : Ref σ α) (a : α) :
ST σ Unit
source
@[extern lean_st_ref_swap]
opaque ST.Prim.Ref.swap {σ α : Type} (r : Ref σ α) (a : α) :
ST σ α
source
@[extern lean_st_ref_take]
unsafe opaque ST.Prim.Ref.take {σ α : Type} (r : Ref σ α) :
ST σ α
source
@[extern lean_st_ref_ptr_eq]
opaque ST.Prim.Ref.ptrEq {σ α : Type} (r1 r2 : Ref σ α) :
ST σ Bool
source
@[inline]
unsafe def ST.Prim.Ref.modifyUnsafe {σ α : Type} (r : Ref σ α) (f : α → α) :
ST σ Unit
Equations

- ST.Prim.Ref.modifyUnsafe r f = do let v ← ST.Prim.Ref.take r ST.Prim.Ref.set r (f v)

Instances For

source
@[inline]
unsafe def ST.Prim.Ref.modifyGetUnsafe {σ α β : Type} (r : Ref σ α) (f : α → β × α) :
ST σ β
Equations

- ST.Prim.Ref.modifyGetUnsafe r f = do let v ← ST.Prim.Ref.take r match f v with | (b, a) => do ST.Prim.Ref.set r a pure b

Instances For

source
@[implemented_by ST.Prim.Ref.modifyUnsafe]
def ST.Prim.Ref.modify {σ α : Type} (r : Ref σ α) (f : α → α) :
ST σ Unit
Equations

- ST.Prim.Ref.modify r f = do let v ← ST.Prim.Ref.get r ST.Prim.Ref.set r (f v)

Instances For

source
@[implemented_by ST.Prim.Ref.modifyGetUnsafe]
def ST.Prim.Ref.modifyGet {σ α β : Type} (r : Ref σ α) (f : α → β × α) :
ST σ β
Equations

- ST.Prim.Ref.modifyGet r f = do let v ← ST.Prim.Ref.get r match f v with | (b, a) => do ST.Prim.Ref.set r a pure b

Instances For

source
@[inline]
def ST.mkRef {σ : Type} {m : Type → Type} [MonadLiftT (ST σ) m] {α : Type} (a : α) :
m (Ref σ α)

Creates a new mutable reference that contains the provided value `a`.

Equations

- ST.mkRef a = liftM (ST.Prim.mkRef a)

Instances For

source
@[inline]
def ST.Ref.get {σ : Type} {m : Type → Type} [MonadLiftT (ST σ) m] {α : Type} (r : Ref σ α) :
m α

Reads the value of a mutable reference.

Equations

- r.get = liftM (ST.Prim.Ref.get r)

Instances For

source
@[inline]
def ST.Ref.set {σ : Type} {m : Type → Type} [MonadLiftT (ST σ) m] {α : Type} (r : Ref σ α) (a : α) :
m Unit

Replaces the value of a mutable reference.

Equations

- r.set a = liftM (ST.Prim.Ref.set r a)

Instances For

source
@[inline]
def ST.Ref.swap {σ : Type} {m : Type → Type} [MonadLiftT (ST σ) m] {α : Type} (r : Ref σ α) (a : α) :
m α

Atomically swaps the value of a mutable reference cell with another value. The reference cell's original value is returned.

Equations

- r.swap a = liftM (ST.Prim.Ref.swap r a)

Instances For

source
@[inline]
unsafe def ST.Ref.take {σ : Type} {m : Type → Type} [MonadLiftT (ST σ) m] {α : Type} (r : Ref σ α) :
m α

Reads the value of a mutable reference cell, removing it.

This causes subsequent attempts to read from or take the reference cell to block until a new value is written using `ST.Ref.set`.

Equations

- r.take = liftM (ST.Prim.Ref.take r)

Instances For

source
@[inline]
def ST.Ref.ptrEq {σ : Type} {m : Type → Type} [MonadLiftT (ST σ) m] {α : Type} (r1 r2 : Ref σ α) :
m Bool

Checks whether two reference cells are in fact aliases for the same cell.

Even if they contain the same value, two references allocated by different executions of `IO.mkRef` or `ST.mkRef` are distinct. Modifying one has no effect on the other. Likewise, a single reference cell may be aliased, and modifications to one alias also modify the other.

Equations

- r1.ptrEq r2 = liftM (ST.Prim.Ref.ptrEq r1 r2)

Instances For

source
@[inline]
def ST.Ref.modify {σ : Type} {m : Type → Type} [MonadLiftT (ST σ) m] {α : Type} (r : Ref σ α) (f : α → α) :
m Unit

Atomically modifies a mutable reference cell by replacing its contents with the result of a function call.

Equations

- r.modify f = liftM (ST.Prim.Ref.modify r f)

Instances For

source
@[inline]
def ST.Ref.modifyGet {σ : Type} {m : Type → Type} [MonadLiftT (ST σ) m] {α β : Type} (r : Ref σ α) (f : α → β × α) :
m β

Atomically modifies a mutable reference cell by replacing its contents with the result of a function call that simultaneously computes a value to return.

Equations

- r.modifyGet f = liftM (ST.Prim.Ref.modifyGet r f)

Instances For

source
def ST.Ref.toMonadStateOf {σ : Type} {m : Type → Type} [MonadLiftT (ST σ) m] {α : Type} (r : Ref σ α) :
MonadStateOf α m

Creates a `MonadStateOf` instance from a reference cell.

This allows programs written against the state monad API to be executed using a mutable reference cell to track the state.

Equations

- r.toMonadStateOf = { get := r.get, set := r.set, modifyGet := fun {α_1 : Type} => r.modifyGet }

Instances For