type PermutationRestoration

bendtorch-core@0.1.0.0 · src/tensor/transform_totality.bend:100

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

100type PermutationRestoration<-input: Shape.Shape, -axes: List<&2, U32>, -original: Core.Tensor<input>> is Data:
101  PermutationRestoration{-first: Layout.Plan<input, axes>, -retained: Core.Tensor<input>, -middle: Core.Tensor<Layout.output(input, axes, first)>,
102    -first_exact: {(retained, Done{Core.Packed{Layout.output(input, axes, first), middle}}) == Transforms.permute_copy(input, original, axes) :
103      Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>},
104    -second: Layout.Plan<Layout.output(input, axes, first), inverse_axes(input, axes)>,
105    -middle_retained: Core.Tensor<Layout.output(input, axes, first)>,
106    -restored: Core.Tensor<Layout.output(Layout.output(input, axes, first), inverse_axes(input, axes), second)>,
107    -second_exact: {(Core.Packed{Layout.output(input, axes, first), middle_retained}, Done{Core.Packed{Layout.output(Layout.output(input, axes, first), inverse_axes(input, axes), second), restored}}) ==
108      Transforms.permute_dynamic(Core.Packed{Layout.output(input, axes, first), middle}, inverse_axes(input, axes)) : Core.Dynamic & Result<&2, &1, Transforms.Error, Core.Dynamic>},
109    -dimensions: {Shape.dimensions(Layout.output(Layout.output(input, axes, first), inverse_axes(input, axes), second)) == Shape.dimensions(input) : List<&2, U32>},
110    -linear: @+index: U32 -> @-inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(input))) == True{} : Bool} ->
111      {Core.observe(Layout.output(Layout.output(input, axes, first), inverse_axes(input, axes), second), restored, index) == Core.observe(input, original, index) : Maybe<&2, F32>}}