Llm.drain: def of bend-kit-llm@0.13.0.1
Import: import bend-kit-llm@0.13.0.1/llm.bend as Llm
Lines 434-458 of bend-kit-llm@0.13.0.1/llm.bend: https://jend.leeeet.dev/read.txt?path=bend-kit-llm@0.13.0.1/llm.bend&start_line=434&end_line=458

import Base
import bend-kit-http@0.38.1.1/http.bend as Http
import bend-kit-bytes@0.3.3.0/bytes.bend as Bytes

# A refused stream's error body, at most f more pieces, then the stream closed.
def drain(f: Nat, x: Http.Stream & Result<&1, &1, Http.Err, Maybe<&1, Bytes.Bytes>>, acc: Bytes.Bytes) -> IO(Bytes.Bytes):
  match f:
    case 0n:
      (h, r) = x
      do IO<Bytes.Bytes>:
        Http.stream.close(h)
        return acc
    case 1n+g:
      (h, r) = x
      match r:
        case Fail{e}:
          do IO<Bytes.Bytes>:
            Http.stream.close(h)
            return acc
        case Done{m}:
          match m:
            case None{}:
              do IO<Bytes.Bytes>:
                Http.stream.close(h)
                return acc
            case Some{b}:
              do IO<Bytes.Bytes>:
                y : Http.Stream & Result<&1, &1, Http.Err, Maybe<&1, Bytes.Bytes>> <- Http.stream.read(h)
                drain(g, y, Bytes.append(acc, b))

Uses (15):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=IO
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=IO.bind
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=IO.pure
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Unit
  https://jend.leeeet.dev/definition.txt?path=bend-kit-bytes@0.3.3.0/bytes.bend&name=Bytes
  https://jend.leeeet.dev/definition.txt?path=bend-kit-bytes@0.3.3.0/bytes.bend&name=append
  https://jend.leeeet.dev/definition.txt?path=bend-kit-http@0.38.2.0/http.bend&name=Err
  https://jend.leeeet.dev/definition.txt?path=bend-kit-http@0.38.2.0/http.bend&name=Stream
  https://jend.leeeet.dev/definition.txt?path=bend-kit-http@0.38.2.0/http.bend&name=stream.close
  https://jend.leeeet.dev/definition.txt?path=bend-kit-http@0.38.2.0/http.bend&name=stream.read