ReduceParallelProof.build_cells: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend as ReduceParallelProof Lines 714-746 of bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend&start_line=714&end_line=746 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 # Whatever the split, every cell of the parallel build holds what CellIs # names: the generic law of `Parallel.build`, with the reduce cell. def build_cells(+depth: Nat, +splits: Nat, +d: Nat, -A: Array, +rows: List<&2, Shape.Row>, +extents: List<&2, Nat>, +count: Nat, +base: Nat, array: Array, -same: {array == A : Array}, -valid: Model.Balanced(F32, d, A)) -> Parallel.Fact: -split = {\{Parallel.Fact: q => q} : Parallel.Fact<({Pair.fst(Array & Unit, Array & Unit, Reduce.halves(Array.clone(F32, A))) == (A, Unit{}) : Array & Unit} & {Pair.snd(Array & Unit, Array & Unit, Reduce.halves(Array.clone(F32, A))) == (A, Unit{}) : Array & Unit})> -> {Pair.fst(Array & Unit, Array & Unit, Reduce.halves(Array.clone(F32, A))) == (A, Unit{}) : Array & Unit} & {Pair.snd(Array & Unit, Array & Unit, Reduce.halves(Array.clone(F32, A))) == (A, Unit{}) : Array & Unit}}( halves_equal(d, A, Array.clone(F32, A), {==}, valid)) -cells = {\{Generic.Fact: q => q} : Generic.Fact, ~Unit, ~Reduce.cell_at, Reduce.fibers(Reduce.Fibers{rows, extents}), (A, Unit{}), depth, count, base, Reduce.build(depth, splits, rows, extents, count, base, array))> -> Generic.Cells(~Reduce.Fibers, ~Array, ~Unit, ~Reduce.cell_at, Reduce.fibers(Reduce.Fibers{rows, extents}), (A, Unit{}), depth, count, base, Reduce.build(depth, splits, rows, extents, count, base, array))}( Generic.build_cells(~Reduce.Fibers, ~Reduce.Fibers, ~Array, ~Unit, ~Reduce.fibers, ~Reduce.split, ~Reduce.cell_at, Reduce.Fibers{rows, extents}, (A, Unit{}), depth, splits, count, base, (array, Unit{}), Equal.cong(Array, Array & Unit, a => (a, Unit{}), array, A, same), at => inside => {\{Parallel.Fact: q => q} : Parallel.Fact<({Pair.snd(F32, Array & Unit, cell_of(rows, extents, at, A, inside)) == (A, Unit{}) : Array & Unit})> -> {Pair.snd(F32, Array & Unit, cell_of(rows, extents, at, A, inside)) == (A, Unit{}) : Array & Unit}}( cell_keeps(d, A, rows, extents, at, inside, valid)), Pair.fst({Pair.fst(Array & Unit, Array & Unit, Reduce.halves(Array.clone(F32, A))) == (A, Unit{}) : Array & Unit}, {Pair.snd(Array & Unit, Array & Unit, Reduce.halves(Array.clone(F32, A))) == (A, Unit{}) : Array & Unit}, split), Pair.snd({Pair.fst(Array & Unit, Array & Unit, Reduce.halves(Array.clone(F32, A))) == (A, Unit{}) : Array & Unit}, {Pair.snd(Array & Unit, Array & Unit, Reduce.halves(Array.clone(F32, A))) == (A, Unit{}) : Array & Unit}, split))) Parallel.Fact{path => {\{Parallel.Fact: q => q} : Parallel.Fact -> CellSpec(d, A, rows, extents, Nat.add(Model.offset(depth, path), base), Nat.is_lt(Nat.add(Model.offset(depth, path), base), count), Model.observe(F32, depth, Reduce.build(depth, splits, rows, extents, count, base, array), path))}( cell_spec(d, A, rows, extents, Nat.add(Model.offset(depth, path), base), Nat.is_lt(Nat.add(Model.offset(depth, path), base), count), Model.observe(F32, depth, Reduce.build(depth, splits, rows, extents, count, base, array), path), cells(path), valid))} Uses (33): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.clone https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong 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=Nat.is_lt https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.fst https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.snd 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.bend&name=Fibers https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce.bend&name=build https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce.bend&name=cell_at https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce.bend&name=fibers https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce.bend&name=halves https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce.bend&name=split https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend&name=CellSpec https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend&name=Cells https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend&name=cell_keeps https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend&name=cell_of https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend&name=cell_spec https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend&name=halves_equal 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/storage/model.bend&name=Balanced https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=observe https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=offset https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend&name=Fact https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&name=Cells https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&name=Fact https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&name=build_cells