encoding

cfamily.Text.utf8Bytes

def Text.utf8Bytes (c : Nat) : List Nat

The UTF-8 bytes of a code point.

cfamily.Text.utf8

def Text.utf8 (text : String) : String

Text as the bytes a program sees: each code point by its UTF-8 bytes, one character per byte.

cfamily.Utf8Decoding

record Utf8Decoding

The decoder’s state between bytes: the continuation bytes still needed and seen, the code point so far, the range the next continuation byte must be in, and the code points decoded (the last first).

cfamily.Text.replacement

def Text.replacement : Nat

The replacement character U+FFFD.

cfamily.Utf8Decoding.ready

def Utf8Decoding.ready (decoded : List Nat) : Utf8Decoding

The decoder at the start of a sequence, with the code points decoded so far.

cfamily.Utf8Decoding.lead

def Utf8Decoding.lead (s : Utf8Decoding) (b : Nat) : Utf8Decoding

A byte that starts a sequence: an ASCII byte is a code point; a lead byte sets how many continuation bytes follow and the range of the first (no overlong forms, surrogates or code points past U+10FFFF); any other byte is U+FFFD.

cfamily.Utf8Decoding.step

def Utf8Decoding.step (s : Utf8Decoding) (b : Nat) : Utf8Decoding

One byte: a continuation byte in range adds to the code point (completing it when the last); one out of range ends the sequence as U+FFFD and starts again from that byte.

cfamily.Text.ofUtf8

def Text.ofUtf8 (bytes : String) : String

The text of the bytes a program wrote (one character per byte): UTF-8 decoded, an invalid sequence as U+FFFD, and one left unfinished at the end too.