638def telemetryRoutedPolicyPlan =
639 (lambda unrestricted policy : (family CapturePolicy) .
640 (lambda unrestricted sites : (family TelemetryPolicySites) .
641 (lambda unrestricted schemas : (family StdList Bytes) .
642 (let unrestricted ordinaryDeclarations =
643 (telemetryPolicySelectedRoutes policy 0 sites)
644 in
645 (let unrestricted reservedDeclarations =
646 (telemetryPolicySelectedRoutes policy 1 sites)
647 in
648 (let unrestricted descriptors =
649 (telemetryPolicyRoutedDescriptors policy sites schemas)
650 in
651 (let unrestricted ordinaryCapacity =
652 (aosChoose
653 Nat
654 (naturalNonzero (telemetryRouteDeclarationsCount ordinaryDeclarations))
655 (capturePolicyOrdinaryCapacity policy)
656 0)
657 in
658 (let unrestricted drain =
659 (telemetryDispatchPlan
660 ordinaryCapacity
661 (capturePolicyReservedCapacity policy)
662 ordinaryDeclarations
663 reservedDeclarations
664 descriptors)
665 in
666 (aosChoose
667 (family TelemetryRoutedPolicyPlan)
668 (naturalAnd
669 (capturePolicyAdmission policy)
670 (naturalAnd
671 (telemetryPolicySitesAdmission policy sites)
672 (naturalAnd
673 (telemetryDrainDescriptorsAdmission descriptors)
674 (telemetryRouteDeclarationsAdmission
675 (telemetryPolicyAllRoutes sites)
676 (constructor TelemetryRouteDeclarations TelemetryRouteDeclarationsEnd)
677 descriptors))))
678 (eliminate
679 TelemetryDispatchPlan
680 (lambda unrestricted current : (family TelemetryDispatchPlan) .
681 (family TelemetryRoutedPolicyPlan))
682 drain
683 (branch
684 TelemetryDispatchReady
685 oc
686 rc
687 ordinaryRoutes
688 reservedRoutes
689 ordinary
690 reserved
691 descriptors
692 bound
693 .
694 (aosChoose
695 (family TelemetryRoutedPolicyPlan)
696 (naturalLessOrEqual
697 (publicationRecordBytes bound)
698 (capturePolicyByteBudget policy))
699 (constructor
700 TelemetryRoutedPolicyPlan
701 TelemetryRoutedPolicyReady
702 policy
703 sites
704 drain)
705 (constructor
706 TelemetryRoutedPolicyPlan
707 TelemetryRoutedPolicyRefused
708 b"native-routed-policy-byte-budget-refused")))
709 (branch
710 TelemetryDispatchRefused
711 reason
712 .
713 (constructor TelemetryRoutedPolicyPlan TelemetryRoutedPolicyRefused reason)))
714 (constructor
715 TelemetryRoutedPolicyPlan
716 TelemetryRoutedPolicyRefused
717 b"native-routed-policy-declaration-refused"))))))))))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.