One reduction per coordinate owner, from `base`: each placement's frames,
then its leaf value, then the next placement.
608def dpoGradientPlacementsFor =
609 (lambda unrestricted c : Nat .
610 (lambda unrestricted u : Nat .
611 (lambda unrestricted system : (family DataParallelSystem c u) .
612 (lambda unrestricted digest : Bytes .
613 (lambda unrestricted topology : (family DataParallelTopology) .
614 (lambda unrestricted role : Nat .
615 (lambda unrestricted base : Nat .
616 (app
617 (app
618 (nat-eliminate
619 (lambda unrestricted current : Nat .
620 (pi unrestricted owner : Nat .
621 (pi unrestricted from : Nat .
622 (family StdList (family NativeCombinePlacement)))))
623 (lambda unrestricted owner : Nat .
624 (lambda unrestricted from : Nat .
625 (constructor StdList StdListEmpty (family NativeCombinePlacement))))
626 (lambda unrestricted previous : Nat .
627 (lambda unrestricted rest : (pi unrestricted owner : Nat . (pi unrestricted from : Nat . (family StdList (family NativeCombinePlacement)))) .
628 (lambda unrestricted owner : Nat .
629 (lambda unrestricted from : Nat .
630 (let unrestricted placement =
631 (constructor
632 NativeCombinePlacement
633 NativeCombinePlacementOf
634 (nativeCombineDeliveringContextFor
635 (dpoGradientAnchor c u system digest topology owner)
636 (dpoGradientDelivery owner)
637 role
638 (dpTree topology (dpOwners c u system)))
639 from
640 (dpoGradientBytes c u system))
641 in
642 (constructor
643 StdList
644 StdListCons
645 (family NativeCombinePlacement)
646 placement
647 (rest
648 (succ owner)
649 (frameAlign
650 (naturalAdd
651 (nativeCombineRegionEnd placement)
652 (dpoGradientBytes c u system))))))))))
653 (dpoGradientOwners c u system))
654 0)
655 base))))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.