726def nativeTelemetrySinkAfterWrite =
727 (lambda unrestricted response : (family LinuxSyscallResponse) .
728 (lambda unrestricted state : (family NativeTelemetrySinkState) .
729 (eliminate
730 LinuxSyscallResponse
731 (lambda unrestricted current : (family LinuxSyscallResponse) .
732 (family NativeTelemetrySinkDecision))
733 response
734 (branch
735 LinuxOpenSucceeded
736 descriptor
737 .
738 (constructor
739 NativeTelemetrySinkDecision
740 NativeTelemetrySinkRejected
741 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
742 state))
743 (branch
744 LinuxReadSucceeded
745 bytes
746 .
747 (constructor
748 NativeTelemetrySinkDecision
749 NativeTelemetrySinkRejected
750 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
751 state))
752 (branch
753 LinuxSeekSucceeded
754 position
755 .
756 (constructor
757 NativeTelemetrySinkDecision
758 NativeTelemetrySinkRejected
759 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
760 state))
761 (branch
762 LinuxWriteSucceeded
763 written
764 .
765 (eliminate
766 NativeTelemetrySinkState
767 (lambda unrestricted current : (family NativeTelemetrySinkState) .
768 (family NativeTelemetrySinkDecision))
769 state
770 (branch
771 NativeTelemetrySinkStateValue
772 path
773 record
774 phase
775 optionalDescriptor
776 telemetry
777 .
778 (eliminate
779 NativeTelemetryOptionalDescriptor
780 (lambda unrestricted current : (family NativeTelemetryOptionalDescriptor) .
781 (family NativeTelemetrySinkDecision))
782 optionalDescriptor
783 (branch
784 NativeTelemetryNoDescriptor
785 .
786 (constructor
787 NativeTelemetrySinkDecision
788 NativeTelemetrySinkRejected
789 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
790 state))
791 (branch
792 NativeTelemetrySomeDescriptor
793 descriptor
794 .
795 (eliminate
796 NativeTelemetryEncodedRecord
797 (lambda unrestricted current : (family NativeTelemetryEncodedRecord) .
798 (family NativeTelemetrySinkDecision))
799 record
800 (branch
801 NativeTelemetryEncodedRecordValue
802 bytes
803 extent
804 digest
805 identity
806 .
807 (nat-eliminate
808 (lambda unrestricted exact : Nat . (family NativeTelemetrySinkDecision))
809 (constructor
810 NativeTelemetrySinkDecision
811 NativeTelemetrySinkRejected
812 (constructor NativeTelemetryErrorCode NativeTelemetryWriteShort)
813 state)
814 (lambda unrestricted exactPredecessor : Nat .
815 (lambda unrestricted ignoredExact : (family NativeTelemetrySinkDecision) .
816 (eliminate
817 NativeTelemetrySinkTelemetry
818 (lambda unrestricted current : (family NativeTelemetrySinkTelemetry) .
819 (family NativeTelemetrySinkDecision))
820 telemetry
821 (branch
822 NativeTelemetrySinkTelemetryValue
823 planned
824 completed
825 plannedBytes
826 oldWritten
827 syncs
828 closes
829 failures
830 fallbacks
831 .
832 (constructor
833 NativeTelemetrySinkDecision
834 NativeTelemetrySinkContinue
835 (constructor
836 NativeTelemetrySinkState
837 NativeTelemetrySinkStateValue
838 path
839 record
840 (constructor
841 NativeTelemetrySinkPhase
842 NativeTelemetrySinkSyncing)
843 optionalDescriptor
844 (constructor
845 NativeTelemetrySinkTelemetry
846 NativeTelemetrySinkTelemetryValue
847 (succ planned)
848 (succ completed)
849 plannedBytes
850 written
851 syncs
852 closes
853 failures
854 fallbacks))
855 (constructor
856 NativeTelemetrySinkAction
857 NativeTelemetrySinkIssueSyscall
858 (constructor LinuxSyscallRequest LinuxFdatasync descriptor)))))))
859 (modelWord64Equal written extent)))))))))
860 (branch
861 LinuxIoctlSucceeded
862 output
863 .
864 (constructor
865 NativeTelemetrySinkDecision
866 NativeTelemetrySinkRejected
867 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
868 state))
869 (branch
870 LinuxMmapSucceeded
871 address
872 .
873 (constructor
874 NativeTelemetrySinkDecision
875 NativeTelemetrySinkRejected
876 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
877 state))
878 (branch
879 LinuxUnitSucceeded
880 .
881 (constructor
882 NativeTelemetrySinkDecision
883 NativeTelemetrySinkRejected
884 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
885 state))
886 (branch
887 LinuxSyscallFailed
888 error
889 errno
890 .
891 (constructor
892 NativeTelemetrySinkDecision
893 NativeTelemetrySinkRejected
894 (constructor NativeTelemetryErrorCode NativeTelemetryWriteFailed)
895 state)))))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.