def cell_word

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

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/observation.bend as Values
import bendtorch-core@0.1.0.0/src/tensor/permute_build.bend as Build
import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement

260# An inside cell holds the input word at `permute_source_index`.
261def cell_word(+input: Shape.Shape, +axes: List<&2, U32>, -a: Array<F32>, +position: Nat) ->
262  Fact<{Pair.fst(F32, Array<F32> & Array<F32>, Build.cell(Build.recipe(Build.Request{input, axes}), position, (a, Array.new(F32, 0n, 0.0)), True{})) ==
263    Refinement.second(F32, Array.get(F32, a, U32.from_nat(Values.permute_source_index(input, axes, position)))) : F32}>:
264  +index = Build.at(Build.recipe(Build.Request{input, axes}), position)
265  Fact{Equal.trans(F32, Pair.fst(F32, Array<F32> & Array<F32>, Build.take(Array.new(F32, 0n, 0.0), Array.get(F32, a, index))),
266    Refinement.second(F32, Array.get(F32, a, index)),
267    Refinement.second(F32, Array.get(F32, a, U32.from_nat(Values.permute_source_index(input, axes, position)))),
268    take_word(Array.new(F32, 0n, 0.0), Array.get(F32, a, index)),
269    Equal.cong(U32, F32, word => Refinement.second(F32, Array.get(F32, a, word)), index,
270      U32.from_nat(Values.permute_source_index(input, axes, position)), source_word(input, axes, position)))}