430def planNativeTreeCheckpoint =
431 (lambda unrestricted context : (family CheckpointEnvelopeContract) .
432 (lambda unrestricted regions : (family StdList (family CheckpointLogicalRegion)) .
433 (lambda unrestricted fanout : Nat .
434 (lambda unrestricted count : Nat .
435 (lambda unrestricted role : Nat .
436 (lambda unrestricted ownOf : (pi unrestricted role : Nat . (family StdList (family CheckpointRegionPartition))) .
437 (lambda unrestricted epoch : Nat .
438 (lambda unrestricted base : Nat .
439 (lambda unrestricted available : Nat .
440 (let unrestricted logical =
441 (checkpointLogicalSchemaBytes regions)
442 in
443 (eliminate
444 StdResult
445 (lambda unrestricted result : (family StdResult (family NativeCheckpointFailure) (family NativeCheckpointLayout)) .
446 (family
447 StdResult
448 (family NativeCheckpointFailure)
449 (family NativeTreeCheckpoint)))
450 (planNativeTreeGroup
451 context
452 logical
453 fanout
454 count
455 (participantTreeNode fanout count role)
456 (ownOf role)
457 base
458 available)
459 (branch
460 StdFailure
461 error
462 .
463 (constructor
464 StdResult
465 StdFailure
466 (family NativeCheckpointFailure)
467 (family NativeTreeCheckpoint)
468 error))
469 (branch
470 StdSuccess
471 group
472 .
473 (eliminate
474 StdResult
475 (lambda unrestricted result : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) .
476 (family
477 StdResult
478 (family NativeCheckpointFailure)
479 (family NativeTreeCheckpoint)))
480 (nativeRegionAppendParts
481 context
482 logical
483 available
484 (ownOf role)
485 (constructor
486 StdResult
487 StdSuccess
488 (family NativeCheckpointFailure)
489 (family NativeRegionCheckpoint)
490 (constructor
491 NativeRegionCheckpoint
492 NativeRegionCheckpointOf
493 group
494 (constructor StdList StdListEmpty (family NativeRegionShard))
495 epoch
496 (nativeCheckpointEnd group))))
497 (branch
498 StdFailure
499 error
500 .
501 (constructor
502 StdResult
503 StdFailure
504 (family NativeCheckpointFailure)
505 (family NativeTreeCheckpoint)
506 error))
507 (branch
508 StdSuccess
509 shards
510 .
511 (planNativeTreeAncestors
512 context
513 logical
514 fanout
515 count
516 ownOf
517 available
518 (participantTreeAncestors fanout count role)
519 (lambda unrestricted at : Nat .
520 (lambda unrestricted planned : (family StdList (family NativeCheckpointLayout)) .
521 (constructor
522 StdResult
523 StdSuccess
524 (family NativeCheckpointFailure)
525 (family NativeTreeCheckpoint)
526 (constructor
527 NativeTreeCheckpoint
528 NativeTreeCheckpointOf
529 group
530 (stdListReverse
531 (family NativeRegionShard)
532 (nativeRegionShards shards))
533 planned
534 epoch
535 at))))
536 (nativeCheckpointAlign (nativeRegionEnd shards))
537 (constructor StdList StdListEmpty (family NativeCheckpointLayout)))))))))))))))))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.