Character parsers

Parsers for character tokens. These work with any iterator of Char, such as CharIterator. Character classes are ASCII only; Unicode classes are planned separately.

@[inline]

def ParseIt.Char.char {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] (c : Char) : ParserT ε ι Char m Char

char c accepts and returns character c.

Equations

• ParseIt.Char.char c = ParseIt.withErrorMessage (toString "expected " ++ toString (repr c)) (ParseIt.token c)

def ParseIt.Char.string {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] (s : String) : ParserT ε ι Char m String

string s accepts the characters of s in order and returns s.

Equations

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

@[inline]

def ParseIt.Char.space {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse space (U+0020).

Equations

• ParseIt.Char.space = ParseIt.withErrorMessage "expected space (U+0020)" (ParseIt.token ' ')

@[inline]

def ParseIt.Char.tab {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse horizontal tab (U+0009).

Equations

• ParseIt.Char.tab = ParseIt.withErrorMessage "expected horizontal tab (U+0009)" (ParseIt.token '\t')

@[inline]

def ParseIt.Char.ASCII.lf {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse line feed (U+000A).

Equations

• ParseIt.Char.ASCII.lf = ParseIt.withErrorMessage "expected line feed (U+000A)" (ParseIt.token '\n')

@[inline]

def ParseIt.Char.ASCII.cr {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse carriage return (U+000D).

Equations

• ParseIt.Char.ASCII.cr = ParseIt.withErrorMessage "expected carriage return (U+000D)" (ParseIt.token '\x0d')

@[inline]

def ParseIt.Char.eol {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse end of line: line feed, optionally preceded by carriage return.

Equations

• ParseIt.Char.eol = ParseIt.withErrorMessage "expected newline" (ParseIt.Char.ASCII.cr *> ParseIt.Char.ASCII.lf <|> ParseIt.Char.ASCII.lf)

def ParseIt.Char.ASCII.whitespace {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse whitespace character (space and U+0009 to U+000D).

Equations

• ParseIt.Char.ASCII.whitespace = ParseIt.withErrorMessage "expected whitespace character" (ParseIt.tokenFilter fun (c : Char) => c == ' ' || decide (c ≥ '\t') && decide (c ≤ '\x0d'))

def ParseIt.Char.ASCII.uppercase {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse uppercase letter character (A to Z).

Equations

• ParseIt.Char.ASCII.uppercase = ParseIt.withErrorMessage "expected uppercase letter character" (ParseIt.tokenFilter fun (c : Char) => decide (c ≥ 'A') && decide (c ≤ 'Z'))

def ParseIt.Char.ASCII.lowercase {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse lowercase letter character (a to z).

Equations

• ParseIt.Char.ASCII.lowercase = ParseIt.withErrorMessage "expected lowercase letter character" (ParseIt.tokenFilter fun (c : Char) => decide (c ≥ 'a') && decide (c ≤ 'z'))

def ParseIt.Char.ASCII.alpha {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse alphabetic character (A to Z and a to z).

Equations

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

def ParseIt.Char.ASCII.numeric {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse numeric character (0 to 9).

Equations

• ParseIt.Char.ASCII.numeric = ParseIt.withErrorMessage "expected decimal digit character" (ParseIt.tokenFilter fun (c : Char) => decide (c ≥ '0') && decide (c ≤ '9'))

def ParseIt.Char.ASCII.alphanum {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse letter or digit character (A to Z, a to z and 0 to 9).

Equations

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

def ParseIt.Char.ASCII.control {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse control character (U+0000 to U+001F and U+007F).

Equations

• ParseIt.Char.ASCII.control = ParseIt.withErrorMessage "expected control character" (ParseIt.tokenFilter fun (c : Char) => decide (c.val < 32) || c.val == 127)

def ParseIt.Char.ASCII.digit {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m (Fin 10)

Parse decimal digit (0 to 9).

Equations

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

def ParseIt.Char.ASCII.binDigit {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m (Fin 2)

Parse binary digit (0 or 1).

Equations

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

def ParseIt.Char.ASCII.octDigit {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m (Fin 8)

Parse octal digit (0 to 7).

Equations

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

def ParseIt.Char.ASCII.hexDigit {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m (Fin 16)

Parse hexadecimal digit (0 to 9, A to F and a to f).

Equations

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