This module contains the implementation of ContextAsync, a monad for asynchronous computations with cooperative cancellation support that must be explicitly checked for and cancelled explicitly.

@[reducible, inline]

abbrev Std.Internal.IO.Async.ContextAsync (α : Type) : Type

An asynchronous computation with cooperative cancellation support via a CancellationContext. ContextAsync α is equivalent to ReaderT CancellationContext Async α, providing a CancellationContext value to async computations.

Equations

• Std.Internal.IO.Async.ContextAsync α = ReaderT Std.CancellationContext Std.Internal.IO.Async.Async α

@[inline]

def Std.Internal.IO.Async.ContextAsync.runIn {α : Type} (ctx : CancellationContext) (x : ContextAsync α) : Async α

Runs a ContextAsync computation with a given context. See also ContextAsync.run for running with a new context that automatically cancels after execution.

Equations

• Std.Internal.IO.Async.ContextAsync.runIn ctx x = x ctx

@[inline]

def Std.Internal.IO.Async.ContextAsync.run {α : Type} (x : ContextAsync α) : Async α

Runs a ContextAsync computation with a new context that cancels after the execution of the computation. See also ContextAsync.runIn for running with an existing context.

Equations

• x.run = do let ctx ← liftM Std.CancellationContext.new x ctx <* liftM (ctx.cancel Std.CancellationReason.cancel)

@[inline]

def Std.Internal.IO.Async.ContextAsync.getContext : ContextAsync CancellationContext

Returns the current context for inspection or to pass to other functions.

Equations

• Std.Internal.IO.Async.ContextAsync.getContext ctx = pure ctx

@[inline]

def Std.Internal.IO.Async.ContextAsync.isCancelled : ContextAsync Bool

Checks if the current context is cancelled. Returns true if the context (or any ancestor) has been cancelled. Long-running operations should periodically check this and exit gracefully when cancelled.

Equations

• Std.Internal.IO.Async.ContextAsync.isCancelled = do let ctx ← Std.Internal.IO.Async.ContextAsync.getContext liftM ctx.isCancelled

@[inline]

def Std.Internal.IO.Async.ContextAsync.getCancellationReason : ContextAsync (Option CancellationReason)

Gets the cancellation reason if the context is cancelled. Returns some reason if cancelled, none otherwise, allowing you to distinguish between different cancellation types.

Equations

• Std.Internal.IO.Async.ContextAsync.getCancellationReason = do let ctx ← Std.Internal.IO.Async.ContextAsync.getContext liftM ctx.getCancellationReason

@[inline]

def Std.Internal.IO.Async.ContextAsync.cancel (reason : CancellationReason) : ContextAsync Unit

Cancels the current context with the given reason, cascading to all child contexts. Cancellation is cooperative, operations must explicitly check isCancelled or use awaitCancellation to respond.

Equations

• Std.Internal.IO.Async.ContextAsync.cancel reason = do let ctx ← Std.Internal.IO.Async.ContextAsync.getContext liftM (ctx.cancel reason)

@[inline]

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

Returns a selector that completes when the current context is cancelled.

Equations

• Std.Internal.IO.Async.ContextAsync.doneSelector = do let ctx ← Std.Internal.IO.Async.ContextAsync.getContext pure ctx.doneSelector

@[inline]

def Std.Internal.IO.Async.ContextAsync.awaitCancellation : ContextAsync Unit

Waits for the current context to be cancelled.

Equations

• Std.Internal.IO.Async.ContextAsync.awaitCancellation = do let ctx ← Std.Internal.IO.Async.ContextAsync.getContext let task ← liftM ctx.done Std.Internal.IO.Async.await task

