def loop_retains

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

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

393def loop_retains(fuel: Nat, +operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +cursor: Nat,
394  -left: Core.Dynamic, -right: Core.Dynamic, state: Elementwise.State<Shape.output_shape(plan)>,
395  -left_same: Totality.SameSource(left, step_left_owner(Shape.output_shape(plan), Elementwise.Continue{state})),
396  -right_same: Totality.SameSource(right, step_right_owner(Shape.output_shape(plan), Elementwise.Continue{state}))) ->
397  Totality.Retention<left, right, Elementwise.loop(fuel, operation, plan, cursor, state)>:
398  match fuel:
399    case 0n:
400      Elementwise.State{retained_left, retained_right, output} = state
401      Totality.Retention{left_same, right_same}
402    case 1n+remaining:
403      loop_finish_retains(remaining, operation, plan, cursor, left, right, Elementwise.natural_step(operation, plan, cursor, state),
404        {\{NaturalSources: l => r => NaturalSources{
405          property => Equal.trans(Totality.Inspection,
406            Totality.inspect(property, natural_left_owner(Shape.output_shape(plan), cursor, Elementwise.natural_step(operation, plan, cursor, state))),
407            Totality.inspect(property, step_left_owner(Shape.output_shape(plan), Elementwise.Continue{state})), Totality.inspect(property, left), l(property), left_same(property)),
408          property => Equal.trans(Totality.Inspection,
409            Totality.inspect(property, natural_right_owner(Shape.output_shape(plan), cursor, Elementwise.natural_step(operation, plan, cursor, state))),
410            Totality.inspect(property, step_right_owner(Shape.output_shape(plan), Elementwise.Continue{state})), Totality.inspect(property, right), r(property), right_same(property))}} :
411          NaturalSources<Shape.output_shape(plan), cursor, step_left_owner(Shape.output_shape(plan), Elementwise.Continue{state}), step_right_owner(Shape.output_shape(plan), Elementwise.Continue{state}),
412            Elementwise.natural_step(operation, plan, cursor, state)> ->
413          NaturalSources<Shape.output_shape(plan), cursor, left, right, Elementwise.natural_step(operation, plan, cursor, state)>}(
414            natural_decided_retains(operation, plan, cursor, U32.from_nat(cursor), Shape.bool_case(Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), cursor)), state)),
415        state => l => r => loop_retains(remaining, operation, plan, 1n+cursor, left, right, state, l, r))