def loop_after_certificate

bendtorch-core@0.1.0.0 · src/tensor/core_PROOF.bend:951

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/elementwise.bend as Elementwise

951def loop_after_certificate(+remaining: Nat, +operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +cursor: Nat,
952  -original_left: Core.Dynamic, -original_right: Core.Dynamic, -original: Elementwise.State<Shape.output_shape(plan)>,
953  -invariant: Elementwise.StateInvariant(operation, plan, original_left, original_right, cursor, original),
954  certificate: Elementwise.NaturalCertificate<operation, plan, cursor, original>,
955  rec: @state: Elementwise.State<Shape.output_shape(plan)> ->
956    @-invariant: Elementwise.StateInvariant(operation, plan, original_left, original_right, 1n+cursor, state) ->
957      Elementwise.LoopCertificate<remaining, operation, plan, 1n+cursor, original_left, original_right, state>) ->
958  Elementwise.LoopCertificate<1n+remaining, operation, plan, cursor, original_left, original_right, original>:
959  Elementwise.NaturalCertificate{result, exact, meaning} = certificate
960  match result:
961    case Elementwise.NaturalStop{left, right, error}:
962      Elementwise.LoopCertificate{((left, right), Fail{error}),
963        Equal.cong(Elementwise.NaturalStep<Shape.output_shape(plan), cursor>, (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic>,
964          step => Elementwise.finish_step(Shape.output_shape(plan), cursor, state => Elementwise.loop(remaining, operation, plan, 1n+cursor, state), step),
965          Elementwise.NaturalStop{left, right, error}, Elementwise.natural_step(operation, plan, cursor, original), exact), Unit{}}
966    case Elementwise.NaturalContinue{state, index, converted}:
967      loop_continue_certificate(remaining, operation, plan, cursor, original_left, original_right, original, state, index, converted, exact,
968        rec(state,
969          {\{Elementwise.InvariantModel: invariant => invariant} :
970            Elementwise.InvariantModel<operation, plan, original_left, original_right, 1n+cursor, state> ->
971              Elementwise.StateInvariant(operation, plan, original_left, original_right, 1n+cursor, state)}(invariant_advance(operation, plan, original_left, original_right, cursor, index, converted,
972                original, state, invariant, meaning))))