Redis.read.loop: def of bend-kit-redis@0.3.1.0
Import: import bend-kit-redis@0.3.1.0/redis.bend as Redis
Lines 775-798 of bend-kit-redis@0.3.1.0/redis.bend: https://jend.leeeet.dev/read.txt?path=bend-kit-redis@0.3.1.0/redis.bend&start_line=775&end_line=798

import Base

# One recv per step. 2^24 reads of up to 64 KiB pass Redis's 512 MiB bulk limit.
def read.loop(fuel: Nat, st: Rd) -> IO(Result<&1, &1, Failure, Conn & Val>):
  match fuel:
    case 0n:
      match st:
        case RNext{tls, sock, key, ms, r}:
          read.fail(tls, sock, Malformed{})
        case RFail{tls, sock, why}:
          read.fail(tls, sock, why)
    case 1n+f:
      match st:
        case RFail{tls, sock, why}:
          read.fail(tls, sock, why)
        case RNext{+tls, sock, +key, +ms, r}:
          (rd, nx) = r
          match nx:
            case Got{v}:
              IO.pure(Result<&1, &1, Failure, Conn & Val>, Done{(Conn{tls, sock, rd, key, ms}, v)})
            case Broken{}:
              read.fail(tls, sock, Malformed{})
            case Want{}:
              do IO<Result<&1, &1, Failure, Conn & Val>>:
                m : Socket & Result<&1, &1, U32 & String, U32 & Array<U32>> <- io.recv(tls, sock, ms)
                read.loop(f, got(tls, key, ms, rd, m))

Uses (19):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  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=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=Socket
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-kit-redis@0.3.1.0/redis.bend&name=Conn
  https://jend.leeeet.dev/definition.txt?path=bend-kit-redis@0.3.1.0/redis.bend&name=Failure
  https://jend.leeeet.dev/definition.txt?path=bend-kit-redis@0.3.1.0/redis.bend&name=Next
  https://jend.leeeet.dev/definition.txt?path=bend-kit-redis@0.3.1.0/redis.bend&name=Rd
  https://jend.leeeet.dev/definition.txt?path=bend-kit-redis@0.3.1.0/redis.bend&name=Val
  https://jend.leeeet.dev/definition.txt?path=bend-kit-redis@0.3.1.0/redis.bend&name=got
  https://jend.leeeet.dev/definition.txt?path=bend-kit-redis@0.3.1.0/redis.bend&name=io.recv
  https://jend.leeeet.dev/definition.txt?path=bend-kit-redis@0.3.1.0/redis.bend&name=read.fail