inductive Control.Monad.STMResult (α : Type) : Type

Result of an STM transaction step.

• success {α : Type} : α → STMResult α
• retry {α : Type} : STMResult α

def Control.Monad.STM (α : Type) : Type

The STM monad. Wraps BaseIO actions that execute under the global STM lock. $$\text{STM}(\alpha) = \text{BaseIO}(\text{STMResult}(\alpha))$$

Equations

• Control.Monad.STM α = BaseIO (Control.Monad.STMResult α)

@[implicit_reducible]

instance Control.Monad.STM.instMonad : Monad STM

Equations

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

@[implicit_reducible]

instance Control.Monad.STM.instMonadLiftTBaseIO : MonadLiftT BaseIO STM

Equations

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

@[inline]

def Control.Monad.STM.retry {α : Type} : STM α

Signal retry: abort this transaction and wait for state changes. $$\text{retry} : \text{STM}(\alpha)$$

Equations

• Control.Monad.STM.retry = pure Control.Monad.STMResult.retry

@[inline]

def Control.Monad.STM.orElse {α : Type} (a b : STM α) : STM α

Try the first transaction; if it retries, try the second. $$\text{orElse}(a, b) = \begin{cases} a & \text{if } a \text{ succeeds} \\ b & \text{if } a \text{ retries} \end{cases}$$

Equations

• a.orElse b = do let result ← a match result with | Control.Monad.STMResult.success v => pure (Control.Monad.STMResult.success v) | Control.Monad.STMResult.retry => b

@[inline]

def Control.Monad.STM.check (cond : Bool) : STM Unit

Check a condition; retry if false. $$\text{check}(p) = \text{if } p \text{ then pure () else retry}$$

Equations

• Control.Monad.STM.check cond = if cond = true then pure () else Control.Monad.STM.retry

partial def Control.Monad.atomically {α : Type} (action : STM α) : IO α

Run an STM transaction atomically. Blocks until the transaction succeeds (i.e., does not retry).

Uses a global Std.Mutex to serialize all transactions. If the transaction signals retry, the lock is released and the thread sleeps briefly before retrying.

$$\text{atomically} : \text{STM}(\alpha) \to \text{IO}(\alpha)$$