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
1522
1523
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}