def read_all

stelliferous@0.0.2.0 · tensor_file.bend:102

import Base

102# A file longer than its shape stops at the fuel and fails the count.
103def read_all(fuel: Nat,reading: Reading,+count: U32) -> IO(Outcome):
104  match fuel reading:
105    case 0n More{file,target}: closed(file,target,True{})
106    case 0n End{file,target,complete}: closed(file,target,complete)
107    case 1n+rest End{file,target,complete}: closed(file,target,complete)
108    case 1n+rest More{file,target}:
109      do IO<Outcome>:
110        read : Read() <- File.read_bytes(file,(chunk() * 4 : U32))
111        read_all(rest,taken(read,target,count),count)