def build_cells

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

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

664# Every slot of the forward build holds what its cell computes from (A, []).
665# The Fact holds the cells eta-expanded: `--verdict` rejects the unexpanded
666# function in this position although `--check-only` accepts it.
667def build_cells(+depth: Nat, +splits: Nat, +plan: Slice.Plan, +count: Nat, +base: Nat, +da: Nat, -A: Array<F32>, a: Array<F32>,
668  -same: {a == A : Array<F32>}, -valid: Model.Balanced(F32, da, A)) ->
669  Parallel.Fact<Generic.Cells(~Slice.Plan, ~Array<F32>, ~Array<F32>, ~Slice.cell, plan, (A, empty()), depth, count, base,
670    Slice.build(depth, splits, plan, count, base, a))>:
671  Parallel.Fact{path =>
672    {\{Generic.Fact: q => q} :
673      Generic.Fact<Generic.Cells(~Slice.Plan, ~Array<F32>, ~Array<F32>, ~Slice.cell, plan, (A, empty()), depth, count, base,
674        Slice.build(depth, splits, plan, count, base, a))> ->
675      Generic.Cells(~Slice.Plan, ~Array<F32>, ~Array<F32>, ~Slice.cell, plan, (A, empty()), depth, count, base,
676        Slice.build(depth, splits, plan, count, base, a))}(
677      Generic.build_cells(~Slice.Plan, ~Slice.Plan, ~Array<F32>, ~Array<F32>, ~Slice.same, ~Elementwise.split, ~Slice.cell,
678        plan, (A, empty()), depth, splits, count, base, (a, empty()), Parallel.pair_equal(a, empty(), A, empty(), same, {==}),
679        at => inside => {\{Parallel.Fact: q => q} :
680          Parallel.Fact<{Pair.snd(F32, Array<F32> & Array<F32>, Slice.cell(plan, at, (A, empty()), inside)) == (A, empty()) : Array<F32> & Array<F32>}> ->
681          {Pair.snd(F32, Array<F32> & Array<F32>, Slice.cell(plan, at, (A, empty()), inside)) == (A, empty()) : Array<F32> & Array<F32>}}(
682          cell_keeps(plan, at, da, A, inside, valid)),
683        Pair.fst({Pair.fst(Array<F32> & Array<F32>, Array<F32> & Array<F32>, Elementwise.split((A, empty()))) == (A, empty()) : Array<F32> & Array<F32>},
684          {Pair.snd(Array<F32> & Array<F32>, Array<F32> & Array<F32>, Elementwise.split((A, empty()))) == (A, empty()) : Array<F32> & Array<F32>},
685          {\{Parallel.Fact: q => q} : Parallel.Fact<SplitFacts(A)> -> SplitFacts(A)}(split_facts(da, A, valid))),
686        Pair.snd({Pair.fst(Array<F32> & Array<F32>, Array<F32> & Array<F32>, Elementwise.split((A, empty()))) == (A, empty()) : Array<F32> & Array<F32>},
687          {Pair.snd(Array<F32> & Array<F32>, Array<F32> & Array<F32>, Elementwise.split((A, empty()))) == (A, empty()) : Array<F32> & Array<F32>},
688          {\{Parallel.Fact: q => q} : Parallel.Fact<SplitFacts(A)> -> SplitFacts(A)}(split_facts(da, A, valid)))))(path)}