def step_mapped_certificate

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

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

623def step_mapped_certificate(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +index: U32,
624  source: Core.Tensor<input>, target: Core.Tensor<Layout.output(input, axes, plan)>,
625  result: Result<&2, &2, Layout.Error, Layout.Mapping<input, axes, plan, index>>,
626  exact: {result == Layout.map_index(input, axes, plan, index) : Result<&2, &2, Layout.Error, Layout.Mapping<input, axes, plan, index>>}) ->
627  Transforms.StepCertificate<input, axes, plan, index, source, target>:
628  match result:
629    case Fail{error}:
630      Transforms.StepCertificate{(source, Fail{Transforms.LayoutError{error}}),
631        Equal.cong(Result<&2, &2, Layout.Error, Layout.Mapping<input, axes, plan, index>>,
632          Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Tensor<Layout.output(input, axes, plan)>>,
633          mapped => Transforms.copy_mapped(input, axes, plan, index, source => target => (source, Done{target}), source, target, mapped),
634          Fail{error}, Layout.map_index(input, axes, plan, index), exact), Unit{}}
635    case Done{+mapping}:
636      step_read_certificate(input, axes, plan, index, source, target, mapping, exact,
637        pair => equality => Equal.trans(Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Tensor<Layout.output(input, axes, plan)>>,
638          pair, Transforms.copy_mapped(input, axes, plan, index, source => target => (source, Done{target}), source, target, Done{mapping}),
639          Transforms.copy_step(input, axes, plan, source, target, index), equality,
640          Equal.cong(Result<&2, &2, Layout.Error, Layout.Mapping<input, axes, plan, index>>,
641            Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Tensor<Layout.output(input, axes, plan)>>,
642            mapped => Transforms.copy_mapped(input, axes, plan, index, source => target => (source, Done{target}), source, target, mapped),
643            Done{mapping}, Layout.map_index(input, axes, plan, index), exact)),
644        Core.read_certificate(input, source, Layout.source_index(input, axes, plan, index, mapping)))