UTF-32

Each code point is a single code unit. A code unit that is a surrogate in D800–DFFF or above 10FFFF is ill-formed.

Decoding uses the decoder of UTF32.decodeIter. decode reports the position of the first ill-formed code unit, as an index in the slice.

def Unicode.UTF32.encodeChar (c : Char) : ScalarArray.UInt32Array

The UTF-32 code unit of c, as a one-element array.

Equations

• Unicode.UTF32.encodeChar c = ScalarArray.UInt32Array.mk #[c.val]

def Unicode.UTF32.encode (s : String) : ScalarArray.UInt32Array

The UTF-32 encoding of s.

Equations

• Unicode.UTF32.encode s = (Std.Iter.map Char.val s.chars).toUInt32Array

def Unicode.UTF32.decode (s : ScalarArray.UInt32Array.Slice) : Except DecodeError String

Decodes the UTF-32 code units of s, or returns an error with the index in s of the first code unit that is not a scalar value.

Equations

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

def Unicode.UTF32.decode? (s : ScalarArray.UInt32Array.Slice) : Option String

Decodes the UTF-32 code units of s, or returns none if s has a code unit that is not a Unicode scalar value.

Equations

• Unicode.UTF32.decode? s = (Unicode.UTF32.decode s).toOption

def Unicode.UTF32.decode! (s : ScalarArray.UInt32Array.Slice) : String

Decodes the UTF-32 code units of s, panicking if s has a code unit that is not a Unicode scalar value.

Equations

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

def Unicode.UTF32.decodeLossy (s : ScalarArray.UInt32Array.Slice) : String

Decodes the UTF-32 code units of s, replacing each code unit that is not a Unicode scalar value with U+FFFD.

Equations

• Unicode.UTF32.decodeLossy s = Unicode.Decoder.foldLossy { } String.push "" (Std.Slice.iter s)

def Unicode.UTF32.validate (s : ScalarArray.UInt32Array.Slice) : Bool

Whether s is well-formed UTF-32, that is, every code unit is a Unicode scalar value.

Equations

• Unicode.UTF32.validate s = s.all fun (x : UInt32) => decide x.isValidChar