def mapping_decided_success

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

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

708def mapping_decided_success(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +index: U32,
709  decision: Shape.BoolCase<U32.is_lt(index, Shape.count(Layout.output(input, axes, plan)))>,
710  inside: {True{} == U32.is_lt(index, Shape.count(Layout.output(input, axes, plan))) : Bool}) ->
711  {Result.is_done(&2, &2, Layout.Error, Layout.Mapping<input, axes, plan, index>, Layout.map_decided(input, axes, plan, index, decision)) == True{} : Bool}:
712  match decision:
713    case Shape.BFalse{equal}:
714      Empty.absurd({False{} == True{} : Bool}, Arith.clash(Equal.trans(Bool, False{}, U32.is_lt(index, Shape.count(Layout.output(input, axes, plan))), True{}, equal,
715        Equal.sym(Bool, True{}, U32.is_lt(index, Shape.count(Layout.output(input, axes, plan))), inside))))
716    case Shape.BTrue{+equal}:
717      mapping_output_success(input, axes, plan, index, Layout.FIndex{index, equal}, {==},
718        Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(Shape.dimensions(Layout.output(input, axes, plan))), index)), {==},
719        Layout.words_check(Shape.dimensions(Layout.output(input, axes, plan)), Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(Shape.dimensions(Layout.output(input, axes, plan))), index))),
720        words_check_success(Shape.dimensions(Layout.output(input, axes, plan)),
721          Layout.reverse_words(Layout.unflatten_words(Layout.reverse_words(Shape.dimensions(Layout.output(input, axes, plan))), index)),
722          decoded_words_valid(Layout.output(input, axes, plan), index,
723            %Equal.sym(Nat, Shape.elements(Layout.output(input, axes, plan)), Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))), Shape.elements_exact(Layout.output(input, axes, plan))) :
724              {True{} == Nat.is_lt(U32.to_nat(index), _) : Bool}
725            Equal.sym(Bool, Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan)))), True{},
726              flat_mathematical_bounded(Layout.output(input, axes, plan), Layout.FIndex{index, equal})))))