def read_contract

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

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/observation.bend as Observation
import bendtorch-core@0.1.0.0/src/tensor/read_write_records.bend as Laws

196def read_contract(+shape: Shape.Shape, +fill: F32, +index: U32, -expected: Result<&2, &2, Storage.Error, F32>,
197  read: {StorageLaws.read(StorageLaws.created(Shape.count(shape), fill), index) == expected : Result<&2, &2, Storage.Error, F32>}) ->
198  Laws.ReadContract<shape, fill, index, Observation.read_status(Core.storage_read_error(expected))>:
199  Laws.ReadContract{
200    new_lift(shape, fill, result => {Observation.read_code(shape, index, result) == Some{Observation.read_status(Core.storage_read_error(expected))} : Maybe<&2, U32>},
201      valid => read_code_done(shape, fill, valid, index, expected, read)),
202    new_lift(shape, fill, result => {Observation.after_dimensions(shape, index, result) == Some{Shape.dimensions(shape)} : Maybe<&2, List<&2, U32>>},
203      valid => read_dimensions_pair(shape, Core.read_flat(shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}, index))),
204    new_lift(shape, fill, result => {Observation.after_length(shape, index, result) == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>},
205      valid => read_length_done(shape, fill, valid, index)),
206    new_lift(shape, fill, result => {Observation.after_count(shape, index, result) == Some{Shape.count(shape)} : Maybe<&2, U32>},
207      valid => read_count_pair(shape, Core.read_flat(shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}, index))),
208    other => inside => new_lift(shape, fill, result => {Observation.after_value(shape, index, other, result) == Some{fill} : Maybe<&2, F32>},
209      valid => read_after_done(shape, fill, valid, index, other, inside))}