GatherPROOF.scatter_cells: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend as GatherPROOF Lines 593-608 of bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend&start_line=593&end_line=608 import Base import bendtorch-core@0.1.0.0/src/storage/model.bend as Model import bendtorch-core@0.1.0.0/src/tensor/gather.bend as Gather import bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend as Generic def scatter_cells(+depth: Nat, +splits: Nat, +kind: Gather.Lookup, +outer: Nat, +rows: Nat, +inner: Nat, +count: Nat, +cells: Nat, +base: Nat, +dg: Nat, -G: Array, g: Array, -same: {g == G : Array}, -valid: Model.Balanced(F32, dg, G), +di: Nat, -I: Array, index: Array, -same_index: {index == I : Array}, -index_valid: Model.Balanced(U32, di, I)) -> Generic.Fact, ~Array, ~Gather.scatter_cell, Gather.Plan{kind, outer, rows, inner, count}, (G, I), depth, cells, base, Gather.scatter_build(depth, splits, Gather.Plan{kind, outer, rows, inner, count}, cells, base, g, index))>: Generic.Fact{path => {\{Generic.Fact: q => q} : Generic.Fact, ~Array, ~Gather.scatter_cell, Gather.Plan{kind, outer, rows, inner, count}, (G, I), depth, cells, base, Gather.scatter_build(depth, splits, Gather.Plan{kind, outer, rows, inner, count}, cells, base, g, index))> -> Generic.Cells(~Gather.Plan, ~Array, ~Array, ~Gather.scatter_cell, Gather.Plan{kind, outer, rows, inner, count}, (G, I), depth, cells, base, Gather.scatter_build(depth, splits, Gather.Plan{kind, outer, rows, inner, count}, cells, base, g, index))}( Generic.build_cells(~Gather.Plan, ~Gather.Plan, ~Array, ~Array, ~Gather.same, ~Gather.split, ~Gather.scatter_cell, Gather.Plan{kind, outer, rows, inner, count}, (G, I), depth, splits, cells, base, (g, index), both(g, index, G, I, same, same_index), at => inside => {\{Generic.Fact: q => q} : Generic.Fact<{Pair.snd(F32, Array & Array, Gather.scatter_cell(Gather.Plan{kind, outer, rows, inner, count}, at, (G, I), inside)) == (G, I) : Array & Array}> -> {Pair.snd(F32, Array & Array, Gather.scatter_cell(Gather.Plan{kind, outer, rows, inner, count}, at, (G, I), inside)) == (G, I) : Array & Array}}( scatter_keeps(kind, outer, rows, inner, count, at, dg, G, di, I, inside, valid, index_valid)), Pair.fst({Pair.fst(Array & Array, Array & Array, Gather.split((G, I))) == (G, I) : Array & Array}, {Pair.snd(Array & Array, Array & Array, Gather.split((G, I))) == (G, I) : Array & Array}, {\{Generic.Fact: q => q} : Generic.Fact -> SplitFacts(G, I)}(split_facts(dg, G, di, I, valid, index_valid))), Pair.snd({Pair.fst(Array & Array, Array & Array, Gather.split((G, I))) == (G, I) : Array & Array}, {Pair.snd(Array & Array, Array & Array, Gather.split((G, I))) == (G, I) : Array & Array}, {\{Generic.Fact: q => q} : Generic.Fact -> SplitFacts(G, I)}(split_facts(dg, G, di, I, valid, index_valid)))))(path)} Uses (22): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat 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=U32 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/tensor/gather.bend&name=Lookup https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather.bend&name=Plan https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather.bend&name=same https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather.bend&name=scatter_build https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather.bend&name=scatter_cell https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather.bend&name=split https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend&name=SplitFacts https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend&name=both https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend&name=scatter_keeps https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend&name=split_facts 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