def load_tree

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

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

1521# fills a tree of 2^d bands (TA.Bands.zeros's shape: each node halves its rows with TA.half) in row order; rr is r at
1522# run time. The tree is walked by its depth, not built first with TA.Bands.zeros and matched: that tree's zero-filled
1523# arrays were dropped unread (NOTES.md, 2026-11-01)
1524def load_tree(+c: Nat, -r: Nat, +d: Nat, +rr: Nat, -e: {rr == r : Nat}, +path: String, +lo: U32, +start: Nat) -> IO(TA.Bands<r, c>):
1525  match d:
1526    case 0n:
1527      do IO<TA.Bands<r, c>>:
1528        band : TA.Mat<r, c> <- get_band(path, r, rr, c, lo, start)
1529        return TA.BLeaf{band}
1530    case 1n+q:
1531      do IO<TA.Bands<r, c>>:
1532        x2 : TA.Bands<TA.half(r), c> <- load_tree(c, TA.half(r), q, TA.half(rr), TA.eq_half(rr, r, e), path, lo, start)
1533        y2 : TA.Bands<Nat.sub(r, TA.half(r)), c> <- load_tree(c, Nat.sub(r, TA.half(r)), q, Nat.sub(rr, TA.half(rr)), TA.eq_rest(rr, r, e), path, lo, Nat.add(start, Nat.mul(TA.half(rr), c)))
1534        return TA.BNode{x2, y2}

Uses (15)

Used by (1)