law slice_axis_refused

bendtorch-core@0.1.0.0 · src/tensor/slice_LAWS.bend:183

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/tensor/slice.bend as Slice

183# PyTorch's checks, in its order. An axis at or past the rank (every axis
184# of a rank-0 input) is refused first, then a step of 0.
185law slice_axis_refused:
186  for +input: Shape.Shape
187  for +dim: U32
188  for +start: U32
189  for +stop: U32
190  for +step: U32
191  for outside: {Nat.is_lt(U32.to_nat(dim), Shape.rank_dimensions(Shape.dimensions(input))) == False{} : Bool}
192  {Slice.plan(input, dim, start, stop, step) == Fail{Slice.LayoutError{Layout.AxisOutOfBounds{}}} :
193    Result<&2, &2, Slice.Error, Slice.Planned>}