@[reducible, inline]

abbrev Data.IORef (α : Type) : Type

A mutable reference in IO, wrapping Lean's IO.Ref. $$\text{IORef}(\alpha) \cong \text{IO.Ref}(\alpha)$$

Equations

• Data.IORef α = IO.Ref α

@[inline]

def Data.newIORef {α : Type} (a : α) : IO (IORef α)

Create a new IORef with an initial value. $$\text{newIORef} : \alpha \to \text{IO}(\text{IORef}\ \alpha)$$

Equations

• Data.newIORef a = liftM (IO.mkRef a)

@[inline]

def Data.readIORef {α : Type} (ref : IORef α) : IO α

Read the current value of an IORef. $$\text{readIORef} : \text{IORef}\ \alpha \to \text{IO}\ \alpha$$

Equations

• Data.readIORef ref = ST.Ref.get ref

@[inline]

def Data.writeIORef {α : Type} (ref : IORef α) (a : α) : IO Unit

Write a new value to an IORef, replacing the old. $$\text{writeIORef} : \text{IORef}\ \alpha \to \alpha \to \text{IO}\ ()$$

Equations

• Data.writeIORef ref a = ST.Ref.set ref a

@[inline]

def Data.modifyIORef {α : Type} (ref : IORef α) (f : α → α) : IO Unit

Apply a function to the value in an IORef. $$\text{modifyIORef}(\text{ref}, f) \equiv \text{ref} \gets f(\text{ref})$$

Equations

• Data.modifyIORef ref f = ST.Ref.modify ref f

@[inline]

def Data.modifyIORef' {α : Type} (ref : IORef α) (f : α → α) : IO Unit

Strict version of modifyIORef. In Lean (strict evaluation) this is identical to modifyIORef. $$\text{modifyIORef'} = \text{modifyIORef}$$

Equations

• Data.modifyIORef' ref f = ST.Ref.modify ref f

def Data.atomicModifyIORef {α β : Type} (ref : IORef α) (f : α → α × β) : IO β

Atomically modify an IORef, returning a derived value. Applies $f$ to the current value, stores the first component, and returns the second. $$\text{atomicModifyIORef}(\text{ref}, f) : \text{IO}\ \beta$$ where $f : \alpha \to (\alpha \times \beta)$

Note: not truly atomic w.r.t. concurrent access (use MVar or Mutex for that).

Equations

• Data.atomicModifyIORef ref f = do let a ← ST.Ref.get ref match f a with | (a', b) => do ST.Ref.set ref a' pure b

def Data.atomicModifyIORef_ {α β : Type} (ref : IORef α) (f : α → α × β) : IO Unit

Atomically modify an IORef without returning a value. $$\text{atomicModifyIORef\_}(\text{ref}, f) \equiv \text{ref} \gets \pi_1(f(\text{ref}))$$

Equations

• Data.atomicModifyIORef_ ref f = do let __discr ← Data.atomicModifyIORef ref f have x : β := __discr pure PUnit.unit

@[inline]

def Data.atomicWriteIORef {α : Type} (ref : IORef α) (a : α) : IO Unit

Atomically write a new value, returning the old. $$\text{atomicWriteIORef}(\text{ref}, a) \equiv \text{writeIORef}(\text{ref}, a)$$ In Lean this is just writeIORef (strict evaluation makes it equivalent).

Equations

• Data.atomicWriteIORef ref a = ST.Ref.set ref a