UTF-8

The well-formed byte sequences are those of the Unicode Standard, Table 3-7. Encoding, strict decoding and validation are core's, which are fast. Ill-formed input goes through the decoder of UTF8.decodeIter: decode reports the byte offset of the first maximal subpart of an ill-formed byte sequence, and decodeLossy replaces each maximal subpart with U+FFFD, following the recommended practice of the Standard, Section 3.9. Core's String.fromUTF8Lossy replaces each run of ill-formed bytes instead, so it can give fewer U+FFFD.

def Unicode.UTF8.encodeChar (c : Char) : ScalarArray.UInt8Array

The UTF-8 bytes of c, one to four of them.

Equations

• Unicode.UTF8.encodeChar c = ScalarArray.UInt8Array.ofFn fun (i : Fin c.utf8Size) => Unicode.Encoder.unit { } c ↑i

def Unicode.UTF8.encode (s : String) : ByteArray

The UTF-8 encoding of s.

Equations

• Unicode.UTF8.encode s = s.toUTF8

def Unicode.UTF8.decode (b : ByteArray) : Except DecodeError String

Decodes the UTF-8 bytes of b, or returns an error with the byte offset of the first maximal subpart of an ill-formed byte sequence.

Equations

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

def Unicode.UTF8.decode? (b : ByteArray) : Option String

Decodes the UTF-8 bytes of b, or returns none if b is ill-formed.

Equations

• Unicode.UTF8.decode? b = String.fromUTF8? b

def Unicode.UTF8.decode! (b : ByteArray) : String

Decodes the UTF-8 bytes of b, panicking if b is ill-formed.

Equations

• Unicode.UTF8.decode! b = String.fromUTF8! b

def Unicode.UTF8.decodeLossy (b : ByteArray) : String

Decodes the UTF-8 bytes of b, replacing each maximal subpart of an ill-formed byte sequence with U+FFFD.

Equations

• Unicode.UTF8.decodeLossy b = match String.fromUTF8? b with | some s => s | none => Unicode.Decoder.foldLossy { } String.push "" b.toUInt8Array.iter

def Unicode.UTF8.validate (b : ByteArray) : Bool

Whether b is well-formed UTF-8.

Equations

• Unicode.UTF8.validate b = b.validateUTF8