mathlib docs: core.data.buffer.parser

source

inductive parse_result :

Type → Type

done : Π (α : Type), ℕ → α → parse_result α
fail : Π (α : Type), ℕ → dlist string → parse_result α

source

def parser :

Type → Type

The parser monad. If you are familiar with the Parsec library in Haskell, you will understand this.

Equations

parser α = (char_buffer → ℕ → parse_result α)

source

def parser.bind {α β : Type} :

parser α → (α → parser β) → parser β

Equations

p.bind f = λ (input : char_buffer) (pos : ℕ), parser.bind._match_1 f input (p input pos)
parser.bind._match_1 f input (parse_result.fail pos expected) = parse_result.fail pos expected
parser.bind._match_1 f input (parse_result.done pos a) = f a input pos

source

def parser.pure {α : Type} :

α → parser α

Equations

parser.pure a = λ (input : char_buffer) (pos : ℕ), parse_result.done pos a

source

def parser.fail {α : Type} :

string → parser α

Equations

parser.fail msg = λ (_x : char_buffer) (pos : ℕ), parse_result.fail pos (dlist.singleton msg)

source

@[instance]

def parser.monad :

monad parser

Equations

parser.monad = monad.mk

source

@[instance]

def parser.is_lawful_monad :

is_lawful_monad parser

Equations

parser.is_lawful_monad = _

source

@[instance]

def parser.monad_fail :

monad_fail parser

Equations

parser.monad_fail = {fail := parser.fail}

source

def parser.failure {α : Type} :

parser α

Equations

parser.failure = λ (_x : char_buffer) (pos : ℕ), parse_result.fail pos dlist.empty

source

def parser.orelse {α : Type} :

parser α → parser α → parser α

Equations

p.orelse q = λ (input : char_buffer) (pos : ℕ), parser.orelse._match_1 q input pos (p input pos)
parser.orelse._match_1 q input pos (parse_result.fail pos₁ expected₁) = ite (pos₁ ≠ pos) (parse_result.fail pos₁ expected₁) (parser.orelse._match_2 pos₁ expected₁ (q input pos))
parser.orelse._match_1 q input pos (parse_result.done pos_1 result) = parse_result.done pos_1 result
parser.orelse._match_2 pos₁ expected₁ (parse_result.fail pos₂ expected₂) = ite (pos₁ < pos₂) (parse_result.fail pos₁ expected₁) (ite (pos₂ < pos₁) (parse_result.fail pos₂ expected₂) (parse_result.fail pos₁ (expected₁ ++ expected₂)))
parser.orelse._match_2 pos₁ expected₁ (parse_result.done pos result) = parse_result.done pos result

source

@[instance]

def parser.alternative :

alternative parser

Equations

parser.alternative = {to_applicative := {to_functor := {map := λ (_x _x_1 : Type) (x : _x → _x_1) (y : parser _x), has_pure.pure x <*> y, map_const := λ (α β : Type), (λ (x : β → α) (y : parser β), has_pure.pure x <*> y) ∘ function.const β}, to_has_pure := applicative.to_has_pure monad.to_applicative, to_has_seq := applicative.to_has_seq monad.to_applicative, to_has_seq_left := {seq_left := λ (α β : Type) (a : parser α) (b : parser β), (λ (_x _x_1 : Type) (x : _x → _x_1) (y : parser _x), has_pure.pure x <*> y) α (β → α) (function.const β) a <*> b}, to_has_seq_right := {seq_right := λ (α β : Type) (a : parser α) (b : parser β), (λ (_x _x_1 : Type) (x : _x → _x_1) (y : parser _x), has_pure.pure x <*> y) α (β → β) (function.const α id) a <*> b}}, to_has_orelse := {orelse := parser.orelse}, failure := parser.failure}

source

@[instance]

def parser.inhabited {α : Type} :

inhabited (parser α)

Equations

parser.inhabited = {default := parser.failure α}

source

def parser.decorate_errors {α : Type} :

thunk (list string) → parser α → parser α

Overrides the expected token name, and does not consume input on failure.

Equations

