AxisAlgebra.reorder: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend as AxisAlgebra
Lines 33-43 of bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&start_line=33&end_line=43

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

def reorder(+axes: List<&2, U32>, +values: List<&2, U32>) ->
  {Layout.reorder(values, axes) == Axis.gather(U32, values, Shape.naturals(axes)) : Maybe<&2, List<&2, U32>>}:
  match axes:
    case Nil{}:
      {==}
    case +axis <> +tail:
      %Equal.sym(Maybe<&2, U32>, Layout.lookup(values, U32.to_nat(axis)), Axis.lookup(U32, values, U32.to_nat(axis)), lookup(values, U32.to_nat(axis))) :
        {Layout.reorder_head(value => Layout.reorder_tail(value, Layout.reorder(values, tail)), _) == Axis.prepend(U32, Axis.lookup(U32, values, U32.to_nat(axis)), Axis.gather(U32, values, Shape.naturals(tail))) : Maybe<&2, List<&2, U32>>}
      %Equal.sym(Maybe<&2, List<&2, U32>>, Layout.reorder(values, tail), Axis.gather(U32, values, Shape.naturals(tail)), reorder(tail, values)) :
        {Layout.reorder_head(value => Layout.reorder_tail(value, _), Axis.lookup(U32, values, U32.to_nat(axis))) == Axis.prepend(U32, Axis.lookup(U32, values, U32.to_nat(axis)), Axis.gather(U32, values, Shape.naturals(tail))) : Maybe<&2, List<&2, U32>>}
      reorder_step(Axis.lookup(U32, values, U32.to_nat(axis)), Axis.gather(U32, values, Shape.naturals(tail)))

Uses (15):
  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=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=naturals
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=lookup
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=reorder_step
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_spec.bend&name=gather
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_spec.bend&name=lookup
  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/layout.bend&name=lookup
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/layout.bend&name=reorder
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/layout.bend&name=reorder_head
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/layout.bend&name=reorder_tail