def attach_length

bendtorch-core@0.1.0.0 · src/tensor/construction_contract_PROOF.bend:266

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
import bendtorch-core@0.1.0.0/src/tensor/observation.bend as Observation

266def attach_length(+shape: Shape.Shape, +index: U32, storage: Storage.Storage,
267  counted: {Lifecycle.logical_length(storage) == Shape.elements(shape) : Nat},
268  kept: {Lifecycle.retained_read(Storage.get(storage, index)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
269  {Observation.after_length(shape, index, Core.attach(shape, storage)) == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>}:
270  match storage:
271    case Storage.Empty{}:
272      attached_length(shape, index, 0n, Shape.bool_case(Nat.is_eq(0n, Shape.elements(shape))), Storage.Empty{}, {==}, counted, kept)
273    case Storage.Owned{+depth, +length, array, balanced, valid}:
274      attached_length(shape, index, length, Shape.bool_case(Nat.is_eq(length, Shape.elements(shape))),
275        Storage.Owned{depth, length, array, balanced, valid}, {==}, counted, kept)