def permutation_dimensions_order

bendtorch-core@0.1.0.0 · src/tensor/permutation_mapping.bend:424

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
import bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend as AxisAlgebra

424def permutation_dimensions_order(+input: Shape.Shape, +axes: List<&2, U32>, plan: Layout.Plan<input, axes>) ->
425  {Shape.dimensions(Layout.output(input, axes, plan)) == Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes)) : List<&2, U32>}:
426  Layout.Permutation{+output, valid, ordered, count} = plan
427  Equal.cong(Maybe<&2, List<&2, U32>>, List<&2, U32>, Axis.values(U32), Some{Shape.dimensions(output)},
428    Some{Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes))},
429    Equal.trans(Maybe<&2, List<&2, U32>>, Some{Shape.dimensions(output)}, Layout.reorder(Shape.dimensions(input), axes),
430      Some{Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes))}, ordered, AxisAlgebra.permutation_complete(input, axes, valid)))