def cell_by_same

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

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

233# With the slots `left_slot` and `right_slot` pick, the cell of a build is
234# the cell with the walk.
235def cell_by_same(+operation: Elementwise.Operation, -le: List<&2, Nat>, -re: List<&2, Nat>, -oe: List<&2, Nat>,
236  +map: Shape.Index<le, re, oe>, inside: Bool, left: Elementwise.Slot, +left_exact: {left == Elementwise.left_slot(le, re, oe, map) : Elementwise.Slot},
237  right: Elementwise.Slot, +right_exact: {right == Elementwise.right_slot(le, re, oe, map) : Elementwise.Slot},
238  +position: Nat, -la: Array<F32>, -ra: Array<F32>) ->
239  {Elementwise.cell_by(inside, left, right, operation, le, re, oe, map, position, la, ra) ==
240    Elementwise.cell(operation, le, re, oe, map, position, la, ra, inside) : F32 & (Array<F32> & Array<F32>)}:
241  match inside left right:
242    case False{} left right:
243      {==}
244    case True{} Elementwise.OwnSlot{} Elementwise.OwnSlot{}:
245      direct_same(operation, le, re, oe, map, Elementwise.OwnSlot{}, left_exact, Elementwise.OwnSlot{}, right_exact, position, la, ra)
246    case True{} Elementwise.OwnSlot{} Elementwise.FirstSlot{}:
247      direct_same(operation, le, re, oe, map, Elementwise.OwnSlot{}, left_exact, Elementwise.FirstSlot{}, right_exact, position, la, ra)
248    case True{} Elementwise.OwnSlot{} Elementwise.WalkedSlot{}:
249      direct_same(operation, le, re, oe, map, Elementwise.OwnSlot{}, left_exact, Elementwise.WalkedSlot{}, right_exact, position, la, ra)
250    case True{} Elementwise.FirstSlot{} Elementwise.OwnSlot{}:
251      direct_same(operation, le, re, oe, map, Elementwise.FirstSlot{}, left_exact, Elementwise.OwnSlot{}, right_exact, position, la, ra)
252    case True{} Elementwise.FirstSlot{} Elementwise.FirstSlot{}:
253      direct_same(operation, le, re, oe, map, Elementwise.FirstSlot{}, left_exact, Elementwise.FirstSlot{}, right_exact, position, la, ra)
254    case True{} Elementwise.FirstSlot{} Elementwise.WalkedSlot{}:
255      direct_same(operation, le, re, oe, map, Elementwise.FirstSlot{}, left_exact, Elementwise.WalkedSlot{}, right_exact, position, la, ra)
256    case True{} Elementwise.WalkedSlot{} Elementwise.OwnSlot{}:
257      direct_same(operation, le, re, oe, map, Elementwise.WalkedSlot{}, left_exact, Elementwise.OwnSlot{}, right_exact, position, la, ra)
258    case True{} Elementwise.WalkedSlot{} Elementwise.FirstSlot{}:
259      direct_same(operation, le, re, oe, map, Elementwise.WalkedSlot{}, left_exact, Elementwise.FirstSlot{}, right_exact, position, la, ra)
260    case True{} Elementwise.WalkedSlot{} Elementwise.WalkedSlot{}:
261      {==}