def clamp_axis

bendtorch-core@0.1.0.0 · src/tensor/slice_PROOF.bend:314

import Base
import bendtorch-core@0.1.0.0/src/tensor/slice.bend as Slice
import bendtorch-core@0.1.0.0/src/tensor/slice_LAWS.bend as Laws

314# The clamp of bounds is PyTorch's, written with min and max.
315def clamp_axis(+n: Nat, +s: Nat, +t: Nat, +p: Nat) ->
316  {(n, Nat.min(s, n), p, Slice.length(Slice.Bounds{Nat.min(s, n), Nat.max(Nat.min(s, n), Nat.min(t, n))}, p)) ==
317    Laws.axis_spec(n, s, t, p) : Nat & Nat & Nat & Nat}:
318  +cs = Bool.pick(Nat, Nat.is_le(s, n), s, n)
319  +ct = Bool.pick(Nat, Nat.is_le(t, n), t, n)
320  %Equal.sym(Nat, Nat.min(s, n), cs, min_pick(s, n)) :
321    {(n, _, p, Slice.length(Slice.Bounds{_, Nat.max(_, Nat.min(t, n))}, p)) == Laws.axis_spec(n, s, t, p) : Nat & Nat & Nat & Nat}
322  %Equal.sym(Nat, Nat.min(t, n), ct, min_pick(t, n)) :
323    {(n, cs, p, Slice.length(Slice.Bounds{cs, Nat.max(cs, _)}, p)) == Laws.axis_spec(n, s, t, p) : Nat & Nat & Nat & Nat}
324  %Equal.sym(Nat, Nat.max(cs, ct), Bool.pick(Nat, Nat.is_le(cs, ct), ct, cs), max_pick(cs, ct)) :
325    {(n, cs, p, Slice.length(Slice.Bounds{cs, _}, p)) == Laws.axis_spec(n, s, t, p) : Nat & Nat & Nat & Nat}
326  {==}