opaque Void.nonemptyType (σ : Type) : NonemptyType

def Void (σ : Type) : Type

Equations

• Void σ = (Void.nonemptyType σ).type

instance Void.instNonempty {σ : Type} : Nonempty (Void σ)

@[extern lean_void_mk]

opaque Void.mk {σ : Type} (x : σ) : Void σ

structure ST.Out (σ α : Type) : Type

• val : α
• state : Void σ

def ST (σ α : 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 σ α = (Void σ → ST.Out σ α)

@[inline]

def ST.pure {α σ : Type} (x : α) : ST σ α

Equations

• ST.pure x s = { val := x, state := s }

@[inline]

def ST.bind {σ α β : Type} (x : ST σ α) (f : α → ST σ β) : ST σ β

Equations

• x.bind f s = match x s with | { val := x, state := s } => f x s

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

Equations

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

@[always_inline]

instance instMonadFinallyST {σ : Type} : MonadFinally (ST σ)

Equations

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

instance instInhabitedST {σ α : Type} [Inhabited α] : Inhabited (ST σ α)

Equations

• instInhabitedST = { default := fun (s : Void σ) => { val := default, state := s } }

inductive EST.Out (ε σ α : Type) : Type

• ok {ε σ α : Type} : α → Void σ → Out ε σ α
• error {ε σ α : Type} : ε → Void σ → Out ε σ α

def EST (ε σ α : 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 ε σ α = (Void σ → EST.Out ε σ α)

@[inline]

def EST.pure {α ε σ : Type} (a : α) : EST ε σ α

Equations

• EST.pure a s = EST.Out.ok a s

@[inline]

def EST.bind {ε σ α β : Type} (x : EST ε σ α) (f : α → EST ε σ β) : EST ε σ β

Equations

• x.bind f s = match x s with | EST.Out.ok a s => f a s | EST.Out.error e s => EST.Out.error e s

@[inline]

def EST.throw {ε σ α : Type} (e : ε) : EST ε σ α

Equations

• EST.throw e s = EST.Out.error e s

@[inline]

def EST.tryCatch {ε σ α : Type} (x : EST ε σ α) (handle : ε → EST ε σ α) : EST ε σ α

Equations

• x.tryCatch handle s = match x s with | EST.Out.ok a s => EST.Out.ok a s | EST.Out.error e s => handle e s

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

Equations

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

@[always_inline]

instance instMonadFinallyEST {ε σ : Type} : MonadFinally (EST ε σ)

Equations

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

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

Equations

• instMonadExceptOfEST ε σ = { throw := fun {α : Type} => EST.throw, tryCatch := fun {α : Type} => EST.tryCatch }

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

Equations

• instInhabitedEST = { default := fun (s : Void σ) => EST.Out.error default s }

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

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

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

Equations

• instSTWorldOfMonadLift = { }

instance instSTWorldST {σ : Type} : STWorld σ (ST σ)

Equations

• instSTWorldST = { }

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 (Void.mk ()) with | EST.Out.ok a a_1 => Except.ok a | EST.Out.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 (Void.mk ()) with | { val := a, state := state } => a

@[always_inline]

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

Equations

• instMonadLiftSTEST = { monadLift := fun {α : Type} (x : ST σ α) (s : Void σ) => match x s with | { val := a, state := s } => EST.Out.ok a s }

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 α

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 }