mathlib documentation

core / data.buffer.parser

inductive parse_result (α : Type) :
Type
def parser (α : Type) :
Type

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

Equations
def parser.bind {α β : Type} (p : parser α) (f : α → parser β) :
Equations
def parser.pure {α : Type} (a : α) :
Equations
def parser.fail {α : Type} (msg : string) :
Equations
@[instance]
Equations
def parser.failure {α : Type} :
Equations
def parser.orelse {α : Type} (p q : parser α) :
Equations
@[instance]
Equations
@[instance]
def parser.inhabited {α : Type} :
Equations
def parser.decorate_errors {α : Type} (msgs : thunk (list string)) (p : parser α) :

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

Equations
def parser.decorate_error {α : Type} (msg : thunk string) (p : parser α) :

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

Equations

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

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

Matches a single character satisfying the given predicate.

Equations

Matches the empty word.

Equations
def parser.ch (c : char) :

Matches the given character.

Equations

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

Equations

Matches one out of a list of characters.

Equations
def parser.str (s : string) :

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

Equations

Number of remaining input characters.

Equations

Matches the end of the input.

Equations
def parser.foldr_core {α β : Type} (f : α → β → β) (p : parser α) (b : β) (reps : ) :
Equations
def parser.foldr {α β : Type} (f : α → β → β) (p : parser α) (b : β) :

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

Equations
def parser.foldl_core {α β : Type} (f : α → β → α) (a : α) (p : parser β) (reps : ) :
Equations
def parser.foldl {α β : Type} (f : α → β → α) (a : α) (p : parser β) :

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

Equations
def parser.many {α : Type} (p : parser α) :

Matches zero or more occurrences of p.

Equations
def parser.many' {α : Type} (p : parser α) :

Matches zero or more occurrences of p.

Equations
def parser.many1 {α : Type} (p : parser α) :

Matches one or more occurrences of p.

Equations

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

Equations
def parser.sep_by1 {α : Type} (sep : parser unit) (p : parser α) :

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

Equations
def parser.sep_by {α : Type} (sep : parser unit) (p : parser α) :

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

Equations
def parser.fix_core {α : Type} (F : parser αparser α) (max_depth : ) :
Equations

Matches a digit (0-9).

Equations

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

Equations
def parser.fix {α : Type} (F : parser αparser α) :

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

Equations
def parser.mk_error_msg (input : char_buffer) (pos : ) (expected : dlist string) :
Equations
def parser.run {α : Type} (p : parser α) (input : char_buffer) :

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

Equations
def parser.run_string {α : Type} (p : parser α) (input : string) :

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

Equations