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.CancellationReason : Type

Reasons for cancellation.

• deadline : CancellationReason

  Cancelled due to a deadline or timeout

• shutdown : CancellationReason

  Cancelled due to shutdown

• cancel : CancellationReason

  Explicitly cancelled

• custom (msg : String) : CancellationReason

  Custom cancellation reason

def Std.instReprCancellationReason.repr : CancellationReason → Nat → Format

@[implicit_reducible]

instance Std.instReprCancellationReason : Repr CancellationReason

@[implicit_reducible]

instance Std.instBEqCancellationReason : BEq CancellationReason

def Std.instBEqCancellationReason.beq : CancellationReason → CancellationReason → Bool

@[implicit_reducible]

instance Std.instToStringCancellationReason : ToString CancellationReason

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

structure Std.CancellationToken.State : Type

The central state structure for a CancellationToken.

• reason : Option CancellationReason

  The cancellation reason if cancelled, none otherwise.

• 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

Creates a new cancellation token.

def Std.CancellationToken.cancel (x : CancellationToken) (reason : CancellationReason := CancellationReason.cancel) : BaseIO Unit

Cancels the token with the given reason, notifying all currently waiting consumers. Once cancelled, the token remains cancelled.

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

Checks if the token is cancelled.

def Std.CancellationToken.getCancellationReason (x : CancellationToken) : BaseIO (Option CancellationReason)

Gets the cancellation reason if the token is cancelled.

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

Waits for cancellation. Returns a task that completes when cancelled.

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

Creates a selector that waits for cancellation.