def natural_decided_retains

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

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/lifecycle.bend as Lifecycle

349def natural_decided_retains(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +cursor: Nat, +index: U32,
350  decision: Shape.BoolCase<Nat.is_eq(U32.to_nat(index), cursor)>, state: Elementwise.State<Shape.output_shape(plan)>) ->
351  NaturalSources<Shape.output_shape(plan), cursor,
352    step_left_owner(Shape.output_shape(plan), Elementwise.Continue{state}), step_right_owner(Shape.output_shape(plan), Elementwise.Continue{state}),
353    Elementwise.natural_step_decided(operation, plan, cursor, index, state, decision)>:
354  match decision:
355    case Shape.BFalse{equal}:
356      Elementwise.State{left, right, output} = state
357      NaturalSources{property => {==}, property => {==}}
358    case Shape.BTrue{equal}:
359      natural_result_retains(Shape.output_shape(plan), cursor, index, Lifecycle.natural_equal(U32.to_nat(index), cursor, equal),
360        step_left_owner(Shape.output_shape(plan), Elementwise.Continue{state}), step_right_owner(Shape.output_shape(plan), Elementwise.Continue{state}),
361        Elementwise.step(operation, plan, index, state),
362        step_indices_retains(operation, Shape.output_shape(plan), index, state, Elementwise.input_indices(plan, index)))