def rf_loop

bend-ml-llama@0.2.1.0 · main.bend:1434

import Base

1434# reads the file in blocks of `blk` bytes; k blocks remaining; m is the block already read
1435def 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>):
1436  match k m:
1437    case 0n Tuple{f, r}:
1438      do IO<List<&2, F32>>:
1439        File.close(f)
1440        return List.concat(&2, F32, List.reverse(&2, List<&2, F32>, acc))
1441    case 1n+p Tuple{f, r}:
1442      do IO<List<&2, F32>>:
1443        bs : List<&2, U32> <- IO.pass(List<&2, U32>, r)
1444        m2 : File & Result<&1, &1, U32 & String, List<&2, U32>> <- File.read_at(f, (off + blk : U32), blk)
1445        rf_loop(p, (off + blk : U32), blk, m2, f32s(bs) <> acc)