def run_arr

bendtorch-core@0.1.0.0 · src/autograd/reduce_replayed_proof.bend:603

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/api.bend as Api
import bendtorch-core@0.1.0.0/src/autograd/reduce.bend as Reduce

603def run_arr(+stride: Nat, +left: Nat, +right: Nat, +rest: List<&2, Shape.Row>, +extent: Nat, +others: List<&2, Nat>,
604  +single: {Reduce.single_rows(rest, others) == True{} : Bool}, +fuel: Nat, +target: Nat, +base: Nat, +digit: Nat, +accumulator: F32,
605  +h: List<&2, Api.Effect>, +d: Nat, +f: F32) ->
606  {Reduce.strided_run(fuel, right, base, digit, Reduce.single_offset(rest, others, Nat.mod(target, left), 0n), accumulator,
607    Array.get(F32, Api.arr(h, d, f), U32.from_nat(Reduce.strided_offset(right, base, digit, Reduce.single_offset(rest, others, Nat.mod(target, left), 0n))))) ==
608    Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 1n+fuel, target, base, digit, accumulator, Api.arr(h, d, f)) : F32 & Array<F32>}:
609  match fuel:
610    case 0n:
611      +lift = Reduce.single_offset(rest, others, Nat.mod(target, left), 0n)
612      +at = Reduce.strided_offset(right, base, digit, lift)
613      %Equal.sym(Array<F32> & F32, Array.get(F32, Api.arr(h, d, f), U32.from_nat(at)), (Api.arr(h, d, f), word_at(h, d, f, at)), got(h, d, f, U32.from_nat(at))) :
614        {Reduce.strided_run(0n, right, base, digit, lift, accumulator, _) ==
615          Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 1n, target, base, digit, accumulator, Api.arr(h, d, f)) : F32 & Array<F32>}
616      Equal.sym(F32 & Array<F32>,
617        Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 1n, target, base, digit, accumulator, Api.arr(h, d, f)),
618        (F32.add(accumulator, word_at(h, d, f, at)), Api.arr(h, d, f)),
619        step_arr(stride, left, right, rest, extent, others, single, 0n, target, base, digit, accumulator, h, d, f))
620    case 1n+remaining:
621      +lift = Reduce.single_offset(rest, others, Nat.mod(target, left), 0n)
622      +at = Reduce.strided_offset(right, base, digit, lift)
623      +next = F32.add(accumulator, word_at(h, d, f, at))
624      %Equal.sym(Array<F32> & F32, Array.get(F32, Api.arr(h, d, f), U32.from_nat(at)), (Api.arr(h, d, f), word_at(h, d, f, at)), got(h, d, f, U32.from_nat(at))) :
625        {Reduce.strided_run(1n+remaining, right, base, digit, lift, accumulator, _) ==
626          Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 2n+remaining, target, base, digit, accumulator, Api.arr(h, d, f)) : F32 & Array<F32>}
627      Equal.trans(F32 & Array<F32>,
628        Reduce.strided_run(remaining, right, base, 1n+digit, lift, next,
629          Array.get(F32, Api.arr(h, d, f), U32.from_nat(Reduce.strided_offset(right, base, 1n+digit, lift)))),
630        Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 1n+remaining, target, base, 1n+digit, next, Api.arr(h, d, f)),
631        Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 2n+remaining, target, base, digit, accumulator, Api.arr(h, d, f)),
632        run_arr(stride, left, right, rest, extent, others, single, remaining, target, base, 1n+digit, next, h, d, f),
633        Equal.sym(F32 & Array<F32>,
634          Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 2n+remaining, target, base, digit, accumulator, Api.arr(h, d, f)),
635          Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 1n+remaining, target, base, 1n+digit, next, Api.arr(h, d, f)),
636          step_arr(stride, left, right, rest, extent, others, single, 1n+remaining, target, base, digit, accumulator, h, d, f)))