Encoding scheme iterators

An encoding scheme is a decoder from bytes to characters and an encoder from characters to bytes, in one layer. EncodingScheme.decodeIter e reads the byte order mark or signature of e, if it has one, then decodes the characters after it; EncodingScheme.encodeIter e writes the mark, then the characters. Positions are byte offsets in the input, it.decodeBase.toUInt8Slice.start for a byte slice, and ill-formed input of every kind is reported by the one decoder: an incomplete code unit at the end as well as an unpaired surrogate or a code unit that is not a scalar value.

As a decoder, e decodes the characters after the mark: utf8BOM decodes as utf8, and utf16 o and utf32 o decode in byte order o. decodeIter gives utf16 o and utf32 o the byte order that the mark tells.

@[inline]

def Unicode.EncodingScheme.decodeChar {ι : Type} [Std.Iterator ι Id UInt8] [Std.Iterators.Productive ι Id] {β : Type} (e : EncodingScheme) (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 bytes of it in scheme e, after any byte order mark or signature. Calls yield with the character and the iterator after it, error with the iterator after the ill-formed input, or done at the end of the input.

Equations

• Unicode.EncodingScheme.utf8.decodeChar it yield error done = Unicode.UTF8.decodeChar it yield error done
• Unicode.EncodingScheme.utf8BOM.decodeChar it yield error done = Unicode.UTF8.decodeChar it yield error done
• Unicode.EncodingScheme.utf16BE.decodeChar it yield error done = Unicode.EncodingScheme.decodeChar16✝ Unicode.ByteOrder.big it yield error done
• Unicode.EncodingScheme.utf16LE.decodeChar it yield error done = Unicode.EncodingScheme.decodeChar16✝ Unicode.ByteOrder.little it yield error done
• (Unicode.EncodingScheme.utf16 o).decodeChar it yield error done = Unicode.EncodingScheme.decodeChar16✝ o it yield error done
• Unicode.EncodingScheme.utf32BE.decodeChar it yield error done = Unicode.EncodingScheme.decodeChar32✝ Unicode.ByteOrder.big it yield error done
• Unicode.EncodingScheme.utf32LE.decodeChar it yield error done = Unicode.EncodingScheme.decodeChar32✝ Unicode.ByteOrder.little it yield error done
• (Unicode.EncodingScheme.utf32 o).decodeChar it yield error done = Unicode.EncodingScheme.decodeChar32✝ o it yield error done

@[instance_reducible]

instance Unicode.instDecoderEncodingSchemeUInt8Char : Decoder EncodingScheme UInt8 Char

Equations

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

@[instance_reducible]

instance Unicode.instEncoderEncodingSchemeCharUInt8 : Encoder EncodingScheme Char UInt8

Equations

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

def Unicode.EncodingScheme.decodeIter {ι : Type} [Std.Iterator ι Id UInt8] [Std.Iterators.Productive ι Id] (e : EncodingScheme) (it : Std.Iter UInt8) : Std.Iter Char

Decodes the bytes of it in scheme e, stopping at the first ill-formed input. A byte order mark or signature of e at the start is skipped, and for utf16 o and utf32 o the mark tells the byte order; without one, the byte order is o.

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

• e.decodeIter it = match Unicode.EncodingScheme.start✝ e it with | (e, it) => Unicode.Decoder.iter e it

def Unicode.EncodingScheme.decodeIterLossy {ι : Type} [Std.Iterator ι Id UInt8] [Std.Iterators.Productive ι Id] (e : EncodingScheme) (it : Std.Iter UInt8) : Std.Iter Char

Decodes the bytes of it in scheme e like decodeIter, replacing each ill-formed input with U+FFFD.

Equations

• e.decodeIterLossy it = match Unicode.EncodingScheme.start✝ e it with | (e, it) => Unicode.Decoder.iterLossy e it

@[inline]

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

Encodes the characters of it as bytes in scheme e, starting with the byte order mark or signature of e if it has one.

Equations

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