This owner's samples into its (numerator, mass) leaf value, in order,
reading the parameters at `parameters`.
748def dpContribute =
749 (lambda unrestricted c : Nat .
750 (lambda unrestricted u : Nat .
751 (lambda unrestricted system : (family DataParallelSystem c u) .
752 (lambda unrestricted layout : (family NativeDataParallelLayout) .
753 (lambda unrestricted parameters : Nat .
754 (lambda unrestricted owner : Nat .
755 (lambda unrestricted contribution : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
756 (lambda unrestricted tail : (family NativePhysicalCommands) .
757 (let unrestricted k =
758 (dpK c u system)
759 in
760 (let unrestricted s =
761 (dpS c u system)
762 in
763 (let unrestricted leaf =
764 (dpLeafAt layout)
765 in
766 (let unrestricted at =
767 (dpContributionAt c u system layout)
768 in
769 (dpEach
770 (succ k)
771 (lambda unrestricted index : Nat .
772 (nativeMemoryStoreWord64
773 b"data-parallel-zero"
774 (nativePointwiseAt leaf index)
775 (nativeLaunchRecipeImmediate 0)))
776 (dpEach
777 (stdListLength
778 (family StdList StdU64)
779 (dataParallelSamplesOf c u system owner))
780 (lambda unrestricted sample : Nat .
781 (lambda unrestricted rest : (family NativePhysicalCommands) .
782 (dpCopy
783 at
784 parameters
785 (dpParameterBytes c u system)
786 (dpCopy
787 (nativePointwiseAt at k)
788 (naturalAdd
789 (dpSamplesAt c u system layout)
790 (naturalMultiply sample (dpSampleBytes c u system)))
791 (dpSampleBytes c u system)
792 (contribution
793 (dpEach
794 k
795 (lambda unrestricted index : Nat .
796 (dpAdd
797 (nativePointwiseAt leaf index)
798 (nativePointwiseAt leaf index)
799 (nativePointwiseAt at (naturalAdd (naturalAdd k s) index))))
800 (dpAdd
801 (nativePointwiseAt leaf k)
802 (nativePointwiseAt leaf k)
803 (dpOneAt c u system layout)
804 rest)))))))
805 tail))))))))))))))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.