def get_checked_length

bendtorch-core@0.1.0.0 · src/tensor/lifecycle.bend:29

import Base
import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model

29def get_checked_length(+d: Nat, +n: Nat, array: Array<F32>, +i: U32, allowed: Bool,
30  -decision: {allowed == Nat.is_lt(U32.to_nat(i), n) : Bool},
31  -balanced: Model.Balanced(F32, d, array), -valid: {Storage.bounds(d, n) == True{} : Bool}) ->
32  {retained_read(Storage.get_checked(d, n, array, i, allowed, decision, balanced, valid)) == n : Nat}:
33  match allowed:
34    case False{}:
35      {==}
36    case True{}:
37      finish_read_length(d, n, array, i, Array.get(F32, array, i), {==}, balanced, valid)