The update is separable under q per-coordinate state words: a coordinate's
assignment reads only its coordinate and shared values, and a shared
assignment reads only shared values.
586def dataParallelSeparable =
587 (lambda unrestricted contribution : Nat .
588 (lambda unrestricted update : Nat .
589 (lambda unrestricted system : (family DataParallelSystem contribution update) .
590 (lambda unrestricted q : Nat .
591 (let unrestricted k =
592 (dataParallelParameters contribution update system)
593 in
594 (let unrestricted m =
595 (dataParallelStateCount contribution update system)
596 in
597 (naturalAnd
598 (naturalLessOrEqual (naturalMultiply q k) m)
599 (stdListFold
600 (family PointwiseAssignment StdU64 update)
601 Nat
602 (lambda unrestricted assignment : (family PointwiseAssignment StdU64 update) .
603 (lambda unrestricted rest : Nat .
604 (eliminate
605 PointwiseAssignment
606 (lambda unrestricted current : (family PointwiseAssignment StdU64 update) .
607 Nat)
608 assignment
609 (branch
610 PointwiseAssign
611 destination
612 expression
613 .
614 (naturalAnd
615 rest
616 (dataParallelReadsClass
617 update
618 k
619 m
620 q
621 (dataParallelSlotClass k m q (stdFinToNatural update destination))
622 expression))))))
623 1
624 (dataParallelUpdateProgram contribution update system)))))))))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.