UTF-8 iterators

UTF8.decodeIter reads characters from UTF-8 bytes, and UTF8.encodeIter writes them back. The well-formed byte sequences are those of the Unicode Standard, Table 3-7. Ill-formed input is a maximal subpart: the longest prefix of a well-formed sequence that it starts with, or a single byte if none. Lossy decoding replaces each maximal subpart with U+FFFD, following the recommended practice of the Standard, Section 3.9.

UTF8.skipSignature skips the bytes EF BB BF that sometimes start UTF-8 data.

structure Unicode.UTF8 : Type

The UTF-8 encoding form, as a decoder from bytes and an encoder to bytes.

@[instance_reducible]

instance Unicode.instInhabitedUTF8 : Inhabited UTF8

Equations

• Unicode.instInhabitedUTF8 = { default := Unicode.instInhabitedUTF8.default }

@[inline]

def Unicode.UTF8.decodeChar {ι : Type} [Std.Iterator ι Id UInt8] [Std.Iterators.Productive ι Id] {β : Type} (it : Std.Iter UInt8) (yield : (rest : Std.Iter UInt8) → Advanced rest it → Char → β) (error : DecodeError.Kind → (rest : Std.Iter UInt8) → Advanced rest it → β) (done : Unit → β) : β

Decodes one character from the UTF-8 bytes of it. Calls yield with the character and the iterator after it, error with the iterator after a maximal subpart of an ill-formed byte sequence, or done at the end of the input.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Unicode.instDecoderUTF8UInt8Char : Decoder UTF8 UInt8 Char

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Unicode.instEncoderUTF8CharUInt8 : Encoder UTF8 Char UInt8

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Unicode.UTF8.decodeIter {ι : Type} (it : Std.Iter UInt8) : Std.Iter Char

Decodes the UTF-8 bytes of it, stopping at the first ill-formed byte sequence.

A for loop or fold over the result ends at ill-formed input just as at the end of the input. To tell them apart, fold with decodeFold, which also returns the iterator where decoding stopped, and check decodeError? there, find the first ill-formed input ahead with decodeFailure?, or decode with decodeIterLossy instead.

Equations

• Unicode.UTF8.decodeIter it = Unicode.Decoder.iter { } it

@[inline]

def Unicode.UTF8.decodeIterLossy {ι : Type} (it : Std.Iter UInt8) : Std.Iter Char

Decodes the UTF-8 bytes of it, replacing each maximal subpart of an ill-formed byte sequence with U+FFFD.

Equations

• Unicode.UTF8.decodeIterLossy it = Unicode.Decoder.iterLossy { } it

@[inline]

def Unicode.UTF8.encodeIter {ι : Type} (it : Std.Iter Char) : Std.Iter UInt8

Encodes the characters of it as UTF-8 bytes.

Equations

• Unicode.UTF8.encodeIter it = Unicode.Encoder.iter { } it

def Unicode.UTF8.skipSignature {ι : Type} [Std.Iterator ι Id UInt8] [Std.Iterators.Productive ι Id] (it : Std.Iter UInt8) : Std.Iter UInt8

The iterator after the UTF-8 signature EF BB BF at it, or it if there is none.

Equations

• One or more equations did not get rendered due to their size.