doc-next-gen

Init.System.ST

Module docstring

{}

EST definition
(ε : Type) (σ : Type) : Type → Type
Full source 
/--
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`.
-/
def EST (ε : Type) (σ : Type) : Type → Type := EStateM ε σ
State and Exception Monad (Restricted IO)
Informal description
The monad `EST ε σ` represents a restricted version of the `IO` monad where the only side effects allowed are mutable state of type `σ` and exceptions of type `ε`. Computations in this monad can be run in a non-monadic context using `runEST`.
ST abbrev
(σ : Type)
Full source 
/--
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`.
-/
abbrev ST (σ : Type) := EST Empty σ
State-Only Restricted IO Monad (`ST`)
Informal description
The `ST` monad is a restricted version of the `IO` monad where the only allowed side effect is mutable state of type `σ$. It can be run in a non-monadic context using `runST`.
instMonadEST instance
(ε σ : Type) : Monad (EST ε σ)
Full source 
instance (ε σ : Type) : Monad (EST ε σ) := inferInstanceAs (Monad (EStateM _ _))
Monad Structure for Stateful Exception Monad (EST)
Informal description
For any types $\varepsilon$ (exception type) and $\sigma$ (state type), the restricted IO monad `EST ε σ` forms a monad structure, supporting the standard monadic operations `pure` and `bind` for sequencing computations with state and exceptions.
instMonadExceptOfEST instance
(ε σ : Type) : MonadExceptOf ε (EST ε σ)
Full source 
instance (ε σ : Type) : MonadExceptOf ε (EST ε σ) := inferInstanceAs (MonadExceptOf ε (EStateM _ _))
Exception-Handling Monad Structure for Restricted IO with State and Exceptions
Informal description
For any types $\varepsilon$ and $\sigma$, the restricted IO monad `EST ε σ` is equipped with a canonical exception-handling monad structure for exceptions of type $\varepsilon$. This means it supports operations for throwing and catching exceptions while maintaining mutable state of type $\sigma$.
instInhabitedEST instance
{ε σ : Type} {α : Type} [Inhabited ε] : Inhabited (EST ε σ α)
Full source 
instance {ε σ : Type} {α : Type} [Inhabited ε] : Inhabited (EST ε σ α) := inferInstanceAs (Inhabited (EStateM _ _ _))
Inhabited Stateful Exception Monad (Restricted IO)
Informal description
For any types $\varepsilon$, $\sigma$, and $\alpha$, if $\varepsilon$ is inhabited (has a default element), then the monad `EST ε σ α` of stateful computations with exceptions is also inhabited.
instMonadST instance
(σ : Type) : Monad (ST σ)
Full source 
instance (σ : Type) : Monad (ST σ) := inferInstanceAs (Monad (EST _ _))
Monad Structure for State-Only Restricted IO Monad (`ST`)
Informal description
For any state type $\sigma$, the state-only restricted IO monad `ST σ` forms a monad structure, supporting the standard monadic operations `pure` and `bind` for sequencing computations with state.
STWorld structure
(σ : outParam Type) (m : Type → Type)
Full source 
/--
An auxiliary class used to infer the “state” of `EST` and `ST` monads.
-/
class STWorld (σ : outParam Type) (m : Type → Type)
State monad world typeclass
Informal description
A typeclass used to infer the state type `σ` for monads `m` that operate on a state of type `σ`. The `outParam` annotation on `σ` indicates that the state type can be inferred from the monad type `m` during typeclass resolution.
instSTWorldOfMonadLift instance
{σ m n} [MonadLift m n] [STWorld σ m] : STWorld σ n
Full source 
instance {σ m n} [MonadLift m n] [STWorld σ m] : STWorld σ n := ⟨⟩
State Monad World Structure Preservation under Monad Lifting
Informal description
For any state type $\sigma$ and monads $m$ and $n$, if there exists a monad lift from $m$ to $n$ and $m$ has a state monad world structure with state type $\sigma$, then $n$ also inherits a state monad world structure with the same state type $\sigma$.
instSTWorldEST instance
{ε σ} : STWorld σ (EST ε σ)
Full source 
instance {ε σ} : STWorld σ (EST ε σ) := ⟨⟩
State Monad World Structure for EST Monad
Informal description
For any exception type $\varepsilon$ and state type $\sigma$, the monad `EST $\varepsilon$ $\sigma$` is equipped with a state monad world structure where the state type is $\sigma$.
runEST definition
{ε α : Type} (x : (σ : Type) → EST ε σ α) : Except ε α
Full source 
/--
Runs an `EST` computation, in which mutable state and exceptions are the only side effects.
-/
@[noinline, nospecialize]
def runEST {ε α : Type} (x : (σ : Type) → EST ε σ α) : Except ε α :=
  match x Unit () with
  | EStateM.Result.okEStateM.Result.ok a _     => Except.ok a
  | EStateM.Result.errorEStateM.Result.error ex _ => Except.error ex
Execution of EST computation with unit state
Informal description
Given a computation `x` in the `EST ε σ` monad, which may involve state manipulation of type `σ` and exceptions of type `ε`, the function `runEST` executes `x` with the state type specialized to `Unit` and returns either a successful result of type `α` or an error of type `ε`. More precisely, for any types `ε` and `α`, and for any function `x` that takes a state type `σ` and returns a computation in `EST ε σ α`, `runEST x` evaluates `x` with `σ = Unit` and returns: - `Except.ok a` if the computation succeeds with result `a`, or - `Except.error ex` if the computation fails with exception `ex`.
runST definition
{α : Type} (x : (σ : Type) → ST σ α) : α
Full source 
/--
Runs an `ST` computation, in which mutable state via `ST.Ref` is the only side effect.
-/
@[noinline, nospecialize]
def runST {α : Type} (x : (σ : Type) → ST σ α) : α :=
  match x Unit () with
  | EStateM.Result.okEStateM.Result.ok a _     => a
  | EStateM.Result.errorEStateM.Result.error ex _ => nomatch ex
Execution of state-only computation (`runST`)
Informal description
The function `runST` executes a stateful computation `x` in the `ST` monad, where the only side effect is mutable state of type `σ`, and returns a result of type `α`. The computation is run with the state type specialized to `Unit`, ensuring that no actual state is maintained during execution.
instMonadLiftSTEST instance
{ε σ} : MonadLift (ST σ) (EST ε σ)
Full source 
@[always_inline]
instance {ε σ} : MonadLift (ST σ) (EST ε σ) := ⟨fun x s =>
  match x s with
  | EStateM.Result.ok a s     => EStateM.Result.ok a s
  | EStateM.Result.error ex _ => nomatch ex⟩
Lifting from State-Only Monad to State-and-Exception Monad
Informal description
For any types $\varepsilon$ and $\sigma$, there is a canonical way to lift computations from the state-only monad $\mathrm{ST} \sigma$ to the combined state and exception monad $\mathrm{EST} \varepsilon \sigma$.
ST.RefPointed opaque
: NonemptyType.{0}
Full source 
/-- References -/
opaque RefPointed : NonemptyTypeNonemptyType.{0}
Nonempty Type of ST Monad Reference Cells
Informal description
The type `ST.RefPointed` is a nonempty type in universe level 0, representing the collection of all nonempty types of mutable reference cells in the ST monad.
ST.Ref structure
(σ : Type) (α : Type)
Full source 
/--
Mutable reference cells that contain values of type `α`. These cells can read from and mutated in
the `ST σ` monad.
-/
structure Ref (σ : Type) (α : Type) : Type where
  ref : RefPointed.type
  h   : Nonempty α
Mutable reference cell in the ST monad
Informal description
A mutable reference cell containing a value of type $\alpha$, which can be read from and modified within the `ST σ` monad.
ST.instNonemptyRef instance
{σ α} [s : Nonempty α] : Nonempty (Ref σ α)
Full source 
instance {σ α} [s : Nonempty α] : Nonempty (Ref σ α) :=
  Nonempty.intro { ref := Classical.choice RefPointed.property, h := s }
Nonemptiness of ST Monad Reference Cells
Informal description
For any types $\sigma$ and $\alpha$, if $\alpha$ is nonempty, then the type of mutable reference cells $\mathrm{Ref}\,\sigma\,\alpha$ in the ST monad is also nonempty.
ST.Prim.mkRef opaque
{σ α} (a : α) : ST σ (Ref σ α)
Full source 
@[extern "lean_st_mk_ref"]
opaque mkRef {σ α} (a : α) : ST σ (Ref σ α) := pure { ref := Classical.choice RefPointed.property, h := Nonempty.intro a }
Creation of Mutable Reference in ST Monad
Informal description
Given a value $a$ of type $\alpha$, the operation `mkRef` creates a new mutable reference cell in the `ST σ` monad containing the value $a$, and returns this reference cell of type $\mathrm{Ref}\,\sigma\,\alpha$.
ST.Prim.Ref.get opaque
{σ α} (r : @& Ref σ α) : ST σ α
Full source 
@[extern "lean_st_ref_get"]
opaque Ref.get {σ α} (r : @& Ref σ α) : ST σ α := inhabitedFromRef r
Retrieve Value from Mutable Reference in ST Monad
Informal description
Given a mutable reference cell `r` of type `Ref σ α` in the `ST σ` monad, the operation `get` retrieves the current value of type `α` stored in `r`.
ST.Prim.Ref.set opaque
{σ α} (r : @& Ref σ α) (a : α) : ST σ Unit
Full source 
@[extern "lean_st_ref_set"]
opaque Ref.set {σ α} (r : @& Ref σ α) (a : α) : ST σ Unit
Update Mutable Reference in ST Monad
Informal description
Given a mutable reference cell `r` of type `Ref σ α` in the `ST σ` monad and a value `a` of type `α`, the operation `set` updates the content of `r` to `a` and returns the unit value `()`.
ST.Prim.Ref.swap opaque
{σ α} (r : @& Ref σ α) (a : α) : ST σ α
Full source 
@[extern "lean_st_ref_swap"]
opaque Ref.swap {σ α} (r : @& Ref σ α) (a : α) : ST σ α := inhabitedFromRef r
Swap Operation for Mutable References in ST Monad
Informal description
Given a mutable reference cell `r` of type `Ref σ α` in the `ST σ` monad and a value `a` of type `α`, the operation `swap` updates the content of `r` to `a` and returns the previous value stored in `r`.
ST.Prim.Ref.take opaque
{σ α} (r : @& Ref σ α) : ST σ α
Full source 
@[extern "lean_st_ref_take"]
unsafe opaque Ref.take {σ α} (r : @& Ref σ α) : ST σ α := inhabitedFromRef r
Take and Remove Value from Mutable Reference in ST Monad
Informal description
Given a mutable reference cell `r` of type `Ref σ α` in the `ST σ` monad, the operation `take` returns the current value of type `α` stored in `r` and removes this value from the reference cell, leaving it in an unspecified state.
ST.Prim.Ref.ptrEq opaque
{σ α} (r1 r2 : @& Ref σ α) : ST σ Bool
Full source 
@[extern "lean_st_ref_ptr_eq"]
opaque Ref.ptrEq {σ α} (r1 r2 : @& Ref σ α) : ST σ Bool
Pointer Equality Check for Mutable References in ST Monad
Informal description
Given two mutable reference cells `r₁` and `r₂` of type `Ref σ α` in the `ST σ` monad, the operation `ptrEq` checks whether they refer to the same memory location, returning a Boolean value `true` if they do and `false` otherwise.
ST.Prim.Ref.modifyUnsafe definition
{σ α : Type} (r : Ref σ α) (f : α → α) : ST σ Unit
Full source 
@[inline] unsafe def Ref.modifyUnsafe {σ α : Type} (r : Ref σ α) (f : α → α) : ST σ Unit := do
  let v ← Ref.take r
  Ref.set r (f v)
Unsafe modification of mutable reference in ST monad
Informal description
The function `modifyUnsafe` takes a mutable reference cell `r` of type `Ref σ α` and a function `f : α → α`, then updates the content of `r` by applying `f` to its current value in the `ST σ` monad. This operation is performed by first taking the current value from `r`, applying `f` to it, and then setting the result back into `r`. The function returns the unit value `()` upon completion.
ST.Prim.Ref.modifyGetUnsafe definition
{σ α β : Type} (r : Ref σ α) (f : α → β × α) : ST σ β
Full source 
@[inline] unsafe def Ref.modifyGetUnsafe {σ α β : Type} (r : Ref σ α) (f : α → β × α) : ST σ β := do
  let v ← Ref.take r
  let (b, a) := f v
  Ref.setRef.set r a
  pure b
Unsafe modify and get operation for mutable references in ST monad
Informal description
Given a mutable reference cell `r` of type `Ref σ α` in the `ST σ` monad and a function `f : α → β × α`, the operation `modifyGetUnsafe` applies `f` to the current value stored in `r`, updates the reference with the second component of the result, and returns the first component.
ST.Prim.Ref.modify definition
{σ α : Type} (r : Ref σ α) (f : α → α) : ST σ Unit
Full source 
@[implemented_by Ref.modifyUnsafe]
def Ref.modify {σ α : Type} (r : Ref σ α) (f : α → α) : ST σ Unit := do
  let v ← Ref.get r
  Ref.set r (f v)
Modify mutable reference in ST monad
Informal description
Given a mutable reference cell `r` of type `Ref σ α` in the `ST σ` monad and a function `f : α → α`, the operation `modify` updates the content of `r` by applying `f` to its current value. The operation returns the unit value `()`.
ST.Prim.Ref.modifyGet definition
{σ α β : Type} (r : Ref σ α) (f : α → β × α) : ST σ β
Full source 
@[implemented_by Ref.modifyGetUnsafe]
def Ref.modifyGet {σ α β : Type} (r : Ref σ α) (f : α → β × α) : ST σ β := do
  let v ← Ref.get r
  let (b, a) := f v
  Ref.setRef.set r a
  pure b
Atomic modify-and-get operation for ST monad references
Informal description
Given a mutable reference cell `r` of type `Ref σ α` in the `ST σ` monad and a function `f : α → β × α`, the operation `modifyGet` performs the following steps: 1. Retrieves the current value `v` from `r` 2. Applies `f` to `v`, obtaining a pair `(b, a)` 3. Updates the reference `r` with the new value `a` 4. Returns the result `b` This operation combines getting, transforming, and setting the reference value in one atomic action.
ST.mkRef definition
{α : Type} (a : α) : m (Ref σ α)
Full source 
/--
Creates a new mutable reference that contains the provided value `a`.
-/
@[inline] def mkRef {α : Type} (a : α) : m (Ref σ α) :=  liftM <| Prim.mkRef a
Create mutable reference in ST monad
Informal description
The function creates a new mutable reference cell in the `ST σ` monad, initialized with the value `a` of type `α`.
ST.Ref.get definition
{α : Type} (r : Ref σ α) : m α
Full source 
/--
Reads the value of a mutable reference.
-/
@[inline] def Ref.get {α : Type} (r : Ref σ α) : m α := liftM <| Prim.Ref.get r
Retrieve value from mutable reference in ST monad
Informal description
Given a mutable reference cell `r` of type `Ref σ α` in the `ST σ` monad, the operation `get` retrieves the current value of type `α` stored in `r`.
ST.Ref.set definition
{α : Type} (r : Ref σ α) (a : α) : m Unit
Full source 
/--
Replaces the value of a mutable reference.
-/
@[inline] def Ref.set {α : Type} (r : Ref σ α) (a : α) : m Unit := liftM <| Prim.Ref.set r a
Update mutable reference in ST monad
Informal description
Given a mutable reference cell `r` of type `Ref σ α` in the `ST σ` monad and a value `a` of type `α`, the operation `ST.Ref.set` updates the content of `r` to `a` and returns the unit value `()`.
ST.Ref.swap definition
{α : Type} (r : Ref σ α) (a : α) : m α
Full source 
/--
Atomically swaps the value of a mutable reference cell with another value. The reference cell's
original value is returned.
-/
@[inline] def Ref.swap {α : Type} (r : Ref σ α) (a : α) : m α := liftM <| Prim.Ref.swap r a
Atomic swap operation for mutable references in the ST monad
Informal description
The operation `ST.Ref.swap` atomically replaces the value stored in the mutable reference cell `r` of type `Ref σ α` with the value `a` of type `α` in the `ST σ` monad, and returns the original value stored in `r`.
ST.Ref.take definition
{α : Type} (r : Ref σ α) : m α
Full source 
/--
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`.
-/
@[inline] unsafe def Ref.take {α : Type} (r : Ref σ α) : m α := liftM <| Prim.Ref.take r
Take and remove value from mutable reference in ST monad
Informal description
The operation `take` on a mutable reference cell `r` of type `Ref σ α` in the `ST σ` monad returns the current value of type `α` stored in `r` and removes this value from the reference cell, leaving it in an unspecified state. Subsequent attempts to read from or take the reference cell will block until a new value is written using `ST.Ref.set`.
ST.Ref.ptrEq definition
{α : Type} (r1 r2 : Ref σ α) : m Bool
Full source 
/--
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.
-/
@[inline] def Ref.ptrEq {α : Type} (r1 r2 : Ref σ α) : m Bool := liftM <| Prim.Ref.ptrEq r1 r2
Pointer equality check for mutable references in ST monad
Informal description
Given two mutable reference cells `r₁` and `r₂` of type `Ref σ α` in the `ST σ` monad, the function `ptrEq` checks whether they are aliases for the same memory location, returning `true` if they are and `false` otherwise. Note that even if two references contain the same value, they are considered distinct unless they were created as aliases of each other.
ST.Ref.modify definition
{α : Type} (r : Ref σ α) (f : α → α) : m Unit
Full source 
/--
Atomically modifies a mutable reference cell by replacing its contents with the result of a function
call.
-/
@[inline] def Ref.modify {α : Type} (r : Ref σ α) (f : α → α) : m Unit := liftM <| Prim.Ref.modify r f
Modify mutable reference in ST monad
Informal description
Given a mutable reference cell `r` of type `Ref σ α` in the `ST σ` monad and a function `f : α → α`, the operation `modify` updates the content of `r` by applying `f` to its current value. The operation returns the unit value `()`.
ST.Ref.modifyGet definition
{α : Type} {β : Type} (r : Ref σ α) (f : α → β × α) : m β
Full source 
/--
Atomically modifies a mutable reference cell by replacing its contents with the result of a function
call that simultaneously computes a value to return.
-/
@[inline] def Ref.modifyGet {α : Type} {β : Type} (r : Ref σ α) (f : α → β × α) : m β := liftM <| Prim.Ref.modifyGet r f
Atomic modify-and-get operation for ST monad references
Informal description
Given a mutable reference cell `r` of type `Ref σ α` in the `ST σ` monad and a function `f : α → β × α`, the operation `modifyGet` atomically performs the following steps: 1. Retrieves the current value `v` from `r` 2. Applies `f` to `v`, obtaining a pair `(b, a)` 3. Updates the reference `r` with the new value `a` 4. Returns the result `b` This combines getting, transforming, and setting the reference value in one atomic action.
ST.Ref.toMonadStateOf definition
(r : Ref σ α) : MonadStateOf α m
Full source 
/--
Creates a `MonadStateOf` instance from a reference cell.

This allows programs written against the [state monad](lean-manual://section/state-monads) API to
be executed using a mutable reference cell to track the state.
-/
def Ref.toMonadStateOf (r : Ref σ α) : MonadStateOf α m where
  get := r.get
  set := r.set
  modifyGet := r.modifyGet
State monad instance from mutable reference
Informal description
Given a mutable reference cell `r` of type `Ref σ α` in the `ST σ` monad, the function `ST.Ref.toMonadStateOf` constructs a `MonadStateOf α m` instance that uses `r` to track the state. This allows programs written using the state monad API to be executed with `r` as the underlying state storage. The instance provides the following operations: - `get`: Retrieves the current value stored in `r` - `set`: Updates the value stored in `r` - `modifyGet`: Atomically modifies and retrieves the value in `r` using a given function