def loop_finish_retains

bendtorch-core@0.1.0.0 · src/tensor/elementwise_PROOF.bend:371

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
import bendtorch-core@0.1.0.0/src/tensor/elementwise_totality.bend as Totality

371def loop_finish_retains(+fuel: Nat, +operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +cursor: Nat,
372  -left: Core.Dynamic, -right: Core.Dynamic, result: Elementwise.NaturalStep<Shape.output_shape(plan), cursor>,
373  -sources: NaturalSources<Shape.output_shape(plan), cursor, left, right, result>,
374  -rec: @state: Elementwise.State<Shape.output_shape(plan)> ->
375    @-l: Totality.SameSource(left, step_left_owner(Shape.output_shape(plan), Elementwise.Continue{state})) ->
376    @-r: Totality.SameSource(right, step_right_owner(Shape.output_shape(plan), Elementwise.Continue{state})) ->
377    Totality.Retention<left, right, Elementwise.loop(fuel, operation, plan, 1n+cursor, state)>) ->
378  Totality.Retention<left, right, Elementwise.finish_step(Shape.output_shape(plan), cursor,
379    state => Elementwise.loop(fuel, operation, plan, 1n+cursor, state), result)>:
380  match result:
381    case Elementwise.NaturalStop{retained_left, retained_right, error}:
382      Totality.Retention{
383        {\{NaturalSources: l => r => l} : NaturalSources<Shape.output_shape(plan), cursor, left, right, Elementwise.NaturalStop{retained_left, retained_right, error}> -> Totality.SameSource(left, retained_left)}(sources),
384        {\{NaturalSources: l => r => r} : NaturalSources<Shape.output_shape(plan), cursor, left, right, Elementwise.NaturalStop{retained_left, retained_right, error}> -> Totality.SameSource(right, retained_right)}(sources)}
385    case Elementwise.NaturalContinue{state, index, exact}:
386      retention_reify(left, right, Elementwise.loop(fuel, operation, plan, 1n+cursor, state),
387        rec(state)(
388          {\{NaturalSources: l => r => l} : NaturalSources<Shape.output_shape(plan), cursor, left, right, Elementwise.NaturalContinue{state, index, exact}> ->
389            Totality.SameSource(left, step_left_owner(Shape.output_shape(plan), Elementwise.Continue{state}))}(sources))(
390          {\{NaturalSources: l => r => r} : NaturalSources<Shape.output_shape(plan), cursor, left, right, Elementwise.NaturalContinue{state, index, exact}> ->
391            Totality.SameSource(right, step_right_owner(Shape.output_shape(plan), Elementwise.Continue{state}))}(sources)))