def ranked_pass

bendtorch-core@0.1.0.0 · src/tensor/permute_contract.bend:69

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats
import bendtorch-core@0.1.0.0/src/tensor/layout.bend as Layout

69def ranked_pass(+input: Shape.Shape, +axes: List<&2, U32>,
70  decision: Shape.BoolCase<Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input)))>,
71  ranked: {Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))) == True{} : Bool}) ->
72  {Layout.plan_ranked(input, axes, decision) == Layout.plan_bounded(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input)))) : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>}:
73  match decision:
74    case Shape.BFalse{no}:
75      Empty.absurd({Layout.plan_ranked(input, axes, Shape.BFalse{no}) == Layout.plan_bounded(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input)))) : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>},
76        Nats.contradiction(Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))),
77          Equal.sym(Bool, Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))), True{}, ranked), no))
78    case Shape.BTrue{yes}:
79      {==}