def direct_same

bendtorch-core@0.1.0.0 · src/tensor/elementwise_walk_proof.bend:210

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/elementwise.bend as Elementwise

210# An inside cell whose slots are known is the cell with the walk.
211def direct_same(+operation: Elementwise.Operation, -le: List<&2, Nat>, -re: List<&2, Nat>, -oe: List<&2, Nat>,
212  +map: Shape.Index<le, re, oe>, +left: Elementwise.Slot, +left_exact: {left == Elementwise.left_slot(le, re, oe, map) : Elementwise.Slot},
213  +right: Elementwise.Slot, +right_exact: {right == Elementwise.right_slot(le, re, oe, map) : Elementwise.Slot},
214  +position: Nat, -la: Array<F32>, -ra: Array<F32>) ->
215  {Elementwise.direct_cell(operation, left_at(left, le, re, oe, map, position), right_at(right, le, re, oe, map, position), la, ra) ==
216    Elementwise.cell(operation, le, re, oe, map, position, la, ra, True{}) : F32 & (Array<F32> & Array<F32>)}:
217  +lw = Elementwise.left_walk(le, re, oe, map, position)
218  +rw = Elementwise.right_walk(le, re, oe, map, position)
219  %Equal.sym(Nat, left_at(left, le, re, oe, map, position), lw,
220    %Equal.sym(Elementwise.Slot, left, Elementwise.left_slot(le, re, oe, map), left_exact) :
221      {left_at(_, le, re, oe, map, position) == lw : Nat}
222    left_index(le, re, oe, map, position)) :
223    {Elementwise.cell_left(operation, ra, U32.from_nat(right_at(right, le, re, oe, map, position)), Array.get(F32, la, U32.from_nat(_))) ==
224      Elementwise.cell_left(operation, ra, U32.from_nat(rw), Array.get(F32, la, U32.from_nat(lw))) : F32 & (Array<F32> & Array<F32>)}
225  %Equal.sym(Nat, right_at(right, le, re, oe, map, position), rw,
226    %Equal.sym(Elementwise.Slot, right, Elementwise.right_slot(le, re, oe, map), right_exact) :
227      {right_at(_, le, re, oe, map, position) == rw : Nat}
228    right_index(le, re, oe, map, position)) :
229    {Elementwise.cell_left(operation, ra, U32.from_nat(_), Array.get(F32, la, U32.from_nat(lw))) ==
230      Elementwise.cell_left(operation, ra, U32.from_nat(rw), Array.get(F32, la, U32.from_nat(lw))) : F32 & (Array<F32> & Array<F32>)}
231  {==}