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

structure Std.Notify.State : Type

The central state structure for 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.

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

Notify all currently waiting consumers.

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.

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.

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

Creates a selector that waits for notifications