UTF-16 iterators #

UTF16.decodeIter reads characters from UTF-16 code units, and UTF16.encodeIter writes them back. An unpaired surrogate is ill-formed. A high surrogate reads its low surrogate by looking ahead; when there is none, only the high surrogate is ill-formed, and lossy decoding goes on from the next code unit.

source

structure Unicode.UTF16 :

Type

The UTF-16 encoding form, as a decoder from code units and an encoder to code units.

Instances For

source

@[instance_reducible]

instance Unicode.instInhabitedUTF16 :

Inhabited UTF16

Equations

Unicode.instInhabitedUTF16 = { default := Unicode.instInhabitedUTF16.default }

source

@[inline]

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

Decodes one character from the UTF-16 code units of it. Calls yield with the character and the iterator after it, error with the iterator after an unpaired surrogate, or done at the end of the input.

Equations

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

Instances For

source

@[instance_reducible]

instance Unicode.UTF16.instDecoderUInt16Char :

Decoder UTF16 UInt16 Char

Equations

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

source

@[instance_reducible]

instance Unicode.UTF16.instEncoderCharUInt16 :

Encoder UTF16 Char UInt16

Equations

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

source

@[inline]

def Unicode.UTF16.decodeIter {ι : Type} (it : Std.Iter UInt16) :

Std.Iter Char

Decodes the UTF-16 code units of it, stopping at the first unpaired surrogate.

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