def newer_step

bendtorch-core@0.1.0.0 · src/autograd/tensor_chain_PROOF.bend:555

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/autograd/gradient.bend as Gradient
import bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend as Backward
import bendtorch-core@0.1.0.0/src/autograd/tensor_chain_LAWS.bend as Laws

555def newer_step(+node: Backward.Node, +shape: Shape.Shape, -value: Core.Dynamic, -saved: Backward.Saved, -slot: Gradient.Slot,
556  -rest: List<&1, Backward.Entry>, -below: Nat, +older: Nat, -slots: List<&1, Gradient.Slot>,
557  out: Passed<rest, below, older, Backward.at_head(below, older), slots>) ->
558  Passed<Backward.Entry{node, shape, value, saved, slot} <> rest, 1n+below, older, False{}, Gradient.Unset{} <> slots>:
559  match out:
560    case PassKept{done, gradients, passed, chained}:
561      PassKept{Backward.Entry{node, shape, value, saved, slot} <> done, Gradient.Unset{} <> gradients,
562        Equal.cong(Backward.Swept(), Backward.Swept(),
563          pair => Backward.finished(Backward.Entry{node, shape, value, saved, slot}, Gradient.Unset{}, pair),
564          Backward.pass(rest, below, older, Backward.at_head(below, older)), (done, Done{gradients}), passed),
565        Equal.cong(Laws.Slots(), Laws.Slots(), result => Backward.prepend(Gradient.Slot, Gradient.Unset{}, result),
566          Laws.chained(rest, slots, below, Nil{}), Done{gradients}, chained)}
567    case PassStopped{done, error, passed}:
568      PassStopped{Backward.Entry{node, shape, value, saved, slot} <> done, error,
569        Equal.cong(Backward.Swept(), Backward.Swept(),
570          pair => Backward.finished(Backward.Entry{node, shape, value, saved, slot}, Gradient.Unset{}, pair),
571          Backward.pass(rest, below, older, Backward.at_head(below, older)), (done, Fail{error}), passed)}