def inverse_words_valid

bendtorch-core@0.1.0.0 · src/tensor/permutation_mapping.bend:509

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/shape/coordinate_proofs.bend as Coordinates
import bendtorch-core@0.1.0.0/src/tensor/axis_spec.bend as Axis
import bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend as AxisAlgebra

509def inverse_words_valid(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +coordinate: Layout.CheckedCoordinate<Layout.output(input, axes, plan)>,
510  +values: List<&2, U32>, inverse: {Some{values} == Layout.inverse_coordinates(Shape.dimensions(input), axes, Layout.coordinate_values(Layout.output(input, axes, plan), coordinate), 0) : Maybe<&2, List<&2, U32>>}) ->
511  Layout.WordsValid(Shape.dimensions(input), values):
512  Layout.Permutation{+output, +accepted, +ordered, +count} = plan
513  Layout.CWord{+coordinates, +valid} = coordinate
514  %Equal.sym(List<&2, U32>, values, Axis.order(U32, coordinates, Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes))),
515    Equal.cong(Maybe<&2, List<&2, U32>>, List<&2, U32>, Axis.values(U32), Some{values},
516      Some{Axis.order(U32, coordinates, Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)))},
517      Equal.trans(Maybe<&2, List<&2, U32>>, Some{values}, Layout.inverse_coordinates(Shape.dimensions(input), axes, coordinates, 0),
518        Some{Axis.order(U32, coordinates, Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)))}, inverse,
519        AxisAlgebra.scatter_complete(input, axes, coordinates, accepted,
520          output_coordinate_rank(input, axes, Layout.Permutation{output, accepted, ordered, count}, Layout.CWord{coordinates, valid}))))) :
521            Layout.WordsValid(Shape.dimensions(input), _)
522  words_valid_of(Shape.dimensions(input), Axis.order(U32, coordinates, Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes))),
523    Coordinates.fits_of(Shape.extents(input),
524      Shape.naturals(Axis.order(U32, coordinates, Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)))),
525      inverse_coordinate_fit(input, axes, coordinates, accepted,
526        output_coordinate_rank(input, axes, Layout.Permutation{output, accepted, ordered, count}, Layout.CWord{coordinates, valid}),
527        %permutation_dimensions_order(input, axes, Layout.Permutation{output, accepted, ordered, count}) :
528          {True{} == Shape.fit(Shape.naturals(_), Shape.naturals(coordinates)) : Bool}
529        words_fit_true(Shape.dimensions(output), coordinates, valid))))