842def utf8EncodeCodepoint =
843 (lambda unrestricted codepoint : (family UTF8Codepoint) .
844 (eliminate
845 UTF8Codepoint
846 (lambda unrestricted current : (family UTF8Codepoint) . (family UTF8CodepointEncodeResult))
847 codepoint
848 (branch
849 UTF8CodepointValue
850 word
851 .
852 (eliminate
853 ModelWord32
854 (lambda unrestricted current : (family ModelWord32) . (family UTF8CodepointEncodeResult))
855 word
856 (branch
857 ModelWord32Value
858 b0
859 b1
860 b2
861 b3
862 .
863 (utf8ChooseEncoded
864 (utf8FlagAnd (byte-equal b3 (byte 0)) (byte-less-than b2 (byte 17)))
865 (lambda unrestricted force : Nat .
866 (utf8ChooseEncoded
867 (byte-equal b2 (byte 0))
868 (lambda unrestricted force : Nat .
869 (utf8ChooseEncoded
870 (utf8FlagAnd (byte-less-than (byte 215) b1) (byte-less-than b1 (byte 224)))
871 (lambda unrestricted force : Nat .
872 (constructor
873 UTF8CodepointEncodeResult
874 UTF8CodepointRejected
875 (constructor UTF8ErrorCode UTF8SurrogateCodepoint)))
876 (lambda unrestricted force : Nat .
877 (utf8ChooseEncoded
878 (utf8FlagAnd (byte-equal b1 (byte 0)) (byte-less-than b0 (byte 128)))
879 (lambda unrestricted force : Nat .
880 (constructor
881 UTF8CodepointEncodeResult
882 UTF8CodepointEncoded
883 (bytes-cons b0 b"")))
884 (lambda unrestricted force : Nat .
885 (utf8ChooseEncoded
886 (byte-less-than b1 (byte 8))
887 (lambda unrestricted force : Nat .
888 (constructor
889 UTF8CodepointEncodeResult
890 UTF8CodepointEncoded
891 (bytes-cons
892 (Std.Byte/byteOr
893 (byte 192)
894 (Std.Byte/byteOr
895 (Std.Byte/byteShiftRight b0 (byte-to-nat (byte 6)))
896 (Std.Byte/byteShiftLeftTruncated b1 (byte-to-nat (byte 2)))))
897 (bytes-cons
898 (Std.Byte/byteOr (byte 128) (Std.Byte/byteAnd b0 (byte 63)))
899 b""))))
900 (lambda unrestricted force : Nat .
901 (constructor
902 UTF8CodepointEncodeResult
903 UTF8CodepointEncoded
904 (bytes-cons
905 (Std.Byte/byteOr
906 (byte 224)
907 (Std.Byte/byteShiftRight b1 (byte-to-nat (byte 4))))
908 (bytes-cons
909 (Std.Byte/byteOr
910 (byte 128)
911 (Std.Byte/byteOr
912 (Std.Byte/byteShiftRight b0 (byte-to-nat (byte 6)))
913 (Std.Byte/byteShiftLeftTruncated
914 (Std.Byte/byteAnd b1 (byte 15))
915 (byte-to-nat (byte 2)))))
916 (bytes-cons
917 (Std.Byte/byteOr (byte 128) (Std.Byte/byteAnd b0 (byte 63)))
918 b"")))))))))))
919 (lambda unrestricted force : Nat .
920 (constructor
921 UTF8CodepointEncodeResult
922 UTF8CodepointEncoded
923 (bytes-cons
924 (Std.Byte/byteOr
925 (byte 240)
926 (Std.Byte/byteShiftRight b2 (byte-to-nat (byte 2))))
927 (bytes-cons
928 (Std.Byte/byteOr
929 (byte 128)
930 (Std.Byte/byteOr
931 (Std.Byte/byteShiftRight b1 (byte-to-nat (byte 4)))
932 (Std.Byte/byteShiftLeftTruncated
933 (Std.Byte/byteAnd b2 (byte 3))
934 (byte-to-nat (byte 4)))))
935 (bytes-cons
936 (Std.Byte/byteOr
937 (byte 128)
938 (Std.Byte/byteOr
939 (Std.Byte/byteShiftRight b0 (byte-to-nat (byte 6)))
940 (Std.Byte/byteShiftLeftTruncated
941 (Std.Byte/byteAnd b1 (byte 15))
942 (byte-to-nat (byte 2)))))
943 (bytes-cons
944 (Std.Byte/byteOr (byte 128) (Std.Byte/byteAnd b0 (byte 63)))
945 b""))))))))
946 (lambda unrestricted force : Nat .
947 (constructor
948 UTF8CodepointEncodeResult
949 UTF8CodepointRejected
950 (constructor UTF8ErrorCode UTF8CodepointOutOfRange)))))))))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.