def mapping_inverse_success

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

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/storage/arith.bend as Arith
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

673def mapping_inverse_success(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +index: U32,
674  +oi: Layout.FlatIndex<Layout.output(input, axes, plan)>, +oc: Layout.CheckedCoordinate<Layout.output(input, axes, plan)>,
675  +requested: {Layout.index_value(Layout.output(input, axes, plan), oi) == index : U32},
676  +decoded: {Layout.coordinate_values(Layout.output(input, axes, plan), oc) == Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(Shape.dimensions(Layout.output(input, axes, plan))), index)) : List<&2, U32>},
677  result: Maybe<&2, List<&2, U32>>,
678  +same: {result == Layout.inverse_coordinates(Shape.dimensions(input), axes, Layout.coordinate_values(Layout.output(input, axes, plan), oc), 0) : Maybe<&2, List<&2, U32>>}) ->
679  {Result.is_done(&2, &2, Layout.Error, Layout.Mapping<input, axes, plan, index>,
680    Layout.map_inverse(input, axes, plan, index, oi, oc, requested, decoded, result, same)) == True{} : Bool}:
681  match result:
682    case None{}:
683      Empty.absurd({False{} == True{} : Bool},
684        Arith.clash(Equal.cong(Maybe<&2, List<&2, U32>>, Bool, metadata_present, None{},
685          Some{Axis.order(U32, Layout.coordinate_values(Layout.output(input, axes, plan), oc), Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)))},
686          Equal.trans(Maybe<&2, List<&2, U32>>, None{}, Layout.inverse_coordinates(Shape.dimensions(input), axes, Layout.coordinate_values(Layout.output(input, axes, plan), oc), 0),
687            Some{Axis.order(U32, Layout.coordinate_values(Layout.output(input, axes, plan), oc), Axis.inverse_axes(Shape.rank_dimensions(Shape.dimensions(input)), Shape.naturals(axes)))}, same,
688            AxisAlgebra.scatter_complete(input, axes, Layout.coordinate_values(Layout.output(input, axes, plan), oc), permutation_checked(input, axes, plan),
689              output_coordinate_rank(input, axes, plan, oc))))))
690    case Some{+values}:
691      mapping_input_success(input, axes, plan, index, oi, oc, requested, decoded, values, same, Layout.words_check(Shape.dimensions(input), values),
692        words_check_success(Shape.dimensions(input), values, inverse_words_valid(input, axes, plan, oc, values, same)))