def pair_eq

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

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/LAWS.bend as StorageLaws
import bendtorch-core@0.1.0.0/src/storage/api.bend as Api
import bendtorch-core@0.1.0.0/src/tensor/contracts/matmul_parallel_proof.bend as Par
import bendtorch-core@0.1.0.0/src/tensor/parallel.bend as Parallel
import bendtorch-core@0.1.0.0/src/autograd/reduce.bend as Reduce

808def pair_eq(+plan: Shape.BroadcastPlan, +rows: List<&2, Shape.Row>,
809  +rows_exact: {rows == Shape.index_table(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan))) : List<&2, Shape.Row>},
810  +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +h: List<&2, Api.Effect>, +d: Nat, +f: F32, +count: Nat, +source: Par.Source<shape, fill, ops, h, d, f>, +facts: Facts<plan, shape, count>, +base: Nat, low: F32 & Array<F32> & Unit,
811  leaf_facts: TreeEq(plan, rows, rows_exact, shape, fill, ops, h, d, f, count, 0n, base, Parallel.leaf(~(Array<F32> & Unit), low))) ->
812  TreeEq(plan, rows, rows_exact, shape, fill, ops, h, d, f, count, 1n, base, Parallel.pair(~Reduce.Fibers, ~Array<F32>, ~Unit, ~Reduce.cell_at, Reduce.fibers(Reduce.Fibers{rows, Shape.extents(Shape.output_shape(plan))}), count, base, low)):
813  (x, state) = low
814  (array, none) = state
815  (ex, ek) = leaf_facts
816  %Equal.sym(Array<F32> & Unit, (array, none), (Api.arr(h, d, f), Unit{}), ek) :
817    TreeEq(plan, rows, rows_exact, shape, fill, ops, h, d, f, count, 1n, base, Parallel.pair_join(~(Array<F32> & Unit), x, Reduce.cell_at(Reduce.fibers(Reduce.Fibers{rows, Shape.extents(Shape.output_shape(plan))}), Nat.add(1n, base), _, Nat.is_lt(Nat.add(1n, base), count))))
818  pair_join_eq(plan, rows, rows_exact, shape, fill, ops, h, d, f, count, base, x, Reduce.cell_at(Reduce.fibers(Reduce.Fibers{rows, Shape.extents(Shape.output_shape(plan))}), Nat.add(1n, base), (Api.arr(h, d, f), Unit{}), Nat.is_lt(Nat.add(1n, base), count)), ex,
819    cell_eq(plan, rows, rows_exact, shape, fill, ops, h, d, f, count, source, facts, Nat.add(1n, base), Nat.is_lt(Nat.add(1n, base), count), {==}))