def natural_decided_success

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

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
import bendtorch-core@0.1.0.0/src/shape/plan_proofs.bend as PlanProof
import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats

740def natural_decided_success(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +cursor: Nat, +index: U32,
741  decision: Shape.BoolCase<Nat.is_eq(U32.to_nat(index), cursor)>, state: Elementwise.State<Shape.output_shape(plan)>,
742  -fits: FittingSources<plan, step_left_owner(Shape.output_shape(plan), Elementwise.Continue{state}), step_right_owner(Shape.output_shape(plan), Elementwise.Continue{state})>,
743  -exact: {U32.to_nat(index) == cursor : Nat}, -inside: {Nat.is_lt(cursor, Shape.elements(Shape.output_shape(plan))) == True{} : Bool}) ->
744  NaturalSuccess<Shape.output_shape(plan), cursor, Elementwise.natural_step_decided(operation, plan, cursor, index, state, decision)>:
745  match decision:
746    case Shape.BFalse{equal}:
747      Elementwise.State{left, right, output} = state
748      NaturalSuccess{Empty.absurd({False{} == True{} : Bool}, Nats.contradiction(Nat.is_eq(U32.to_nat(index), cursor), PlanProof.eq_true(U32.to_nat(index), cursor, exact), equal))}
749    case Shape.BTrue{equal}:
750      natural_result_success(Shape.output_shape(plan), cursor, index, Lifecycle.natural_equal(U32.to_nat(index), cursor, equal),
751        Elementwise.step(operation, plan, index, state),
752        {\{StepSuccess: successful => successful} : StepSuccess<Shape.output_shape(plan), Elementwise.step(operation, plan, index, state)> ->
753          {step_succeeded(Shape.output_shape(plan), Elementwise.step(operation, plan, index, state)) == True{} : Bool}}(
754            actual_step_success(operation, plan, index, state, fits,
755              %Equal.sym(Nat, U32.to_nat(index), cursor, exact) : {Nat.is_lt(_, Shape.elements(Shape.output_shape(plan))) == True{} : Bool}
756              inside)))