247def nativeRegionAppend =
248 (lambda unrestricted context : (family CheckpointEnvelopeContract) .
249 (lambda unrestricted logical : Bytes .
250 (lambda unrestricted available : Nat .
251 (lambda unrestricted ordinal : Nat .
252 (lambda unrestricted interval : (family LogicalInterval) .
253 (lambda unrestricted result : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) .
254 (eliminate
255 StdResult
256 (lambda unrestricted current : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) .
257 (family
258 StdResult
259 (family NativeCheckpointFailure)
260 (family NativeRegionCheckpoint)))
261 result
262 (branch
263 StdFailure
264 error
265 .
266 (constructor
267 StdResult
268 StdFailure
269 (family NativeCheckpointFailure)
270 (family NativeRegionCheckpoint)
271 error))
272 (branch
273 StdSuccess
274 plan
275 .
276 (eliminate
277 StdResult
278 (lambda unrestricted current : (family StdResult (family NativeCheckpointFailure) (family NativeCheckpointLayout)) .
279 (family
280 StdResult
281 (family NativeCheckpointFailure)
282 (family NativeRegionCheckpoint)))
283 (planNativeCheckpoint
284 (nativeRegionContract
285 context
286 (bytes-append
287 b"ALPHA-REGION-SHARD-1\x00"
288 (bytes-append logical (nativeRegionDescriptor ordinal interval)))
289 (naturalAdd nativeRegionCaptureBytes (intervalExtent interval)))
290 (nativeCheckpointAlign (nativeRegionEnd plan))
291 0
292 nativeCheckpointWordBytes
293 available)
294 (branch
295 StdFailure
296 error
297 .
298 (constructor
299 StdResult
300 StdFailure
301 (family NativeCheckpointFailure)
302 (family NativeRegionCheckpoint)
303 error))
304 (branch
305 StdSuccess
306 layout
307 .
308 (constructor
309 StdResult
310 StdSuccess
311 (family NativeCheckpointFailure)
312 (family NativeRegionCheckpoint)
313 (constructor
314 NativeRegionCheckpoint
315 NativeRegionCheckpointOf
316 (nativeRegionManifest plan)
317 (constructor
318 StdList
319 StdListCons
320 (family NativeRegionShard)
321 (constructor
322 NativeRegionShard
323 NativeRegionShardOf
324 ordinal
325 interval
326 layout)
327 (nativeRegionShards plan))
328 (nativeRegionEpoch plan)
329 (nativeCheckpointEnd layout)))))))))))))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.