def unset_step

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

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

321def unset_step(+node: Backward.Node, +shape: Shape.Shape, -value: Core.Dynamic, -saved: Backward.Saved, -slot: Gradient.Slot,
322  -rest: List<&1, Backward.Entry>, -more: List<&1, Gradient.Slot>, +below: Nat, -slots: List<&1, Gradient.Slot>, -log: Laws.Log(),
323  -w: Gradient.Slot, -older: List<&1, Gradient.Slot>, -left: Laws.Log(),
324  at: {slots == w <> older : List<&1, Gradient.Slot>}, took: {Laws.take(log, below, w) == (Done{Gradient.Unset{}}, left) : Laws.Taken()},
325  out: Run<rest, more, below, older, left>) ->
326  Run<Backward.Entry{node, shape, value, saved, slot} <> rest, Gradient.Unset{} <> more, 1n+below, slots, log>:
327  match out:
328    case Kept{done, gradients, swept, pulled}:
329      Kept{Backward.Entry{node, shape, value, saved, slot} <> done, Gradient.Unset{} <> gradients,
330        Equal.cong(Backward.Swept(), Backward.Swept(),
331          pair => Backward.finished(Backward.Entry{node, shape, value, saved, slot}, Gradient.Unset{}, pair),
332          Backward.sweep(rest, Done{more}, below), (done, Done{gradients}), swept),
333        Equal.trans(Laws.Slots(), Laws.chained(Backward.Entry{node, shape, value, saved, slot} <> rest, slots, 1n+below, log),
334          Laws.chained(Backward.Entry{node, shape, value, saved, slot} <> rest, w <> older, 1n+below, log),
335          Done{Gradient.Unset{} <> gradients},
336          Equal.cong(List<&1, Gradient.Slot>, Laws.Slots(),
337            list => Laws.chained(Backward.Entry{node, shape, value, saved, slot} <> rest, list, 1n+below, log), slots, w <> older, at),
338          Equal.trans(Laws.Slots(), Laws.reached(node, saved, Laws.take(log, below, w), next => Laws.chained(rest, older, below, next)),
339            Laws.reached(node, saved, (Done{Gradient.Unset{}}, left), next => Laws.chained(rest, older, below, next)),
340            Done{Gradient.Unset{} <> gradients},
341            Equal.cong(Laws.Taken(), Laws.Slots(), taken => Laws.reached(node, saved, taken, next => Laws.chained(rest, older, below, next)),
342              Laws.take(log, below, w), (Done{Gradient.Unset{}}, left), took),
343            Equal.cong(Laws.Slots(), Laws.Slots(), result => Backward.prepend(Gradient.Slot, Gradient.Unset{}, result),
344              Laws.chained(rest, older, below, left), Done{gradients}, pulled)))}
345    case Stopped{done, error, swept}:
346      Stopped{Backward.Entry{node, shape, value, saved, slot} <> done, error,
347        Equal.cong(Backward.Swept(), Backward.Swept(),
348          pair => Backward.finished(Backward.Entry{node, shape, value, saved, slot}, Gradient.Unset{}, pair),
349          Backward.sweep(rest, Done{more}, below), (done, Fail{error}), swept)}