This module provides a tree-structured cancellation context called CancellationToken where cancelling a parent automatically cancels all child contexts.

structure Std.CancellationContext.State : Type

• tokens : TreeMap UInt64 (CancellationToken × Array UInt64) compare

  Map of token IDs to optional tokens and their children.

• id : UInt64

  Next available ID

structure Std.CancellationContext : Type

A cancellation context that allows multiple consumers to wait until cancellation is requested. Forms a tree structure where cancelling a parent cancels all children.

• state : Mutex State
• token : CancellationToken
• id : UInt64

def Std.CancellationContext.new : BaseIO CancellationContext

Creates a new root cancellation context.

Equations

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

def Std.CancellationContext.fork (root : CancellationContext) : BaseIO CancellationContext

Forks a child context from a parent. If the parent is already cancelled, returns the parent context. Otherwise, creates a new child that will be cancelled when the parent is cancelled.

Equations

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

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

Cancels this context and all child contexts with the given reason.

Equations

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

@[inline]

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

Checks if the context is cancelled.

Equations

• x.isCancelled = x.token.isCancelled

@[inline]

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

Returns the cancellation reason if the context is cancelled.

Equations

• x.getCancellationReason = x.token.getCancellationReason

@[inline]

def Std.CancellationContext.done (x : CancellationContext) : IO (Internal.IO.Async.AsyncTask Unit)

Waits for cancellation. Returns a task that completes when the context is cancelled.

Equations

• x.done = x.token.wait

@[inline]

def Std.CancellationContext.doneSelector (x : CancellationContext) : Internal.IO.Async.Selector Unit

Creates a selector that waits for cancellation.

Equations

• x.doneSelector = x.token.selector

def Std.CancellationContext.countAliveTokens (x : CancellationContext) : BaseIO Nat

Counts the number of alive (non-cancelled) tokens in the context tree, including this context and all its descendants.

Equations

• x.countAliveTokens = x.state.atomically do let st ← get pure (Std.CancellationContext.countAliveTokensRec✝ st x.id)