structure Concurrency.MVar (a : Type) : Type

• taking : Std.Condvar
• putting : Std.Condvar
• state : Std.Mutex (State a)

def Concurrency.MVar.new {a : Type} (value : a) : BaseIO (MVar a)

Equations

• Concurrency.MVar.new value = Concurrency.MVar.mk✝ <$> Std.Condvar.new <*> Std.Condvar.new <*> Std.Mutex.new (Concurrency.MVar.State.full value)

def Concurrency.MVar.empty {a : Type} : BaseIO (MVar a)

Equations

• Concurrency.MVar.empty = Concurrency.MVar.mk✝ <$> Std.Condvar.new <*> Std.Condvar.new <*> Std.Mutex.new Concurrency.MVar.State.empty

def Concurrency.MVar.isEmpty {a : Type} {m : Type → Type u_1} [Monad m] [MonadState (State a) m] : m Bool

Equations

• Concurrency.MVar.isEmpty = Concurrency.MVar.State.isEmpty <$> get

def Concurrency.MVar.isFull {a : Type} {m : Type → Type u_1} [Monad m] [MonadState (State a) m] : m Bool

Equations

• Concurrency.MVar.isFull = Concurrency.MVar.State.isFull <$> get

def Concurrency.MVar.take {a : Type} [Inhabited a] (self : MVar a) : BaseIO a

Returns the content of the MVar. If the MVar is currently empty, take will wait until it is fill. After a take, the MVar is left empty.

Single-wakeup LIFO order

Equations

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

def Concurrency.MVar.put {a : Type} (self : MVar a) (value : a) : BaseIO Unit

Put a value into the MVar. If the MVar is currently full, put will wait until it becomes empty.

Single-wakeup FIFO order

Equations

• self.put value = self.state.atomicallyOnce self.putting Concurrency.MVar.isEmpty do set (Concurrency.MVar.State.full value) liftM self.taking.notifyOne

def Concurrency.MVar.read {a : Type} [Inhabited a] (self : MVar a) : IO a

Equations

• self.read = do let result ← liftM self.take liftM (self.put result) pure result

def Concurrency.MVar.read? {a : Type} (self : MVar a) : BaseIO (Option a)

Equations

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

def Concurrency.MVar.replace {a : Type} [Inhabited a] (self : MVar a) (value : a) : BaseIO Unit

Equations

• self.replace value = self.take *> self.put value