def write_inside

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

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

192def write_inside(+shape: Shape.Shape, +fill: F32, +index: U32, +value: F32,
193  inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) -> Laws.WriteInside<shape, fill, index, value>:
194  +inside = inside
195  Laws.WriteInside{
196    write_contract(shape, fill, index, value, Done{Unit{}},
197      StorageLaws.replay_set(Shape.count(shape), fill, [], index, value, Conversion.shape_count_within(shape), Reads.word_inside(shape, index, inside))),
198    written_value(shape, fill, index, value, index, value, inside, pick_hit(shape, index, value, fill, inside)),
199    other => inside_other => different =>
200      written_value(shape, fill, index, value, other, fill, inside_other, pick_frame(shape, index, value, other, fill, inside, different))}