The means the update reads: every coordinate's from the replicated sum,
or, with gradient partitioning, only this owner's coordinates' from its
reduction (word idx of owner r's value is coordinate r + idx n).
849def dpoMeans =
850 (lambda unrestricted c : Nat .
851 (lambda unrestricted u : Nat .
852 (lambda unrestricted system : (family DataParallelSystem c u) .
853 (lambda unrestricted layout : (family NativeDataParallelOwnedLayout) .
854 (lambda unrestricted role : Nat .
855 (lambda unrestricted at : Nat .
856 (lambda unrestricted tail : (family NativePhysicalCommands) .
857 (let unrestricted k =
858 (dpK c u system)
859 in
860 (let unrestricted m =
861 (dpM c u system)
862 in
863 (let unrestricted owners =
864 (dpOwners c u system)
865 in
866 (nat-eliminate
867 (lambda unrestricted partitioned : Nat . (family NativePhysicalCommands))
868 (let unrestricted total =
869 (nativeCombineResultAt (dpoSum layout))
870 in
871 (dpEach
872 k
873 (lambda unrestricted index : Nat .
874 (dpDivide
875 (nativePointwiseAt at (naturalAdd (naturalAdd k m) index))
876 (nativePointwiseAt total index)
877 (nativePointwiseAt total k)))
878 tail))
879 (lambda unrestricted previous : Nat .
880 (lambda unrestricted ignored : (family NativePhysicalCommands) .
881 (let unrestricted owned =
882 (nativeCombineResultAt (dpoGradientAt layout role))
883 in
884 (dpEach
885 k
886 (lambda unrestricted index : Nat .
887 (lambda unrestricted rest : (family NativePhysicalCommands) .
888 (nat-eliminate
889 (lambda unrestricted held : Nat .
890 (family NativePhysicalCommands))
891 rest
892 (lambda unrestricted previous : Nat .
893 (lambda unrestricted ignored : (family NativePhysicalCommands) .
894 (dpDivide
895 (nativePointwiseAt at (naturalAdd (naturalAdd k m) index))
896 (nativePointwiseAt
897 owned
898 (naturalDivideUnchecked index owners))
899 (nativePointwiseAt owned (dpoPerOwner k owners))
900 rest)))
901 (dpoOwns owners role index))))
902 tail))))
903 (naturalNonzero
904 (stdListLength (family NativeCombinePlacement) (dpoGradients layout))))))))))))))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.