def copy_read_success

bendtorch-core@0.1.0.0 · src/tensor/transform_PROOF.bend:1811

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/layout.bend as Layout
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/transforms.bend as Transforms
import bendtorch-core@0.1.0.0/src/tensor/transform_totality.bend as Totality

1811def copy_read_success(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +index: U32, +source_index: U32,
1812  -source: Core.Tensor<input>, target: Core.Tensor<Layout.output(input, axes, plan)>,
1813  certificate: ReadSuccessModel<input, source, source_index>,
1814  +inside: {True{} == U32.is_lt(index, Shape.count(Layout.output(input, axes, plan))) : Bool}) ->
1815  Totality.CopySuccess<input, axes, plan, Transforms.copy_read(input, axes, plan, index,
1816    source => target => (source, Done{target}), target, Core.read_flat(input, source, source_index))>:
1817  Totality.CopySuccess{
1818    {\{ReadSuccessModel: success =>
1819      {\{ReadSuccess: retained => value => exact =>
1820        %exact : {Totality.copy_succeeded(input, axes, plan, Transforms.copy_read(input, axes, plan, index,
1821          source => target => (source, Done{target}), target, _)) == True{} : Bool}
1822        {\{Totality.CopySuccess: successful => successful} :
1823          Totality.CopySuccess<input, axes, plan, Transforms.copy_read(input, axes, plan, index,
1824            source => target => (source, Done{target}), target, (retained, Done{value}))> ->
1825              {Totality.copy_succeeded(input, axes, plan, Transforms.copy_read(input, axes, plan, index,
1826                source => target => (source, Done{target}), target, (retained, Done{value}))) == True{} : Bool}}(
1827                  copy_value_success(input, axes, plan, index, retained, target, value, inside))} :
1828                    ReadSuccess<input, source, source_index> ->
1829                      {Totality.copy_succeeded(input, axes, plan, Transforms.copy_read(input, axes, plan, index,
1830                        source => target => (source, Done{target}), target, Core.read_flat(input, source, source_index))) == True{} : Bool}}(success)} :
1831                          ReadSuccessModel<input, source, source_index> ->
1832                            {Totality.copy_succeeded(input, axes, plan, Transforms.copy_read(input, axes, plan, index,
1833                              source => target => (source, Done{target}), target, Core.read_flat(input, source, source_index))) == True{} : Bool}}(certificate)}