def transpose_output_axes

bendtorch-core@0.1.0.0 · src/tensor/transform_PROOF.bend:2487

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/transform_totality.bend as Totality
import bendtorch-core@0.1.0.0/src/tensor/permutation_mapping.bend as Mapping
import bendtorch-core@0.1.0.0/src/tensor/transpose_PROOF.bend as TransposeProof
import bendtorch-core@0.1.0.0/src/tensor/transpose_spec.bend as TransposeSpec

2487def transpose_output_axes(+input: Shape.Shape, +a: U32, +b: U32,
2488  +plan: Layout.Plan<input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0)>,
2489  +inside: {True{} == TransposeSpec.valid(input, a, b) : Bool}) ->
2490  {Layout.transpose_axes(Shape.dimensions(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan)), a, b, 0) ==
2491    Totality.inverse_axes(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0)) : List<&2, U32>}:
2492  Equal.trans(List<&2, U32>, Layout.transpose_axes(Shape.dimensions(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan)), a, b, 0),
2493    TransposeSpec.requested_axes(Shape.rank_dimensions(Shape.dimensions(input)), U32.to_nat(a), U32.to_nat(b)),
2494    Totality.inverse_axes(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0)),
2495    Equal.trans(List<&2, U32>, Layout.transpose_axes(Shape.dimensions(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan)), a, b, 0),
2496      TransposeSpec.requested_axes(Shape.rank_dimensions(Shape.dimensions(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan))), U32.to_nat(a), U32.to_nat(b)),
2497      TransposeSpec.requested_axes(Shape.rank_dimensions(Shape.dimensions(input)), U32.to_nat(a), U32.to_nat(b)),
2498      TransposeProof.transpose_axes_requested(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan), a, b, transpose_output_inside(input, a, b, plan, inside)),
2499      Equal.cong(Nat, List<&2, U32>, rank => TransposeSpec.requested_axes(rank, U32.to_nat(a), U32.to_nat(b)),
2500        Shape.rank_dimensions(Shape.dimensions(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan))),
2501        Shape.rank_dimensions(Shape.dimensions(input)), Mapping.permutation_output_rank(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan))),
2502    Equal.trans(List<&2, U32>, TransposeSpec.requested_axes(Shape.rank_dimensions(Shape.dimensions(input)), U32.to_nat(a), U32.to_nat(b)),
2503      Layout.transpose_axes(Shape.dimensions(input), a, b, 0), Totality.inverse_axes(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0)),
2504      Equal.sym(List<&2, U32>, Layout.transpose_axes(Shape.dimensions(input), a, b, 0),
2505        TransposeSpec.requested_axes(Shape.rank_dimensions(Shape.dimensions(input)), U32.to_nat(a), U32.to_nat(b)), TransposeProof.transpose_axes_requested(input, a, b, inside)),
2506      Equal.sym(List<&2, U32>, Totality.inverse_axes(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0)), Layout.transpose_axes(Shape.dimensions(input), a, b, 0),
2507        Equal.trans(List<&2, U32>, Totality.inverse_axes(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0)),
2508          Shape.words(Shape.naturals(Layout.transpose_axes(Shape.dimensions(input), a, b, 0))), Layout.transpose_axes(Shape.dimensions(input), a, b, 0),
2509          Equal.cong(List<&2, Nat>, List<&2, U32>, Shape.words,
2510            Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(Layout.transpose_axes(Shape.dimensions(input), a, b, 0))),
2511            Shape.naturals(Layout.transpose_axes(Shape.dimensions(input), a, b, 0)), TransposeProof.inverse_axes(input, a, b, inside)),
2512          words_naturals(Layout.transpose_axes(Shape.dimensions(input), a, b, 0))))))