def transpose_decided_permutation

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

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/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/transforms.bend as Transforms
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/tensor/transpose_spec.bend as TransposeSpec

2361def transpose_decided_permutation(+input: Shape.Shape, +a: U32, +b: U32,
2362  decision: Shape.BoolCase<TransposeSpec.valid(input, a, b)>, source: Core.Tensor<input>,
2363  +inside: {True{} == TransposeSpec.valid(input, a, b) : Bool}) ->
2364  {Transforms.transpose_decided(input, source, a, b, decision) == Transforms.permute_copy(input, source, Layout.transpose_axes(Shape.dimensions(input), a, b, 0)) :
2365    Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>}:
2366  match decision:
2367    case Shape.BFalse{equal}:
2368      Empty.absurd({(source, Fail{Transforms.LayoutError{Layout.AxisOutOfBounds{}}}) ==
2369        Transforms.permute_copy(input, source, Layout.transpose_axes(Shape.dimensions(input), a, b, 0)) : Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>},
2370          Arith.clash(Equal.trans(Bool, False{}, TransposeSpec.valid(input, a, b), True{}, equal,
2371            Equal.sym(Bool, True{}, TransposeSpec.valid(input, a, b), inside))))
2372    case Shape.BTrue{equal}:
2373      {==}