Documentation

Std.Sync.StreamMap

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) :

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.

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

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

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

      Create an empty StreamMap

      Equations
        Instances For
          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
            Instances For
              def Std.StreamMap.ofArray {α β : Type} [BEq α] (streams : Array (α × AnyAsyncStream β)) :
              StreamMap α β

              Create a StreamMap from an array of named streams

              Equations
                Instances For

                  Get a combined selector that returns the stream name and value

                  Equations
                    Instances For
                      def Std.StreamMap.recv {α β : Type} (stream : StreamMap α β) :

                      Wait for the first value inside of the stream map.

                      Equations
                        Instances For
                          def Std.StreamMap.tryRecv {α β : Type} (stream : StreamMap α β) :

                          Wait for the first value inside of the stream map.

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

                              Remove a stream by name

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

                                  Check if a stream with the given name exists

                                  Equations
                                    Instances For
                                      def Std.StreamMap.size {α β : Type} (sm : StreamMap α β) :

                                      Get the number of registered streams

                                      Equations
                                        Instances For
                                          def Std.StreamMap.isEmpty {α β : Type} (sm : StreamMap α β) :

                                          Check if the StreamMap is empty

                                          Equations
                                            Instances For
                                              def Std.StreamMap.keys {α β : Type} (sm : StreamMap α β) :

                                              Get all registered stream names

                                              Equations
                                                Instances For
                                                  def Std.StreamMap.get? {α β : Type} [BEq α] (sm : StreamMap α β) (name : α) :

                                                  Get a specific stream selector by name

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

                                                      Filter streams based on their names

                                                      Equations
                                                        Instances For

                                                          Convert to array of name-selector pairs

                                                          Equations
                                                            Instances For
                                                              def Std.StreamMap.close {α β : Type} (sm : StreamMap α β) :

                                                              Cleanup function

                                                              Equations
                                                                Instances For