def accepted_taken

bendtorch-core@0.1.0.0 · src/tensor/gather_PROOF.bend:71

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
import bendtorch-core@0.1.0.0/src/tensor/gather.bend as Gather
import bendtorch-core@0.1.0.0/src/tensor/gather_LAWS.bend as Laws

71# An accepted request's plan and output are what the laws name.
72def accepted_taken(+kind: Gather.Lookup, +dimensions: List<&2, U32>, +at: Nat, +count: Nat) ->
73  {Gather.accepted(kind, dimensions, at, count) == Laws.taken(kind, dimensions, at, count) : Result<&2, &2, Gather.Error, Gather.Planned>}:
74  Equal.trans(Result<&2, &2, Gather.Error, Gather.Planned>, Gather.accepted(kind, dimensions, at, count),
75    Gather.shaped(Laws.viewed(kind, Slice.sized(dimensions, at, Slice.holds_zero(dimensions)), count),
76      Slice.resized(dimensions, at, U32.from_nat(count)), Shape.construct(Slice.resized(dimensions, at, U32.from_nat(count)))),
77    Laws.taken(kind, dimensions, at, count),
78    Equal.cong(Gather.Plan, Result<&2, &2, Gather.Error, Gather.Planned>,
79      p => Gather.shaped(p, Slice.resized(dimensions, at, U32.from_nat(count)), Shape.construct(Slice.resized(dimensions, at, U32.from_nat(count)))),
80      Gather.viewed(kind, Slice.sized(dimensions, at, Slice.holds_zero(dimensions)), count),
81      Laws.viewed(kind, Slice.sized(dimensions, at, Slice.holds_zero(dimensions)), count),
82      viewed_same(kind, Slice.sized(dimensions, at, Slice.holds_zero(dimensions)), count)),
83    shaped_same(Laws.viewed(kind, Slice.sized(dimensions, at, Slice.holds_zero(dimensions)), count),
84      Slice.resized(dimensions, at, U32.from_nat(count)), Shape.construct(Slice.resized(dimensions, at, U32.from_nat(count)))))