def fired_go

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

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

244def fired_go(+node: Backward.Node, +shape: Shape.Shape, -value: Core.Dynamic, -saved: Backward.Saved, -slot: Gradient.Slot,
245  -g: Core.Dynamic, -rest: List<&1, Backward.Entry>, -more: List<&1, Gradient.Slot>, +below: Nat, -older: List<&1, Gradient.Slot>,
246  -left: Laws.Log(), -items: Laws.Log(), -pending: List<&1, Gradient.Slot>,
247  delivered: {Done{pending} == Backward.deliver(items, below, Done{more}) : Laws.Slots()},
248  out: Run<rest, pending, below, older, List.reverse.go(&1, Backward.Contribution, items, left)>) ->
249  Fired<node, shape, value, slot, rest, more, below, older, left, Backward.Pass{saved, g, Done{items}}>:
250  match out:
251    case Kept{done, gradients, swept, pulled}:
252      FiredKept{Backward.Entry{node, shape, value, saved, slot} <> done, Gradient.Held{g} <> gradients,
253        Equal.trans(Backward.Swept(),
254          Backward.finished(Backward.Entry{node, shape, value, saved, slot}, Gradient.Held{g},
255            Backward.sweep(rest, Backward.deliver(items, below, Done{more}), below)),
256          Backward.finished(Backward.Entry{node, shape, value, saved, slot}, Gradient.Held{g}, Backward.sweep(rest, Done{pending}, below)),
257          Backward.finished(Backward.Entry{node, shape, value, saved, slot}, Gradient.Held{g}, (done, Done{gradients})),
258          Equal.cong(Laws.Slots(), Backward.Swept(),
259            state => Backward.finished(Backward.Entry{node, shape, value, saved, slot}, Gradient.Held{g}, Backward.sweep(rest, state, below)),
260            Backward.deliver(items, below, Done{more}), Done{pending},
261            Equal.sym(Laws.Slots(), Done{pending}, Backward.deliver(items, below, Done{more}), delivered)),
262          Equal.cong(Backward.Swept(), Backward.Swept(),
263            pair => Backward.finished(Backward.Entry{node, shape, value, saved, slot}, Gradient.Held{g}, pair),
264            Backward.sweep(rest, Done{pending}, below), (done, Done{gradients}), swept)),
265        Equal.cong(Laws.Slots(), Laws.Slots(), result => Backward.prepend(Gradient.Slot, Gradient.Held{g}, result),
266          Laws.chained(rest, older, below, List.reverse.go(&1, Backward.Contribution, items, left)), Done{gradients}, pulled)}
267    case Stopped{done, error, swept}:
268      FiredStopped{Backward.Entry{node, shape, value, saved, slot} <> done, error,
269        Equal.trans(Backward.Swept(),
270          Backward.finished(Backward.Entry{node, shape, value, saved, slot}, Gradient.Held{g},
271            Backward.sweep(rest, Backward.deliver(items, below, Done{more}), below)),
272          Backward.finished(Backward.Entry{node, shape, value, saved, slot}, Gradient.Held{g}, Backward.sweep(rest, Done{pending}, below)),
273          Backward.finished(Backward.Entry{node, shape, value, saved, slot}, Gradient.Held{g}, (done, Fail{error})),
274          Equal.cong(Laws.Slots(), Backward.Swept(),
275            state => Backward.finished(Backward.Entry{node, shape, value, saved, slot}, Gradient.Held{g}, Backward.sweep(rest, state, below)),
276            Backward.deliver(items, below, Done{more}), Done{pending},
277            Equal.sym(Laws.Slots(), Done{pending}, Backward.deliver(items, below, Done{more}), delivered)),
278          Equal.cong(Backward.Swept(), Backward.Swept(),
279            pair => Backward.finished(Backward.Entry{node, shape, value, saved, slot}, Gradient.Held{g}, pair),
280            Backward.sweep(rest, Done{pending}, below), (done, Fail{error}), swept))}