def attach_value

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

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/storage/LAWS.bend as StorageLaws
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

203def attach_value(+shape: Shape.Shape, +fill: F32, +index: U32, +other: U32, storage: Storage.Storage,
204  counted: {Lifecycle.logical_length(storage) == Shape.elements(shape) : Nat},
205  kept: {Lifecycle.read_value(Storage.get(StorageLaws.kept(storage, index), other)) == Some{fill} : Maybe<&2, F32>}) ->
206  {Observation.after_value(shape, index, other, Core.attach(shape, storage)) == Some{fill} : Maybe<&2, F32>}:
207  match storage:
208    case Storage.Empty{}:
209      attached_value(shape, fill, index, other, 0n, Shape.bool_case(Nat.is_eq(0n, Shape.elements(shape))), Storage.Empty{}, {==}, counted, kept)
210    case Storage.Owned{+depth, +length, array, balanced, valid}:
211      attached_value(shape, fill, index, other, length, Shape.bool_case(Nat.is_eq(length, Shape.elements(shape))),
212        Storage.Owned{depth, length, array, balanced, valid}, {==}, counted, kept)