def left_pick

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

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

167# The slot `left_slot` picks is where the walk of every position lands.
168def left_pick(-le: List<&2, Nat>, -re: List<&2, Nat>, -oe: List<&2, Nat>, +rows: List<&2, Shape.Row>,
169  +exact: {rows == Shape.index_table(le, re, oe) : List<&2, Shape.Row>},
170  same: Bool, +same_exact: {same == Elementwise.same_left(rows) : Bool},
171  zero: Bool, +zero_exact: {zero == Elementwise.zero_left(rows) : Bool}, +i: Nat) ->
172  {left_at(Elementwise.slot_of(same, zero), le, re, oe, Shape.Indexed{rows, exact}, i) == Shape.walk_left(rows, i) : Nat}:
173  match same zero:
174    case True{} zero:
175      Equal.sym(Nat, Shape.walk_left(rows, i), i, walk_left_same(rows, Equal.sym(Bool, True{}, Elementwise.same_left(rows), same_exact), i))
176    case False{} True{}:
177      Equal.sym(Nat, Shape.walk_left(rows, i), 0n, walk_left_zero(rows, Equal.sym(Bool, True{}, Elementwise.zero_left(rows), zero_exact), i))
178    case False{} False{}:
179      {==}