law gather_count_refused

bendtorch-core@0.1.0.0 · src/tensor/gather_LAWS.bend:115

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/signed.bend as Signed
import bendtorch-core@0.1.0.0/src/tensor/gather.bend as Gather

115# gather(dim, index): an entry count other than the element count of the
116# index's shape is refused first, then the axis, an index of another rank, one
117# with another extent at another axis, and an entry at or past the extent;
118# any other request is planned, with the index's extent at the axis.
119law gather_count_refused:
120  for +input: Shape.Shape
121  for +dim: Signed.Position
122  for +index: Shape.Shape
123  for +entries: List<&2, U32>
124  for miscounted: {Nat.is_eq(length(entries), Shape.elements(index)) == False{} : Bool}
125  {Gather.gather_plan(input, dim, Gather.Index{index, entries}) == Fail{Gather.TensorError{Core.ValueCountMismatch{}}} :
126    Result<&2, &2, Gather.Error, Gather.Planned>}