The global shard number of a word (dpoPartitions' order: parameters, one
per word when partitioned; shared state; coordinate words), which names
its file.
231def dpotGlobalOf =
232 (lambda unrestricted c : Nat .
233 (lambda unrestricted u : Nat .
234 (lambda unrestricted system : (family DataParallelSystem c u) .
235 (lambda unrestricted q : Nat .
236 (lambda unrestricted p : Nat .
237 (lambda unrestricted ordinal : Nat .
238 (lambda unrestricted begin : Nat .
239 (let unrestricted shared =
240 (dpoShared c u system q)
241 in
242 (let unrestricted word =
243 (naturalDivideUnchecked begin dpWord)
244 in
245 (let unrestricted parameters =
246 (naturalSelect p (dpK c u system) 1)
247 in
248 (naturalSelect
249 (naturalIsZero ordinal)
250 (naturalSelect p word 0)
251 (naturalSelect
252 (naturalEqual ordinal (dpoCoordinateOrdinal shared))
253 (naturalAdd (naturalAdd parameters (naturalNonzero shared)) word)
254 parameters))))))))))))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.