def transfer.loop

bend-kit-stream@0.3.1.0 · stream.bend:118

import Base

118# cap+1 reads suffice even if every successful nonempty read contains one byte.
119# Fuel is first among runtime parameters; no fixed read ceiling or unsafe recursion.
120def transfer.loop(~S: Type, ~D: Type,
121  ~read: S -> U32 -> Bool -> U32 -> IO(S & Result<&1, &1, U32 & String, U32 & Array<U32>>),
122  ~write: D -> U32 -> Array<U32> -> Bool -> IO(D & Result<&1, &1, U32 & String, Unit>),
123  fuel: Nat, state: Transfer<S, D>, +tls: Bool, +chunk: U32, +cap: U32, +ms: U32) ->
124  IO(S & D & Outcome):
125  match fuel:
126    case 0n:
127      match state:
128        case Stop{source, destination, outcome}:
129          IO.pure(S & D & Outcome, (source, destination, outcome))
130        case More{source, destination, count}:
131          # Unreachable under the read.words bounds and positive-progress contract.
132          IO.pure(S & D & Outcome, (source, destination, Failed{count, Limit{}}))
133    case 1n+rest:
134      match state:
135        case Stop{source, destination, outcome}:
136          IO.pure(S & D & Outcome, (source, destination, outcome))
137        case More{source, destination, +count}:
138          +remaining = (cap - count : U32)
139          do IO<S & D & Outcome>:
140            pair : S & Result<&1, &1, U32 & String, U32 & Array<U32>> <-
141              read(source, request(chunk, remaining), tls, ms)
142            next : Transfer<S, D> <- transfer.read(~S, ~D, ~write,
143              pair, destination, count, remaining, tls)
144            transfer.loop(~S, ~D, ~read, ~write, rest, next, tls, chunk, cap, ms)