AlphaGitHub
Source/Packages

Runtime.NativeDataParallelOwnedTree

packages/execution/src/Runtime/NativeDataParallelOwnedTree.alpha

979 lines34 declarations47.0 KiBSHA-256 5e555474696d
Download exact fileView at revisionbcc11a4e7647d31628

def · lines 169–184

dpotReplicatedOf

Full file
The replicated words the root alone publishes: the parameters when they are replicated, then the shared state.
169def dpotReplicatedOf =
170  (lambda unrestricted c : Nat .
171    (lambda unrestricted u : Nat .
172      (lambda unrestricted system : (family DataParallelSystem c u) .
173        (lambda unrestricted q : Nat .
174          (lambda unrestricted p : Nat .
175            (let unrestricted shared =
176              (dpoShared c u system q)
177              in
178              (dpotPart
179                0
180                (dpotWhole (naturalIsZero p) (dpParameterBytes c u system))
181                (dpotPart
182                  dpoSharedOrdinal
183                  (dpotWhole (naturalNonzero shared) (naturalMultiply dpWord shared))
184                  (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.