This module contains the implementation of Std.Notify. Std.Notify provides a lightweight notification primitive for signaling between tasks or threads. It supports both synchronous and asynchronous waiting, and is useful for cases where you want to notify one or more waiters that an event has occurred.

Unlike a channel, Std.Notify does not buffer messages or carry data. It's simply a trigger. If no one is waiting, notifications are lost. If one or more waiters are present, exactly one will be woken up per notification.

inductive Std.Notify.Consumer (α : Type) : Type

• normal {α : Type} (promise : IO.Promise α) : Consumer α
• select {α : Type} (finished : Internal.IO.Async.Waiter α) : Consumer α

def Std.Notify.Consumer.resolve {α : Type} (c : Consumer α) (x : α) : BaseIO Bool

Equations

• (Std.Notify.Consumer.normal promise).resolve x = do IO.Promise.resolve x promise pure true
• (Std.Notify.Consumer.select waiter).resolve x = waiter.race (pure false) fun (promise : IO.Promise (Except IO.Error α)) => do IO.Promise.resolve (Except.ok x) promise pure true

structure Std.Notify.State : Type

The central state structure for an a Notify.

• consumers : Queue (Consumer Unit)

  Consumers that are blocked waiting for a notification.

structure Std.Notify : Type

A notify is a synchronization primitive that allows multiple consumers to wait until notify is called.

• state : Mutex State

def Std.Notify.new : BaseIO Notify

Create a new notify.

Equations

• Std.Notify.new = do let __do_lift ← Std.Mutex.new { consumers := ∅ } pure { state := __do_lift }

def Std.Notify.notify (x : Notify) : BaseIO Unit

Notify all currently waiting consumers.

Equations

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

def Std.Notify.notifyOne (x : Notify) : BaseIO Bool

Notify exactly one waiting consumer (if any). Returns true if a consumer was notified, false if no consumers were waiting.

Equations

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

def Std.Notify.wait (x : Notify) : IO (Internal.IO.Async.AsyncTask Unit)

Wait to be notified. Returns a task that completes when notify is called. Note: if notify was called before wait, this will wait for the next notify call.

Equations

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

def Std.Notify.selector (notify : Notify) : Internal.IO.Async.Selector Unit

Creates a selector that waits for notifications

Equations

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