def loop_dimensions

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

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

483def loop_dimensions(fuel: Nat, +operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +cursor: Nat,
484  state: Elementwise.State<Shape.output_shape(plan)>) ->
485  Totality.DimensionsModel<Shape.dimensions(Shape.output_shape(plan)), Elementwise.loop(fuel, operation, plan, cursor, state)>:
486  match fuel:
487    case 0n:
488      Elementwise.State{left, right, output} = state
489      Totality.DimensionsModel{{==}}
490    case 1n+remaining:
491      loop_finish_dimensions(remaining, operation, plan, cursor, Elementwise.natural_step(operation, plan, cursor, state),
492        state => loop_dimensions(remaining, operation, plan, 1n+cursor, state))