def rf_loop

bend-ml-llama@0.2.0.0 · main.bend:1130

import Base

1130# reads the file in blocks of `blk` bytes; k blocks remaining; m is the block already read
1131def rf_loop(k: Nat, +off: U32, +blk: U32, m: File & Result<&1, &1, U32 & String, List<&2, U32>>, acc: List<&2, List<&2, F32>>) -> IO(List<&2, F32>):
1132  match k m:
1133    case 0n Tuple{f, r}:
1134      do IO<List<&2, F32>>:
1135        File.close(f)
1136        return List.concat(&2, F32, List.reverse(&2, List<&2, F32>, acc))
1137    case 1n+p Tuple{f, r}:
1138      do IO<List<&2, F32>>:
1139        bs : List<&2, U32> <- IO.pass(List<&2, U32>, r)
1140        m2 : File & Result<&1, &1, U32 & String, List<&2, U32>> <- File.read_at(f, (off + blk : U32), blk)
1141        rf_loop(p, (off + blk : U32), blk, m2, f32s(bs) <> acc)