615def nativeTelemetrySiteWith =
616 (lambda unrestricted applicationBytes : Nat .
617 (lambda unrestricted policy : (family CapturePolicy) .
618 (lambda unrestricted site : (family CaptureSite) .
619 (lambda unrestricted ordinaryCapacity : Nat .
620 (lambda unrestricted reservedCapacity : Nat .
621 (lambda unrestricted bound : Nat .
622 (lambda unrestricted decisionAt : Nat .
623 (lambda unrestricted recipe : (family TelemetryRecordPlan) .
624 (lambda unrestricted values : (family NativeTelemetrySourceValues) .
625 (lambda unrestricted coordinate : (family NativePhysicalOperand) .
626 (lambda unrestricted resultSlot : Nat .
627 (lambda unrestricted workSlot : Nat .
628 (lambda unrestricted identity : Bytes .
629 (lambda unrestricted capture : (pi unrestricted commands : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
630 (lambda unrestricted tail : (family NativePhysicalCommands) .
631 (nativeLaunchRecipeCommand
632 (constructor
633 NativePhysicalOperation
634 NativePhysicalStoreWord64
635 (nativeTelemetryPolicyState
636 (naturalAdd decisionAt captureWordBytes))
637 (constructor
638 NativePhysicalOperand
639 NativePhysicalLoopAffine
640 (modelWord64FromNaturalTruncated 0)
641 (modelWord64FromNaturalTruncated 1)))
642 identity
643 (nativeLaunchRecipeCommand
644 (constructor
645 NativePhysicalOperation
646 NativePhysicalMachineRoutine
647 (nativeTelemetrySiteSelectionRoutine
648 ordinaryCapacity
649 reservedCapacity
650 (capturePolicyRequired policy)
651 (captureSiteSelected policy site)
652 (captureSiteStride site)
653 bound)
654 (constructor
655 NativePhysicalArguments
656 NativePhysicalArgumentsValue
657 (nativeTelemetryPolicyState
658 (captureControlAt applicationBytes))
659 (nativeTelemetryPolicyState
660 (publicationBase
661 applicationBytes
662 ordinaryCapacity
663 reservedCapacity))
664 (aosChoose
665 (family NativePhysicalOperand)
666 (naturalAnd
667 (captureSiteSelected policy site)
668 (naturalIsZero (naturalEqual (captureSiteStride site) 1)))
669 coordinate
670 (nativeLaunchRecipeImmediate 0))
671 (nativeTelemetryPolicyState decisionAt)
672 (nativeLaunchRecipeImmediate
673 (publicationArenaBytesForBody bound))
674 (nativeLaunchRecipeImmediate 0))
675 (nativeLaunchRecipeStore workSlot))
676 identity
677 (nativeLaunchRecipeCommand
678 (constructor
679 NativePhysicalOperation
680 NativePhysicalMachineRoutine
681 recordStatusRoutine
682 (nativeLaunchRecipeArguments
683 (nativeTelemetryPolicyState decisionAt)
684 (nativeLaunchRecipeImmediate 0)
685 (nativeLaunchRecipeImmediate 0)
686 (nativeLaunchRecipeImmediate 0))
687 (nativeLaunchRecipeStore resultSlot))
688 identity
689 (nativeLaunchRecipeCommand
690 (constructor
691 NativePhysicalOperation
692 NativePhysicalRepeatBeginCounted
693 (nativeLaunchRecipeSlotValue workSlot))
694 identity
695 (nativeTelemetryPolicyFillSelected
696 applicationBytes
697 ordinaryCapacity
698 reservedCapacity
699 recipe
700 values
701 (captureSiteSelected policy site)
702 decisionAt
703 identity
704 (capture
705 (nativeLaunchRecipeCommand
706 (constructor
707 NativePhysicalOperation
708 NativePhysicalRepeatEnd)
709 identity
710 tail))))))))))))))))))))))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.