law slice_plan_view

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

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/slice.bend as Slice

156# For an input with an element, the plan's view is the element counts of the
157# prefix and of the suffix, the row-major view around the axis.
158law slice_plan_view:
159  for +prefix: List<&2, U32>
160  for +extent: U32
161  for +suffix: List<&2, U32>
162  for +dim: U32
163  for at: {U32.to_nat(dim) == Shape.rank_dimensions(prefix) : Nat}
164  for +start: U32
165  for +stop: U32
166  for +step: U32
167  for nonempty: {Nat.is_lt(0n, Shape.logical_numel(List.append(&2, U32, prefix, extent <> suffix))) == True{} : Bool}
168  {view_part(Slice.plan_of(List.append(&2, U32, prefix, extent <> suffix), dim, start, stop, step)) ==
169    (Shape.logical_numel(prefix), Shape.logical_numel(suffix)) : Nat & Nat}