---- start, publication ----
Fresh: the declared words. Resume: the verified manifest path, this
owner's own shards and, below the root, the root's replicated shards, then
the restored prefix and a new membership epoch.
639def dpotStart =
640 (lambda unrestricted c : Nat .
641 (lambda unrestricted u : Nat .
642 (lambda unrestricted system : (family DataParallelSystem c u) .
643 (lambda unrestricted q : Nat .
644 (lambda unrestricted p : Nat .
645 (lambda unrestricted layout : (family NativeDataParallelOwnedLayout) .
646 (lambda unrestricted tree : (family NativeDataParallelOwnedTreeLayout) .
647 (lambda unrestricted fanout : Nat .
648 (lambda unrestricted role : Nat .
649 (lambda unrestricted resume : Nat .
650 (lambda unrestricted tail : (family NativePhysicalCommands) .
651 (let unrestricted checkpoint =
652 (dpotCheckpoint tree)
653 in
654 (let unrestricted owners =
655 (dpOwners c u system)
656 in
657 (let unrestricted destination =
658 (lambda unrestricted shard : (family NativeRegionShard) .
659 (naturalAdd
660 (dpoStateAt layout)
661 (dpoShardOffset c u system q p shard)))
662 in
663 (let unrestricted rootGlobals =
664 (dpotOwnGlobals c u system q p 0)
665 in
666 (constructor
667 StdResult
668 StdSuccess
669 (family NativeCheckpointFailure)
670 (family NativePhysicalCommands)
671 (nat-eliminate
672 (lambda unrestricted mode : Nat .
673 (family NativePhysicalCommands))
674 (dpoFresh c u system q p layout role tail)
675 (lambda unrestricted previous : Nat .
676 (lambda unrestricted ignored : (family NativePhysicalCommands) .
677 (nativeTreeRestoreManifests
678 checkpoint
679 fanout
680 owners
681 role
682 (dpotOwnOf c u system q p)
683 (dpotPaths c u system q p role)
684 (nativeTreeRestoreOwn
685 checkpoint
686 (dpotPaths c u system q p role)
687 destination
688 (nativeTreeRestoreShardsFrom
689 (nativeTreeRootLayout checkpoint)
690 (dpotReplicatedFirst c u system p)
691 (nativeRegionShards (dpotRootShards tree))
692 (lambda unrestricted index : Nat .
693 (succ (naturalAdd owners (dpotNth rootGlobals index))))
694 destination
695 (dpResumed
696 (dpoGeneric layout)
697 (nativeTreeRestoredCaptureAt checkpoint)
698 tail))))))
699 resume)))))))))))))))))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.