argv for n owners and h global shards, positions after the program name:
1 the previous root manifest; 1 + r the previous group manifest of role
r >= 1; n + 1 + g the previous shard g; n + 1 + h + 2r and n + 2 + h + 2r
the candidate and committed group manifest of role r (role 0's is the
published root); 3n + 1 + h + 2g and 3n + 2 + h + 2g the candidate and
committed shard g; 3n + 1 + 3h the generation directory. Every owner
receives the same argv; a role's own shard j is the global shard its
record names.
300def dpotPaths =
301 (lambda unrestricted c : Nat .
302 (lambda unrestricted u : Nat .
303 (lambda unrestricted system : (family DataParallelSystem c u) .
304 (lambda unrestricted q : Nat .
305 (lambda unrestricted p : Nat .
306 (lambda unrestricted role : Nat .
307 (let unrestricted owners =
308 (dpOwners c u system)
309 in
310 (let unrestricted shards =
311 (dpoShardCount c u system q p)
312 in
313 (let unrestricted groups =
314 (naturalAdd (succ owners) shards)
315 in
316 (let unrestricted outputs =
317 (naturalAdd (succ (naturalMultiply 3 owners)) shards)
318 in
319 (let unrestricted globals =
320 (dpotOwnGlobals c u system q p role)
321 in
322 (constructor
323 NativeTreePaths
324 NativeTreePathsOf
325 (lambda unrestricted at : Nat . (succ at))
326 (lambda unrestricted index : Nat .
327 (succ (naturalAdd owners (dpotNth globals index))))
328 (naturalAdd groups (naturalMultiply 2 role))
329 (succ (naturalAdd groups (naturalMultiply 2 role)))
330 (lambda unrestricted index : Nat .
331 (naturalAdd outputs (naturalMultiply 2 (dpotNth globals index))))
332 (lambda unrestricted index : Nat .
333 (succ (naturalAdd outputs (naturalMultiply 2 (dpotNth globals index)))))
334 (naturalAdd (succ (naturalMultiply 3 owners)) (naturalMultiply 3 shards))))))))))))))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.