This module contains the implementation of Std.CancellationToken. Std.CancellationToken provides a cancellation primitive for signaling cancellation 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 a cancellation has occurred.

inductive Std.CancellationToken.Consumer : Type

• normal (promise : IO.Promise Unit) : Consumer
• select (finished : Internal.IO.Async.Waiter Unit) : Consumer

def Std.CancellationToken.Consumer.resolve (c : Consumer) : BaseIO Bool

Equations

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

structure Std.CancellationToken.State : Type

The central state structure for a CancellationToken.

• cancelled : Bool

  Whether this token has been cancelled.

• consumers : Queue Consumer

  Consumers that are blocked waiting for cancellation.

structure Std.CancellationToken : Type

A cancellation token is a synchronization primitive that allows multiple consumers to wait until cancellation is requested.

• state : Mutex State

def Std.CancellationToken.new : BaseIO CancellationToken

Create a new cancellation token.

Equations

• Std.CancellationToken.new = do let __do_lift ← Std.Mutex.new { cancelled := false, consumers := ∅ } pure { state := __do_lift }

def Std.CancellationToken.cancel (x : CancellationToken) : BaseIO Unit

Cancel the token, notifying all currently waiting consumers with true. Once cancelled, the token remains cancelled.

Equations

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

def Std.CancellationToken.isCancelled (x : CancellationToken) : BaseIO Bool

Check if the token is cancelled.

Equations

• x.isCancelled = x.state.atomically do let st ← get pure st.cancelled

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

Wait for cancellation. Returns a task that completes when cancelled,

Equations

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

def Std.CancellationToken.selector (token : CancellationToken) : Internal.IO.Async.Selector Unit

Creates a selector that waits for cancellation

Equations

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