One shard per owned word (each parameter word too when partitioned), so
each lies wholly in its owner's state.
1789def dpoPartitions =
1790 (lambda unrestricted c : Nat .
1791 (lambda unrestricted u : Nat .
1792 (lambda unrestricted system : (family DataParallelSystem c u) .
1793 (lambda unrestricted q : Nat .
1794 (lambda unrestricted p : Nat .
1795 (let unrestricted k =
1796 (dpK c u system)
1797 in
1798 (let unrestricted shared =
1799 (dpoShared c u system q)
1800 in
1801 (constructor
1802 StdList
1803 StdListCons
1804 (family CheckpointRegionPartition)
1805 (constructor
1806 CheckpointRegionPartition
1807 CheckpointRegionPartitionOf
1808 0
1809 (nat-eliminate
1810 (lambda unrestricted current : Nat .
1811 (family StdList (family LogicalInterval)))
1812 (constructor
1813 StdList
1814 StdListCons
1815 (family LogicalInterval)
1816 (dpoInterval 0 (dpParameterBytes c u system))
1817 (constructor StdList StdListEmpty (family LogicalInterval)))
1818 (lambda unrestricted previous : Nat .
1819 (lambda unrestricted ignored : (family StdList (family LogicalInterval)) .
1820 (dpoWordIntervals k)))
1821 p))
1822 (stdListAppend
1823 (family CheckpointRegionPartition)
1824 (nat-eliminate
1825 (lambda unrestricted words : Nat .
1826 (family StdList (family CheckpointRegionPartition)))
1827 (constructor StdList StdListEmpty (family CheckpointRegionPartition))
1828 (lambda unrestricted previous : Nat .
1829 (lambda unrestricted ignored : (family StdList (family CheckpointRegionPartition)) .
1830 (constructor
1831 StdList
1832 StdListCons
1833 (family CheckpointRegionPartition)
1834 (constructor
1835 CheckpointRegionPartition
1836 CheckpointRegionPartitionOf
1837 dpoSharedOrdinal
1838 (constructor
1839 StdList
1840 StdListCons
1841 (family LogicalInterval)
1842 (dpoInterval 0 (naturalMultiply dpWord shared))
1843 (constructor StdList StdListEmpty (family LogicalInterval))))
1844 (constructor StdList StdListEmpty (family CheckpointRegionPartition)))))
1845 shared)
1846 (nat-eliminate
1847 (lambda unrestricted words : Nat .
1848 (family StdList (family CheckpointRegionPartition)))
1849 (constructor StdList StdListEmpty (family CheckpointRegionPartition))
1850 (lambda unrestricted previous : Nat .
1851 (lambda unrestricted ignored : (family StdList (family CheckpointRegionPartition)) .
1852 (constructor
1853 StdList
1854 StdListCons
1855 (family CheckpointRegionPartition)
1856 (constructor
1857 CheckpointRegionPartition
1858 CheckpointRegionPartitionOf
1859 (dpoCoordinateOrdinal shared)
1860 (dpoWordIntervals (naturalMultiply q k)))
1861 (constructor StdList StdListEmpty (family CheckpointRegionPartition)))))
1862 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.