def PlannedAs

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

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

205# What an accepted slice plans: the view around the axis, the start and
206# stop clamped to the extent, the step, the length of the sliced axis, and
207# the output's dimensions, the input's with that length at the axis.
208def PlannedAs(+dimensions: List<&2, U32>, +dim: U32, +start: U32, +stop: U32, +step: U32,
209  result: Result<&2, &2, Slice.Error, Slice.Planned>) -> Type:
210  match result:
211    case Fail{error}:
212      Unit
213    case Done{Slice.Planned{plan, output}}:
214      {plan == Slice.plan_of(dimensions, dim, start, stop, step) : Slice.Plan} &
215        {Shape.dimensions(output) == Slice.resized(dimensions, U32.to_nat(dim), U32.from_nat(Slice.plan_length(plan))) : List<&2, U32>}