The publication's arena: both frame templates, the tree checkpoint's
staging and, below the root, the root's replicated shard layouts.
790def dpotResidents =
791 (lambda unrestricted layout : (family NativeDataParallelOwnedLayout) .
792 (lambda unrestricted tree : (family NativeDataParallelOwnedTreeLayout) .
793 (let unrestricted staged =
794 (nativeTreeResidents (dpotCheckpoint tree))
795 in
796 (let unrestricted rootBase =
797 (nativeCheckpointAlign (nativeTreeEnd (dpotCheckpoint tree)))
798 in
799 (let unrestricted rootBytes =
800 (naturalSaturatingSubtract (nativeRegionEnd (dpotRootShards tree)) rootBase)
801 in
802 (constructor
803 ArenaResidents
804 ArenaResidentsNext
805 (constructor
806 ArenaResident
807 ArenaResidentValue
808 b"tree-commitment-frame"
809 (frameBase (dpotCommitment tree))
810 (naturalSaturatingSubtract
811 (frameEnd (dpotCommitment tree))
812 (frameBase (dpotCommitment tree)))
813 1)
814 (constructor
815 ArenaResidents
816 ArenaResidentsNext
817 (constructor
818 ArenaResident
819 ArenaResidentValue
820 b"tree-release-frame"
821 (frameBase (dpotRelease tree))
822 (naturalSaturatingSubtract
823 (frameEnd (dpotRelease tree))
824 (frameBase (dpotRelease tree)))
825 1)
826 (nat-eliminate
827 (lambda unrestricted current : Nat . (family ArenaResidents))
828 staged
829 (lambda unrestricted previous : Nat .
830 (lambda unrestricted ignored : (family ArenaResidents) .
831 (constructor
832 ArenaResidents
833 ArenaResidentsNext
834 (constructor
835 ArenaResident
836 ArenaResidentValue
837 b"tree-root-shards"
838 rootBase
839 rootBytes
840 nativeCheckpointWordBytes)
841 staged)))
842 (naturalNonzero rootBytes)))))))))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.