def bounded_pass

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

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

91def bounded_pass(+input: Shape.Shape, +axes: List<&2, U32>, decision: Shape.BoolCase<Layout.bounded(axes, Shape.rank(input))>,
92  bounded: {Layout.bounded(axes, Shape.rank(input)) == True{} : Bool}) ->
93  {Layout.plan_bounded(input, axes, decision) == Layout.plan_unique(input, axes, Shape.bool_case(Layout.unique(axes))) : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>}:
94  match decision:
95    case Shape.BFalse{no}:
96      Empty.absurd({Layout.plan_bounded(input, axes, Shape.BFalse{no}) == Layout.plan_unique(input, axes, Shape.bool_case(Layout.unique(axes))) : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>},
97        Nats.contradiction(Layout.bounded(axes, Shape.rank(input)), Equal.sym(Bool, Layout.bounded(axes, Shape.rank(input)), True{}, bounded), no))
98    case Shape.BTrue{yes}:
99      {==}