UTF-8 Character parsers

@[reducible, inline]

abbrev Parser.Utf8Parser (ε : Type) (g : Grade) (α : Type) : Type

Equations

• Parser.Utf8Parser ε g α = Parser ByteArray Char ε g α

def Parser.runParser {α ε : Type} {g : Grade} (p : Parser ByteArray Char ε g α) (s : String) : Except ε α

Run a parser on a String.

Equations

• p.runParser s = p.runOn (Input.ofString s)

def Parser.runOption {α ε : Type} {ge gc : Necessity} (p : Parser ByteArray Char ε { errors := ge, consumes := gc } α) (s : String) : Option α

Run a parser on a String, discarding the error and returning the value as an Option.

Equations

• p.runOption s = (p.runParser s).toOption

def Parser.Utf8.anyByte : Utf8Parser Error conditional UInt8

Consume a single byte.

Equations

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

@[reducible, inline]

abbrev Parser.Utf8.anyChar : Utf8Parser Error conditional Char

Consume a single UTF-8 character.

Equations

• Parser.Utf8.anyChar = Parser.anyTok

def Parser.Utf8.char (c : Char) : Utf8Parser Error conditional PUnit.{1}

Match a specific character.

Equations

• Parser.Utf8.char c = Parser.skipSatisfy fun (x : Char) => x == c

def Parser.Utf8.string (str : String) (h : str ≠ "" := by decide) : Utf8Parser Error conditional PUnit.{1}

Match an exact non-empty string

Equations

• Parser.Utf8.string str h = match s : str.toList with | [] => ⋯.elim | c :: cs => Parser.Utf8.string.go c cs

def Parser.Utf8.string.go (c : Char) : List Char → Utf8Parser Error conditional PUnit.{1}

Equations

