def scatter_cells

bendtorch-core@0.1.0.0 · src/tensor/slice_PROOF.bend:690

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/tensor/slice.bend as Slice
import bendtorch-core@0.1.0.0/src/tensor/elementwise.bend as Elementwise
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

690def scatter_cells(+depth: Nat, +splits: Nat, +plan: Slice.Plan, +count: Nat, +base: Nat, +da: Nat, -A: Array<F32>, a: Array<F32>,
691  -same: {a == A : Array<F32>}, -valid: Model.Balanced(F32, da, A)) ->
692  Parallel.Fact<Generic.Cells(~Slice.Plan, ~Array<F32>, ~Array<F32>, ~Slice.scatter_cell, plan, (A, empty()), depth, count, base,
693    Slice.scatter_build(depth, splits, plan, count, base, a))>:
694  Parallel.Fact{path =>
695    {\{Generic.Fact: q => q} :
696      Generic.Fact<Generic.Cells(~Slice.Plan, ~Array<F32>, ~Array<F32>, ~Slice.scatter_cell, plan, (A, empty()), depth, count, base,
697        Slice.scatter_build(depth, splits, plan, count, base, a))> ->
698      Generic.Cells(~Slice.Plan, ~Array<F32>, ~Array<F32>, ~Slice.scatter_cell, plan, (A, empty()), depth, count, base,
699        Slice.scatter_build(depth, splits, plan, count, base, a))}(
700      Generic.build_cells(~Slice.Plan, ~Slice.Plan, ~Array<F32>, ~Array<F32>, ~Slice.same, ~Elementwise.split, ~Slice.scatter_cell,
701        plan, (A, empty()), depth, splits, count, base, (a, empty()), Parallel.pair_equal(a, empty(), A, empty(), same, {==}),
702        at => inside => {\{Parallel.Fact: q => q} :
703          Parallel.Fact<{Pair.snd(F32, Array<F32> & Array<F32>, Slice.scatter_cell(plan, at, (A, empty()), inside)) == (A, empty()) : Array<F32> & Array<F32>}> ->
704          {Pair.snd(F32, Array<F32> & Array<F32>, Slice.scatter_cell(plan, at, (A, empty()), inside)) == (A, empty()) : Array<F32> & Array<F32>}}(
705          scatter_keeps(plan, at, da, A, inside, valid)),
706        Pair.fst({Pair.fst(Array<F32> & Array<F32>, Array<F32> & Array<F32>, Elementwise.split((A, empty()))) == (A, empty()) : Array<F32> & Array<F32>},
707          {Pair.snd(Array<F32> & Array<F32>, Array<F32> & Array<F32>, Elementwise.split((A, empty()))) == (A, empty()) : Array<F32> & Array<F32>},
708          {\{Parallel.Fact: q => q} : Parallel.Fact<SplitFacts(A)> -> SplitFacts(A)}(split_facts(da, A, valid))),
709        Pair.snd({Pair.fst(Array<F32> & Array<F32>, Array<F32> & Array<F32>, Elementwise.split((A, empty()))) == (A, empty()) : Array<F32> & Array<F32>},
710          {Pair.snd(Array<F32> & Array<F32>, Array<F32> & Array<F32>, Elementwise.split((A, empty()))) == (A, empty()) : Array<F32> & Array<F32>},
711          {\{Parallel.Fact: q => q} : Parallel.Fact<SplitFacts(A)> -> SplitFacts(A)}(split_facts(da, A, valid)))))(path)}