Documentation

UnicodeFormat.EncodingScheme

Encoding schemes #

An encoding scheme serializes the code units of an encoding form as bytes (Unicode Standard, Section 3.10). UTF-16BE and UTF-32BE put the most significant byte of each code unit first, UTF-16LE and UTF-32LE the least significant byte. In these four schemes, a leading U+FEFF is a character like any other. The UTF-16 and UTF-32 schemes start with the byte order mark U+FEFF, which tells the byte order of the rest and is not part of the text. UTF-8 has no byte order, but its data sometimes starts with U+FEFF as a signature.

A byte sequence whose size is not a multiple of the code unit size is ill-formed: lossy decoding replaces the incomplete code unit at the end with U+FFFD. Lossy UTF-8 decoding replaces each maximal subpart of an ill-formed byte sequence with U+FFFD, following the recommended practice of the Standard, Section 3.9, like UTF8.decodeLossy. Core's String.fromUTF8Lossy replaces each run of ill-formed bytes instead, so it can give fewer U+FFFD.

decode reports the first ill-formed input with its byte offset, counting the byte order mark or signature.

detect? finds the scheme of bytes that start with a byte order mark or signature, and name and ofName? convert to and from the IANA charset names of the schemes.

For streaming, UnicodeFormat.Iterator.EncodingScheme makes each scheme a decoder and an encoder between bytes and characters, with decodeIter and encodeIter.

inductive Unicode.EncodingScheme :

A Unicode encoding scheme.

utf8 : EncodingScheme
UTF-8, where a leading U+FEFF is a character.
utf8BOM : EncodingScheme
UTF-8 with a signature: encoding writes a leading U+FEFF and decoding skips one.
utf16BE : EncodingScheme
UTF-16 in big-endian byte order.
utf16LE : EncodingScheme
UTF-16 in little-endian byte order.
utf16 (order : ByteOrder := ByteOrder.big) : EncodingScheme
UTF-16 with a byte order mark. Encoding writes the mark, then the code units in byte order order. Decoding follows the mark, or reads in byte order order if there is none; the Standard calls for big-endian, the default.
utf32BE : EncodingScheme
UTF-32 in big-endian byte order.
utf32LE : EncodingScheme
UTF-32 in little-endian byte order.
utf32 (order : ByteOrder := ByteOrder.big) : EncodingScheme
UTF-32 with a byte order mark. Encoding writes the mark, then the code units in byte order order. Decoding follows the mark, or reads in byte order order if there is none; the Standard calls for big-endian, the default.

Instances For

@[instance_reducible]

instance Unicode.instInhabitedEncodingScheme :

Inhabited EncodingScheme

Equations

Unicode.instInhabitedEncodingScheme = { default := Unicode.instInhabitedEncodingScheme.default }

@[instance_reducible]

instance Unicode.instDecidableEqEncodingScheme :

DecidableEq EncodingScheme

Equations

Unicode.instDecidableEqEncodingScheme = Unicode.instDecidableEqEncodingScheme.decEq

def Unicode.instDecidableEqEncodingScheme.decEq (x✝ x✝¹ : EncodingScheme) :

Decidable (x✝ = x✝¹)

Equations

Instances For

@[instance_reducible]

instance Unicode.instReprEncodingScheme :

Repr EncodingScheme

Equations

Unicode.instReprEncodingScheme = { reprPrec := Unicode.instReprEncodingScheme.repr }

def Unicode.instReprEncodingScheme.repr :

EncodingScheme → Nat → Std.Format

Equations

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

Instances For

Code units and bytes

Byte order marks

Encoding and decoding

def Unicode.EncodingScheme.encode (e : EncodingScheme) (s : String) :

The encoding of s in the scheme e.

Equations

Instances For

def Unicode.EncodingScheme.decode (e : EncodingScheme) (b : ByteArray) :

Except DecodeError String

Decodes b in the scheme e, or returns the first ill-formed input with its byte offset in b.

Equations

One or more equations did not get rendered due to their size.
Unicode.EncodingScheme.utf8.decode b = Unicode.UTF8.decode b
Unicode.EncodingScheme.utf16BE.decode b = Unicode.EncodingScheme.decode16✝ Unicode.ByteOrder.big (Unicode.EncodingScheme.bytes✝ b)
Unicode.EncodingScheme.utf16LE.decode b = Unicode.EncodingScheme.decode16✝ Unicode.ByteOrder.little (Unicode.EncodingScheme.bytes✝ b)
(Unicode.EncodingScheme.utf16 a).decode b = match Unicode.EncodingScheme.readBOM16✝ a b with | (o, s) => Unicode.EncodingScheme.decode16✝ o s
Unicode.EncodingScheme.utf32BE.decode b = Unicode.EncodingScheme.decode32✝ Unicode.ByteOrder.big (Unicode.EncodingScheme.bytes✝ b)
Unicode.EncodingScheme.utf32LE.decode b = Unicode.EncodingScheme.decode32✝ Unicode.ByteOrder.little (Unicode.EncodingScheme.bytes✝ b)
(Unicode.EncodingScheme.utf32 a).decode b = match Unicode.EncodingScheme.readBOM32✝ a b with | (o, s) => Unicode.EncodingScheme.decode32✝ o s

