def row_block_run_certified

bendtorch-core@0.1.0.0 · src/tensor/matmul.bend:648

import Base
import bendtorch-core@0.1.0.0/src/tensor/parallel.bend as Parallel

648def row_block_run_certified(fuel: Nat, +lo: Order, +ro: Order, +inner: Nat, +rows: Nat, +columns: Nat, +base: Nat,
649  la: Array<F32>, ra: Array<F32>) ->
650  Parallel.Certified<(Array<F32> & Array<F32>), 3n, row_block_run(fuel, lo, ro, inner, rows, columns, base, la, ra)>:
651  match fuel:
652    case 0n:
653      eight_leaves_of_certified(Eight{0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0}, (la, ra))
654    case 1n+rest:
655      eight_leaves_certified(row_run(rest, stride(lo, rows), stride(ro, columns), read_offset(lo, inner, rows, row_of(columns, base), 0n),
656        read_offset(ro, inner, columns, column_of(columns, base), 0n), read_offset(ro, inner, columns, column_of(columns, Nat.add(1n, base)), 0n), read_offset(ro, inner, columns, column_of(columns, Nat.add(2n, base)), 0n), read_offset(ro, inner, columns, column_of(columns, Nat.add(3n, base)), 0n), read_offset(ro, inner, columns, column_of(columns, Nat.add(4n, base)), 0n), read_offset(ro, inner, columns, column_of(columns, Nat.add(5n, base)), 0n), read_offset(ro, inner, columns, column_of(columns, Nat.add(6n, base)), 0n), read_offset(ro, inner, columns, column_of(columns, Nat.add(7n, base)), 0n),
657        Eight{0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0}, Array.get(F32, la, U32.from_nat(read_offset(lo, inner, rows, row_of(columns, base), 0n))),
658        read_eight(ra, read_offset(ro, inner, columns, column_of(columns, base), 0n), read_offset(ro, inner, columns, column_of(columns, Nat.add(1n, base)), 0n), read_offset(ro, inner, columns, column_of(columns, Nat.add(2n, base)), 0n), read_offset(ro, inner, columns, column_of(columns, Nat.add(3n, base)), 0n), read_offset(ro, inner, columns, column_of(columns, Nat.add(4n, base)), 0n), read_offset(ro, inner, columns, column_of(columns, Nat.add(5n, base)), 0n), read_offset(ro, inner, columns, column_of(columns, Nat.add(6n, base)), 0n), read_offset(ro, inner, columns, column_of(columns, Nat.add(7n, base)), 0n))))