def attach_point

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

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

79def attach_point(+shape: Shape.Shape, +fill: F32, +index: U32, storage: Storage.Storage,
80  counted: {Lifecycle.logical_length(storage) == Shape.elements(shape) : Nat},
81  value: {Lifecycle.read_value(Storage.get(storage, index)) == Some{fill} : Maybe<&2, F32>}) ->
82  {Observation.point(shape, index, Core.attach(shape, storage)) == Some{fill} : Maybe<&2, F32>}:
83  match storage:
84    case Storage.Empty{}:
85      attached_point(shape, fill, index, 0n, Shape.bool_case(Nat.is_eq(0n, Shape.elements(shape))),
86        Storage.Empty{}, {==}, counted, value)
87    case Storage.Owned{+depth, +length, array, balanced, valid}:
88      attached_point(shape, fill, index, length, Shape.bool_case(Nat.is_eq(length, Shape.elements(shape))),
89        Storage.Owned{depth, length, array, balanced, valid}, {==}, counted, value)