def scatter_cells

bendtorch-core@0.1.0.0 · src/tensor/gather_PROOF.bend:593

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

593def scatter_cells(+depth: Nat, +splits: Nat, +kind: Gather.Lookup, +outer: Nat, +rows: Nat, +inner: Nat, +count: Nat, +cells: Nat, +base: Nat,
594  +dg: Nat, -G: Array<F32>, g: Array<F32>, -same: {g == G : Array<F32>}, -valid: Model.Balanced(F32, dg, G), +di: Nat, -I: Array<U32>,
595  index: Array<U32>, -same_index: {index == I : Array<U32>}, -index_valid: Model.Balanced(U32, di, I)) ->
596  Generic.Fact<Generic.Cells(~Gather.Plan, ~Array<F32>, ~Array<U32>, ~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))>:
597  Generic.Fact{path =>
598    {\{Generic.Fact: q => q} : Generic.Fact<Generic.Cells(~Gather.Plan, ~Array<F32>, ~Array<U32>, ~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<F32>, ~Array<U32>, ~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))}(
599      Generic.build_cells(~Gather.Plan, ~Gather.Plan, ~Array<F32>, ~Array<U32>, ~Gather.same, ~Gather.split, ~Gather.scatter_cell,
600        Gather.Plan{kind, outer, rows, inner, count}, (G, I), depth, splits, cells, base, (g, index), both(g, index, G, I, same, same_index),
601        at => inside => {\{Generic.Fact: q => q} :
602          Generic.Fact<{Pair.snd(F32, Array<F32> & Array<U32>, Gather.scatter_cell(Gather.Plan{kind, outer, rows, inner, count}, at, (G, I), inside)) == (G, I) : Array<F32> & Array<U32>}> ->
603          {Pair.snd(F32, Array<F32> & Array<U32>, Gather.scatter_cell(Gather.Plan{kind, outer, rows, inner, count}, at, (G, I), inside)) == (G, I) : Array<F32> & Array<U32>}}(
604          scatter_keeps(kind, outer, rows, inner, count, at, dg, G, di, I, inside, valid, index_valid)),
605        Pair.fst({Pair.fst(Array<F32> & Array<U32>, Array<F32> & Array<U32>, Gather.split((G, I))) == (G, I) : Array<F32> & Array<U32>}, {Pair.snd(Array<F32> & Array<U32>, Array<F32> & Array<U32>, Gather.split((G, I))) == (G, I) : Array<F32> & Array<U32>},
606          {\{Generic.Fact: q => q} : Generic.Fact<SplitFacts(G, I)> -> SplitFacts(G, I)}(split_facts(dg, G, di, I, valid, index_valid))),
607        Pair.snd({Pair.fst(Array<F32> & Array<U32>, Array<F32> & Array<U32>, Gather.split((G, I))) == (G, I) : Array<F32> & Array<U32>}, {Pair.snd(Array<F32> & Array<U32>, Array<F32> & Array<U32>, Gather.split((G, I))) == (G, I) : Array<F32> & Array<U32>},
608          {\{Generic.Fact: q => q} : Generic.Fact<SplitFacts(G, I)> -> SplitFacts(G, I)}(split_facts(dg, G, di, I, valid, index_valid)))))(path)}