The same learner with its input sequence split into `owners` contiguous
shares whose sizes differ by at most one, larger first.
470def dataParallelRepartitioned =
471 (lambda erased contribution : Nat .
472 (lambda erased update : Nat .
473 (lambda unrestricted system : (family DataParallelSystem contribution update) .
474 (lambda unrestricted owners : Nat .
475 (let unrestricted samples =
476 (dataParallelAllSamples contribution update system)
477 in
478 (let unrestricted total =
479 (stdListLength (family StdList StdU64) samples)
480 in
481 (let unrestricted base =
482 (naturalDivideUnchecked total owners)
483 in
484 (let unrestricted extra =
485 (naturalModuloUnchecked total owners)
486 in
487 (eliminate
488 DataParallelSystem
489 (lambda unrestricted current : (family DataParallelSystem contribution update) .
490 (family DataParallelSystem contribution update))
491 system
492 (branch
493 DataParallelSystemOf
494 parameters
495 width
496 program
497 rule
498 initial
499 state
500 rate
501 held
502 .
503 (constructor
504 DataParallelSystem
505 DataParallelSystemOf
506 contribution
507 update
508 parameters
509 width
510 program
511 rule
512 initial
513 state
514 rate
515 (stdListMap
516 Nat
517 (family StdList (family StdList StdU64))
518 (lambda unrestricted share : Nat .
519 (stdListTake
520 (family StdList StdU64)
521 (naturalAdd base (naturalLess share extra))
522 (stdListDrop
523 (family StdList StdU64)
524 (naturalAdd
525 (naturalMultiply share base)
526 (naturalMinimum share extra))
527 samples)))
528 (stdListNaturalsBelow owners)))))))))))))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.