ReduceReplayedProof.pair_join_eq: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/autograd/reduce_replayed_proof.bend as ReduceReplayedProof Lines 794-806 of bendtorch-core@0.1.0.0/src/autograd/reduce_replayed_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_replayed_proof.bend&start_line=794&end_line=806 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/parallel.bend as Parallel # The depth-1 tree: the leaf of cell `base` and the leaf of the cell after # it, which reads the state the first hands back. def pair_join_eq(+plan: Shape.BroadcastPlan, +rows: List<&2, Shape.Row>, +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>}, +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +h: List<&2, Api.Effect>, +d: Nat, +f: F32, +count: Nat, +base: Nat, x: F32, high: F32 & Array & Unit, ex: {ALeaf{x} == out_spec(plan, Shape.Indexed{rows, rows_exact}, shape, fill, ops, count, 0n, base) : Array}, leaf_facts: TreeEq(plan, rows, rows_exact, shape, fill, ops, h, d, f, count, 0n, Nat.add(1n, base), Parallel.leaf(~(Array & Unit), high))) -> TreeEq(plan, rows, rows_exact, shape, fill, ops, h, d, f, count, 1n, base, Parallel.pair_join(~(Array & Unit), x, high)): (y, inputs) = high (ey, kept) = leaf_facts (%Equal.sym(Array, ALeaf{x}, out_spec(plan, Shape.Indexed{rows, rows_exact}, shape, fill, ops, count, 0n, base), ex) : {ANode{_, ALeaf{y}} == ANode{out_spec(plan, Shape.Indexed{rows, rows_exact}, shape, fill, ops, count, 0n, base), out_spec(plan, Shape.Indexed{rows, rows_exact}, shape, fill, ops, count, 0n, Nat.add(1n, base))} : Array} %Equal.sym(Array, ALeaf{y}, out_spec(plan, Shape.Indexed{rows, rows_exact}, shape, fill, ops, count, 0n, Nat.add(1n, base)), ey) : {ANode{out_spec(plan, Shape.Indexed{rows, rows_exact}, shape, fill, ops, count, 0n, base), _} == ANode{out_spec(plan, Shape.Indexed{rows, rows_exact}, shape, fill, ops, count, 0n, base), out_spec(plan, Shape.Indexed{rows, rows_exact}, shape, fill, ops, count, 0n, Nat.add(1n, base))} : Array} {==}, kept) Uses (24): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Unit https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_replayed_proof.bend&name=TreeEq https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_replayed_proof.bend&name=out_spec https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=BroadcastPlan https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Index https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Row https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Shape https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=extents https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=index_table https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=left_shape https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=output_shape https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=right_shape https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/LAWS.bend&name=Op https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/api.bend&name=Effect https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel.bend&name=leaf https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel.bend&name=pair_join