def shifted_off

bendtorch-core@0.1.0.0 · src/autograd/reduce_fiber_proof.bend:513

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

513def shifted_off(+n: Nat, +stride: Nat, +left: Nat, +right: Nat, +rest: List<&2, Shape.Row>, +target: Nat, +base: Nat,
514  +digit: Nat, +q: Nat, +room: {Nat.is_le(Nat.add(q, n), stride) == True{} : Bool}, +mode: OffMode<rest, left, stride, digit, target>) ->
515  {masked(n, Shape.Row{stride, left, right} <> rest, target, base, Nat.add(Nat.mul(digit, stride), q)) == Nil{} : List<&2, Nat>}:
516  match n:
517    case 0n:
518      {==}
519    case 1n+m:
520      +rows : List<&2, Shape.Row> = Shape.Row{stride, left, right} <> rest
521      +c = Nat.add(Nat.mul(digit, stride), q)
522      +below = lt_of_room(q, m, stride, room)
523      +dq = div_of(c, stride, digit, q, below, {==})
524      +mq = mod_of(c, stride, digit, q, below, {==})
525      +tail = masked(m, rows, target, base, 1n+c)
526      +position = Nat.add(base, Shape.walk_right(rows, c))
527      %Equal.sym(Nat, Nat.div(c, stride), digit, dq) :
528        {kept(Nat.is_eq(Nat.add(Nat.mul(left, _), Shape.walk_left(rest, Nat.mod(c, stride))), target), position, tail) == Nil{} : List<&2, Nat>}
529      %Equal.sym(Nat, Nat.mod(c, stride), q, mq) :
530        {kept(Nat.is_eq(Nat.add(Nat.mul(left, digit), Shape.walk_left(rest, _)), target), position, tail) == Nil{} : List<&2, Nat>}
531      %off_mask(rest, left, stride, digit, target, mode, q, below) :
532        {kept(_, position, tail) == Nil{} : List<&2, Nat>}
533      %Arith.add_succ(Nat.mul(digit, stride), q) : {masked(m, rows, target, base, _) == Nil{} : List<&2, Nat>}
534      shifted_off(m, stride, left, right, rest, target, base, digit, 1n+q, le_step(q, m, stride, room), mode)