This module provides StreamMap, a container that maps keys to async streams. It allows for dynamic management of multiple named streams with async operations.

inductive Std.AnyAsyncStream (α : Type) : Type 1

This is an existential wrapper for AsyncStream that is used for the .ofArray function with CoeDep so it's easier and we keep StreamMap on Type 0.

• mk {α t : Type} [Internal.Async.IO.AsyncStream t α] : t → AnyAsyncStream α

def Std.AnyAsyncStream.getSelector {α : Type} : AnyAsyncStream α → Internal.IO.Async.Selector α × IO Unit

Equations

• (Std.AnyAsyncStream.mk stream).getSelector = (Std.Internal.Async.IO.AsyncStream.next stream, Std.Internal.Async.IO.AsyncStream.stop stream)

instance Std.instCoeDepAnyAsyncStreamOfAsyncStream {t α : Type} {x : t} [Internal.Async.IO.AsyncStream t α] : CoeDep t x (AnyAsyncStream α)

Equations

• Std.instCoeDepAnyAsyncStreamOfAsyncStream = { coe := Std.AnyAsyncStream.mk x }

structure Std.StreamMap (α β : Type) : Type

A container that maps keys to async streams, enabling dynamic stream management and unified selection operations across multiple named data sources.

• streams : Array (α × Std.Internal.IO.Async.Selector β × IO Unit)

def Std.StreamMap.empty {β α : Type} : StreamMap α β

Create an empty StreamMap

Equations

• Std.StreamMap.empty = { streams := #[] }

def Std.StreamMap.register {α t β : Type} [BEq α] [Internal.Async.IO.AsyncStream t β] (sm : StreamMap α β) (name : α) (reader : t) : StreamMap α β

Register a new async stream with the given name

Equations

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

def Std.StreamMap.ofArray {α β : Type} [BEq α] (streams : Array (α × AnyAsyncStream β)) : StreamMap α β

Create a StreamMap from an array of named streams

Equations

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

def Std.StreamMap.selector {α β : Type} (stream : StreamMap α β) : Internal.IO.Async.Async (Internal.IO.Async.Selector (α × β))

Get a combined selector that returns the stream name and value

Equations

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

def Std.StreamMap.recv {α β : Type} (stream : StreamMap α β) : Internal.IO.Async.Async (α × β)

Wait for the first value inside of the stream map.

Equations

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

def Std.StreamMap.tryRecv {α β : Type} (stream : StreamMap α β) : Internal.IO.Async.Async (Option (α × β))

Wait for the first value inside of the stream map.

Equations

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

def Std.StreamMap.unregister {α β : Type} [BEq α] (sm : StreamMap α β) (name : α) : StreamMap α β

Remove a stream by name

Equations

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

def Std.StreamMap.contains {α β : Type} [BEq α] (sm : StreamMap α β) (name : α) : Bool

Check if a stream with the given name exists

Equations

• sm.contains name = (Std.StreamMap.streams✝ sm).any fun (x : α × Std.Internal.IO.Async.Selector β × IO Unit) => match x with | (n, snd) => n == name

def Std.StreamMap.size {α β : Type} (sm : StreamMap α β) : Nat

Get the number of registered streams

Equations

• sm.size = (Std.StreamMap.streams✝ sm).size

def Std.StreamMap.isEmpty {α β : Type} (sm : StreamMap α β) : Bool

Check if the StreamMap is empty

Equations

• sm.isEmpty = (Std.StreamMap.streams✝ sm).isEmpty

def Std.StreamMap.keys {α β : Type} (sm : StreamMap α β) : Array α

Get all registered stream names

Equations

• sm.keys = Array.map (fun (x : α × Std.Internal.IO.Async.Selector β × IO Unit) => x.fst) (Std.StreamMap.streams✝ sm)

def Std.StreamMap.get? {α β : Type} [BEq α] (sm : StreamMap α β) (name : α) : Option (Internal.IO.Async.Selector β)

Get a specific stream selector by name

Equations

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

def Std.StreamMap.filterByName {α β : Type} (sm : StreamMap α β) (pred : α → Bool) : StreamMap α β

Filter streams based on their names

Equations

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

def Std.StreamMap.toArray {α β : Type} (sm : StreamMap α β) : Array (α × Internal.IO.Async.Selector β)

Convert to array of name-selector pairs

Equations

• sm.toArray = Array.map (fun (x : α × Std.Internal.IO.Async.Selector β × IO Unit) => match x with | (n, s, snd) => (n, s)) (Std.StreamMap.streams✝ sm)

def Std.StreamMap.close {α β : Type} (sm : StreamMap α β) : IO Unit

Cleanup function

Equations

• sm.close = Array.forM (fun (x : α × Std.Internal.IO.Async.Selector β × IO Unit) => match x with | (fst, fst_1, cleanup) => cleanup) (Std.StreamMap.streams✝ sm)