def run_of

bendtorch-core@0.1.0.0 · src/autograd/reduce_parallel_proof.bend:644

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend as Parallel
import bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend as Generic
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/autograd/reduce.bend as Reduce

644def run_of(+d: Nat, A: Array<F32>, +rows: List<&2, Shape.Row>, +extents: List<&2, Nat>, +position: Nat, -valid: Model.Balanced(F32, d, A)) ->
645  Parallel.Fact<FiberRun<d, A, visited_of(rows, extents, position), 0.0, Reduce.fiber_of(rows, extents, position, A)>>:
646  +fuel = Reduce.first_span(rows, extents)
647  +digit = Reduce.first_digit(rows, position)
648  Parallel.Fact{
649    %Equal.sym(F32 & Array<F32>, Reduce.fiber_of(rows, extents, position, A), Reduce.fiber(rows, extents, fuel, position, 0n, digit, 0.0, A),
650      {\{Generic.Fact: p => p} : Generic.Fact<({Reduce.fiber_of(rows, extents, position, A) == Reduce.fiber(rows, extents, fuel, position, 0n, digit, 0.0, A) : F32 & Array<F32>})> ->
651        {Reduce.fiber_of(rows, extents, position, A) == Reduce.fiber(rows, extents, fuel, position, 0n, digit, 0.0, A) : F32 & Array<F32>}}(
652        fast_fiber(rows, extents, fuel, Reduce.single_below(rows, extents), single_ok(rows, extents, Reduce.single_below(rows, extents), {==}),
653          position, 0n, digit, 0.0, A))) :
654      FiberRun<d, A, visited_of(rows, extents, position), 0.0, _>
655    {\{Parallel.Fact: p => p} : Parallel.Fact<FiberRun<d, A, visited_of(rows, extents, position), 0.0, Reduce.fiber(rows, extents, fuel, position, 0n, digit, 0.0, A)>> ->
656      FiberRun<d, A, visited_of(rows, extents, position), 0.0, Reduce.fiber(rows, extents, fuel, position, 0n, digit, 0.0, A)>}(
657      fiber_run(rows, extents, fuel, position, 0n, digit, d, A, 0.0, A, {==}, valid))}