def seeded_out

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

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

507def seeded_out(+node: Backward.Node, +shape: Shape.Shape, -value: Core.Dynamic, -saved: Backward.Saved, -slot: Gradient.Slot,
508  -rest: List<&1, Backward.Entry>, +older: Nat, -ones: Core.Tensor<shape>, -copy: List<&1, Gradient.Slot>,
509  made: {Core.new(shape, 1.0) == Done{ones} : Result<&2, &1, Core.Error, Core.Tensor<shape>>},
510  same: {copy == Gradient.Held{Core.Packed{shape, ones}} <> Backward.unsets(older) : List<&1, Gradient.Slot>},
511  out: Run<Backward.Entry{node, shape, value, saved, slot} <> rest, copy, 1n+older,
512    Gradient.Held{Core.Packed{shape, ones}} <> Backward.unsets(older), Nil{}>) ->
513  Passed<Backward.Entry{node, shape, value, saved, slot} <> rest, 1n+older, older, True{},
514    Gradient.Held{Core.Packed{shape, ones}} <> Backward.unsets(older)>:
515  match out:
516    case Kept{done, gradients, swept, chained}:
517      PassKept{done, gradients,
518        Equal.trans(Backward.Swept(), Backward.seeded(node, shape, value, saved, slot, rest, older, Core.new(shape, 1.0)),
519          Backward.seeded(node, shape, value, saved, slot, rest, older, Done{ones}), (done, Done{gradients}),
520          Equal.cong(Result<&2, &1, Core.Error, Core.Tensor<shape>>, Backward.Swept(),
521            made_ones => Backward.seeded(node, shape, value, saved, slot, rest, older, made_ones), Core.new(shape, 1.0), Done{ones}, made),
522          Equal.trans(Backward.Swept(), Backward.seeded(node, shape, value, saved, slot, rest, older, Done{ones}),
523            Backward.sweep(Backward.Entry{node, shape, value, saved, slot} <> rest, Done{copy}, 1n+older), (done, Done{gradients}),
524            Equal.cong(List<&1, Gradient.Slot>, Backward.Swept(),
525              list => Backward.sweep(Backward.Entry{node, shape, value, saved, slot} <> rest, Done{list}, 1n+older),
526              Gradient.Held{Core.Packed{shape, ones}} <> Backward.unsets(older), copy,
527              Equal.sym(List<&1, Gradient.Slot>, copy, Gradient.Held{Core.Packed{shape, ones}} <> Backward.unsets(older), same)),
528            swept)),
529        chained}
530    case Stopped{done, error, swept}:
531      PassStopped{done, error,
532        Equal.trans(Backward.Swept(), Backward.seeded(node, shape, value, saved, slot, rest, older, Core.new(shape, 1.0)),
533          Backward.seeded(node, shape, value, saved, slot, rest, older, Done{ones}), (done, Fail{error}),
534          Equal.cong(Result<&2, &1, Core.Error, Core.Tensor<shape>>, Backward.Swept(),
535            made_ones => Backward.seeded(node, shape, value, saved, slot, rest, older, made_ones), Core.new(shape, 1.0), Done{ones}, made),
536          Equal.trans(Backward.Swept(), Backward.seeded(node, shape, value, saved, slot, rest, older, Done{ones}),
537            Backward.sweep(Backward.Entry{node, shape, value, saved, slot} <> rest, Done{copy}, 1n+older), (done, Fail{error}),
538            Equal.cong(List<&1, Gradient.Slot>, Backward.Swept(),
539              list => Backward.sweep(Backward.Entry{node, shape, value, saved, slot} <> rest, Done{list}, 1n+older),
540              Gradient.Held{Core.Packed{shape, ones}} <> Backward.unsets(older), copy,
541              Equal.sym(List<&1, Gradient.Slot>, copy, Gradient.Held{Core.Packed{shape, ones}} <> Backward.unsets(older), same)),
542            swept))}