1914def dpoShardOffset =
1915 (lambda unrestricted c : Nat .
1916 (lambda unrestricted u : Nat .
1917 (lambda unrestricted system : (family DataParallelSystem c u) .
1918 (lambda unrestricted q : Nat .
1919 (lambda unrestricted p : Nat .
1920 (lambda unrestricted shard : (family NativeRegionShard) .
1921 (let unrestricted k =
1922 (dpK c u system)
1923 in
1924 (let unrestricted owners =
1925 (dpOwners c u system)
1926 in
1927 (let unrestricted shared =
1928 (dpoShared c u system q)
1929 in
1930 (let unrestricted ordinal =
1931 (nativeRegionOrdinal shard)
1932 in
1933 (let unrestricted replicated =
1934 (dpoReplicatedParameterBytes c u system p)
1935 in
1936 (let unrestricted owned =
1937 (naturalAdd replicated (naturalMultiply dpWord shared))
1938 in
1939 (naturalAdd
1940 nativeRegionCaptureBytes
1941 (naturalSelect
1942 (naturalIsZero ordinal)
1943 (naturalSelect
1944 p
1945 (naturalAdd owned (dpoWordOffset k owners 0 (dpoShardWord shard)))
1946 (intervalBegin (nativeRegionInterval shard)))
1947 (naturalSelect
1948 (naturalEqual ordinal (dpoCoordinateOrdinal shared))
1949 (naturalAdd
1950 owned
1951 (dpoWordOffset
1952 k
1953 owners
1954 (naturalAdd (naturalDivideUnchecked (dpoShardWord shard) k) p)
1955 (naturalModuloUnchecked (dpoShardWord shard) k)))
1956 (naturalAdd replicated (intervalBegin (nativeRegionInterval shard))))))))))))))))))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.