ReduceFiberProof.reduced_blocks: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend as ReduceFiberProof
Lines 662-691 of bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&start_line=662&end_line=691

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/autograd/reduce.bend as Reduce

# A reduced row (left stride 0) walks every digit: the blocks digit ..
# digit + f - 1 of the masked positions are what the walk visits.
def reduced_blocks(+f: Nat, +stride: Nat, +right: Nat, +rest: List<&2, Shape.Row>, +extent: Nat, +others: List<&2, Nat>,
  +target: Nat, +base: Nat, +digit: Nat, +walk: RestWalk(rest, others, target, stride)) ->
  {masked(Nat.mul(f, stride), Shape.Row{stride, 0n, right} <> rest, target, base, Nat.mul(digit, stride)) ==
    visited(Shape.Row{stride, 0n, right} <> rest, extent <> others, f, target, base, digit) : List<&2, Nat>}:
  match f:
    case 0n:
      {==}
    case 1n+g:
      +rows : List<&2, Shape.Row> = Shape.Row{stride, 0n, right} <> rest
      +c = Nat.mul(digit, stride)
      +w = visited(rest, others, Reduce.first_span(rest, others), target, Nat.add(base, Nat.mul(right, digit)), Reduce.first_digit(rest, target))
      +v = visited(rows, extent <> others, g, target, base, 1n+digit)
      %Equal.sym(List<&2, Nat>, masked(Nat.add(stride, Nat.mul(g, stride)), rows, target, base, c),
        List.append(&2, Nat, masked(stride, rows, target, base, c), masked(Nat.mul(g, stride), rows, target, base, Nat.add(c, stride))),
        masked_split(stride, Nat.mul(g, stride), rows, target, base, c)) :
        {_ == List.append(&2, Nat, w, v) : List<&2, Nat>}
      %Equal.sym(List<&2, Nat>, masked(stride, rows, target, base, c), masked(stride, rest, target, Nat.add(base, Nat.mul(right, digit)), 0n),
        block(stride, 0n, right, rest, target, target, base, digit, Free{{==}, {==}})) :
        {List.append(&2, Nat, _, masked(Nat.mul(g, stride), rows, target, base, Nat.add(c, stride))) == List.append(&2, Nat, w, v) : List<&2, Nat>}
      %Equal.sym(List<&2, Nat>, masked(stride, rest, target, Nat.add(base, Nat.mul(right, digit)), 0n), w,
        rest_at(rest, others, target, stride, walk, Nat.add(base, Nat.mul(right, digit)))) :
        {List.append(&2, Nat, _, masked(Nat.mul(g, stride), rows, target, base, Nat.add(c, stride))) == List.append(&2, Nat, w, v) : List<&2, Nat>}
      %next_cursor(digit, stride) :
        {List.append(&2, Nat, w, masked(Nat.mul(g, stride), rows, target, base, _)) == List.append(&2, Nat, w, v) : List<&2, Nat>}
      %Equal.sym(List<&2, Nat>, masked(Nat.mul(g, stride), rows, target, base, Nat.mul(1n+digit, stride)), v,
        reduced_blocks(g, stride, right, rest, extent, others, target, base, 1n+digit, walk)) :
        {List.append(&2, Nat, w, _) == List.append(&2, Nat, w, v) : List<&2, Nat>}
      {==}

Uses (17):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.append
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce.bend&name=first_digit
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce.bend&name=first_span
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=MaskMode
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=RestWalk
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=block
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=masked
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=masked_split
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=next_cursor
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=rest_at
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=visited
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Row