def gathered

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

import Base
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

27# With no entry left, the pull side gathers exactly the pending slots.
28def gathered(pending: List<&1, Gradient.Slot>, +count: Nat, -slots: List<&1, Gradient.Slot>, -log: Laws.Log(),
29  pulls: Pulls(pending, slots, count, log)) -> {Laws.gather(slots, count, log) == Done{pending} : Laws.Slots()}:
30  match pending count:
31    case Nil{} count:
32      %Equal.sym(List<&1, Gradient.Slot>, slots, Nil{}, pulls) : {Laws.gather(_, count, log) == Done{Nil{}} : Laws.Slots()}
33      {==}
34    case Con{x, rest} 0n:
35      %Equal.sym(List<&1, Gradient.Slot>, slots, x <> rest, pulls) : {Laws.gather(_, 0n, log) == Done{x <> rest} : Laws.Slots()}
36      {==}
37    case Con{x, rest} 1n+below:
38      Cell{w, older, left, at, took, tail} = pulls
39      %Equal.sym(List<&1, Gradient.Slot>, slots, w <> older, at) : {Laws.gather(_, 1n+below, log) == Done{x <> rest} : Laws.Slots()}
40      %Equal.sym(Laws.Taken(), Laws.take(log, below, w), (Done{x}, left), took) :
41        {Laws.gather_step(_, more => Laws.gather(older, below, more)) == Done{x <> rest} : Laws.Slots()}
42      Equal.cong(Laws.Slots(), Laws.Slots(), result => Backward.prepend(Gradient.Slot, x, result),
43        Laws.gather(older, below, left), Done{rest}, gathered(rest, below, older, left, tail))