UTF-32 iterators #

UTF32.decodeIter reads characters from UTF-32 code units, and UTF32.encodeIter writes them back. A code unit that is a surrogate or above U+10FFFF is ill-formed.

source

structure Unicode.UTF32 :

Type

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

Instances For

source

@[instance_reducible]

instance Unicode.instInhabitedUTF32 :

Inhabited UTF32

Equations

Unicode.instInhabitedUTF32 = { default := Unicode.instInhabitedUTF32.default }

source

@[inline]

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

Decodes one character from the UTF-32 code units of it. Calls yield with the character and the iterator after it, error with the iterator after a code unit that is not a scalar value, 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.UTF32.instDecoderUInt32Char :

Decoder UTF32 UInt32 Char

Equations

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

source

@[instance_reducible]

instance Unicode.UTF32.instEncoderCharUInt32 :

Encoder UTF32 Char UInt32

Equations

Unicode.UTF32.instEncoderCharUInt32 = { length := fun (x : Unicode.UTF32) (x_1 : Char) => 1, unit := fun (x : Unicode.UTF32) (c : Char) (x_1 : Nat) => c.val }

source

@[inline]

def Unicode.UTF32.decodeIter {ι : Type} (it : Std.Iter UInt32) :

Std.Iter Char

Decodes the UTF-32 code units of it, stopping at the first that is not a scalar value.

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