Prepare the shards held by `owner`, each from `stateBase` plus its offset,
keeping each shard's index for its paths. Shards are independent: each has
its own checkpoint layout, so grouping them by owner preserves the plan.
126def nativeRegionPrepareOwner =
127 (lambda unrestricted plan : (family NativeRegionCheckpoint) .
128 (lambda unrestricted captureAt : Nat .
129 (lambda unrestricted ownerOf : (pi unrestricted shard : (family NativeRegionShard) . Nat) .
130 (lambda unrestricted offsetOf : (pi unrestricted shard : (family NativeRegionShard) . Nat) .
131 (lambda unrestricted owner : Nat .
132 (lambda unrestricted stateBase : Nat .
133 (lambda unrestricted paths : (family NativeRegionPaths) .
134 (lambda unrestricted tail : (family NativePhysicalCommands) .
135 (stdListFold
136 (family NativeRegionShard)
137 (pi unrestricted index : Nat . (family NativePhysicalCommands))
138 (lambda unrestricted shard : (family NativeRegionShard) .
139 (lambda unrestricted next : (pi unrestricted index : Nat . (family NativePhysicalCommands)) .
140 (lambda unrestricted index : Nat .
141 (nat-eliminate
142 (lambda unrestricted held : Nat . (family NativePhysicalCommands))
143 (next (succ index))
144 (lambda unrestricted previous : Nat .
145 (lambda unrestricted ignored : (family NativePhysicalCommands) .
146 (nativeRegionPrepareShard
147 shard
148 (nativeMemoryState captureAt)
149 (nativeMemoryState (naturalAdd stateBase (offsetOf shard)))
150 (nativeRegionShardPath paths index 0)
151 (nativeRegionShardPath paths index 1)
152 (nativeRegionPathArgument (nativeRegionDirectoryIndex paths))
153 nativePeerListenerSlot
154 nativePeerScratchSlot
155 (next (succ index)))))
156 (naturalEqual (ownerOf shard) owner)))))
157 (lambda unrestricted index : Nat . tail)
158 (nativeRegionShards plan)
159 0)))))))))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.