def run_next

bendtorch-core@0.1.0.0 · src/tensor/batched_matmul_PROOF.bend:158

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
import bendtorch-core@0.1.0.0/src/tensor/matmul.bend as Matrix
import bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend as Parallel

158def run_next(+rest: Nat, +dl: Nat, +dr: Nat, -A: Array<F32>, -B: Array<F32>, +ls: Nat, +rs: Nat, +lp: Nat, +rp: Nat, -accumulator: F32,
159  pl: Array<F32> & F32, pr: Array<F32> & F32, -read: Read<dl, dr, A, B, lp, rp, pl, pr>,
160  -next: @value: F32 -> @-l: Array<F32> -> @-r: Array<F32> -> @-el: {l == A : Array<F32>} -> @-er: {r == B : Array<F32>} ->
161    Parallel.Fact<StridedRun<1n+rest, dl, dr, A, B, ls, rs, Nat.add(ls, lp), Nat.add(rs, rp), value,
162      Matrix.product_run(rest, ls, rs, Nat.add(ls, lp), Nat.add(rs, rp), value,
163        Array.get(F32, l, U32.from_nat(Nat.add(ls, lp))), Array.get(F32, r, U32.from_nat(Nat.add(rs, rp))))>>) ->
164  Parallel.Fact<StridedRun<2n+rest, dl, dr, A, B, ls, rs, lp, rp, accumulator, Matrix.product_run(1n+rest, ls, rs, lp, rp, accumulator, pl, pr)>>:
165  (kl, x) = pl
166  (kr, y) = pr
167  -ex = {\{Read: ex => ey => left_kept => right_kept => ex} : Read<dl, dr, A, B, lp, rp, (kl, x), (kr, y)> ->
168    {Model.observe(F32, dl, A, Refinement.route(dl, U32.from_nat(lp))) == Some{x} : Maybe<&2, F32>}}(read)
169  -ey = {\{Read: ex => ey => left_kept => right_kept => ey} : Read<dl, dr, A, B, lp, rp, (kl, x), (kr, y)> ->
170    {Model.observe(F32, dr, B, Refinement.route(dr, U32.from_nat(rp))) == Some{y} : Maybe<&2, F32>}}(read)
171  -left_kept = {\{Read: ex => ey => left_kept => right_kept => left_kept} : Read<dl, dr, A, B, lp, rp, (kl, x), (kr, y)> ->
172    {kl == A : Array<F32>}}(read)
173  -right_kept = {\{Read: ex => ey => left_kept => right_kept => right_kept} : Read<dl, dr, A, B, lp, rp, (kl, x), (kr, y)> ->
174    {kr == B : Array<F32>}}(read)
175  run_extend(1n+rest, dl, dr, A, B, ls, rs, lp, rp, accumulator, x, y, ex, ey,
176    Matrix.product_run(rest, ls, rs, Nat.add(ls, lp), Nat.add(rs, rp), F32.add(accumulator, F32.mul(x, y)),
177      Array.get(F32, kl, U32.from_nat(Nat.add(ls, lp))), Array.get(F32, kr, U32.from_nat(Nat.add(rs, rp)))),
178    next(F32.add(accumulator, F32.mul(x, y)))(kl)(kr)(left_kept)(right_kept))