def step_write_certificate

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

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

528def step_write_certificate(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +index: U32,
529  -original_source: Core.Tensor<input>, -original_target: Core.Tensor<Layout.output(input, axes, plan)>,
530  +mapping: Layout.Mapping<input, axes, plan, index>, +value: F32,
531  -map_exact: {Done{mapping} == Layout.map_index(input, axes, plan, index) : Result<&2, &2, Layout.Error, Layout.Mapping<input, axes, plan, index>>},
532  certificate: Core.Write<Layout.output(input, axes, plan), original_target, index, value>,
533  retained: Core.Tensor<input>,
534  lift: @-pair: Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Tensor<Layout.output(input, axes, plan)>> ->
535    {pair == Transforms.copy_written(input, axes, plan, source => target => (source, Done{target}), retained,
536      Core.write_flat(Layout.output(input, axes, plan), original_target, index, value)) :
537        Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Tensor<Layout.output(input, axes, plan)>>} ->
538    {pair == Transforms.copy_step(input, axes, plan, original_source, original_target, index) :
539      Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Tensor<Layout.output(input, axes, plan)>>},
540  -read_exact: {(retained, Done{value}) == Core.read_flat(input, original_source, Layout.source_index(input, axes, plan, index, mapping)) :
541    Core.Tensor<input> & Result<&2, &2, Core.Error, F32>},
542  -read_model: Core.SourceRead<input, original_source, Layout.source_index(input, axes, plan, index, mapping)>,
543  -keep_model: Core.SourceReadKeeps<input, original_source, Layout.source_index(input, axes, plan, index, mapping)>,
544  -write_model: Core.CheckedUpdateModel<Layout.output(input, axes, plan), original_target, index, value>) ->
545  Transforms.StepCertificate<input, axes, plan, index, original_source, original_target>:
546  Core.Write{target, result, exact} = certificate
547  match result:
548    case Fail{error}:
549      Transforms.StepCertificate{(retained, Fail{Transforms.TensorError{error}}),
550        lift((retained, Fail{Transforms.TensorError{error}}),
551          Equal.cong(Core.Tensor<Layout.output(input, axes, plan)> & Result<&2, &2, Core.Error, Unit>,
552            Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Tensor<Layout.output(input, axes, plan)>>,
553            pair => Transforms.copy_written(input, axes, plan, source => target => (source, Done{target}), retained, pair),
554            (target, Fail{error}), Core.write_flat(Layout.output(input, axes, plan), original_target, index, value), exact)), Unit{}}
555    case Done{unit}:
556      Transforms.StepCertificate{(retained, Done{target}),
557        lift((retained, Done{target}),
558          Equal.cong(Core.Tensor<Layout.output(input, axes, plan)> & Result<&2, &2, Core.Error, Unit>,
559            Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Tensor<Layout.output(input, axes, plan)>>,
560            pair => Transforms.copy_written(input, axes, plan, source => target => (source, Done{target}), retained, pair),
561            (target, Done{unit}), Core.write_flat(Layout.output(input, axes, plan), original_target, index, value), exact)),
562        {\{SuccessfulStep: meaning => meaning} : SuccessfulStep<input, axes, plan, index, original_source, original_target, retained, target> ->
563          Transforms.StepMeaning(input, axes, plan, index, original_source, original_target, (retained, Done{target}))}(
564            successful_step(input, axes, plan, index, original_source, original_target, retained, target, mapping, value, unit, map_exact,
565              source_value(input, original_source, retained, Layout.source_index(input, axes, plan, index, mapping), value, read_exact, read_model),
566              source_kept(input, original_source, retained, Layout.source_index(input, axes, plan, index, mapping), value, read_exact, keep_model),
567              known_checked_update(Layout.output(input, axes, plan), original_target, target, index, value, unit, exact, write_model)))}