@[inline, specialize #[]]

def Std.Internal.IO.Async.ContextAsync.concurrently {α β : Type} (x : ContextAsync α) (y : ContextAsync β) (prio : Task.Priority := Task.Priority.default) : ContextAsync (α × β)

Runs two computations concurrently and returns both results. Each computation runs in its own child context; if either fails or is cancelled, both are cancelled immediately and the exception is propagated.

Equations

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

@[inline, specialize #[]]

def Std.Internal.IO.Async.ContextAsync.race {α : Type} [Inhabited α] (x y : ContextAsync α) (prio : Task.Priority := Task.Priority.default) : ContextAsync α

Runs two computations concurrently and returns the result of the first to complete. Each computation runs in its own child context; when either completes, the other is cancelled immediately.

Equations

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

@[inline, specialize #[]]

def Std.Internal.IO.Async.ContextAsync.concurrentlyAll {α : Type} (xs : Array (ContextAsync α)) (prio : Task.Priority := Task.Priority.default) : ContextAsync (Array α)

Runs all computations concurrently and collects results in the same order. Each runs in its own child context; if any computation fails, all others are cancelled and the exception is propagated.

Equations

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

@[inline, specialize #[]]

def Std.Internal.IO.Async.ContextAsync.background {α : Type} (action : ContextAsync α) (prio : Task.Priority := Task.Priority.default) : ContextAsync Unit

Launches a ContextAsync computation in the background, discarding its result.

The computation runs independently in the background in its own child context. The parent computation does not wait for background tasks to complete. This means that if the parent finishes its execution it will cause the cancellation of the background functions. See also disown for launching tasks that continue independently even after parent cancellation.

Equations

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

@[inline, specialize #[]]

def Std.Internal.IO.Async.ContextAsync.disown {α : Type} (action : ContextAsync α) (prio : Task.Priority := Task.Priority.default) : ContextAsync Unit

Launches a ContextAsync computation in the background, discarding its result. It's similar to background, but the child context is not automatically cancelled when the action completes. This allows the disowned computation to continue running independently, even if the parent context is cancelled. The child context will remain alive as long as the computation needs it. See also background for launching tasks that are cancelled when the parent finishes.

Equations

• action.disown prio = do let childCtx ← liftM Std.CancellationContext.new Std.Internal.IO.Async.background (liftM (action childCtx)) prio

def Std.Internal.IO.Async.ContextAsync.raceAll {c : Type u_1} {α : Type} [ForM ContextAsync c (ContextAsync α)] (xs : c) (prio : Task.Priority := Task.Priority.default) : ContextAsync α

Runs all computations concurrently and returns the first result. Each computation runs in its own child context; when the first completes successfully, all others are cancelled immediately.

Equations

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

@[inline, specialize #[]]

def Std.Internal.IO.Async.ContextAsync.async {α : Type} (x : ContextAsync α) (prio : Task.Priority := Task.Priority.default) : ContextAsync (AsyncTask α)

Launches a ContextAsync computation as an asynchronous task with a forked child context. The child context is automatically cancelled when the task completes or fails.

Equations

• x.async prio ctx = do let childCtx ← liftM ctx.fork Std.Internal.IO.Async.async (tryFinally (x childCtx) (liftM (childCtx.cancel Std.CancellationReason.cancel))) prio

instance Std.Internal.IO.Async.ContextAsync.instMonadAsyncAsyncTask : MonadAsync AsyncTask ContextAsync

Equations

• Std.Internal.IO.Async.ContextAsync.instMonadAsyncAsyncTask = { async := fun {α : Type} (x : Std.Internal.IO.Async.ContextAsync α) (prio : Task.Priority) => x.async prio }

instance Std.Internal.IO.Async.ContextAsync.instFunctor : Functor ContextAsync

Equations

• Std.Internal.IO.Async.ContextAsync.instFunctor = { map := fun {α β : Type} (f : α → β) (x : Std.Internal.IO.Async.ContextAsync α) (ctx : Std.CancellationContext) => f <$> x ctx }

instance Std.Internal.IO.Async.ContextAsync.instMonad : Monad ContextAsync

Equations

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

instance Std.Internal.IO.Async.ContextAsync.instMonadLiftIO : MonadLift IO ContextAsync

Equations

• Std.Internal.IO.Async.ContextAsync.instMonadLiftIO = { monadLift := fun {α : Type} (x : IO α) (x_1 : Std.CancellationContext) => Std.Internal.IO.Async.Async.ofIOTask (Task.pure <$> x) }

instance Std.Internal.IO.Async.ContextAsync.instMonadLiftBaseIO : MonadLift BaseIO ContextAsync

Equations

• Std.Internal.IO.Async.ContextAsync.instMonadLiftBaseIO = { monadLift := fun {α : Type} (x : BaseIO α) (x_1 : Std.CancellationContext) => liftM (liftM x) }

instance Std.Internal.IO.Async.ContextAsync.instMonadExceptError : MonadExcept IO.Error ContextAsync

Equations

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

instance Std.Internal.IO.Async.ContextAsync.instMonadFinally : MonadFinally ContextAsync

Equations

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

instance Std.Internal.IO.Async.ContextAsync.instInhabited {α : Type} [Inhabited α] : Inhabited (ContextAsync α)

Equations

• Std.Internal.IO.Async.ContextAsync.instInhabited = { default := fun (x : Std.CancellationContext) => default }

instance Std.Internal.IO.Async.ContextAsync.instMonadAwaitAsyncTask : MonadAwait AsyncTask ContextAsync

Equations

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

def Std.Internal.IO.Async.Selector.cancelled : ContextAsync (Selector Unit)

Returns a selector that completes when the current context is cancelled. This is useful for selecting on cancellation alongside other asynchronous operations.

Equations

• Std.Internal.IO.Async.Selector.cancelled = Std.Internal.IO.Async.ContextAsync.doneSelector