def loop_finish_dimensions

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

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
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

471def loop_finish_dimensions(+fuel: Nat, +operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +cursor: Nat,
472  result: Elementwise.NaturalStep<Shape.output_shape(plan), cursor>,
473  -rec: @state: Elementwise.State<Shape.output_shape(plan)> ->
474    Totality.DimensionsModel<Shape.dimensions(Shape.output_shape(plan)), Elementwise.loop(fuel, operation, plan, 1n+cursor, state)>) ->
475  Totality.DimensionsModel<Shape.dimensions(Shape.output_shape(plan)), Elementwise.finish_step(Shape.output_shape(plan), cursor,
476    state => Elementwise.loop(fuel, operation, plan, 1n+cursor, state), result)>:
477  match result:
478    case Elementwise.NaturalStop{left, right, error}:
479      Totality.DimensionsModel{Unit{}}
480    case Elementwise.NaturalContinue{state, index, exact}:
481      dimensions_reify(Shape.dimensions(Shape.output_shape(plan)), Elementwise.loop(fuel, operation, plan, 1n+cursor, state), rec(state))