UTF-8, UTF-16 and UTF-32 inputs

Experimental. This module's API may change in any release.

Parsers over the characters of UTF-8, UTF-16 and UTF-32 input, using the decoding iterators of UnicodeFormat. Positions are those of the encoded input: byte offsets for UTF-8, and code unit indices for UTF-16 and UTF-32.

A strict decoding iterator ends at the first ill-formed input, so a parser sees the end of the input there. Parser.parseDecoded and the parseUTF8, parseUTF16 and parseUTF32 runners report the ill-formed input as an error when the parser stops where decoding stopped, or fails there. A parser that goes on after ill-formed input instead can consume it with UTF.illFormed.

@[instance_reducible]

instance ParseIt.instHasPosDecodeIterator {δ ι τ σ : Type} [Unicode.Decoder δ τ σ] [Std.Iterator ι Id τ] [Std.Iterators.Productive ι Id] [HasPos ι τ] : HasPos (Unicode.DecodeIterator δ ι) σ

Positions are those of the input iterator, at the start of the next token to decode.

Equations

• ParseIt.instHasPosDecodeIterator = { Pos := ParseIt.HasPos.Pos ι, pos := fun (it : Std.Iter σ) => ParseIt.HasPos.pos it.decodeBase }

@[reducible, inline]

abbrev ParseIt.UTF8Iterator : Type

The iterator over the characters of UTF-8 bytes.

Equations

• ParseIt.UTF8Iterator = Unicode.DecodeIterator Unicode.UTF8 ScalarArray.UInt8Array.SliceIterator

@[reducible, inline]

abbrev ParseIt.UTF16Iterator : Type

The iterator over the characters of UTF-16 code units.

Equations

• ParseIt.UTF16Iterator = Unicode.DecodeIterator Unicode.UTF16 ScalarArray.UInt16Array.SliceIterator

@[reducible, inline]

abbrev ParseIt.UTF32Iterator : Type

The iterator over the characters of UTF-32 code units.

Equations

• ParseIt.UTF32Iterator = Unicode.DecodeIterator Unicode.UTF32 ScalarArray.UInt32Array.SliceIterator

@[inline]

def ParseIt.UTF.illFormed {ε δ ι τ : Type} {m : Type → Type} [Unicode.Decoder δ τ Char] [Std.Iterator ι Id τ] [Std.Iterators.Finite ι Id] [Pure m] [Error ε (Unicode.DecodeIterator δ ι) Char] : ParserT ε (Unicode.DecodeIterator δ ι) Char m Unicode.DecodeError.Kind

illFormed consumes the ill-formed input where a strict decoding iterator stopped, and returns its kind, so that a parser can report it and go on after it. Fails, consuming nothing, at well-formed input and at the end of the input. On a lossy decoding iterator, it consumes ill-formed input before it is replaced with U+FFFD.

Equations

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

def ParseIt.Parser.parseDecoded {ε δ ι τ α : Type} [Unicode.Decoder δ τ Char] [Std.Iterator ι Id τ] [Std.Iterators.Finite ι Id] [Error ε (Unicode.DecodeIterator δ ι) Char] (p : Parser ε (Unicode.DecodeIterator δ ι) Char α) (it : Std.Iter Char) : Except ε α

p.parseDecoded it runs p on the characters of the decoding iterator it. When it is strict and stops at ill-formed input, and p succeeds and stops there, that input is reported as an error at its position. When p fails, its error is kept, and a message about the first ill-formed input of it is added to it, which Error.Simple records and Error.Basic discards. That message is about the first ill-formed input even when p consumed it with UTF.illFormed and failed later.

Equations

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

@[inline]

def ParseIt.Parser.parseUTF8 {ε α : Type} [Error ε UTF8Iterator Char] (p : Parser ε UTF8Iterator Char α) (b : ByteArray) : Except ε α

Run p on the characters of the UTF-8 bytes b, reporting ill-formed bytes as errors. Positions are byte offsets.

Equations

• p.parseUTF8 b = p.parseDecoded (Unicode.UTF8.decodeIter b.toUInt8Array.iter)

@[inline]

def ParseIt.Parser.parseUTF16 {ε α : Type} [Error ε UTF16Iterator Char] (p : Parser ε UTF16Iterator Char α) (s : ScalarArray.UInt16Array.Slice) : Except ε α

Run p on the characters of the UTF-16 code units s, reporting unpaired surrogates as errors. Positions are indices in the array of s.

Equations

• p.parseUTF16 s = p.parseDecoded (Unicode.UTF16.decodeIter (Std.Slice.iter s))

@[inline]

def ParseIt.Parser.parseUTF32 {ε α : Type} [Error ε UTF32Iterator Char] (p : Parser ε UTF32Iterator Char α) (s : ScalarArray.UInt32Array.Slice) : Except ε α

Run p on the characters of the UTF-32 code units s, reporting code units that are not scalar values as errors. Positions are indices in the array of s.

Equations

• p.parseUTF32 s = p.parseDecoded (Unicode.UTF32.decodeIter (Std.Slice.iter s))