def owned_read_property
bendtorch-core@0.1.0.0 · src/tensor/elementwise_PROOF.bend:149
import bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend as ElementwisePROOF
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/model.bend as Model
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/elementwise_totality.bend as Totality
149def owned_read_property(+shape: Shape.Shape, +depth: Nat, +length: Nat, +index: U32, property: Totality.Property,
150 -array: Array<F32>, -balanced: Model.Balanced(F32, depth, array), -valid: {Storage.bounds(depth, length) == True{} : Bool},
151 -exact: {length == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
152 InspectionModel<Totality.inspect(property, dynamic_read_owner(Core.read_dynamic(Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}}, index))),
153 Totality.inspect(property, Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}})>:
154 match property:
155 case Totality.Dimensions{}:
156 InspectionModel{Equal.trans(Totality.Inspection,
157 Totality.inspect(Totality.Dimensions{}, dynamic_read_owner(Core.read_dynamic(Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}}, index))),
158 Totality.inspect(Totality.Dimensions{}, Core.Packed{shape, tensor_read_owner(shape, Core.read_flat(shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, index))}),
159 Totality.Dims{Shape.dimensions(shape)},
160 dynamic_read_projection(shape, Totality.Dimensions{}, Core.read_flat(shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, index)),
161 tensor_read_dimensions(shape, Core.read_flat(shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, index)))}
162 case Totality.Checked{+other}:
163 InspectionModel{Equal.trans(Totality.Inspection,
164 Totality.inspect(Totality.Checked{other}, dynamic_read_owner(Core.read_dynamic(Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}}, index))),
165 storage_inspect(Totality.Checked{other}, read_owner(Storage.get(Storage.Owned{depth, length, array, balanced, valid}, index))),
166 array_inspect(depth, length, Totality.Checked{other}, array),
167 Equal.trans(Totality.Inspection,
168 Totality.inspect(Totality.Checked{other}, dynamic_read_owner(Core.read_dynamic(Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}}, index))),
169 Totality.inspect(Totality.Checked{other}, Core.Packed{shape, tensor_read_owner(shape, Core.read_flat(shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, index))}),
170 storage_inspect(Totality.Checked{other}, read_owner(Storage.get(Storage.Owned{depth, length, array, balanced, valid}, index))),
171 dynamic_read_projection(shape, Totality.Checked{other}, Core.read_flat(shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, index)),
172 core_read_projection(shape, Storage.Owned{depth, length, array, balanced, valid}, exact, index, Totality.Checked{other}, Storage.get(Storage.Owned{depth, length, array, balanced, valid}, index), {==})),
173 {\{InspectionModel: equal => equal} :
174 InspectionModel<storage_inspect(Totality.Checked{other}, read_owner(Storage.get(Storage.Owned{depth, length, array, balanced, valid}, index))),
175 array_inspect(depth, length, Totality.Checked{other}, array)> ->
176 {storage_inspect(Totality.Checked{other}, read_owner(Storage.get(Storage.Owned{depth, length, array, balanced, valid}, index))) ==
177 array_inspect(depth, length, Totality.Checked{other}, array) : Totality.Inspection}}(
178 read_checked_inspect(depth, length, index, Nat.is_lt(U32.to_nat(index), length), Totality.Checked{other}, array, {==}, balanced, valid)))}
179 case Totality.Raw{+other}:
180 InspectionModel{Equal.trans(Totality.Inspection,
181 Totality.inspect(Totality.Raw{other}, dynamic_read_owner(Core.read_dynamic(Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}}, index))),
182 storage_inspect(Totality.Raw{other}, read_owner(Storage.get(Storage.Owned{depth, length, array, balanced, valid}, index))),
183 array_inspect(depth, length, Totality.Raw{other}, array),
184 Equal.trans(Totality.Inspection,
185 Totality.inspect(Totality.Raw{other}, dynamic_read_owner(Core.read_dynamic(Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}}, index))),
186 Totality.inspect(Totality.Raw{other}, Core.Packed{shape, tensor_read_owner(shape, Core.read_flat(shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, index))}),
187 storage_inspect(Totality.Raw{other}, read_owner(Storage.get(Storage.Owned{depth, length, array, balanced, valid}, index))),
188 dynamic_read_projection(shape, Totality.Raw{other}, Core.read_flat(shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, index)),
189 core_read_projection(shape, Storage.Owned{depth, length, array, balanced, valid}, exact, index, Totality.Raw{other}, Storage.get(Storage.Owned{depth, length, array, balanced, valid}, index), {==})),
190 {\{InspectionModel: equal => equal} :
191 InspectionModel<storage_inspect(Totality.Raw{other}, read_owner(Storage.get(Storage.Owned{depth, length, array, balanced, valid}, index))),
192 array_inspect(depth, length, Totality.Raw{other}, array)> ->
193 {storage_inspect(Totality.Raw{other}, read_owner(Storage.get(Storage.Owned{depth, length, array, balanced, valid}, index))) ==
194 array_inspect(depth, length, Totality.Raw{other}, array) : Totality.Inspection}}(
195 read_checked_inspect(depth, length, index, Nat.is_lt(U32.to_nat(index), length), Totality.Raw{other}, array, {==}, balanced, valid)))}