def actual_advanced

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

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

851def actual_advanced(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +cursor: Nat,
852  -original: Core.Tensor<input>, -before_source: Core.Tensor<input>, -after_source: Core.Tensor<input>,
853  -before_target: Core.Tensor<Layout.output(input, axes, plan)>, -after_target: Core.Tensor<Layout.output(input, axes, plan)>,
854  prefix: Transforms.Prefix<input, axes, plan, original, before_source, before_target, cursor>,
855  canonical: CanonicalStep<input, axes, plan, cursor, before_source, before_target, after_source, after_target>) ->
856  Transforms.Advanced<input, axes, plan, original, before_source, after_source, before_target, after_target, cursor>:
857  Transforms.Prefix{source_prior, words_prior, checked_prior, written_prior} = prefix
858  CanonicalStep{converted, meaning} = canonical
859  Transforms.Advanced{converted,
860    step_source(input, axes, plan, U32.from_nat(cursor), before_source, before_target, after_source, after_target, meaning),
861    Equal.trans(Maybe<&2, F32>, Core.checked_observe(Layout.output(input, axes, plan), after_target, U32.from_nat(cursor)),
862      Transforms.expected_output(input, axes, plan, before_source, U32.from_nat(cursor)),
863      Transforms.expected_output(input, axes, plan, original, U32.from_nat(cursor)),
864      step_value(input, axes, plan, U32.from_nat(cursor), before_source, before_target, after_source, after_target, meaning),
865      {\{ExpectedSame: equal => equal} : ExpectedSame<input, axes, plan, original, before_source, U32.from_nat(cursor)> ->
866        {Transforms.expected_output(input, axes, plan, before_source, U32.from_nat(cursor)) ==
867          Transforms.expected_output(input, axes, plan, original, U32.from_nat(cursor)) : Maybe<&2, F32>}}(
868            expected_same(input, axes, plan, original, before_source, U32.from_nat(cursor), source_prior))),
869    step_route(input, axes, plan, U32.from_nat(cursor), before_source, before_target, after_source, after_target, meaning),
870    other => earlier => {\{PastFrame: checked => equal => checked} :
871      PastFrame<Layout.output(input, axes, plan), before_target, after_target, other> ->
872        Core.ObservationChecked(Core.Packed{Layout.output(input, axes, plan), after_target}, U32.from_nat(other))}(
873          past_frame(Layout.output(input, axes, plan), before_target, after_target, cursor, other, converted,
874            words_prior(other, earlier), checked_prior(other, earlier), earlier,
875            step_frame(input, axes, plan, U32.from_nat(cursor), before_source, before_target, after_source, after_target, meaning))),
876    other => earlier => {\{PastFrame: checked => equal => equal} :
877      PastFrame<Layout.output(input, axes, plan), before_target, after_target, other> ->
878        {Core.checked_observe(Layout.output(input, axes, plan), after_target, U32.from_nat(other)) ==
879          Core.checked_observe(Layout.output(input, axes, plan), before_target, U32.from_nat(other)) : Maybe<&2, F32>}}(
880          past_frame(Layout.output(input, axes, plan), before_target, after_target, cursor, other, converted,
881            words_prior(other, earlier), checked_prior(other, earlier), earlier,
882            step_frame(input, axes, plan, U32.from_nat(cursor), before_source, before_target, after_source, after_target, meaning)))}