def missed_k

bendtorch-core@0.1.0.0 · src/tensor/slice_PROOF.bend:826

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/tensor/slice.bend as Slice

826# Input cell (o, i, r) that no k below the length reaches reads nothing.
827def missed_k(+outer: Nat, +extent: Nat, +inner: Nat, +start: Nat, +step: Nat, +length: Nat, +row: Nat, +r: Nat, +i: Nat, +k: Nat,
828  missed: @+k: Nat -> @below: {Nat.is_lt(k, length) == True{} : Bool} -> {Nat.is_eq(Nat.add(start, Nat.mul(k, step)), i) == False{} : Bool},
829  decision: Shape.BoolCase<Slice.hits(start, step, length, i, k)>) ->
830  {picked_k(outer, extent, inner, start, step, length, row, r, i, k) == None{} : Maybe<&2, Nat>}:
831  match decision:
832    case Shape.BFalse{equal}:
833      %equal : {Slice.picked(Slice.Plan{outer, extent, inner, start, step, length}, row, r, i, k, _) == None{} : Maybe<&2, Nat>}
834      {==}
835    case Shape.BTrue{equal}:
836      +rest = Arith.and_right(Nat.is_le(start, i), Bool.and(Nat.is_lt(k, length), Nat.is_eq(Nat.add(start, Nat.mul(k, step)), i)),
837        Equal.sym(Bool, True{}, Slice.hits(start, step, length, i, k), equal))
838      Empty.absurd({picked_k(outer, extent, inner, start, step, length, row, r, i, k) == None{} : Maybe<&2, Nat>},
839        Arith.clash(Equal.trans(Bool, False{}, Nat.is_eq(Nat.add(start, Nat.mul(k, step)), i), True{},
840          Equal.sym(Bool, Nat.is_eq(Nat.add(start, Nat.mul(k, step)), i), False{},
841            missed(k, Arith.and_left(Nat.is_lt(k, length), Nat.is_eq(Nat.add(start, Nat.mul(k, step)), i), rest))),
842          Arith.and_right(Nat.is_lt(k, length), Nat.is_eq(Nat.add(start, Nat.mul(k, step)), i), rest))))