SstStreamIo.exact.loop: def of mylsm-lsm-store@0.6.0.1 Import: import mylsm-lsm-store@0.6.0.1/src/SstStreamIo.bend as SstStreamIo Lines 51-91 of mylsm-lsm-store@0.6.0.1/src/SstStreamIo.bend: https://jend.leeeet.dev/read.txt?path=mylsm-lsm-store@0.6.0.1/src/SstStreamIo.bend&start_line=51&end_line=91 import Base import mylsm-lsm-store@0.6.0.1/src/Fs.bend as Fs import bend-kit-bytes@0.3.2.0/bytes.bend as Bytes def exact.loop( fuel: Nat, state: ExactState ) -> IO(File & Result<&1, &1, U32 & String, ExactResult>): match fuel: case 0n: match state: case ExactNeed{file, remaining, chunks}: match remaining: case 0n: exact.complete(file, chunks, True{}) case 1n+_: IO.pure(File & Result<&1, &1, U32 & String, ExactResult>, (file, Fail{(U32.from_nat(7n), "bounded read exhausted")})) case ExactRead{pair, _, _}: match pair: case (file, Fail{error}): IO.pure(File & Result<&1, &1, U32 & String, ExactResult>, (file, Fail{error})) case (file, Done{_}): IO.pure(File & Result<&1, &1, U32 & String, ExactResult>, (file, Fail{(U32.from_nat(7n), "bounded read exhausted")})) case 1n+rest: match state: case ExactNeed{file, +remaining, chunks}: match remaining: case 0n: exact.complete(file, chunks, True{}) case 1n+_: do IO>: next : File & Result<&1, &1, U32 & String, Bytes.Bytes> <- Fs.read_bytes(file, U32.from_nat(Nat.min(1048576n, remaining))) exact.loop(rest, ExactRead{next, remaining, chunks}) case ExactRead{pair, remaining, chunks}: match pair: case (file, Fail{error}): IO.pure(File & Result<&1, &1, U32 & String, ExactResult>, (file, Fail{error})) case (file, Done{Bytes.Bytes{0, _}}): exact.complete(file, chunks, False{}) case (file, Done{Bytes.Bytes{+len, buf}}): exact.loop(rest, ExactNeed{file, (remaining - U32.to_nat(len) : Nat), Con{Bytes.Bytes{len, buf}, chunks}}) Uses (23): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=File 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=List https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.min https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub 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=String https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Con https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Nil 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=mylsm-lsm-store@0.6.0.1/src/Fs.bend&name=read_bytes https://jend.leeeet.dev/definition.txt?path=mylsm-lsm-store@0.6.0.1/src/SstStreamIo.bend&name=ExactResult https://jend.leeeet.dev/definition.txt?path=mylsm-lsm-store@0.6.0.1/src/SstStreamIo.bend&name=ExactState https://jend.leeeet.dev/definition.txt?path=mylsm-lsm-store@0.6.0.1/src/SstStreamIo.bend&name=exact.complete