1717def dpoRegions =
1718 (lambda unrestricted c : Nat .
1719 (lambda unrestricted u : Nat .
1720 (lambda unrestricted system : (family DataParallelSystem c u) .
1721 (lambda unrestricted q : Nat .
1722 (let unrestricted shared =
1723 (dpoShared c u system q)
1724 in
1725 (constructor
1726 StdList
1727 StdListCons
1728 (family CheckpointLogicalRegion)
1729 (constructor
1730 CheckpointLogicalRegion
1731 CheckpointLogicalRegionOf
1732 b"parameters"
1733 b"f64-le"
1734 (dpParameterBytes c u system))
1735 (stdListAppend
1736 (family CheckpointLogicalRegion)
1737 (nat-eliminate
1738 (lambda unrestricted words : Nat .
1739 (family StdList (family CheckpointLogicalRegion)))
1740 (constructor StdList StdListEmpty (family CheckpointLogicalRegion))
1741 (lambda unrestricted previous : Nat .
1742 (lambda unrestricted ignored : (family StdList (family CheckpointLogicalRegion)) .
1743 (constructor
1744 StdList
1745 StdListCons
1746 (family CheckpointLogicalRegion)
1747 (constructor
1748 CheckpointLogicalRegion
1749 CheckpointLogicalRegionOf
1750 b"shared-optimizer-state"
1751 b"f64-le"
1752 (naturalMultiply dpWord shared))
1753 (constructor StdList StdListEmpty (family CheckpointLogicalRegion)))))
1754 shared)
1755 (nat-eliminate
1756 (lambda unrestricted words : Nat .
1757 (family StdList (family CheckpointLogicalRegion)))
1758 (constructor StdList StdListEmpty (family CheckpointLogicalRegion))
1759 (lambda unrestricted previous : Nat .
1760 (lambda unrestricted ignored : (family StdList (family CheckpointLogicalRegion)) .
1761 (constructor
1762 StdList
1763 StdListCons
1764 (family CheckpointLogicalRegion)
1765 (constructor
1766 CheckpointLogicalRegion
1767 CheckpointLogicalRegionOf
1768 b"coordinate-optimizer-state"
1769 b"f64-le"
1770 (naturalMultiply dpWord (naturalMultiply q (dpK c u system))))
1771 (constructor StdList StdListEmpty (family CheckpointLogicalRegion)))))
1772 q))))))))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.