def g_len

bend-ml-tensor-array@0.1.19.0 · main.bend:1841

import Base

1841# whatever the gemm wrote, reading 1 + p rows back gives 1 + p numbers (G has one constructor, so
1842# matching g opens it, and leaf_len counts the list)
1843def g_len(-r: Nat, -c: Nat, +p: Nat, g: G) -> {bl_len(r, c, bv_g(r, c, p, g)) == 1n+p : Nat}:
1844  match g:
1845    case G{a, b, y}:
1846      zero_out(bl_len(r, c, bv_g2(r, c, b, read_l(p, U32.from_nat(p), Nil{}, Array.get(F32, y, U32.from_nat(p))))), 1n+p, leaf_len(r, c, b, p, U32.from_nat(p), Nil{}, Array.get(F32, y, U32.from_nat(p))))