def mapping_input_success

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

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

656def mapping_input_success(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +index: U32,
657  +oi: Layout.FlatIndex<Layout.output(input, axes, plan)>, +oc: Layout.CheckedCoordinate<Layout.output(input, axes, plan)>,
658  +requested: {Layout.index_value(Layout.output(input, axes, plan), oi) == index : U32},
659  +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>},
660  +values: List<&2, U32>, +inverse: {Some{values} == Layout.inverse_coordinates(Shape.dimensions(input), axes, Layout.coordinate_values(Layout.output(input, axes, plan), oc), 0) : Maybe<&2, List<&2, U32>>},
661  checked: Result<&2, &2, Shape.Error, Layout.WordsValid(Shape.dimensions(input), values)>,
662  successful: {Result.is_done(&2, &2, Shape.Error, Layout.WordsValid(Shape.dimensions(input), values), checked) == True{} : Bool}) ->
663  {Result.is_done(&2, &2, Layout.Error, Layout.Mapping<input, axes, plan, index>,
664    Layout.map_input(input, axes, plan, index, oi, oc, requested, decoded, values, inverse, checked)) == True{} : Bool}:
665  match checked:
666    case Fail{error}:
667      Empty.absurd({False{} == True{} : Bool}, Arith.clash(successful))
668    case Done{+valid}:
669      mapping_roundtrip_success(input, axes, plan, index, oi, oc, Layout.CWord{values, valid}, requested, decoded, inverse,
670        Shape.bool_case(Layout.maybe_same(Layout.reorder(values, axes), Some{Layout.coordinate_values(Layout.output(input, axes, plan), oc)})),
671        inverse_words_roundtrip(input, axes, plan, oc, values, inverse))