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

• instInhabitedEST
• instMonadEST
• instMonadExceptOfEST
• instMonadLiftSTEST
• instSTWorldEST

@[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

• IO.instMonadLiftSTRealWorldBaseIO
• instMonadLiftSTEST
• instMonadST

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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

Instances

• instSTWorldEST
• instSTWorldOfMonadLift

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

Equations

• instSTWorldOfMonadLift = { }

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

Equations

• instSTWorldEST = { }

@[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

@[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

@[always_inline]

instance instMonadLiftSTEST {ε σ : Type} : MonadLift (ST σ) (EST ε σ)

Equations

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

opaque ST.RefPointed : NonemptyType

References

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

• ST.instNonemptyRef

instance ST.instNonemptyRef {σ α : Type} [s : Nonempty α] : Nonempty (Ref σ α)

@[extern lean_st_mk_ref]

opaque ST.Prim.mkRef {σ α : Type} (a : α) : ST σ (Ref σ α)

@[extern lean_st_ref_get]

opaque ST.Prim.Ref.get {σ α : Type} (r : Ref σ α) : ST σ α

@[extern lean_st_ref_set]

opaque ST.Prim.Ref.set {σ α : Type} (r : Ref σ α) (a : α) : ST σ Unit

@[extern lean_st_ref_swap]

opaque ST.Prim.Ref.swap {σ α : Type} (r : Ref σ α) (a : α) : ST σ α

@[extern lean_st_ref_take]

unsafe opaque ST.Prim.Ref.take {σ α : Type} (r : Ref σ α) : ST σ α

@[extern lean_st_ref_ptr_eq]

opaque ST.Prim.Ref.ptrEq {σ α : Type} (r1 r2 : Ref σ α) : ST σ Bool

@[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)

@[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

@[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)

@[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

@[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)

@[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)

@[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)

@[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)

@[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)

@[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)

@[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)

@[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)

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 }