parser.decorate_errors msgs p = λ (input : char_buffer) (pos : ℕ), parser.decorate_errors._match_1 msgs pos (p input pos)
parser.decorate_errors._match_1 msgs pos (parse_result.fail _x expected) = parse_result.fail pos (dlist.lazy_of_list (λ («_» : unit), msgs ()))
parser.decorate_errors._match_1 msgs pos (parse_result.done pos_1 result) = parse_result.done pos_1 result

source

def parser.decorate_error {α : Type} :

thunk string → parser α → parser α

Overrides the expected token name, and does not consume input on failure.

Equations

parser.decorate_error msg p = parser.decorate_errors (λ («_» : unit), [msg ()]) p

source

def parser.any_char :

parser char

Matches a single character. Fails only if there is no more input.

Equations

parser.any_char = λ (input : char_buffer) (pos : ℕ), dite (pos < buffer.size input) (λ (h : pos < buffer.size input), let c : char := buffer.read input ⟨pos, h⟩ in parse_result.done (pos + 1) c) (λ (h : ¬pos < buffer.size input), parse_result.fail pos dlist.empty)

source

def parser.sat (p : char → Prop) [decidable_pred p] :

parser char

Matches a single character satisfying the given predicate.

Equations

parser.sat p = λ (input : char_buffer) (pos : ℕ), dite (pos < buffer.size input) (λ (h : pos < buffer.size input), let c : char := buffer.read input ⟨pos, h⟩ in ite (p c) (parse_result.done (pos + 1) c) (parse_result.fail pos dlist.empty)) (λ (h : ¬pos < buffer.size input), parse_result.fail pos dlist.empty)

source

def parser.eps :

parser unit

Matches the empty word.

Equations

parser.eps = return ()

source

def parser.ch :

char → parser unit

Matches the given character.

Equations

parser.ch c = parser.decorate_error (λ («_» : unit), c.to_string) (parser.sat (λ (_x : char), _x = c) >> parser.eps)

source

def parser.char_buf :

char_buffer → parser unit

Matches a whole char_buffer. Does not consume input in case of failure.

Equations