Instances For

def Unicode.EncodingScheme.decode? (e : EncodingScheme) (b : ByteArray) :

Decodes b in the scheme e, or returns none if b is ill-formed.

Equations

e.decode? b = (e.decode b).toOption

Instances For

def Unicode.EncodingScheme.decode! (e : EncodingScheme) (b : ByteArray) :

Decodes b in the scheme e, panicking if b is ill-formed.

Equations

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

Instances For

def Unicode.EncodingScheme.decodeLossy (e : EncodingScheme) (b : ByteArray) :

Decodes b in the scheme e, replacing each ill-formed code unit with U+FFFD, or in UTF-8 each maximal subpart of an ill-formed byte sequence.

Equations

Instances For

def Unicode.EncodingScheme.validate (e : EncodingScheme) (b : ByteArray) :

Whether b is well-formed in the scheme e.

Equations

One or more equations did not get rendered due to their size.
Unicode.EncodingScheme.utf8.validate b = Unicode.UTF8.validate b
Unicode.EncodingScheme.utf8BOM.validate b = Unicode.UTF8.validate (Unicode.EncodingScheme.dropSignature✝ b)

Instances For

def Unicode.EncodingScheme.transcode (src dst : EncodingScheme) (b : ByteArray) :

Except DecodeError ByteArray

Converts b from the scheme src to the scheme dst, or returns the first ill-formed input in src with its byte offset in b.

Equations

src.transcode dst b = Except.map dst.encode (src.decode b)

Instances For

def Unicode.EncodingScheme.transcode? (src dst : EncodingScheme) (b : ByteArray) :

Option ByteArray

Converts b from the scheme src to the scheme dst, or returns none if b is ill-formed in src.

Equations

src.transcode? dst b = (src.transcode dst b).toOption

Instances For

def Unicode.EncodingScheme.transcodeLossy (src dst : EncodingScheme) (b : ByteArray) :

Converts b from the scheme src to the scheme dst, replacing each ill-formed code unit with U+FFFD, or in UTF-8 each maximal subpart of an ill-formed byte sequence.

Equations

src.transcodeLossy dst b = dst.encode (src.decodeLossy b)

Instances For

Detection and names

def Unicode.EncodingScheme.detect? (b : ByteArray) :

Option EncodingScheme

The scheme given by the byte order mark or UTF-8 signature at the start of b, if there is one: utf8BOM, utf16 o or utf32 o, so decoding b in that scheme skips the mark. The bytes FF FE 00 00 start both UTF-32LE with a byte order mark and UTF-16LE with a byte order mark followed by U+0000; they are taken as UTF-32LE, as is usual.

Only the mark counts: without one, the result is none, even for bytes that are plainly not UTF-8, such as UTF-16 or UTF-32 text without a mark. Callers then choose the scheme, often utf8.

Equations

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

Instances For

def Unicode.EncodingScheme.name (e : EncodingScheme) :

The IANA charset name of the scheme e: "UTF-8", "UTF-16BE", "UTF-16LE", "UTF-16", "UTF-32BE", "UTF-32LE" or "UTF-32". UTF-8 with a signature has no name of its own, and the names of the UTF-16 and UTF-32 schemes do not tell the byte order of utf16 o and utf32 o.

Equations

Unicode.EncodingScheme.utf8.name = "UTF-8"
Unicode.EncodingScheme.utf8BOM.name = "UTF-8"
Unicode.EncodingScheme.utf16BE.name = "UTF-16BE"
Unicode.EncodingScheme.utf16LE.name = "UTF-16LE"
(Unicode.EncodingScheme.utf16 a).name = "UTF-16"
Unicode.EncodingScheme.utf32BE.name = "UTF-32BE"
Unicode.EncodingScheme.utf32LE.name = "UTF-32LE"
(Unicode.EncodingScheme.utf32 a).name = "UTF-32"

Instances For

def Unicode.EncodingScheme.ofName? (s : String) :

Option EncodingScheme

The scheme with the IANA charset name or alias s, ignoring ASCII case: UTF-8, UTF-16BE, UTF-16LE, UTF-16, UTF-32BE, UTF-32LE and UTF-32, and their aliases csUTF8, csUTF16BE and so on. UTF-8 is utf8, and UTF-16 and UTF-32 are utf16 .big and utf32 .big, which read a byte order mark if there is one.

The labels of the WHATWG Encoding Standard are not names here: some of them conflict with IANA names, such as utf-16, which WHATWG takes as UTF-16LE, and WHATWG decoding follows a byte order mark whatever the label.

Equations

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

Instances For