This owner's destinations on restore: replicated parameters, shared state
and its own words (its parameters when partitioned, its coordinates'
optimizer state).
2038def dpoDestinations =
2039 (lambda unrestricted c : Nat .
2040 (lambda unrestricted u : Nat .
2041 (lambda unrestricted system : (family DataParallelSystem c u) .
2042 (lambda unrestricted q : Nat .
2043 (lambda unrestricted p : Nat .
2044 (lambda unrestricted layout : (family NativeDataParallelOwnedLayout) .
2045 (lambda unrestricted role : Nat .
2046 (let unrestricted k =
2047 (dpK c u system)
2048 in
2049 (let unrestricted owners =
2050 (dpOwners c u system)
2051 in
2052 (let unrestricted shared =
2053 (dpoShared c u system q)
2054 in
2055 (let unrestricted owned =
2056 (dpoOwnedAt c u system q p layout)
2057 in
2058 (let unrestricted ownedWords =
2059 (lambda unrestricted ordinal : Nat .
2060 (lambda unrestricted count : Nat .
2061 (lambda unrestricted first : Nat .
2062 (stdListFold
2063 Nat
2064 (family StdList (family NativeRegionDestination))
2065 (lambda unrestricted index : Nat .
2066 (lambda unrestricted rest : (family StdList (family NativeRegionDestination)) .
2067 (let unrestricted word =
2068 (naturalDivideUnchecked index k)
2069 in
2070 (let unrestricted coordinate =
2071 (naturalModuloUnchecked index k)
2072 in
2073 (nat-eliminate
2074 (lambda unrestricted held : Nat .
2075 (family StdList (family NativeRegionDestination)))
2076 rest
2077 (lambda unrestricted previous : Nat .
2078 (lambda unrestricted ignored : (family StdList (family NativeRegionDestination)) .
2079 (constructor
2080 StdList
2081 StdListCons
2082 (family NativeRegionDestination)
2083 (constructor
2084 NativeRegionDestination
2085 NativeRegionDestinationOf
2086 ordinal
2087 (dpoInterval (naturalMultiply dpWord index) dpWord)
2088 (naturalAdd
2089 owned
2090 (dpoWordOffset k owners (naturalAdd word first) coordinate)))
2091 rest)))
2092 (dpoOwns owners role coordinate))))))
2093 (constructor
2094 StdList
2095 StdListEmpty
2096 (family NativeRegionDestination))
2097 (stdListNaturalsBelow count)))))
2098 in
2099 (stdListAppend
2100 (family NativeRegionDestination)
2101 (nat-eliminate
2102 (lambda unrestricted current : Nat .
2103 (family StdList (family NativeRegionDestination)))
2104 (constructor
2105 StdList
2106 StdListCons
2107 (family NativeRegionDestination)
2108 (constructor
2109 NativeRegionDestination
2110 NativeRegionDestinationOf
2111 0
2112 (dpoInterval 0 (dpParameterBytes c u system))
2113 (dpoParametersAt layout))
2114 (constructor StdList StdListEmpty (family NativeRegionDestination)))
2115 (lambda unrestricted previous : Nat .
2116 (lambda unrestricted ignored : (family StdList (family NativeRegionDestination)) .
2117 (ownedWords 0 k 0)))
2118 p)
2119 (stdListAppend
2120 (family NativeRegionDestination)
2121 (nat-eliminate
2122 (lambda unrestricted words : Nat .
2123 (family StdList (family NativeRegionDestination)))
2124 (constructor StdList StdListEmpty (family NativeRegionDestination))
2125 (lambda unrestricted previous : Nat .
2126 (lambda unrestricted ignored : (family StdList (family NativeRegionDestination)) .
2127 (constructor
2128 StdList
2129 StdListCons
2130 (family NativeRegionDestination)
2131 (constructor
2132 NativeRegionDestination
2133 NativeRegionDestinationOf
2134 dpoSharedOrdinal
2135 (dpoInterval 0 (naturalMultiply dpWord shared))
2136 (dpoSharedAt c u system p layout))
2137 (constructor
2138 StdList
2139 StdListEmpty
2140 (family NativeRegionDestination)))))
2141 shared)
2142 (ownedWords (dpoCoordinateOrdinal shared) (naturalMultiply q k) p)))))))))))))))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.