def transpose_requested_certificate

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

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/transform_LAWS.bend as Laws
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/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

2436def transpose_requested_certificate(+input: Shape.Shape, -source: Core.Tensor<input>, +a: U32, +b: U32,
2437  +inside: {True{} == TransposeSpec.valid(input, a, b) : Bool},
2438  certificate: Totality.TypedPermutation<input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), source,
2439    Transforms.permute_copy(input, source, Layout.transpose_axes(Shape.dimensions(input), a, b, 0))>) -> Totality.RequestedTranspose<input, source, a, b>:
2440  Totality.TypedPermutation{+plan, retained, target, exact, prefix} = certificate
2441  Totality.RequestedTranspose{plan, retained, target,
2442    Equal.trans(Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>,
2443      (retained, Done{Core.Packed{Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan), target}}),
2444      Transforms.permute_copy(input, source, Layout.transpose_axes(Shape.dimensions(input), a, b, 0)), Transforms.transpose_copy(input, source, a, b), exact,
2445      Equal.sym(Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>, Transforms.transpose_copy(input, source, a, b),
2446        Transforms.permute_copy(input, source, Layout.transpose_axes(Shape.dimensions(input), a, b, 0)), transpose_permutation(input, source, a, b, inside))),
2447    Equal.trans(List<&2, U32>, Shape.dimensions(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan)),
2448      Axis.order(U32, Shape.dimensions(input), Shape.naturals(Layout.transpose_axes(Shape.dimensions(input), a, b, 0))),
2449      Axis.order(U32, Shape.dimensions(input), Shape.naturals(TransposeSpec.requested_axes(Shape.rank_dimensions(Shape.dimensions(input)), U32.to_nat(a), U32.to_nat(b)))),
2450      Mapping.permutation_dimensions_order(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan),
2451      Equal.cong(List<&2, U32>, List<&2, U32>, axes => Axis.order(U32, Shape.dimensions(input), Shape.naturals(axes)),
2452        Layout.transpose_axes(Shape.dimensions(input), a, b, 0), TransposeSpec.requested_axes(Shape.rank_dimensions(Shape.dimensions(input)), U32.to_nat(a), U32.to_nat(b)),
2453        TransposeProof.transpose_axes_requested(input, a, b, inside))),
2454    prefix, index => mapping =>
2455      %TransposeProof.transpose_axes_requested(input, a, b, inside) :
2456          {Some{Layout.source_index(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index, mapping)} ==
2457            Layout.reference_source_coordinates(Shape.dimensions(input), Axis.scatter(U32, Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(_),
2458              Shape.words(Shape.digits(Shape.extents(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan)), U32.to_nat(index))), 0n)) : Maybe<&2, U32>}
2459      Laws.mapping_reference(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index, mapping),
2460    index => logical =>
2461      {\{Totality.MappingDone: mapping => map_exact =>
2462        {\{Totality.TransposeObservation: equal => equal} :
2463          Totality.TransposeObservation<input, Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan), source, target, a, b, index> ->
2464            {Core.observe(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan), target, index) ==
2465              Totality.reference_observe(input, source, Totality.transpose_reference(input, Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan), a, b, index)) : Maybe<&2, F32>}}(
2466                transpose_observation_mapped(input, a, b, plan, source, retained, target, index, mapping, map_exact, prefix, logical, inside))} :
2467                  Totality.MappingDone<input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index,
2468                    Layout.map_index(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index)> ->
2469                      {Core.observe(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan), target, index) ==
2470                        Totality.reference_observe(input, source, Totality.transpose_reference(input, Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan), a, b, index)) : Maybe<&2, F32>}}(
2471                          mapping_done(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan, index,
2472                            logical_index_bounded(Layout.output(input, Layout.transpose_axes(Shape.dimensions(input), a, b, 0), plan), index, logical)))}