def new_checked_length

bendtorch-core@0.1.0.0 · src/tensor/allocation_PROOF.bend:31

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
import bendtorch-core@0.1.0.0/src/storage/api.bend as Api
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/tensor/allocation_spec.bend as Allocation

31def new_checked_length(+length: Nat, +fill: F32, allowed: Bool, accepted: {allowed == True{} : Bool},
32  limit: {Nat.is_le(length, Model.capacity(20n)) == True{} : Bool}) ->
33  {Allocation.storage_length(Storage.new_checked(length, fill, allowed)) == Some{length} : Maybe<&2, Nat>}:
34  match length allowed:
35    case 0n False{}:
36      {==}
37    case 0n True{}:
38      {==}
39    case 1n+p False{}:
40      Empty.absurd({None{} == Some{1n+p} : Maybe<&2, Nat>}, Arith.clash(accepted))
41    case 1n+p True{}:
42      allocate_at_length(1n+p, fill, Storage.depth_seek(20n, 1n+p, 0n, 1n, Nat.is_le(1n+p, 1n)), Api.seek(1n+p, limit, {==}))