470def admitResourceSchedule =
471 (lambda unrestricted entryBudget : Nat .
472 (lambda unrestricted pairBudget : Nat .
473 (lambda unrestricted schedule : (family ResourceSchedule) .
474 (let unrestricted graph =
475 (resourceScheduleGraph schedule)
476 in
477 (let unrestricted placements =
478 (resourceSchedulePlacements schedule)
479 in
480 (let unrestricted leases =
481 (resourceScheduleLeases schedule)
482 in
483 (let unrestricted entries =
484 (resourceScheduleEntries schedule)
485 in
486 (resourceRequire
487 (family ResourceSchedule)
488 (naturalAnd
489 (naturalLessOrEqual entries entryBudget)
490 (naturalLessOrEqual
491 entries
492 (naturalDivideUnchecked
493 pairBudget
494 (naturalSelect (naturalNonzero entries) entries 1))))
495 (constructor ResourceFailure ResourceBudgetExceeded)
496 (resourceRequire
497 (family ResourceSchedule)
498 (resourceGraphValid graph)
499 (constructor ResourceFailure ResourceMalformedGraph)
500 (resourceRequire
501 (family ResourceSchedule)
502 (naturalAnd
503 (resourceDistinct
504 (family ResourcePlacement)
505 (lambda unrestricted a : (family ResourcePlacement) .
506 (lambda unrestricted b : (family ResourcePlacement) .
507 (naturalEqual (resourcePlacementRole a) (resourcePlacementRole b))))
508 placements)
509 (naturalAnd
510 (resourceAll
511 (family ResourcePlacement)
512 (resourcePlacementValid graph)
513 placements)
514 1))
515 (constructor ResourceFailure ResourceInvalidPlacement)
516 (resourceRequire
517 (family ResourceSchedule)
518 (naturalAnd
519 (resourceDistinct
520 (family ResourceLease)
521 (lambda unrestricted a : (family ResourceLease) .
522 (lambda unrestricted b : (family ResourceLease) .
523 (bytes-equal (resourceLeaseIdentity a) (resourceLeaseIdentity b))))
524 leases)
525 (naturalAnd
526 (resourceAll (family ResourceLease) (resourceLeaseValid graph) leases)
527 1))
528 (constructor ResourceFailure ResourceInvalidLease)
529 (resourceRequire
530 (family ResourceSchedule)
531 (resourceAll (family ResourceLease) (resourceLeaseKnown graph) leases)
532 (constructor ResourceFailure ResourceCapacityUnavailable)
533 (resourceRequire
534 (family ResourceSchedule)
535 (resourceAll
536 (family ResourceLease)
537 (resourceLeaseFits graph leases)
538 leases)
539 (constructor ResourceFailure ResourceCapacityExceeded)
540 (constructor
541 StdResult
542 StdSuccess
543 (family ResourceFailure)
544 (family ResourceSchedule)
545 schedule))))))))))))))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.