mathlib documentation

data.buffer.parser.basic

Parsers #

parser α is the type that describes a computation that can ingest a char_buffer and output, if successful, a term of type α. This file expands on the definitions in the core library, proving that all the core library parsers are mono. There are also lemmas on the composability of parsers.

Main definitions #

Implementation details #

Lemmas about how parsers are mono are in the mono namespace. That allows using projection notation for shorter term proofs that are parallel to the definitions of the parsers in structure.

@[simp]
def parse_result.pos {α : Type} :

For some parse_result α, give the position at which the result was provided, in either the done or the fail case.

Equations
theorem parser.mono.le {α : Type} (p : parser α) (cb : char_buffer) (n : ) [p.mono] :
n (p cb n).pos
theorem parser.fail_iff {α : Type} (p : parser α) (cb : char_buffer) (n : ) :
(∀ (pos' : ) (result : α), p cb n parse_result.done pos' result) ∃ (pos' : ) (err : dlist string), p cb n = parse_result.fail pos' err
theorem parser.success_iff {α : Type} (p : parser α) (cb : char_buffer) (n : ) :
(∀ (pos' : ) (err : dlist string), p cb n parse_result.fail pos' err) ∃ (pos' : ) (result : α), p cb n = parse_result.done pos' result
theorem parser.mono.of_done {α : Type} {p : parser α} {cb : char_buffer} {n n' : } {a : α} [p.mono] (h : p cb n = parse_result.done n' a) :
n n'
theorem parser.mono.of_fail {α : Type} {p : parser α} {cb : char_buffer} {n n' : } {err : dlist string} [p.mono] (h : p cb n = parse_result.fail n' err) :
n n'
theorem parser.decorate_errors_fail {α : Type} {msgs : thunk (list string)} {p : parser α} {cb : char_buffer} {n n' : } {err : dlist string} (h : p cb n = parse_result.fail n' err) :
theorem parser.decorate_errors_success {α : Type} {msgs : thunk (list string)} {p : parser α} {cb : char_buffer} {n n' : } {a : α} (h : p cb n = parse_result.done n' a) :
theorem parser.decorate_error_fail {α : Type} {msg : thunk string} {p : parser α} {cb : char_buffer} {n n' : } {err : dlist string} (h : p cb n = parse_result.fail n' err) :
parser.decorate_error msg p cb n = parse_result.fail n (dlist.lazy_of_list (λ («_» : unit), [msg ()]))
theorem parser.decorate_error_success {α : Type} {msg : thunk string} {p : parser α} {cb : char_buffer} {n n' : } {a : α} (h : p cb n = parse_result.done n' a) :
@[simp]
theorem parser.decorate_errors_eq_done {α : Type} {msgs : thunk (list string)} {p : parser α} {cb : char_buffer} {n n' : } {a : α} :
@[simp]
theorem parser.decorate_error_eq_done {α : Type} {msg : thunk string} {p : parser α} {cb : char_buffer} {n n' : } {a : α} :
@[simp]
theorem parser.decorate_errors_eq_fail {α : Type} {msgs : thunk (list string)} {p : parser α} {cb : char_buffer} {n : } {err : dlist string} :
parser.decorate_errors msgs p cb n = parse_result.fail n err err = dlist.lazy_of_list (λ («_» : unit), msgs ()) ∃ (np : ) (err' : dlist string), p cb n = parse_result.fail np err'
@[simp]
theorem parser.decorate_error_eq_fail {α : Type} {msg : thunk string} {p : parser α} {cb : char_buffer} {n : } {err : dlist string} :
parser.decorate_error msg p cb n = parse_result.fail n err err = dlist.lazy_of_list (λ («_» : unit), [msg ()]) ∃ (np : ) (err' : dlist string), p cb n = parse_result.fail np err'
@[simp]
theorem parser.return_eq_pure {α : Type} {a : α} :
theorem parser.pure_eq_done {α : Type} {a : α} :
pure a = λ (_x : char_buffer) (n : ), parse_result.done n a
@[simp]
theorem parser.pure_ne_fail {α : Type} {cb : char_buffer} {n n' : } {err : dlist string} {a : α} :
pure a cb n parse_result.fail n' err
@[simp]
theorem parser.bind_eq_bind {α β : Type} {p : parser α} (f : α → parser β) :
p.bind f = p >>= f
@[simp]
theorem parser.bind_eq_done {α β : Type} {p : parser α} {cb : char_buffer} {n n' : } {b : β} {f : α → parser β} :
(p >>= f) cb n = parse_result.done n' b ∃ (np : ) (a : α), p cb n = parse_result.done np a f a cb np = parse_result.done n' b
@[simp]
theorem parser.bind_eq_fail {α β : Type} {p : parser α} {cb : char_buffer} {n n' : } {err : dlist string} {f : α → parser β} :
(p >>= f) cb n = parse_result.fail n' err p cb n = parse_result.fail n' err ∃ (np : ) (a : α), p cb n = parse_result.done np a f a cb np = parse_result.fail n' err
@[simp]
theorem parser.and_then_eq_bind {α β : Type} {m : Type → Type} [monad m] (a : m α) (b : m β) :
a >> b = a >>= λ (_x : α), b
theorem parser.and_then_fail {α : Type} {p : parser α} {cb : char_buffer} {n n' : } {err : dlist string} :
(p >> return ()) cb n = parse_result.fail n' err p cb n = parse_result.fail n' err
theorem parser.and_then_success {α : Type} {p : parser α} {cb : char_buffer} {n n' : } :
(p >> return ()) cb n = parse_result.done n' () ∃ (a : α), p cb n = parse_result.done n' a
@[simp]
theorem parser.map_eq_done {α β : Type} {p : parser α} {cb : char_buffer} {n n' : } {b : β} {f : α → β} :
(f <$> p) cb n = parse_result.done n' b ∃ (a : α), p cb n = parse_result.done n' a f a = b
@[simp]
theorem parser.map_eq_fail {α β : Type} {p : parser α} {cb : char_buffer} {n n' : } {err : dlist string} {f : α → β} :
(f <$> p) cb n = parse_result.fail n' err p cb n = parse_result.fail n' err
@[simp]
theorem parser.map_const_eq_done {α β : Type} {p : parser α} {cb : char_buffer} {n n' : } {b b' : β} :
(b <$ p) cb n = parse_result.done n' b' ∃ (a : α), p cb n = parse_result.done n' a b = b'
@[simp]
theorem parser.map_const_eq_fail {α β : Type} {p : parser α} {cb : char_buffer} {n n' : } {err : dlist string} {b : β} :
(b <$ p) cb n = parse_result.fail n' err p cb n = parse_result.fail n' err
theorem parser.map_const_rev_eq_done {α β : Type} {p : parser α} {cb : char_buffer} {n n' : } {b b' : β} :
(p $> b) cb n = parse_result.done n' b' ∃ (a : α), p cb n = parse_result.done n' a b = b'
theorem parser.map_rev_const_eq_fail {α β : Type} {p : parser α} {cb : char_buffer} {n n' : } {err : dlist string} {b : β} :
(p $> b) cb n = parse_result.fail n' err p cb n = parse_result.fail n' err
@[simp]
theorem parser.orelse_eq_orelse {α : Type} {p q : parser α} :
p.orelse q = (p <|> q)
@[simp]
theorem parser.orelse_eq_done {α : Type} {p q : parser α} {cb : char_buffer} {n n' : } {a : α} :
(p <|> q) cb n = parse_result.done n' a p cb n = parse_result.done n' a q cb n = parse_result.done n' a ∃ (err : dlist string), p cb n = parse_result.fail n err
@[simp]
theorem parser.orelse_eq_fail_eq {α : Type} {p q : parser α} {cb : char_buffer} {n : } {err : dlist string} :
(p <|> q) cb n = parse_result.fail n err (p cb n = parse_result.fail n err ∃ (nq : ) (errq : dlist string), n < nq q cb n = parse_result.fail nq errq) ∃ (errp errq : dlist string), p cb n = parse_result.fail n errp q cb n = parse_result.fail n errq errp ++ errq = err
theorem parser.orelse_eq_fail_not_mono_lt {α : Type} {p q : parser α} {cb : char_buffer} {n n' : } {err : dlist string} (hn : n' < n) :
(p <|> q) cb n = parse_result.fail n' err p cb n = parse_result.fail n' err q cb n = parse_result.fail n' err ∃ (errp : dlist string), p cb n = parse_result.fail n errp
theorem parser.orelse_eq_fail_of_mono_ne {α : Type} {p q : parser α} {cb : char_buffer} {n n' : } {err : dlist string} [q.mono] (hn : n n') :
(p <|> q) cb n = parse_result.fail n' err p cb n = parse_result.fail n' err
@[simp]
@[simp]
theorem parser.failure_def {α : Type} {cb : char_buffer} {n : } :
theorem parser.not_failure_eq_done {α : Type} {cb : char_buffer} {n n' : } {a : α} :
theorem parser.failure_eq_fail {α : Type} {cb : char_buffer} {n n' : } {err : dlist string} :
theorem parser.seq_eq_done {α β : Type} {cb : char_buffer} {n n' : } {b : β} {f : parser (α → β)} {p : parser α} :
(f <*> p) cb n = parse_result.done n' b ∃ (nf : ) (f' : α → β) (a : α), f cb n = parse_result.done nf f' p cb nf = parse_result.done n' a f' a = b
theorem parser.seq_eq_fail {α β : Type} {cb : char_buffer} {n n' : } {err : dlist string} {f : parser (α → β)} {p : parser α} :
(f <*> p) cb n = parse_result.fail n' err f cb n = parse_result.fail n' err ∃ (nf : ) (f' : α → β), f cb n = parse_result.done nf f' p cb nf = parse_result.fail n' err
theorem parser.seq_left_eq_done {α β : Type} {cb : char_buffer} {n n' : } {a : α} {p : parser α} {q : parser β} :
(p <* q) cb n = parse_result.done n' a ∃ (np : ) (b : β), p cb n = parse_result.done np a q cb np = parse_result.done n' b
theorem parser.seq_left_eq_fail {α β : Type} {cb : char_buffer} {n n' : } {err : dlist string} {p : parser α} {q : parser β} :
(p <* q) cb n = parse_result.fail n' err p cb n = parse_result.fail n' err ∃ (np : ) (a : α), p cb n = parse_result.done np a q cb np = parse_result.fail n' err
theorem parser.seq_right_eq_done {α β : Type} {cb : char_buffer} {n n' : } {b : β} {p : parser α} {q : parser β} :
(p *> q) cb n = parse_result.done n' b ∃ (np : ) (a : α), p cb n = parse_result.done np a q cb np = parse_result.done n' b
theorem parser.seq_right_eq_fail {α β : Type} {cb : char_buffer} {n n' : } {err : dlist string} {p : parser α} {q : parser β} :
(p *> q) cb n = parse_result.fail n' err p cb n = parse_result.fail n' err ∃ (np : ) (a : α), p cb n = parse_result.done np a q cb np = parse_result.fail n' err
theorem parser.mmap_eq_done {α β : Type} {cb : char_buffer} {n n' : } {f : α → parser β} {a : α} {l : list α} {b : β} {l' : list β} :
mmap f (a :: l) cb n = parse_result.done n' (b :: l') ∃ (np : ), f a cb n = parse_result.done np b mmap f l cb np = parse_result.done n' l'
theorem parser.mmap'_eq_done {α β : Type} {cb : char_buffer} {n n' : } {f : α → parser β} {a : α} {l : list α} :
mmap' f (a :: l) cb n = parse_result.done n' () ∃ (np : ) (b : β), f a cb n = parse_result.done np b mmap' f l cb np = parse_result.done n' ()
theorem parser.guard_eq_done {cb : char_buffer} {n n' : } {p : Prop} [decidable p] :
guard p cb n = parse_result.done n' () p n = n'
theorem parser.guard_eq_fail {cb : char_buffer} {n n' : } {err : dlist string} {p : Prop} [decidable p] :
guard p cb n = parse_result.fail n' err ¬p n = n' err = dlist.empty
@[instance]
def parser.mono.pure {α : Type} {a : α} :
@[instance]
def parser.mono.bind {α β : Type} {p : parser α} {f : α → parser β} [p.mono] [∀ (a : α), (f a).mono] :
(p >>= f).mono
@[instance]
def parser.mono.and_then {α β : Type} {p : parser α} {q : parser β} [p.mono] [q.mono] :
(p >> q).mono
@[instance]
def parser.mono.map {α β : Type} {p : parser α} [p.mono] {f : α → β} :
@[instance]
def parser.mono.seq {α β : Type} {p : parser α} {f : parser (α → β)} [f.mono] [p.mono] :
(f <*> p).mono
@[instance]
def parser.mono.mmap {α β : Type} {l : list α} {f : α → parser β} [∀ (a : α), a l(f a).mono] :
(mmap f l).mono
@[instance]
def parser.mono.mmap' {α β : Type} {l : list α} {f : α → parser β} [∀ (a : α), a l(f a).mono] :
(mmap' f l).mono
@[instance]
def parser.mono.failure {α : Type} :
@[instance]
def parser.mono.guard {p : Prop} [decidable p] :
@[instance]
def parser.mono.orelse {α : Type} {p q : parser α} [p.mono] [q.mono] :
(p <|> q).mono
@[instance]
def parser.mono.decorate_errors {α : Type} {msgs : thunk (list string)} {p : parser α} [p.mono] :
@[instance]
def parser.mono.decorate_error {α : Type} {msg : thunk string} {p : parser α} [p.mono] :
@[instance]
def parser.mono.sat {p : char → Prop} [decidable_pred p] :
@[instance]
@[instance]
def parser.mono.ch {c : char} :
@[instance]
@[instance]
@[instance]
@[instance]
@[instance]
def parser.mono.foldr_core {α β : Type} {p : parser α} {f : α → β → β} {b : β} [p.mono] {reps : } :
(parser.foldr_core f p b reps).mono
@[instance]
def parser.mono.foldr {α β : Type} {p : parser α} {b : β} {f : α → β → β} [p.mono] :
@[instance]
def parser.mono.foldl_core {α β : Type} {f : α → β → α} {p : parser β} [p.mono] {a : α} {reps : } :
(parser.foldl_core f a p reps).mono
@[instance]
def parser.mono.foldl {α β : Type} {a : α} {f : α → β → α} {p : parser β} [p.mono] :
@[instance]
def parser.mono.many {α : Type} {p : parser α} [p.mono] :
@[instance]
@[instance]
def parser.mono.many' {α : Type} {p : parser α} [p.mono] :
@[instance]
def parser.mono.many1 {α : Type} {p : parser α} [p.mono] :
@[instance]
@[instance]
def parser.mono.sep_by1 {α : Type} {p : parser α} {sep : parser unit} [p.mono] [sep.mono] :
(sep.sep_by1 p).mono
@[instance]
def parser.mono.sep_by {α : Type} {p : parser α} {sep : parser unit} [p.mono] [hs : sep.mono] :
(sep.sep_by p).mono
theorem parser.mono.fix_core {α : Type} {F : parser αparser α} (hF : ∀ (p : parser α), p.mono(F p).mono) (max_depth : ) :
(parser.fix_core F max_depth).mono
@[instance]
theorem parser.mono.fix {α : Type} {F : parser αparser α} (hF : ∀ (p : parser α), p.mono(F p).mono) :
@[simp]
theorem parser.orelse_pure_eq_fail {α : Type} {p : parser α} {cb : char_buffer} {n n' : } {err : dlist string} {a : α} :
(p <|> pure a) cb n = parse_result.fail n' err p cb n = parse_result.fail n' err n n'
theorem parser.any_char_eq_done {cb : char_buffer} {n n' : } (hn : n < buffer.size cb) {c : char} :
parser.any_char cb n = parse_result.done n' c n' = n + 1 buffer.read cb n, hn⟩ = c
theorem parser.sat_eq_done {cb : char_buffer} {n n' : } (hn : n < buffer.size cb) {c : char} {p : char → Prop} [decidable_pred p] :
parser.sat p cb n = parse_result.done n' c p c n' = n + 1 buffer.read cb n, hn⟩ = c
theorem parser.eps_eq_done {cb : char_buffer} {n n' : } :
theorem parser.ch_eq_done {cb : char_buffer} {n n' : } (hn : n < buffer.size cb) {c : char} :
parser.ch c cb n = parse_result.done n' () n' = n + 1 buffer.read cb n, hn⟩ = c
theorem parser.one_of_eq_done {cb : char_buffer} {n n' : } (hn : n < buffer.size cb) {c : char} {cs : list char} :
parser.one_of cs cb n = parse_result.done n' c c cs n' = n + 1 buffer.read cb n, hn⟩ = c
theorem parser.one_of'_eq_done {cb : char_buffer} {n n' : } (hn : n < buffer.size cb) {cs : list char} :
parser.one_of' cs cb n = parse_result.done n' () buffer.read cb n, hn⟩ cs n' = n + 1
@[simp]
theorem parser.foldr_core_zero_eq_done {α β : Type} {cb : char_buffer} {n n' : } {b : β} {f : α → β → β} {p : parser α} {b' : β} :
theorem parser.foldr_core_eq_done {α β : Type} {cb : char_buffer} {n n' : } {b : β} {f : α → β → β} {p : parser α} {reps : } {b' : β} :
parser.foldr_core f p b (reps + 1) cb n = parse_result.done n' b' (∃ (np : ) (a : α) (xs : β), p cb n = parse_result.done np a parser.foldr_core f p b reps cb np = parse_result.done n' xs f a xs = b') n = n' b = b' ∃ (err : dlist string), p cb n = parse_result.fail n err ∃ (np : ) (a : α), p cb n = parse_result.done np a parser.foldr_core f p b reps cb np = parse_result.fail n err
@[simp]
theorem parser.foldr_core_zero_eq_fail {α β : Type} {cb : char_buffer} {n n' : } {b : β} {f : α → β → β} {p : parser α} {err : dlist string} :
parser.foldr_core f p b 0 cb n = parse_result.fail n' err n = n' err = dlist.empty
theorem parser.foldr_core_succ_eq_fail {α β : Type} {cb : char_buffer} {n n' : } {b : β} {f : α → β → β} {p : parser α} {reps : } {err : dlist string} :
parser.foldr_core f p b (reps + 1) cb n = parse_result.fail n' err n n' (p cb n = parse_result.fail n' err ∃ (np : ) (a : α), p cb n = parse_result.done np a parser.foldr_core f p b reps cb np = parse_result.fail n' err)
theorem parser.foldr_eq_done {α β : Type} {cb : char_buffer} {n n' : } {b : β} {f : α → β → β} {p : parser α} {b' : β} :
parser.foldr f p b cb n = parse_result.done n' b' (∃ (np : ) (a : α) (x : β), p cb n = parse_result.done np a parser.foldr_core f p b (buffer.size cb - n) cb np = parse_result.done n' x f a x = b') n = n' b = b' ∃ (err : dlist string), p cb n = parse_result.fail n err ∃ (np : ) (x : α), p cb n = parse_result.done np x parser.foldr_core f p b (buffer.size cb - n) cb np = parse_result.fail n err
theorem parser.foldr_eq_fail_iff_mono_at_end {α β : Type} {cb : char_buffer} {n n' : } {b : β} {f : α → β → β} {p : parser α} {err : dlist string} [p.mono] (hc : buffer.size cb n) :
parser.foldr f p b cb n = parse_result.fail n' err n < n' (p cb n = parse_result.fail n' err ∃ (a : α), p cb n = parse_result.done n' a err = dlist.empty)
theorem parser.foldr_eq_fail {α β : Type} {cb : char_buffer} {n n' : } {b : β} {f : α → β → β} {p : parser α} {err : dlist string} :
parser.foldr f p b cb n = parse_result.fail n' err n n' (p cb n = parse_result.fail n' err ∃ (np : ) (a : α), p cb n = parse_result.done np a parser.foldr_core f p b (buffer.size cb - n) cb np = parse_result.fail n' err)
@[simp]
theorem parser.foldl_core_zero_eq_done {α β : Type} {cb : char_buffer} {n n' : } {b : β} {f : β → α → β} {p : parser α} {b' : β} :
theorem parser.foldl_core_eq_done {α β : Type} {cb : char_buffer} {n n' : } {b : β} {f : β → α → β} {p : parser α} {reps : } {b' : β} :
parser.foldl_core f b p (reps + 1) cb n = parse_result.done n' b' (∃ (np : ) (a : α), p cb n = parse_result.done np a parser.foldl_core f (f b a) p reps cb np = parse_result.done n' b') n = n' b = b' ∃ (err : dlist string), p cb n = parse_result.fail n err ∃ (np : ) (a : α), p cb n = parse_result.done np a parser.foldl_core f (f b a) p reps cb np = parse_result.fail n err
@[simp]
theorem parser.foldl_core_zero_eq_fail {α β : Type} {cb : char_buffer} {n n' : } {b : β} {f : β → α → β} {p : parser α} {err : dlist string} :
parser.foldl_core f b p 0 cb n = parse_result.fail n' err n = n' err = dlist.empty
theorem parser.foldl_core_succ_eq_fail {α β : Type} {cb : char_buffer} {n n' : } {b : β} {f : β → α → β} {p : parser α} {reps : } {err : dlist string} :
parser.foldl_core f b p (reps + 1) cb n = parse_result.fail n' err n n' (p cb n = parse_result.fail n' err ∃ (np : ) (a : α), p cb n = parse_result.done np a parser.foldl_core f (f b a) p reps cb np = parse_result.fail n' err)
theorem parser.foldl_eq_done {α β : Type} {cb : char_buffer} {n n' : } {b : β} {f : β → α → β} {p : parser α} {b' : β} :
parser.foldl f b p cb n = parse_result.done n' b' (∃ (np : ) (a : α), p cb n = parse_result.done np a parser.foldl_core f (f b a) p (buffer.size cb - n) cb np = parse_result.done n' b') n = n' b = b' ∃ (err : dlist string), p cb n = parse_result.fail n err ∃ (np : ) (a : α), p cb n = parse_result.done np a parser.foldl_core f (f b a) p (buffer.size cb - n) cb np = parse_result.fail n err
theorem parser.foldl_eq_fail {α β : Type} {cb : char_buffer} {n n' : } {b : β} {f : β → α → β} {p : parser α} {err : dlist string} :
parser.foldl f b p cb n = parse_result.fail n' err n n' (p cb n = parse_result.fail n' err ∃ (np : ) (a : α), p cb n = parse_result.done np a parser.foldl_core f (f b a) p (buffer.size cb - n) cb np = parse_result.fail n' err)
theorem parser.foldl_eq_fail_iff_mono_at_end {α β : Type} {cb : char_buffer} {n n' : } {b : β} {f : β → α → β} {p : parser α} {err : dlist string} [p.mono] (hc : buffer.size cb n) :
parser.foldl f b p cb n = parse_result.fail n' err n < n' (p cb n = parse_result.fail n' err ∃ (a : α), p cb n = parse_result.done n' a err = dlist.empty)
theorem parser.many_eq_done_nil {α : Type} {cb : char_buffer} {n n' : } {p : parser α} :
p.many cb n = parse_result.done n' list.nil n = n' ∃ (err : dlist string), p cb n = parse_result.fail n err ∃ (np : ) (a : α), p cb n = parse_result.done np a parser.foldr_core list.cons p list.nil (buffer.size cb - n) cb np = parse_result.fail n err
theorem parser.many_eq_done {α : Type} {cb : char_buffer} {n n' : } {p : parser α} {x : α} {xs : list α} :
p.many cb n = parse_result.done n' (x :: xs) ∃ (np : ), p cb n = parse_result.done np x parser.foldr_core list.cons p list.nil (buffer.size cb - n) cb np = parse_result.done n' xs
theorem parser.many_eq_fail {α : Type} {cb : char_buffer} {n n' : } {p : parser α} {err : dlist string} :
p.many cb n = parse_result.fail n' err n n' (p cb n = parse_result.fail n' err ∃ (np : ) (a : α), p cb n = parse_result.done np a parser.foldr_core list.cons p list.nil (buffer.size cb - n) cb np = parse_result.fail n' err)
theorem parser.many_char_eq_done_empty {cb : char_buffer} {n n' : } {p : parser char} :
p.many_char cb n = parse_result.done n' "" n = n' ∃ (err : dlist string), p cb n = parse_result.fail n err ∃ (np : ) (c : char), p cb n = parse_result.done np c parser.foldr_core list.cons p list.nil (buffer.size cb - n) cb np = parse_result.fail n err
theorem parser.many'_eq_done {α : Type} {cb : char_buffer} {n n' : } {p : parser α} :
p.many' cb n = parse_result.done n' () p.many cb n = parse_result.done n' list.nil ∃ (np : ) (a : α) (l : list α), p.many cb n = parse_result.done n' (a :: l) p cb n = parse_result.done np a parser.foldr_core list.cons p list.nil (buffer.size cb - n) cb np = parse_result.done n' l
@[simp]
theorem parser.many1_ne_done_nil {α : Type} {cb : char_buffer} {n n' : } {p : parser α} :
theorem parser.many1_eq_done {α : Type} {cb : char_buffer} {n n' : } {a : α} {p : parser α} {l : list α} :
p.many1 cb n = parse_result.done n' (a :: l) ∃ (np : ), p cb n = parse_result.done np a p.many cb np = parse_result.done n' l
theorem parser.many1_eq_fail {α : Type} {cb : char_buffer} {n n' : } {p : parser α} {err : dlist string} :
p.many1 cb n = parse_result.fail n' err p cb n = parse_result.fail n' err ∃ (np : ) (a : α), p cb n = parse_result.done np a p.many cb np = parse_result.fail n' err
@[simp]
theorem parser.many_char1_ne_empty {cb : char_buffer} {n n' : } {p : parser char} :
theorem parser.many_char1_eq_done {cb : char_buffer} {n n' : } {p : parser char} {s : string} (h : s "") :
p.many_char1 cb n = parse_result.done n' s ∃ (np : ), p cb n = parse_result.done np s.head p.many_char cb np = parse_result.done n' (s.popn 1)
@[simp]
theorem parser.sep_by1_ne_done_nil {α : Type} {cb : char_buffer} {n n' : } {sep : parser unit} {p : parser α} :
theorem parser.sep_by1_eq_done {α : Type} {cb : char_buffer} {n n' : } {a : α} {sep : parser unit} {p : parser α} {l : list α} :
sep.sep_by1 p cb n = parse_result.done n' (a :: l) ∃ (np : ), p cb n = parse_result.done np a (sep >> p).many cb np = parse_result.done n' l
theorem parser.sep_by_eq_done_nil {α : Type} {cb : char_buffer} {n n' : } {sep : parser unit} {p : parser α} :
sep.sep_by p cb n = parse_result.done n' list.nil n = n' ∃ (err : dlist string), sep.sep_by1 p cb n = parse_result.fail n err
@[simp]
theorem parser.fix_core_ne_done_zero {α : Type} {cb : char_buffer} {n n' : } {a : α} {F : parser αparser α} :
theorem parser.fix_core_eq_done {α : Type} {cb : char_buffer} {n n' : } {a : α} {F : parser αparser α} {max_depth : } :
parser.fix_core F (max_depth + 1) cb n = parse_result.done n' a F (parser.fix_core F max_depth) cb n = parse_result.done n' a
theorem parser.digit_eq_done {cb : char_buffer} {n n' : } (hn : n < buffer.size cb) {k : } :
parser.digit cb n = parse_result.done n' k n' = n + 1 k 9 (buffer.read cb n, hn⟩).to_nat - '0'.to_nat = k '0' buffer.read cb n, hn⟩ buffer.read cb n, hn⟩ '9'