• Parser.Utf8.string.go c [] = Parser.skipSatisfy fun (x : Char) => x == c
• Parser.Utf8.string.go c (c' :: cs) = (Parser.skipSatisfy fun (x : Char) => x == c) >>=ᵍ fun (__r : Unit) => Parser.Utf8.string.go c' cs

def Parser.Utf8.takeWhile (f : Char → Bool) : Utf8Parser Error flexible String

Consume characters while f holds, returning the collected string.

Equations

• Parser.Utf8.takeWhile f = String.ofList <$>ᵍ (Parser.satisfy f).many

def Parser.Utf8.takeWhile1 (f : Char → Bool) : Utf8Parser Error conditional String

Consume one or more characters while f holds.

Equations

• Parser.Utf8.takeWhile1 f = (String.ofList ∘ NonEmptyList.toList) <$>ᵍ (Parser.satisfy f).many1

def Parser.Utf8.skipWhile (f : Char → Bool) : Utf8Parser Error flexible PUnit.{1}

Skip characters while f holds.

Equations

• Parser.Utf8.skipWhile f = () <$ᵍ Parser.Utf8.takeWhile f

def Parser.Utf8.skipWhile1 (f : Char → Bool) : Utf8Parser Error conditional PUnit.{1}

Skip one or more characters while f holds.

Equations

• Parser.Utf8.skipWhile1 f = () <$ᵍ Parser.Utf8.takeWhile1 f

theorem Parser.Utf8.many_go_satisfy_restSize {n : ℕ} (f : Char → Bool) (t : Input ByteArray n) : (many.go (satisfy f) t).restSize = ↑(Input.skipWhile f t)

theorem Parser.Utf8.many_go_satisfy_result {n : ℕ} (f : Char → Bool) (t : Input ByteArray n) : String.ofList (many.go (satisfy f) t).result = Input.takeWhile f t

theorem Parser.Utf8.takeWhile1_run_accept {n : ℕ} {f : Char → Bool} {c : Char} {t : Input ByteArray n} (h : t.nextTok = some c := by assumption) (hf : f c = true := by assumption) : (takeWhile1 f).run t = success { result := Input.takeWhile f t, restSize := ↑(Input.skipWhile f t), witness := ⋯ }

theorem Parser.Utf8.takeWhile1_run_failure {n : ℕ} {f : Char → Bool} {t : Input ByteArray n} {fl : Failure n Error} (hs : (satisfy f).run t = failure fl) : (takeWhile1 f).run t = failure fl

takeWhile1 fails exactly as the leading satisfy does.

theorem Parser.Utf8.skipWhile1_run_accept {n : ℕ} {f : Char → Bool} {c : Char} {t : Input ByteArray n} (h : t.nextTok = some c) (hf : f c = true) : (skipWhile1 f).run t = success { result := (), restSize := ↑(Input.skipWhile f t), witness := ⋯ }

theorem Parser.Utf8.skipWhile1_run_failure {n : ℕ} {f : Char → Bool} {t : Input ByteArray n} {fl : Failure n Error} (hs : (satisfy f).run t = failure fl) : (skipWhile1 f).run t = failure fl

skipWhile1 fails exactly as takeWhile1 does.

def Parser.Utf8.whitespace : Utf8Parser Error flexible PUnit.{1}

Skip zero or more whitespace characters.

Equations

• Parser.Utf8.whitespace = Parser.Utf8.skipWhile Char.isWhitespace

def Parser.Utf8.whitespace1 : Utf8Parser Error conditional PUnit.{1}

Skip one or more whitespace characters.

Equations

• Parser.Utf8.whitespace1 = Parser.Utf8.skipWhile1 Char.isWhitespace

def Parser.Utf8.lexeme {α : Type} {ge gc : Necessity} (p : Utf8Parser Error { errors := ge, consumes := gc } α) : Utf8Parser Error { errors := ge, consumes := max gc possibly } α

Run p then skip trailing whitespace.

Equations

• Parser.Utf8.lexeme p = gcast ⋯ (p >>=ᵍ fun (r : α) => Parser.Utf8.whitespace >>=ᵍ fun (__r : Unit) => gpure r)

def Parser.Utf8.lparen : Utf8Parser Error conditional PUnit.{1}

Equations

• Parser.Utf8.lparen = Parser.Utf8.char '('

def Parser.Utf8.rparen : Utf8Parser Error conditional PUnit.{1}

Equations

• Parser.Utf8.rparen = Parser.Utf8.char ')'

def Parser.Utf8.lbracket : Utf8Parser Error conditional PUnit.{1}

Equations

• Parser.Utf8.lbracket = Parser.Utf8.char '['

def Parser.Utf8.rbracket : Utf8Parser Error conditional PUnit.{1}

Equations

• Parser.Utf8.rbracket = Parser.Utf8.char ']'

def Parser.Utf8.lbrace : Utf8Parser Error conditional PUnit.{1}

Equations

• Parser.Utf8.lbrace = Parser.Utf8.char '{'

def Parser.Utf8.rbrace : Utf8Parser Error conditional PUnit.{1}

Equations

• Parser.Utf8.rbrace = Parser.Utf8.char '}'

def Parser.Utf8.dquote : Utf8Parser Error conditional PUnit.{1}

Equations

• Parser.Utf8.dquote = Parser.Utf8.char '\"'

def Parser.Utf8.comma : Utf8Parser Error conditional PUnit.{1}

Equations

• Parser.Utf8.comma = Parser.Utf8.char ','

def Parser.Utf8.bracket {α : Type} {ge gc : Necessity} (l r : Utf8Parser Error conditional PUnit.{1}) (p : Utf8Parser Error { errors := ge, consumes := gc } α) : Utf8Parser Error { errors := max ge possibly, consumes := always } α

Parse p surrounded by the delimiters l and r. Delimiters consume whitespace after them.

Equations

• Parser.Utf8.bracket l r p = Parser.rawBracket (Parser.Utf8.lexeme l) (Parser.Utf8.lexeme r) p

def Parser.Utf8.parens {α : Type} {ge gc : Necessity} (p : Utf8Parser Error { errors := ge, consumes := gc } α) : Utf8Parser Error { errors := max ge possibly, consumes := always } α

Parse p surrounded by parentheses.

Equations

• Parser.Utf8.parens p = Parser.Utf8.bracket Parser.Utf8.lparen Parser.Utf8.rparen p

def Parser.Utf8.brackets {α : Type} {ge gc : Necessity} (p : Utf8Parser Error { errors := ge, consumes := gc } α) : Utf8Parser Error { errors := max ge possibly, consumes := always } α

Parse p surrounded by square brackets.

Equations

• Parser.Utf8.brackets p = Parser.Utf8.bracket Parser.Utf8.lbracket Parser.Utf8.rbracket p

def Parser.Utf8.braces {α : Type} {ge gc : Necessity} (p : Utf8Parser Error { errors := ge, consumes := gc } α) : Utf8Parser Error { errors := max ge possibly, consumes := always } α

Parse p surrounded by curly braces.

Equations

• Parser.Utf8.braces p = Parser.Utf8.bracket Parser.Utf8.lbrace Parser.Utf8.rbrace p

def Parser.Utf8.digit : Utf8Parser Error conditional ℕ

Parse a single decimal digit, returning its numeric value.

Equations

• Parser.Utf8.digit = Parser.token fun (c : Char) => if c.isDigit = true then some (c.toNat - '0'.toNat) else none

theorem Parser.Utf8.digit_run_accept {n : ℕ} {c : Char} {t : Input ByteArray n} (h : t.nextTok = some c := by assumption) (hd : c.isDigit = true := by assumption) : digit.run t = success { result := c.toNat - '0'.toNat, restSize := n - Reader.width ByteArray c, witness := ⋯ }

theorem Parser.Utf8.digit_run_reject {n : ℕ} {c : Char} {t : Input ByteArray n} (h : t.nextTok = some c := by assumption) (hd : ¬c.isDigit = true := by assumption) : digit.run t = failure { error := Error.fail, restSize := n - Reader.width ByteArray c, witness := ⋯ }

theorem Parser.Utf8.digit_run_eof {n : ℕ} {t : Input ByteArray n} (h : t.nextTok = none := by first | assumption | exact Input.nextTok_eq_none) : digit.run t = failure { error := Error.eof, restSize := n, witness := ⋯ }

def Parser.Utf8.nat : Utf8Parser Error conditional ℕ

Parse a natural number (one or more digits).

Equations

• Parser.Utf8.nat = Parser.Utf8.digit >>=ᵍ fun (d : ℕ) => Parser.many Parser.Utf8.digit >>=ᵍ fun (ds : List ℕ) => gpure (List.foldl (fun (acc d : ℕ) => acc * 10 + d) d ds)

def Parser.Utf8.int : Utf8Parser Error conditional ℤ

Parse an integer (optional leading - followed by digits).

Equations

• Parser.Utf8.int = Parser.optional (Parser.Utf8.char '-') >>=ᵍ fun (neg : Option PUnit.{1}) => Parser.Utf8.nat >>=ᵍ fun (n : ℕ) => gpure (if neg.isSome = true then -↑n else ↑n)

def Parser.Utf8.space : Utf8Parser Error conditional PUnit.{1}

Equations

• Parser.Utf8.space = Parser.skipSatisfy fun (x : Char) => x == ' '

def Parser.Utf8.tab : Utf8Parser Error conditional PUnit.{1}

Equations

• Parser.Utf8.tab = Parser.skipSatisfy fun (x : Char) => x == '\t'

def Parser.Utf8.ASCII.lf : Utf8Parser Error conditional PUnit.{1}

Equations

• Parser.Utf8.ASCII.lf = Parser.skipSatisfy fun (x : Char) => x == '\n'

def Parser.Utf8.ASCII.cr : Utf8Parser Error conditional PUnit.{1}

Equations

• Parser.Utf8.ASCII.cr = Parser.skipSatisfy fun (x : Char) => x == '\x0d'

def Parser.Utf8.ASCII.uppercase : Utf8Parser Error conditional Char

Match an ASCII uppercase letter.

Equations

• Parser.Utf8.ASCII.uppercase = Parser.satisfy Char.isUpper

def Parser.Utf8.ASCII.lowercase : Utf8Parser Error conditional Char

Match an ASCII lowercase letter.

Equations

• Parser.Utf8.ASCII.lowercase = Parser.satisfy Char.isLower

def Parser.Utf8.ASCII.alpha : Utf8Parser Error conditional Char

Match an ASCII letter.

Equations

• Parser.Utf8.ASCII.alpha = Parser.satisfy Char.isAlpha

def Parser.Utf8.ASCII.alphanum : Utf8Parser Error conditional Char

Match an ASCII letter or digit.

Equations

• Parser.Utf8.ASCII.alphanum = Parser.satisfy Char.isAlphanum

def Parser.Utf8.ASCII.control : Utf8Parser Error conditional Char

Match an ASCII control character.

Equations

• Parser.Utf8.ASCII.control = Parser.satisfy fun (c : Char) => decide (c.val < 32) || c.val == 127

def Parser.Utf8.ASCII.binDigit : Utf8Parser Error conditional Bool

Match a binary digit.

Equations

• Parser.Utf8.ASCII.binDigit = Parser.token fun (x : Char) => match x with | '0' => some false | '1' => some true | x => none

def Parser.Utf8.ASCII.octDigit : Utf8Parser Error conditional (Fin 8)

Match an octal digit, returning its numeric value.

Equations

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

def Parser.Utf8.ASCII.hexDigit : Utf8Parser Error conditional (Fin 16)

Match a hexadecimal digit, returning its numeric value.

Equations

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

def Parser.Utf8.eol : Utf8Parser Error conditional PUnit.{1}

Match a line terminator: LF or CRLF.

Equations

• Parser.Utf8.eol = Parser.skipOptional Parser.Utf8.ASCII.cr >>=ᵍ fun (__r : Unit) => Parser.Utf8.ASCII.lf