def dynamic_read_retains

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

import Base
import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
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

209def dynamic_read_retains(original: Core.Dynamic, +index: U32) -> SourceModel<original, dynamic_read_owner(Core.read_dynamic(original, index))>:
210  Core.Packed{+shape, Core.TTensor{storage, exact}} = original
211  match storage:
212    case Storage.Empty{}:
213      SourceModel{property => {\{InspectionModel: equal => equal} :
214        InspectionModel<Totality.inspect(property, dynamic_read_owner(Core.read_dynamic(Core.Packed{shape, Core.TTensor{Storage.Empty{}, exact}}, index))),
215          Totality.inspect(property, Core.Packed{shape, Core.TTensor{Storage.Empty{}, exact}})> ->
216        {Totality.inspect(property, dynamic_read_owner(Core.read_dynamic(Core.Packed{shape, Core.TTensor{Storage.Empty{}, exact}}, index))) ==
217          Totality.inspect(property, Core.Packed{shape, Core.TTensor{Storage.Empty{}, exact}}) : Totality.Inspection}}(
218            empty_read_property(shape, index, property, exact))}
219    case Storage.Owned{+depth, +length, array, balanced, valid}:
220      SourceModel{property => {\{InspectionModel: equal => equal} :
221        InspectionModel<Totality.inspect(property, dynamic_read_owner(Core.read_dynamic(Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}}, index))),
222          Totality.inspect(property, Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}})> ->
223        {Totality.inspect(property, dynamic_read_owner(Core.read_dynamic(Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}}, index))) ==
224          Totality.inspect(property, Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}}) : Totality.Inspection}}(
225            owned_read_property(shape, depth, length, index, property, array, balanced, valid, exact))}