Byte order iterators

The encoding schemes UTF-16BE, UTF-16LE, UTF-32BE and UTF-32LE serialize code units as bytes. ByteOrder.decodeIter16 reads UTF-16 code units from bytes and ByteOrder.encodeIter16 writes them, and likewise decodeIter32 and encodeIter32 for UTF-32. Bytes that end in the middle of a code unit are ill-formed; lossy decoding replaces that code unit with 0xFFFD, which decodes to U+FFFD.

To read characters from bytes, EncodingScheme.decodeIter is faster than decoding the code units of these iterators with UTF16.decodeIter or UTF32.decodeIter, about 3.5 times for UTF-16. It reads code units and characters in one layer. Over two layers, the compiler allocates the inner iterator for each character rather than update it in place.

The UTF-16 and UTF-32 schemes start with a byte order mark: ByteOrder.readBOM16 and readBOM32 read it, and give the byte order it tells and the iterator after it.

structure Unicode.Bytes16 : Type

Code units of 2 bytes, in byte order order.

• order : ByteOrder

  The byte order.

@[instance_reducible]

instance Unicode.instInhabitedBytes16 : Inhabited Bytes16

Equations

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

structure Unicode.Bytes32 : Type

Code units of 4 bytes, in byte order order.

• order : ByteOrder

  The byte order.

@[instance_reducible]

instance Unicode.instInhabitedBytes32 : Inhabited Bytes32

Equations

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

@[inline]

def Unicode.ByteOrder.byte16 (o : ByteOrder) (u : UInt16) (i : Nat) : UInt8

Byte i of the UTF-16 code unit u in byte order o.

Equations

• o.byte16 u i = (u >>> (Unicode.ByteOrder.shift✝ o 2 i).toUInt16).toUInt8

@[inline]

def Unicode.ByteOrder.byte32 (o : ByteOrder) (u : UInt32) (i : Nat) : UInt8

Byte i of the UTF-32 code unit u in byte order o.

Equations

• o.byte32 u i = (u >>> Unicode.ByteOrder.shift✝ o 4 i).toUInt8

@[inline]

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

Reads one UTF-16 code unit from the bytes of it in byte order o. Calls yield with the code unit and the iterator after it, error with the iterator after an incomplete code unit at the end of the input, or done at the end of the input.

Equations

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

@[inline]

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

Reads one UTF-32 code unit from the bytes of it in byte order o. Calls yield with the code unit and the iterator after it, error with the iterator after an incomplete code unit at the end of the input, 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.instDecoderBytes16UInt8UInt16 : Decoder Bytes16 UInt8 UInt16

Equations

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

@[instance_reducible]

instance Unicode.instDecoderBytes32UInt8UInt32 : Decoder Bytes32 UInt8 UInt32

Equations

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

@[instance_reducible]

instance Unicode.instEncoderBytes16UInt16UInt8 : Encoder Bytes16 UInt16 UInt8

Equations

• Unicode.instEncoderBytes16UInt16UInt8 = { length := fun (x : Unicode.Bytes16) (x_1 : UInt16) => 2, unit := fun (d : Unicode.Bytes16) => d.order.byte16 }

@[instance_reducible]

instance Unicode.instEncoderBytes32UInt32UInt8 : Encoder Bytes32 UInt32 UInt8

Equations

• Unicode.instEncoderBytes32UInt32UInt8 = { length := fun (x : Unicode.Bytes32) (x_1 : UInt32) => 4, unit := fun (d : Unicode.Bytes32) => d.order.byte32 }

@[inline]

def Unicode.ByteOrder.decodeIter16 {ι : Type} (o : ByteOrder) (it : Std.Iter UInt8) : Std.Iter UInt16

Decodes the bytes of it as UTF-16 code units in byte order o, stopping at an incomplete code unit.

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 decodeIter16Lossy instead.

Equations

• o.decodeIter16 it = Unicode.Decoder.iter { order := o } it

@[inline]

def Unicode.ByteOrder.decodeIter16Lossy {ι : Type} (o : ByteOrder) (it : Std.Iter UInt8) : Std.Iter UInt16

Decodes the bytes of it as UTF-16 code units in byte order o, replacing an incomplete code unit with 0xFFFD.

Equations

• o.decodeIter16Lossy it = Unicode.Decoder.iterLossy { order := o } it

@[inline]

def Unicode.ByteOrder.encodeIter16 {ι : Type} (o : ByteOrder) (it : Std.Iter UInt16) : Std.Iter UInt8

Encodes the UTF-16 code units of it as bytes in byte order o.

Equations

• o.encodeIter16 it = Unicode.Encoder.iter { order := o } it

@[inline]

def Unicode.ByteOrder.decodeIter32 {ι : Type} (o : ByteOrder) (it : Std.Iter UInt8) : Std.Iter UInt32

Decodes the bytes of it as UTF-32 code units in byte order o, stopping at an incomplete code unit.

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 decodeIter32Lossy instead.

Equations

• o.decodeIter32 it = Unicode.Decoder.iter { order := o } it

@[inline]

def Unicode.ByteOrder.decodeIter32Lossy {ι : Type} (o : ByteOrder) (it : Std.Iter UInt8) : Std.Iter UInt32

Decodes the bytes of it as UTF-32 code units in byte order o, replacing an incomplete code unit with 0xFFFD.

Equations

• o.decodeIter32Lossy it = Unicode.Decoder.iterLossy { order := o } it

@[inline]

def Unicode.ByteOrder.encodeIter32 {ι : Type} (o : ByteOrder) (it : Std.Iter UInt32) : Std.Iter UInt8

Encodes the UTF-32 code units of it as bytes in byte order o.

Equations

• o.encodeIter32 it = Unicode.Encoder.iter { order := o } it

def Unicode.ByteOrder.readBOM16 {ι : Type} [Std.Iterator ι Id UInt8] [Std.Iterators.Productive ι Id] (o : ByteOrder) (it : Std.Iter UInt8) : ByteOrder × Std.Iter UInt8

The byte order given by the UTF-16 byte order mark at it, or o if there is none, and the iterator after the mark.

Equations

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

def Unicode.ByteOrder.readBOM32 {ι : Type} [Std.Iterator ι Id UInt8] [Std.Iterators.Productive ι Id] (o : ByteOrder) (it : Std.Iter UInt8) : ByteOrder × Std.Iter UInt8

The byte order given by the UTF-32 byte order mark at it, or o if there is none, and the iterator after the mark.

Equations

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