def newer_chain

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

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

573def newer_chain(newer: List<&1, Backward.Entry>, +node: Backward.Node, +shape: Shape.Shape, value: Core.Dynamic, saved: Backward.Saved,
574  slot: Gradient.Slot, rest: List<&1, Backward.Entry>, +older: Nat, ones: Core.Tensor<shape>,
575  made: {Core.new(shape, 1.0) == Done{ones} : Result<&2, &1, Core.Error, Core.Tensor<shape>>}) ->
576  Passed<List.append(&1, Backward.Entry, newer, Backward.Entry{node, shape, value, saved, slot} <> rest),
577    1n+Nat.add(older, List.length(&1, Backward.Entry, newer)), older,
578    Backward.at_head(1n+Nat.add(older, List.length(&1, Backward.Entry, newer)), older),
579    Laws.seeds(List.length(&1, Backward.Entry, newer), shape, ones, older)>:
580  match newer:
581    case Nil{}:
582      %add_zero(older) :
583        Passed<Backward.Entry{node, shape, value, saved, slot} <> rest, 1n+_, older, Backward.at_head(1n+_, older),
584          Laws.seeds(0n, shape, ones, older)>
585      %eq_refl(older) :
586        Passed<Backward.Entry{node, shape, value, saved, slot} <> rest, 1n+older, older, _, Laws.seeds(0n, shape, ones, older)>
587      seeded_run(node, shape, value, saved, slot, rest, older, ones, made,
588        started(Gradient.Held{Core.Packed{shape, ones}} <> Backward.unsets(older), 1n+older))
589    case Con{Backward.Entry{+top, +top_shape, top_value, top_saved, top_slot}, tail}:
590      %older_ne(older, List.length(&1, Backward.Entry, tail)) :
591        Passed<Backward.Entry{top, top_shape, top_value, top_saved, top_slot} <>
592            List.append(&1, Backward.Entry, tail, Backward.Entry{node, shape, value, saved, slot} <> rest),
593          1n+Nat.add(older, 1n+List.length(&1, Backward.Entry, tail)), older, _,
594          Laws.seeds(1n+List.length(&1, Backward.Entry, tail), shape, ones, older)>
595      %add_succ(older, List.length(&1, Backward.Entry, tail)) :
596        Passed<Backward.Entry{top, top_shape, top_value, top_saved, top_slot} <>
597            List.append(&1, Backward.Entry, tail, Backward.Entry{node, shape, value, saved, slot} <> rest),
598          1n+_, older, False{}, Laws.seeds(1n+List.length(&1, Backward.Entry, tail), shape, ones, older)>
599      newer_step(top, top_shape, top_value, top_saved, top_slot,
600        List.append(&1, Backward.Entry, tail, Backward.Entry{node, shape, value, saved, slot} <> rest),
601        1n+Nat.add(older, List.length(&1, Backward.Entry, tail)), older,
602        Laws.seeds(List.length(&1, Backward.Entry, tail), shape, ones, older),
603        newer_chain(tail, node, shape, value, saved, slot, rest, older, ones, made))