def loop_after_natural

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

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

942def loop_after_natural(+fuel: Nat, +input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +cursor: Nat,
943  -original: Core.Tensor<input>, -before_source: Core.Tensor<input>, -before_target: Core.Tensor<Layout.output(input, axes, plan)>,
944  -prefix: Transforms.Prefix<input, axes, plan, original, before_source, before_target, cursor>,
945  certificate: Transforms.NaturalCertificate<input, axes, plan, cursor, before_source, before_target>,
946  rec: @source: Core.Tensor<input> -> @target: Core.Tensor<Layout.output(input, axes, plan)> ->
947    @-prefix: Transforms.Prefix<input, axes, plan, original, source, target, 1n+cursor> ->
948      Transforms.LoopCertificate<input, axes, plan, original, fuel, 1n+cursor, source, target>) ->
949  Transforms.LoopCertificate<input, axes, plan, original, 1n+fuel, cursor, before_source, before_target>:
950  Transforms.NaturalCertificate{result, exact, meaning} = certificate
951  match result:
952    case Transforms.NaturalError{source}:
953      Transforms.LoopCertificate{(source, Fail{Transforms.LayoutError{Layout.MappingError{}}}),
954        Equal.cong(Transforms.NaturalCopy<input, axes, plan, cursor>,
955          Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Tensor<Layout.output(input, axes, plan)>>,
956          step => Transforms.natural_next(input, axes, plan, cursor,
957            source => target => Transforms.copy_loop(fuel, input, axes, plan, source, target, 1n+cursor), step),
958          Transforms.NaturalError{source}, Transforms.natural_step(input, axes, plan, cursor, before_source, before_target), exact), Unit{}}
959    case Transforms.NaturalCopied{pair, index, converted, candidate}:
960      loop_after_pair(fuel, input, axes, plan, cursor, original, before_source, before_target, index, converted, candidate, prefix,
961        pair, exact, meaning, rec)