def plan_counted_success

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

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

210def plan_counted_success(+input: Shape.Shape, +axes: List<&2, U32>, +output: Shape.Shape,
211  +valid: {True{} == Layout.bijective(input, axes) : Bool},
212  +ordered: {Some{Shape.dimensions(output)} == Layout.reorder(Shape.dimensions(input), axes) : Maybe<&2, List<&2, U32>>},
213  decision: Shape.BoolCase<Nat.is_eq(Shape.elements(input), Shape.elements(output))>,
214  same: {Shape.elements(input) == Shape.elements(output) : Nat}) ->
215  {Result.is_done(&2, &2, Layout.Error, Layout.Plan<input, axes>, Layout.plan_counted(input, axes, output, valid, ordered, decision)) == True{} : Bool}:
216  match decision:
217    case Shape.BFalse{equal}:
218      Empty.absurd({False{} == True{} : Bool},
219        Arith.clash(Equal.trans(Bool, False{}, Nat.is_eq(Shape.elements(input), Shape.elements(output)), True{}, equal,
220          natural_equal_true(Shape.elements(input), Shape.elements(output), same))))
221    case Shape.BTrue{equal}:
222      {==}