def cell_keeps

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

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/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/autograd/reduce.bend as Reduce

659# Every cell hands the contribution array back.
660def cell_keeps(+d: Nat, A: Array<F32>, +rows: List<&2, Shape.Row>, +extents: List<&2, Nat>, +position: Nat, inside: Bool,
661  -valid: Model.Balanced(F32, d, A)) ->
662  Parallel.Fact<{Pair.snd(F32, Array<F32> & Unit, cell_of(rows, extents, position, A, inside)) == (A, Unit{}) : Array<F32> & Unit}>:
663  match inside:
664    case False{}:
665      Parallel.Fact{{==}}
666    case True{}:
667      Parallel.Fact{{\{FiberRun: words => seen => total => kept =>
668        %Equal.sym(F32 & (Array<F32> & Unit), Reduce.keep(Reduce.fiber_of(rows, extents, position, A), Unit{}),
669          (Pair.fst(F32, Array<F32>, Reduce.fiber_of(rows, extents, position, A)), (Pair.snd(F32, Array<F32>, Reduce.fiber_of(rows, extents, position, A)), Unit{})),
670          keep_equal(Reduce.fiber_of(rows, extents, position, A), Unit{})) :
671          {Pair.snd(F32, Array<F32> & Unit, _) == (A, Unit{}) : Array<F32> & Unit}
672        Equal.cong(Array<F32>, Array<F32> & Unit, a => (a, Unit{}), Pair.snd(F32, Array<F32>, Reduce.fiber_of(rows, extents, position, A)), A, kept)} :
673        FiberRun<d, A, visited_of(rows, extents, position), 0.0, Reduce.fiber_of(rows, extents, position, A)> ->
674        {Pair.snd(F32, Array<F32> & Unit, cell_of(rows, extents, position, A, True{})) == (A, Unit{}) : Array<F32> & Unit}}(
675        {\{Parallel.Fact: p => p} : Parallel.Fact<FiberRun<d, A, visited_of(rows, extents, position), 0.0, Reduce.fiber_of(rows, extents, position, A)>> ->
676          FiberRun<d, A, visited_of(rows, extents, position), 0.0, Reduce.fiber_of(rows, extents, position, A)>}(
677          run_of(d, A, rows, extents, position, valid)))}