def build_cell

bendtorch-core@0.1.0.0 · src/tensor/permute_build_proof.bend:301

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/permute_build.bend as Build
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend as Generic

301# Every slot of the build holds what its cell function computes.
302def build_cell(+depth: Nat, +input: Shape.Shape, +axes: List<&2, U32>, +count: Nat, +d: Nat, -a: Array<F32>, +path: Model.Path(depth),
303  -valid: Model.Balanced(F32, d, a)) ->
304  Fact<{Model.observe(F32, depth, Build.build(depth, Build.Request{input, axes}, count, a), path) ==
305    Some{Pair.fst(F32, Array<F32> & Array<F32>, Build.cell(Build.recipe(Build.Request{input, axes}), Nat.add(Model.offset(depth, path), 0n), (a, Array.new(F32, 0n, 0.0)),
306      Nat.is_lt(Nat.add(Model.offset(depth, path), 0n), count)))} : Maybe<&2, F32>}>:
307  +request : Build.Request = Build.Request{input, axes}
308  Fact{{\{Generic.Fact: q => q} :
309    Generic.Fact<Generic.Cells(~Build.Recipe, ~Array<F32>, ~Array<F32>, ~Build.cell, Build.recipe(request), (a, Array.new(F32, 0n, 0.0)), depth, count, 0n,
310      Build.build(depth, request, count, a))> ->
311    Generic.Cells(~Build.Recipe, ~Array<F32>, ~Array<F32>, ~Build.cell, Build.recipe(request), (a, Array.new(F32, 0n, 0.0)), depth, count, 0n,
312      Build.build(depth, request, count, a))}(
313    Generic.build_cells(~Build.Request, ~Build.Recipe, ~Array<F32>, ~Array<F32>, ~Build.recipe, ~Build.split, ~Build.cell,
314      request, (a, Array.new(F32, 0n, 0.0)), depth, Build.splits(depth), count, 0n, (a, Array.new(F32, 0n, 0.0)), {==},
315      at => inside => {\{Fact: q => q} : Fact<{Pair.snd(F32, Array<F32> & Array<F32>, Build.cell(Build.recipe(request), at, (a, Array.new(F32, 0n, 0.0)), inside)) == (a, Array.new(F32, 0n, 0.0)) : Array<F32> & Array<F32>}> ->
316        {Pair.snd(F32, Array<F32> & Array<F32>, Build.cell(Build.recipe(request), at, (a, Array.new(F32, 0n, 0.0)), inside)) == (a, Array.new(F32, 0n, 0.0)) : Array<F32> & Array<F32>}}(cell_keeps(d, a, request, at, inside, valid)),
317      Pair.fst({Pair.fst(Array<F32> & Array<F32>, Array<F32> & Array<F32>, Build.split((a, Array.new(F32, 0n, 0.0)))) == (a, Array.new(F32, 0n, 0.0)) : Array<F32> & Array<F32>}, {Pair.snd(Array<F32> & Array<F32>, Array<F32> & Array<F32>, Build.split((a, Array.new(F32, 0n, 0.0)))) == (a, Array.new(F32, 0n, 0.0)) : Array<F32> & Array<F32>},
318        {\{Fact: q => q} : Fact<SplitFacts(a)> -> SplitFacts(a)}(split_equal(d, a, valid))),
319      Pair.snd({Pair.fst(Array<F32> & Array<F32>, Array<F32> & Array<F32>, Build.split((a, Array.new(F32, 0n, 0.0)))) == (a, Array.new(F32, 0n, 0.0)) : Array<F32> & Array<F32>}, {Pair.snd(Array<F32> & Array<F32>, Array<F32> & Array<F32>, Build.split((a, Array.new(F32, 0n, 0.0)))) == (a, Array.new(F32, 0n, 0.0)) : Array<F32> & Array<F32>},
320        {\{Fact: q => q} : Fact<SplitFacts(a)> -> SplitFacts(a)}(split_equal(d, a, valid)))))(path)}