~/jendhub

def ranked_failure

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

import bendtorch-core@0.1.0.0/src/tensor/permute_contract.bend as PermuteContract
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

57def ranked_failure(+input: Shape.Shape, +axes: List<&2, U32>,
58  decision: Shape.BoolCase<Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input)))>,
59  wrong: {Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))) == False{} : Bool}) ->
60  {Layout.plan_ranked(input, axes, decision) == Fail{Layout.AxesLengthMismatch{}} : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>}:
61  match decision:
62    case Shape.BFalse{no}:
63      {==}
64    case Shape.BTrue{yes}:
65      Empty.absurd({Layout.plan_ranked(input, axes, Shape.BTrue{yes}) == Fail{Layout.AxesLengthMismatch{}} : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>},
66        Nats.contradiction(Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))), yes,
67          Equal.sym(Bool, Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))), False{}, wrong)))

Uses (15)

Used by (1)