def permuted_output

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

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

1003def permuted_output(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>,
1004  -original: Core.Tensor<input>, -source: Core.Tensor<input>, -target: Core.Tensor<Layout.output(input, axes, plan)>,
1005  prefix: Transforms.Prefix<input, axes, plan, original, source, target,
1006    Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan)))>) ->
1007  Transforms.PermuteOutput<input, axes, original, source, Core.Packed{Layout.output(input, axes, plan), target}>:
1008  Transforms.Prefix{kept, words, checked, written} = prefix
1009  Transforms.PermuteOutput{plan, {==}, kept, words, checked, written,
1010    other => bound => Equal.trans(Maybe<&2, F32>, Core.observe(Layout.output(input, axes, plan), target, U32.from_nat(other)),
1011      Core.checked_observe(Layout.output(input, axes, plan), target, U32.from_nat(other)),
1012      Transforms.expected_output(input, axes, plan, original, U32.from_nat(other)),
1013      {\{ObserveBridge: equal => Equal.sym(Maybe<&2, F32>,
1014        Core.checked_observe(Layout.output(input, axes, plan), target, U32.from_nat(other)),
1015        Core.observe(Layout.output(input, axes, plan), target, U32.from_nat(other)), equal)} :
1016          ObserveBridge<Layout.output(input, axes, plan), target, U32.from_nat(other)> ->
1017            {Core.observe(Layout.output(input, axes, plan), target, U32.from_nat(other)) ==
1018              Core.checked_observe(Layout.output(input, axes, plan), target, U32.from_nat(other)) : Maybe<&2, F32>}}(
1019                observe_bridge(Layout.output(input, axes, plan), target, U32.from_nat(other), checked(other, bound))),
1020      written(other, bound))}