PermuteBuildProof.scatter_digits: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend as PermuteBuildProof
Lines 109-127 of bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&start_line=109&end_line=127

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/axis_spec.bend as Axis
import bendtorch-core@0.1.0.0/src/tensor/permute_build.bend as Build

# The list `Axis.scatter` builds from the output coordinates of x is the
# picks' coordinates.
def scatter_digits(+rank: Nat, +axes: List<&2, Nat>, +out: List<&2, Nat>, +x: Nat, +cursor: Nat) ->
  {Axis.scatter(U32, rank, axes, Shape.words(Shape.digits(out, x)), cursor) == coordinates_of(Build.picks(rank, axes, out, cursor), x) :
    Maybe<&2, List<&2, U32>>}:
  match rank:
    case 0n:
      {==}
    case 1n+p:
      +position = Axis.position(axes, cursor)
      %Equal.sym(Maybe<&2, U32>, Axis.select(U32, Shape.words(Shape.digits(out, x)), position), coordinate_of(Build.located(out, position), x),
        select_digits(out, x, position)) :
        {Axis.prepend(U32, _, Axis.scatter(U32, p, axes, Shape.words(Shape.digits(out, x)), 1n+cursor)) ==
          coordinates_of(Axis.prepend(Build.Pick, Build.located(out, position), Build.picks(p, axes, out, 1n+cursor)), x) : Maybe<&2, List<&2, U32>>}
      %Equal.sym(Maybe<&2, List<&2, U32>>, Axis.scatter(U32, p, axes, Shape.words(Shape.digits(out, x)), 1n+cursor),
        coordinates_of(Build.picks(p, axes, out, 1n+cursor), x), scatter_digits(p, axes, out, x, 1n+cursor)) :
        {Axis.prepend(U32, coordinate_of(Build.located(out, position), x), _) ==
          coordinates_of(Axis.prepend(Build.Pick, Build.located(out, position), Build.picks(p, axes, out, 1n+cursor)), x) : Maybe<&2, List<&2, U32>>}
      prepend_coordinates(Build.located(out, position), Build.picks(p, axes, out, 1n+cursor), x)

Uses (18):
  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=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=digits
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=words
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_spec.bend&name=position
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_spec.bend&name=prepend
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_spec.bend&name=scatter
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_spec.bend&name=select
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build.bend&name=Pick
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build.bend&name=located
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build.bend&name=picks
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&name=coordinate_of
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&name=coordinates_of
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&name=prepend_coordinates
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&name=select_digits