A role's own partitions, in region order: its parameter words (all of them
at the root when replicated), the shared state at the root, its
coordinates' optimizer-state words.
189def dpotOwnOf =
190 (lambda unrestricted c : Nat .
191 (lambda unrestricted u : Nat .
192 (lambda unrestricted system : (family DataParallelSystem c u) .
193 (lambda unrestricted q : Nat .
194 (lambda unrestricted p : Nat .
195 (lambda unrestricted role : Nat .
196 (let unrestricted k =
197 (dpK c u system)
198 in
199 (let unrestricted owners =
200 (dpOwners c u system)
201 in
202 (let unrestricted shared =
203 (dpoShared c u system q)
204 in
205 (let unrestricted root =
206 (naturalIsZero role)
207 in
208 (dpotPart
209 0
210 (nat-eliminate
211 (lambda unrestricted current : Nat .
212 (family StdList (family LogicalInterval)))
213 (dpotWhole root (dpParameterBytes c u system))
214 (lambda unrestricted previous : Nat .
215 (lambda unrestricted ignored : (family StdList (family LogicalInterval)) .
216 (dpotOwnedWords k owners role k)))
217 p)
218 (dpotPart
219 dpoSharedOrdinal
220 (dpotWhole
221 (naturalAnd root (naturalNonzero shared))
222 (naturalMultiply dpWord shared))
223 (dpotPart
224 (dpoCoordinateOrdinal shared)
225 (dpotOwnedWords k owners role (naturalMultiply q k))
226 (constructor StdList StdListEmpty (family CheckpointRegionPartition)))))))))))))))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.