def fired_run

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

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

351def fired_run(+node: Backward.Node, +shape: Shape.Shape, -value: Core.Dynamic, -saved: Backward.Saved, -slot: Gradient.Slot,
352  -rest: List<&1, Backward.Entry>, -g: Core.Dynamic, -more: List<&1, Gradient.Slot>, +below: Nat, -slots: List<&1, Gradient.Slot>,
353  -log: Laws.Log(), -w: Gradient.Slot, -older: List<&1, Gradient.Slot>, -left: Laws.Log(),
354  at: {slots == w <> older : List<&1, Gradient.Slot>}, took: {Laws.take(log, below, w) == (Done{Gradient.Held{g}}, left) : Laws.Taken()},
355  out: Fired<node, shape, value, slot, rest, more, below, older, left, Backward.vjp(node, saved, g)>) ->
356  Run<Backward.Entry{node, shape, value, saved, slot} <> rest, Gradient.Held{g} <> more, 1n+below, slots, log>:
357  match out:
358    case FiredKept{done, gradients, swept, pulled}:
359      Kept{done, gradients, swept,
360        Equal.trans(Laws.Slots(), Laws.chained(Backward.Entry{node, shape, value, saved, slot} <> rest, slots, 1n+below, log),
361          Laws.chained(Backward.Entry{node, shape, value, saved, slot} <> rest, w <> older, 1n+below, log),
362          Done{gradients},
363          Equal.cong(List<&1, Gradient.Slot>, Laws.Slots(),
364            list => Laws.chained(Backward.Entry{node, shape, value, saved, slot} <> rest, list, 1n+below, log), slots, w <> older, at),
365          Equal.trans(Laws.Slots(), Laws.reached(node, saved, Laws.take(log, below, w), next => Laws.chained(rest, older, below, next)),
366            Laws.reached(node, saved, (Done{Gradient.Held{g}}, left), next => Laws.chained(rest, older, below, next)),
367            Done{gradients},
368            Equal.cong(Laws.Taken(), Laws.Slots(), taken => Laws.reached(node, saved, taken, next => Laws.chained(rest, older, below, next)),
369              Laws.take(log, below, w), (Done{Gradient.Held{g}}, left), took),
370            pulled))}
371    case FiredStopped{done, error, swept}:
372      Stopped{done, error, swept}