def step_read_certificate

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

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

589def step_read_certificate(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +index: U32,
590  -original_source: Core.Tensor<input>, original_target: Core.Tensor<Layout.output(input, axes, plan)>,
591  +mapping: Layout.Mapping<input, axes, plan, index>,
592  -map_exact: {Done{mapping} == Layout.map_index(input, axes, plan, index) : Result<&2, &2, Layout.Error, Layout.Mapping<input, axes, plan, index>>},
593  lift: @-pair: Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Tensor<Layout.output(input, axes, plan)>> ->
594    {pair == Transforms.copy_read(input, axes, plan, index, source => target => (source, Done{target}), original_target,
595      Core.read_flat(input, original_source, Layout.source_index(input, axes, plan, index, mapping))) :
596        Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Tensor<Layout.output(input, axes, plan)>>} ->
597    {pair == Transforms.copy_step(input, axes, plan, original_source, original_target, index) :
598      Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Tensor<Layout.output(input, axes, plan)>>},
599  certificate: Core.Read<input, original_source, Layout.source_index(input, axes, plan, index, mapping)>) ->
600  Transforms.StepCertificate<input, axes, plan, index, original_source, original_target>:
601  Core.Read{retained, result, exact} = certificate
602  match result:
603    case Fail{error}:
604      Transforms.StepCertificate{(retained, Fail{Transforms.TensorError{error}}),
605        lift((retained, Fail{Transforms.TensorError{error}}),
606          Equal.cong(Core.Tensor<input> & Result<&2, &2, Core.Error, F32>,
607            Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Tensor<Layout.output(input, axes, plan)>>,
608            pair => Transforms.copy_read(input, axes, plan, index, source => target => (source, Done{target}), original_target, pair),
609            (retained, Fail{error}), Core.read_flat(input, original_source, Layout.source_index(input, axes, plan, index, mapping)), exact)), Unit{}}
610    case Done{+value}:
611      step_target_info(input, axes, plan, index, original_source, original_target, mapping, value, map_exact,
612        target_info(Layout.output(input, axes, plan), original_target, index, value), retained,
613        pair => equality => lift(pair,
614          Equal.trans(Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Tensor<Layout.output(input, axes, plan)>>,
615            pair, Transforms.copy_read(input, axes, plan, index, source => target => (source, Done{target}), original_target, (retained, Done{value})),
616            Transforms.copy_read(input, axes, plan, index, source => target => (source, Done{target}), original_target,
617              Core.read_flat(input, original_source, Layout.source_index(input, axes, plan, index, mapping))), equality,
618            Equal.cong(Core.Tensor<input> & Result<&2, &2, Core.Error, F32>,
619              Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Tensor<Layout.output(input, axes, plan)>>,
620              read => Transforms.copy_read(input, axes, plan, index, source => target => (source, Done{target}), original_target, read),
621              (retained, Done{value}), Core.read_flat(input, original_source, Layout.source_index(input, axes, plan, index, mapping)), exact))), exact)