Documentation

Init.Data.Channel

structure IO.Channel.State (α : Type) :

Internal state of an Channel.

We maintain the invariant that at all times either consumers or values is empty.

Instances For
    Equations
    • IO.Channel.instInhabitedState = { default := { values := default, consumers := default, closed := default } }
    def IO.Channel (α : Type) :

    FIFO channel with unbounded buffer, where recv? returns a Task.

    A channel can be closed. Once it is closed, all sends are ignored, and recv? returns none once the queue is empty.

    Equations
    Instances For

      Creates a new Channel.

      Equations
      Instances For
        def IO.Channel.send {α : Type} (v : α) (ch : IO.Channel α) :

        Sends a message on an Channel.

        This function does not block.

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

          Closes an Channel.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            def IO.Channel.recv? {α : Type} (ch : IO.Channel α) :

            Receives a message, without blocking. The returned task waits for the message. Every message is only received once.

            Returns none if the channel is closed and the queue is empty.

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

              ch.forAsync f calls f for every messages received on ch.

              Note that if this function is called twice, each forAsync only gets half the messages.

              Receives all currently queued messages from the channel.

              Those messages are dequeued and will not be returned by recv?.

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

                Type tag for synchronous (blocking) operations on a Channel.

                Equations
                Instances For

                  Accesses synchronous (blocking) version of channel operations.

                  For example, ch.sync.recv? blocks until the next message, and for msg in ch.sync do ... iterates synchronously over the channel. These functions should only be used in dedicated threads.

                  Equations
                  Instances For

                    Synchronously receives a message from the channel.

                    Every message is only received once. Returns none if the channel is closed and the queue is empty.

                    Equations
                    Instances For
                      instance IO.instForInSync {m : TypeType u_1} {α : Type} [MonadLiftT BaseIO m] :

                      for msg in ch.sync do ... receives all messages in the channel until it is closed.

                      Equations