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

Equations

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

instance Std.instReprCancellationReason : Repr CancellationReason

Equations

• Std.instReprCancellationReason = { reprPrec := Std.instReprCancellationReason.repr }

instance Std.instBEqCancellationReason : BEq CancellationReason

Equations

• Std.instBEqCancellationReason = { beq := Std.instBEqCancellationReason.beq }

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

Equations

• Std.instBEqCancellationReason.beq Std.CancellationReason.deadline Std.CancellationReason.deadline = true
• Std.instBEqCancellationReason.beq Std.CancellationReason.shutdown Std.CancellationReason.shutdown = true
• Std.instBEqCancellationReason.beq Std.CancellationReason.cancel Std.CancellationReason.cancel = true
• Std.instBEqCancellationReason.beq (Std.CancellationReason.custom a) (Std.CancellationReason.custom b) = (a == b)
• Std.instBEqCancellationReason.beq x✝¹ x✝ = false

instance Std.instToStringCancellationReason : ToString CancellationReason

Equations

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

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.

• 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.

Equations

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

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.

Equations

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

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

Checks if the token is cancelled.

Equations

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

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

Gets the cancellation reason if the token is cancelled.

Equations

• x.getCancellationReason = x.state.atomically do let st ← get pure st.reason

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

Waits 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.