The assignments one owner runs: every shared assignment and those of the
coordinates `owns` names (owns i = 1), in program order.
628def dataParallelOwnedProgram =
629 (lambda unrestricted contribution : Nat .
630 (lambda unrestricted update : Nat .
631 (lambda unrestricted system : (family DataParallelSystem contribution update) .
632 (lambda unrestricted q : Nat .
633 (lambda unrestricted owns : (pi unrestricted coordinate : Nat . Nat) .
634 (let unrestricted k =
635 (dataParallelParameters contribution update system)
636 in
637 (let unrestricted m =
638 (dataParallelStateCount contribution update system)
639 in
640 (stdListFold
641 (family PointwiseAssignment StdU64 update)
642 (family StdList (family PointwiseAssignment StdU64 update))
643 (lambda unrestricted assignment : (family PointwiseAssignment StdU64 update) .
644 (lambda unrestricted rest : (family StdList (family PointwiseAssignment StdU64 update)) .
645 (eliminate
646 PointwiseAssignment
647 (lambda unrestricted current : (family PointwiseAssignment StdU64 update) .
648 (family StdList (family PointwiseAssignment StdU64 update)))
649 assignment
650 (branch
651 PointwiseAssign
652 destination
653 expression
654 .
655 (let unrestricted class =
656 (dataParallelSlotClass k m q (stdFinToNatural update destination))
657 in
658 (nat-eliminate
659 (lambda unrestricted current : Nat .
660 (family StdList (family PointwiseAssignment StdU64 update)))
661 rest
662 (lambda unrestricted previous : Nat .
663 (lambda unrestricted ignored : (family StdList (family PointwiseAssignment StdU64 update)) .
664 (constructor
665 StdList
666 StdListCons
667 (family PointwiseAssignment StdU64 update)
668 assignment
669 rest)))
670 (naturalOr (naturalIsZero class) (owns (naturalPredecessor class)))))))))
671 (constructor StdList StdListEmpty (family PointwiseAssignment StdU64 update))
672 (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.