def storage_read_source

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

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/lifecycle.bend as Lifecycle

195def storage_read_source(-shape: Shape.Shape, -storage: Storage.Storage,
196  -valid: {Lifecycle.logical_length(storage) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32,
197  certificate: Lifecycle.StorageReadModel<storage, index>) -> SourceRead<shape, TTensor{storage, valid}, index>:
198  Lifecycle.StorageReadModel{meaning} = certificate
199  SourceRead{Equal.trans(Maybe<&2, F32>, read_value(shape, read_flat(shape, TTensor{storage, valid}, index)),
200    Lifecycle.read_value(Storage.get(storage, index)), Lifecycle.checked_observe(storage, index),
201    read_result_value(shape, storage, valid, index, Storage.get(storage, index), {==}), meaning)}