def get_band

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

import Base
import bend-ml-tensor-array@0.1.19.0/main.bend as TA

1512# rr x c numbers from number `start` of the tensor at byte lo, into a band of r rows (rr == r, see load_tree; the
1513# Array is sized for rr * c numbers as Mat.zeros would size it)
1514def get_band(path: String, -r: Nat, +rr: Nat, +c: Nat, +lo: U32, +start: Nat) -> IO(TA.Mat<r, c>):
1515  do IO<TA.Mat<r, c>>:
1516    +off : U32 = (lo + U32.from_nat(Nat.mul(start, 2n)) : U32)
1517    f : File <- IO.try(File, File.open(path, "r"))
1518    m : File & Result<&1, &1, U32 & String, List<&2, U32>> <- File.read_at(f, off, U32.from_nat(Nat.min(1048576n, Nat.mul(Nat.mul(rr, c), 2n))))
1519    stream_exact(blocks_of(Nat.mul(Nat.mul(rr, c), 2n), 1048576n), r, c, Nat.mul(Nat.mul(rr, c), 2n), off, 0, m, TA.Mat{Array.new(F32, TA.cap_depth(Nat.mul(rr, c)), 0.0)})