mean = numerator / mass, then the update program on (parameters, state,
mean, rate), then the logical position advances. Every owner runs this on
the replicated root value.
810def dpUpdate =
811 (lambda unrestricted c : Nat .
812 (lambda unrestricted u : Nat .
813 (lambda unrestricted system : (family DataParallelSystem c u) .
814 (lambda unrestricted layout : (family NativeDataParallelLayout) .
815 (lambda unrestricted update : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
816 (lambda unrestricted tail : (family NativePhysicalCommands) .
817 (let unrestricted k =
818 (dpK c u system)
819 in
820 (let unrestricted m =
821 (dpM c u system)
822 in
823 (let unrestricted total =
824 (nativeCombineResultAt (dpPlacement layout))
825 in
826 (let unrestricted at =
827 (dpUpdateAt c u system layout)
828 in
829 (dpEach
830 k
831 (lambda unrestricted index : Nat .
832 (dpDivide
833 (nativePointwiseAt at (naturalAdd (naturalAdd k m) index))
834 (nativePointwiseAt total index)
835 (nativePointwiseAt total k)))
836 (dpCopy
837 at
838 (dpParametersAt layout)
839 (dpReplicatedBytes c u system)
840 (nativeMemoryStoreWord64
841 b"data-parallel-rate"
842 (nativePointwiseAt at (naturalAdd (naturalMultiply 2 k) m))
843 (nativeLaunchRecipeImmediate
844 (modelWord64Natural (dataParallelRateWord c u system)))
845 (update
846 (dpCopy
847 (dpParametersAt layout)
848 at
849 (dpReplicatedBytes c u system)
850 (niAdvanceAt (dpStateAt layout) 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.