def read_inside

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

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/LAWS.bend as StorageLaws
import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion
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

219def read_inside(+shape: Shape.Shape, +fill: F32, +index: U32,
220  inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) -> Laws.ReadInside<shape, fill, index>:
221  +inside = inside
222  Laws.ReadInside{
223    read_contract(shape, fill, index, Done{fill},
224      StorageLaws.replay_get(Shape.count(shape), fill, [], index, Conversion.shape_count_within(shape), word_inside(shape, index, inside))),
225    new_lift(shape, fill, result => {Observation.point(shape, index, result) == Some{fill} : Maybe<&2, F32>},
226      valid => read_point_done(shape, fill, valid, index, inside))}