parser.char_buf s = parser.decorate_error (λ («_» : unit), buffer.to_string s) (list.mmap' parser.ch (buffer.to_list s))

source

def parser.one_of :

list char → parser char

Matches one out of a list of characters.

Equations

parser.one_of cs = parser.decorate_errors (λ («_» : unit), cs >>= λ (c : char), return c.to_string) (parser.sat (λ (_x : char), _x ∈ cs))

source

def parser.one_of' :

list char → parser unit

Equations

parser.one_of' cs = parser.one_of cs >> parser.eps

source

def parser.str :

string → parser unit

Matches a string. Does not consume input in case of failure.

Equations

parser.str s = parser.decorate_error (λ («_» : unit), s) (list.mmap' parser.ch s.to_list)

source

def parser.remaining :

parser ℕ

Number of remaining input characters.

Equations

parser.remaining = λ (input : char_buffer) (pos : ℕ), parse_result.done pos (buffer.size input - pos)

source

def parser.eof :

parser unit

Matches the end of the input.

Equations

parser.eof = parser.decorate_error (λ («_» : unit), "") (parser.remaining >>= λ (rem : ℕ), guard (rem = 0))

source

def parser.foldr_core {α β : Type} :

(α → β → β) → parser α → β → ℕ → parser β

Equations

parser.foldr_core f p b (reps + 1) = ((p >>= λ (x : α), parser.foldr_core f p b reps >>= λ (xs : β), return (f x xs)) <|> return b)
parser.foldr_core f p b 0 = failure

source

def parser.foldr {α β : Type} :

(α → β → β) → parser α → β → parser β

Matches zero or more occurrences of p, and folds the result.

Equations

parser.foldr f p b = λ (input : char_buffer) (pos : ℕ), parser.foldr_core f p b (buffer.size input - pos + 1) input pos

source

def parser.foldl_core {α β : Type} :

(α → β → α) → α → parser β → ℕ → parser α

Equations

parser.foldl_core f a p (reps + 1) = ((p >>= λ (x : β), parser.foldl_core f (f a x) p reps) <|> return a)
parser.foldl_core f a p 0 = failure

source

def parser.foldl {α β : Type} :

(α → β → α) → α → parser β → parser α

Matches zero or more occurrences of p, and folds the result.

Equations

parser.foldl f a p = λ (input : char_buffer) (pos : ℕ), parser.foldl_core f a p (buffer.size input - pos + 1) input pos

source

def parser.many {α : Type} :

parser α → parser (list α)

Matches zero or more occurrences of p.

Equations

p.many = parser.foldr list.cons p list.nil

source

def parser.many_char :

parser char → parser string

Equations

p.many_char = list.as_string <$> p.many

source

def parser.many' {α : Type} :

parser α → parser unit

Matches zero or more occurrences of p.

Equations

p.many' = p.many >> parser.eps

source

def parser.many1 {α : Type} :

parser α → parser (list α)

Matches one or more occurrences of p.

Equations

p.many1 = list.cons <$> p <*> p.many

source

def parser.many_char1 :

parser char → parser string

Matches one or more occurences of the char parser p and implodes them into a string.

Equations

p.many_char1 = list.as_string <$> p.many1

source

def parser.sep_by1 {α : Type} :

parser unit → parser α → parser (list α)

Matches one or more occurrences of p, separated by sep.

Equations

sep.sep_by1 p = list.cons <$> p <*> (sep >> p).many

source

def parser.sep_by {α : Type} :

parser unit → parser α → parser (list α)

Matches zero or more occurrences of p, separated by sep.

Equations

sep.sep_by p = (sep.sep_by1 p <|> return list.nil)

source

def parser.fix_core {α : Type} :

(parser α → parser α) → ℕ → parser α

Equations

parser.fix_core F (max_depth + 1) = F (parser.fix_core F max_depth)
parser.fix_core F 0 = failure

source

def parser.digit :

parser ℕ

Matches a digit (0-9).

Equations

parser.digit = parser.decorate_error (λ («_» : unit), "") (parser.sat (λ (c : char), '0' ≤ c ∧ c ≤ '9') >>= λ (c : char), has_pure.pure (c.to_nat - '0'.to_nat))

source

def parser.nat :

parser ℕ

Matches a natural number. Large numbers may cause performance issues, so don't run this parser on untrusted input.

Equations

parser.nat = parser.decorate_error (λ («_» : unit), "") (parser.digit.many1 >>= λ (digits : list ℕ), has_pure.pure (list.foldr (λ (digit : ℕ) (_x : ℕ × ℕ), parser.nat._match_1 digit _x) (0, 1) digits).fst)
parser.nat._match_1 digit (sum, magnitude) = (sum + digit * magnitude, magnitude * 10)

source

def parser.fix {α : Type} :

(parser α → parser α) → parser α

Fixpoint combinator satisfying fix F = F (fix F).

Equations

parser.fix F = λ (input : char_buffer) (pos : ℕ), parser.fix_core F (buffer.size input - pos + 1) input pos

source

def parser.mk_error_msg :

char_buffer → ℕ → dlist string → char_buffer

Equations

parser.mk_error_msg input pos expected = let left_ctx : buffer char := (buffer.take input pos).take_right 10, right_ctx : buffer char := (buffer.drop input pos).take 10 in left_ctx.map make_monospaced ++ right_ctx.map make_monospaced ++ "\n".to_char_buffer ++ left_ctx.map (λ (_x : char), ' ') ++ "^\n".to_char_buffer ++ "\n".to_char_buffer ++ "expected: ".to_char_buffer ++ (" | ".intercalate expected.to_list).to_char_buffer ++ "\n".to_char_buffer

source

def parser.run {α : Type} :

parser α → char_buffer → string ⊕ α

Runs a parser on the given input. The parser needs to match the complete input.

Equations

p.run input = parser.run._match_1 input ((p <* parser.eof) input 0)
parser.run._match_1 input (parse_result.fail pos expected) = sum.inl (buffer.to_string (parser.mk_error_msg input pos expected))
parser.run._match_1 input (parse_result.done pos res) = sum.inr res

source

def parser.run_string {α : Type} :

parser α → string → string ⊕ α

Runs a parser on the given input. The parser needs to match the complete input.

Equations

p.run_string input = p.run input.to_char_buffer

mathlib documentation

core.data.buffer.parser

General documentation

Additional documentation

Library

mathlib documentation

core.​data.​buffer.​parser

General documentation

Additional documentation

Library

core.data.buffer.parser