mathlib3 documentation

data.buffer.parser.basic

Parsers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

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

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

Equations
source
@[class]
structure parser.mono {α : Type} (p : parser α) :
Prop

A p : parser α is defined to be mono if the result p cb n it gives, for some cb : char_buffer and n : ℕ, (whether done or fail), is always at a parse_result.pos that is at least n. The mono property is used mainly for proper orelse behavior.

Instances of this typeclass
source
theorem parser.mono.le {α : Type} (p : parser α) (cb : char_buffer) (n : ℕ) [p.mono] :
n ≤ (p cb n).pos
source
@[class]
structure parser.static {α : Type} (p : parser α) :
Prop

A parser α is defined to be static if it does not move on success.

Instances of this typeclass
source
@[class]
structure parser.err_static {α : Type} (p : parser α) :
Prop

A parser α is defined to be err_static if it does not move on error.

Instances of this typeclass
source
@[class]
structure parser.step {α : Type} (p : parser α) :
Prop

A parser α is defined to be step if it always moves exactly one char forward on success.

Instances of this typeclass
source
@[class]
structure parser.prog {α : Type} (p : parser α) :
Prop

A parser α is defined to be prog if it always moves forward on success.

Instances of this typeclass
source
@[class]
structure parser.bounded {α : Type} (p : parser α) :
Prop

A parser a is defined to be bounded if it produces a fail parse_result when it is parsing outside the provided char_buffer.

Instances of this typeclass
source
theorem parser.bounded.exists {α : Type} (p : parser α) [p.bounded] {cb : char_buffer} {n : ℕ} (h : buffer.size cb ≤ n) :
∃ (n' : ℕ) (err : dlist string), p cb n = parse_result.fail n' err
source
@[class]
structure parser.unfailing {α : Type} (p : parser α) :
Prop

A parser a is defined to be unfailing if it always produces a done parse_result.

Instances of this typeclass
source
@[class]
structure parser.conditionally_unfailing {α : Type} (p : parser α) :
Prop

A parser a is defined to be conditionally_unfailing if it produces a done parse_result as long as it is parsing within the provided char_buffer.

Instances of this typeclass
source
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
source
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
source
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'
source
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'
source
theorem parser.bounded.of_done {α : Type} {p : parser α} {cb : char_buffer} {n n' : ℕ} {a : α} [p.bounded] (h : p cb n = parse_result.done n' a) :
n < buffer.size cb
source
theorem parser.static.iff {α : Type} {p : parser α} :
p.static ↔ ∀ (cb : char_buffer) (n n' : ℕ) (a : α), p cb n = parse_result.done n' a → n = n'
source
theorem parser.exists_done {α : Type} (p : parser α) [p.unfailing] (cb : char_buffer) (n : ℕ) :
∃ (n' : ℕ) (a : α), p cb n = parse_result.done n' a
source
theorem parser.unfailing.of_fail {α : Type} {p : parser α} {cb : char_buffer} {n n' : ℕ} {err : dlist string} [p.unfailing] (h : p cb n = parse_result.fail n' err) :
false
source
@[protected, instance]
def parser.conditionally_unfailing_of_unfailing {α : Type} {p : parser α} [p.unfailing] :
p.conditionally_unfailing
source
theorem parser.exists_done_in_bounds {α : Type} (p : parser α) [p.conditionally_unfailing] {cb : char_buffer} {n : ℕ} (h : n < buffer.size cb) :
∃ (n' : ℕ) (a : α), p cb n = parse_result.done n' a
source
theorem parser.conditionally_unfailing.of_fail {α : Type} {p : parser α} {cb : char_buffer} {n n' : ℕ} {err : dlist string} [p.conditionally_unfailing] (h : p cb n = parse_result.fail n' err) (hn : n < buffer.size cb) :
false
source
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) :
parser.decorate_errors msgs p cb n = parse_result.fail n (dlist.lazy_of_list (λ («_» : unit), msgs unit.star()))
source
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) :
parser.decorate_errors msgs p cb n = parse_result.done n' a
source
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 unit.star()]))
source
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) :
parser.decorate_error msg p cb n = parse_result.done n' a
source
@[simp]
theorem parser.decorate_errors_eq_done {α : Type} {msgs : thunk (list string)} {p : parser α} {cb : char_buffer} {n n' : ℕ} {a : α} :
parser.decorate_errors msgs p cb n = parse_result.done n' a ↔ p cb n = parse_result.done n' a
source
@[simp]
theorem parser.decorate_error_eq_done {α : Type} {msg : thunk string} {p : parser α} {cb : char_buffer} {n n' : ℕ} {a : α} :
parser.decorate_error msg p cb n = parse_result.done n' a ↔ p cb n = parse_result.done n' a
source
@[simp]
theorem parser.decorate_errors_eq_fail {α : Type} {msgs : thunk (list string)} {p : parser α} {cb : char_buffer} {n n' : ℕ} {err : dlist string} :
parser.decorate_errors msgs p cb n = parse_result.fail n' err ↔ n = n' ∧ err = dlist.lazy_of_list (λ («_» : unit), msgs unit.star()) ∧ ∃ (np : ℕ) (err' : dlist string), p cb n = parse_result.fail np err'
source
@[simp]
theorem parser.decorate_error_eq_fail {α : Type} {msg : thunk string} {p : parser α} {cb : char_buffer} {n n' : ℕ} {err : dlist string} :
parser.decorate_error msg p cb n = parse_result.fail n' err ↔ n = n' ∧ err = dlist.lazy_of_list (λ («_» : unit), [msg unit.star()]) ∧ ∃ (np : ℕ) (err' : dlist string), p cb n = parse_result.fail np err'
source
@[simp]
theorem parser.return_eq_pure {α : Type} {a : α} :
return a = has_pure.pure a
source
theorem parser.pure_eq_done {α : Type} {a : α} :
has_pure.pure a = λ (_x : char_buffer) (n : ℕ), parse_result.done n a
source
@[simp]
theorem parser.pure_ne_fail {α : Type} {cb : char_buffer} {n n' : ℕ} {err : dlist string} {a : α} :
has_pure.pure a cb n ≠ parse_result.fail n' err
source
@[simp]
theorem parser.bind_eq_bind {α β : Type} {p : parser α} (f : α → parser β) :
p.bind f = p >>= f
source
@[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
source
@[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
source
@[simp]
theorem parser.and_then_eq_bind {α β : Type} {m : Type → Type} [monad m] (a : m α) (b : m β) :
a >> b = a >>= λ (_x : α), b
source
theorem parser.and_then_fail {α : Type} {p : parser α} {cb : char_buffer} {n n' : ℕ} {err : dlist string} :
(p >> return unit.star()) cb n = parse_result.fail n' err ↔ p cb n = parse_result.fail n' err
source
theorem parser.and_then_success {α : Type} {p : parser α} {cb : char_buffer} {n n' : ℕ} :
(p >> return unit.star()) cb n = parse_result.done n' unit.star() ↔ ∃ (a : α), p cb n = parse_result.done n' a
source
@[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
source
@[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
source
@[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'
source
@[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
source
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'
source
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
source
@[simp]
theorem parser.orelse_eq_orelse {α : Type} {p q : parser α} :
p.orelse q = (p <|> q)
source
@[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
source
@[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
source
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
source
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
source
@[simp]
theorem parser.failure_eq_failure {α : Type} :
parser.failure = failure
source
@[simp]
theorem parser.failure_def {α : Type} {cb : char_buffer} {n : ℕ} :
failure cb n = parse_result.fail n dlist.empty
source
theorem parser.not_failure_eq_done {α : Type} {cb : char_buffer} {n n' : ℕ} {a : α} :
¬failure cb n = parse_result.done n' a
source
theorem parser.failure_eq_fail {α : Type} {cb : char_buffer} {n n' : ℕ} {err : dlist string} :
failure cb n = parse_result.fail n' err ↔ n = n' ∧ err = dlist.empty
source
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
source
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
source
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
source
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
source
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
source
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
source
theorem parser.mmap_eq_done {α β : Type} {cb : char_buffer} {n n' : ℕ} {f : α → parser β} {a : α} {l : list α} {b : β} {l' : list β} :
list.mmap f (a :: l) cb n = parse_result.done n' (b :: l') ↔ ∃ (np : ℕ), f a cb n = parse_result.done np b ∧ list.mmap f l cb np = parse_result.done n' l'
source
theorem parser.mmap'_eq_done {α β : Type} {cb : char_buffer} {n n' : ℕ} {f : α → parser β} {a : α} {l : list α} :
list.mmap' f (a :: l) cb n = parse_result.done n' unit.star() ↔ ∃ (np : ℕ) (b : β), f a cb n = parse_result.done np b ∧ list.mmap' f l cb np = parse_result.done n' unit.star()
source
theorem parser.guard_eq_done {cb : char_buffer} {n n' : ℕ} {p : Prop} [decidable p] {u : unit} :
guard p cb n = parse_result.done n' u ↔ p ∧ n = n'
source
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
source
@[protected, instance]
def parser.mono.pure {α : Type} {a : α} :
(has_pure.pure a).mono
source
@[protected, instance]
def parser.mono.bind {α β : Type} {p : parser α} {f : α → parser β} [p.mono] [∀ (a : α), (f a).mono] :
(p >>= f).mono
source
@[protected, instance]
def parser.mono.and_then {α β : Type} {p : parser α} {q : parser β} [p.mono] [q.mono] :
(p >> q).mono
source
@[protected, instance]
def parser.mono.map {α β : Type} {p : parser α} [p.mono] {f : α → β} :
parser.mono (f <$> p)
source
@[protected, instance]
def parser.mono.seq {α β : Type} {p : parser α} {f : parser (α → β)} [f.mono] [p.mono] :
(f <*> p).mono
source
@[protected, instance]
def parser.mono.mmap {α β : Type} {l : list α} {f : α → parser β} [∀ (a : α), a ∈ l → (f a).mono] :
(list.mmap f l).mono
source
@[protected, instance]
def parser.mono.mmap' {α β : Type} {l : list α} {f : α → parser β} [∀ (a : α), a ∈ l → (f a).mono] :
(list.mmap' f l).mono
source
@[protected, instance]
def parser.mono.failure {α : Type} :
failure.mono
source
@[protected, instance]
def parser.mono.guard {p : Prop} [decidable p] :
(guard p).mono
source
@[protected, instance]
def parser.mono.orelse {α : Type} {p q : parser α} [p.mono] [q.mono] :
(p <|> q).mono
source
@[protected, instance]
def parser.mono.decorate_errors {α : Type} {msgs : thunk (list string)} {p : parser α} [p.mono] :
(parser.decorate_errors msgs p).mono
source
@[protected, instance]
def parser.mono.decorate_error {α : Type} {msg : thunk string} {p : parser α} [p.mono] :
(parser.decorate_error msg p).mono
source
@[protected, instance]
def parser.mono.any_char  :
parser.any_char.mono
source
@[protected, instance]
def parser.mono.sat {p : char → Prop} [decidable_pred p] :
(parser.sat p).mono
source
@[protected, instance]
def parser.mono.eps  :
parser.eps.mono
source
@[protected, instance]
def parser.mono.ch {c : char} :
(parser.ch c).mono
source
@[protected, instance]
def parser.mono.char_buf {s : char_buffer} :
(parser.char_buf s).mono
source
@[protected, instance]
def parser.mono.one_of {cs : list char} :
(parser.one_of cs).mono
source
@[protected, instance]
def parser.mono.one_of' {cs : list char} :
(parser.one_of' cs).mono
source
@[protected, instance]
def parser.mono.str {s : string} :
(parser.str s).mono
source
@[protected, instance]
def parser.mono.remaining  :
parser.remaining.mono
source
@[protected, instance]
def parser.mono.eof  :
parser.eof.mono
source
@[protected, instance]
def parser.mono.foldr_core {α β : Type} {p : parser α} {f : α → β → β} {b : β} [p.mono] {reps : ℕ} :
(parser.foldr_core f p b reps).mono
source
@[protected, instance]
def parser.mono.foldr {α β : Type} {p : parser α} {b : β} {f : α → β → β} [p.mono] :
(parser.foldr f p b).mono
source
@[protected, instance]
def parser.mono.foldl_core {α β : Type} {f : α → β → α} {p : parser β} [p.mono] {a : α} {reps : ℕ} :
(parser.foldl_core f a p reps).mono
source
@[protected, instance]
def parser.mono.foldl {α β : Type} {a : α} {f : α → β → α} {p : parser β} [p.mono] :
(parser.foldl f a p).mono
source
@[protected, instance]
def parser.mono.many {α : Type} {p : parser α} [p.mono] :
p.many.mono
source
@[protected, instance]
def parser.mono.many_char {p : parser char} [p.mono] :
p.many_char.mono
source
@[protected, instance]
def parser.mono.many' {α : Type} {p : parser α} [p.mono] :
p.many'.mono
source
@[protected, instance]
def parser.mono.many1 {α : Type} {p : parser α} [p.mono] :
p.many1.mono
source
@[protected, instance]
def parser.mono.many_char1 {p : parser char} [p.mono] :
p.many_char1.mono
source
@[protected, instance]
def parser.mono.sep_by1 {α : Type} {p : parser α} {sep : parser unit} [p.mono] [sep.mono] :
(sep.sep_by1 p).mono
source
@[protected, instance]
def parser.mono.sep_by {α : Type} {p : parser α} {sep : parser unit} [p.mono] [hs : sep.mono] :
(sep.sep_by p).mono
source
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
source
@[protected, instance]
def parser.mono.digit  :
parser.digit.mono
source
@[protected, instance]
def parser.mono.nat  :
parser.nat.mono
source
theorem parser.mono.fix {α : Type} {F : parser α → parser α} (hF : ∀ (p : parser α), p.mono → (F p).mono) :
(parser.fix F).mono
source
@[simp]
theorem parser.orelse_pure_eq_fail {α : Type} {p : parser α} {cb : char_buffer} {n n' : ℕ} {err : dlist string} {a : α} :
(p <|> has_pure.pure a) cb n = parse_result.fail n' err ↔ p cb n = parse_result.fail n' err ∧ n ≠ n'
source
theorem parser.any_char_eq_done {cb : char_buffer} {n n' : ℕ} {c : char} :
parser.any_char cb n = parse_result.done n' c ↔ ∃ (hn : n < buffer.size cb), n' = n + 1 ∧ buffer.read cb ⟨n, hn⟩ = c
source
theorem parser.any_char_eq_fail {cb : char_buffer} {n n' : ℕ} {err : dlist string} :
parser.any_char cb n = parse_result.fail n' err ↔ n = n' ∧ err = dlist.empty ∧ buffer.size cb ≤ n
source
theorem parser.sat_eq_done {cb : char_buffer} {n n' : ℕ} {c : char} {p : char → Prop} [decidable_pred p] :
parser.sat p cb n = parse_result.done n' c ↔ ∃ (hn : n < buffer.size cb), p c ∧ n' = n + 1 ∧ buffer.read cb ⟨n, hn⟩ = c
source
theorem parser.sat_eq_fail {cb : char_buffer} {n n' : ℕ} {err : dlist string} {p : char → Prop} [decidable_pred p] :
parser.sat p cb n = parse_result.fail n' err ↔ n = n' ∧ err = dlist.empty ∧ ∀ (h : n < buffer.size cb), ¬p (buffer.read cb ⟨n, h⟩)
source
theorem parser.eps_eq_done {cb : char_buffer} {n n' : ℕ} {u : unit} :
parser.eps cb n = parse_result.done n' u ↔ n = n'
source
theorem parser.ch_eq_done {cb : char_buffer} {n n' : ℕ} {c : char} {u : unit} :
parser.ch c cb n = parse_result.done n' u ↔ ∃ (hn : n < buffer.size cb), n' = n + 1 ∧ buffer.read cb ⟨n, hn⟩ = c
source
theorem parser.char_buf_eq_done {cb : char_buffer} {n n' : ℕ} {u : unit} {cb' : char_buffer} :
parser.char_buf cb' cb n = parse_result.done n' u ↔ n + buffer.size cb' = n' ∧ buffer.to_list cb' <+: list.drop n (buffer.to_list cb)
source
theorem parser.one_of_eq_done {cb : char_buffer} {n n' : ℕ} {c : char} {cs : list char} :
parser.one_of cs cb n = parse_result.done n' c ↔ ∃ (hn : n < buffer.size cb), c ∈ cs ∧ n' = n + 1 ∧ buffer.read cb ⟨n, hn⟩ = c
source
theorem parser.one_of'_eq_done {cb : char_buffer} {n n' : ℕ} {u : unit} {cs : list char} :
parser.one_of' cs cb n = parse_result.done n' u ↔ ∃ (hn : n < buffer.size cb), buffer.read cb ⟨n, hn⟩ ∈ cs ∧ n' = n + 1
source
theorem parser.str_eq_char_buf (s : string) :
parser.str s = parser.char_buf s.to_list.to_buffer
source
theorem parser.str_eq_done {cb : char_buffer} {n n' : ℕ} {u : unit} {s : string} :
parser.str s cb n = parse_result.done n' u ↔ n + s.length = n' ∧ s.to_list <+: list.drop n (buffer.to_list cb)
source
theorem parser.remaining_eq_done {cb : char_buffer} {n n' r : ℕ} :
parser.remaining cb n = parse_result.done n' r ↔ n = n' ∧ buffer.size cb - n = r
source
theorem parser.remaining_ne_fail {cb : char_buffer} {n n' : ℕ} {err : dlist string} :
parser.remaining cb n ≠ parse_result.fail n' err
source
theorem parser.eof_eq_done {cb : char_buffer} {n n' : ℕ} {u : unit} :
parser.eof cb n = parse_result.done n' u ↔ n = n' ∧ buffer.size cb ≤ n
source
@[simp]
theorem parser.foldr_core_zero_eq_done {α β : Type} {cb : char_buffer} {n n' : ℕ} {b : β} {f : α → β → β} {p : parser α} {b' : β} :
parser.foldr_core f p b 0 cb n ≠ parse_result.done n' b'
source
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
source
@[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
source
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)
source
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
source
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)
source
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)
source
@[simp]
theorem parser.foldl_core_zero_eq_done {α β : Type} {cb : char_buffer} {n n' : ℕ} {b : β} {f : β → α → β} {p : parser α} {b' : β} :
parser.foldl_core f b p 0 cb n = parse_result.done n' b' ↔ false
source
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
source
@[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
source
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)
source
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
source
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)
source
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)
source
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
source
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
source
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)
source
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
source
theorem parser.many_char_eq_done_not_empty {cb : char_buffer} {n n' : ℕ} {p : parser char} {s : string} (h : s ≠ "") :
p.many_char cb n = parse_result.done n' s ↔ ∃ (np : ℕ), p cb n = parse_result.done np s.head ∧ parser.foldr_core list.cons p list.nil (buffer.size cb - n) cb np = parse_result.done n' (s.popn 1).to_list
source
theorem parser.many_char_eq_many_of_to_list {cb : char_buffer} {n n' : ℕ} {p : parser char} {s : string} :
p.many_char cb n = parse_result.done n' s ↔ p.many cb n = parse_result.done n' s.to_list
source
theorem parser.many'_eq_done {α : Type} {cb : char_buffer} {n n' : ℕ} {u : unit} {p : parser α} :
p.many' cb n = parse_result.done n' u ↔ 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
source
@[simp]
theorem parser.many1_ne_done_nil {α : Type} {cb : char_buffer} {n n' : ℕ} {p : parser α} :
p.many1 cb n ≠ parse_result.done n' list.nil
source
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
source
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
source
@[simp]
theorem parser.many_char1_ne_empty {cb : char_buffer} {n n' : ℕ} {p : parser char} :
p.many_char1 cb n ≠ parse_result.done n' ""
source
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)
source
@[simp]
theorem parser.sep_by1_ne_done_nil {α : Type} {cb : char_buffer} {n n' : ℕ} {sep : parser unit} {p : parser α} :
sep.sep_by1 p cb n ≠ parse_result.done n' list.nil
source
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
source
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
source
@[simp]
theorem parser.fix_core_ne_done_zero {α : Type} {cb : char_buffer} {n n' : ℕ} {a : α} {F : parser α → parser α} :
parser.fix_core F 0 cb n ≠ parse_result.done n' a
source
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
source
theorem parser.digit_eq_done {cb : char_buffer} {n n' k : ℕ} :
parser.digit cb n = parse_result.done n' k ↔ ∃ (hn : n < buffer.size cb), 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'
source
theorem parser.digit_eq_fail {cb : char_buffer} {n n' : ℕ} {err : dlist string} :
parser.digit cb n = parse_result.fail n' err ↔ n = n' ∧ err = dlist.of_list [""] ∧ ∀ (h : n < buffer.size cb), ¬(λ (c : char), '0' ≤ c ∧ c ≤ '9') (buffer.read cb ⟨n, h⟩)
source
theorem parser.static.not_of_ne {α : Type} {p : parser α} {cb : char_buffer} {n' n : ℕ} {a : α} (h : p cb n = parse_result.done n' a) (hne : n ≠ n') :
¬p.static
source
@[protected, instance]
def parser.static.pure {α : Type} {a : α} :
(has_pure.pure a).static
source
@[protected, instance]
def parser.static.bind {α β : Type} {p : parser α} {f : α → parser β} [p.static] [∀ (a : α), (f a).static] :
(p >>= f).static
source
@[protected, instance]
def parser.static.and_then {α β : Type} {p : parser α} {q : parser β} [p.static] [q.static] :
(p >> q).static
source
@[protected, instance]
def parser.static.map {α β : Type} {p : parser α} [p.static] {f : α → β} :
parser.static (f <$> p)
source
@[protected, instance]
def parser.static.seq {α β : Type} {p : parser α} {f : parser (α → β)} [f.static] [p.static] :
(f <*> p).static
source
@[protected, instance]
def parser.static.mmap {α β : Type} {l : list α} {f : α → parser β} [∀ (a : α), (f a).static] :
(list.mmap f l).static
source
@[protected, instance]
def parser.static.mmap' {α β : Type} {l : list α} {f : α → parser β} [∀ (a : α), (f a).static] :
(list.mmap' f l).static
source
@[protected, instance]
def parser.static.failure {α : Type} :
failure.static
source
@[protected, instance]
def parser.static.guard {p : Prop} [decidable p] :
(guard p).static
source
@[protected, instance]
def parser.static.orelse {α : Type} {p q : parser α} [p.static] [q.static] :
(p <|> q).static
source
@[protected, instance]
def parser.static.decorate_errors {α : Type} {p : parser α} {msgs : thunk (list string)} [p.static] :
(parser.decorate_errors msgs p).static
source
@[protected, instance]
def parser.static.decorate_error {α : Type} {p : parser α} {msg : thunk string} [p.static] :
(parser.decorate_error msg p).static
source
theorem parser.static.any_char  :
¬parser.any_char.static
source
theorem parser.static.sat_iff {p : char → Prop} [decidable_pred p] :
(parser.sat p).static ↔ ∀ (c : char), ¬p c
source
@[protected, instance]
def parser.static.sat  :
(parser.sat (λ (_x : char), false)).static
source
@[protected, instance]
def parser.static.eps  :
parser.eps.static
source
theorem parser.static.ch (c : char) :
¬(parser.ch c).static
source
theorem parser.static.char_buf_iff {cb' : char_buffer} :
(parser.char_buf cb').static ↔ cb' = buffer.nil
source
theorem parser.static.one_of_iff {cs : list char} :
(parser.one_of cs).static ↔ cs = list.nil
source
@[protected, instance]
def parser.static.one_of  :
(parser.one_of list.nil).static
source
theorem parser.static.one_of'_iff {cs : list char} :
(parser.one_of' cs).static ↔ cs = list.nil
source
@[protected, instance]
def parser.static.one_of'  :
(parser.one_of list.nil).static
source
theorem parser.static.str_iff {s : string} :
(parser.str s).static ↔ s = ""
source
@[protected, instance]
def parser.static.remaining  :
parser.remaining.static
source
@[protected, instance]
def parser.static.eof  :
parser.eof.static
source
@[protected, instance]
def parser.static.foldr_core {α β : Type} {p : parser α} {f : α → β → β} [p.static] {b : β} {reps : ℕ} :
(parser.foldr_core f p b reps).static
source
@[protected, instance]
def parser.static.foldr {α β : Type} {p : parser α} {b : β} {f : α → β → β} [p.static] :
(parser.foldr f p b).static
source
@[protected, instance]
def parser.static.foldl_core {α β : Type} {f : α → β → α} {p : parser β} [p.static] {a : α} {reps : ℕ} :
(parser.foldl_core f a p reps).static
source
@[protected, instance]
def parser.static.foldl {α β : Type} {a : α} {f : α → β → α} {p : parser β} [p.static] :
(parser.foldl f a p).static
source
@[protected, instance]
def parser.static.many {α : Type} {p : parser α} [p.static] :
p.many.static
source
@[protected, instance]
def parser.static.many_char {p : parser char} [p.static] :
p.many_char.static
source
@[protected, instance]
def parser.static.many' {α : Type} {p : parser α} [p.static] :
p.many'.static
source
@[protected, instance]
def parser.static.many1 {α : Type} {p : parser α} [p.static] :
p.many1.static
source
@[protected, instance]
def parser.static.many_char1 {p : parser char} [p.static] :
p.many_char1.static
source
@[protected, instance]
def parser.static.sep_by1 {α : Type} {p : parser α} {sep : parser unit} [p.static] [sep.static] :
(sep.sep_by1 p).static
source
@[protected, instance]
def parser.static.sep_by {α : Type} {p : parser α} {sep : parser unit} [p.static] [sep.static] :
(sep.sep_by p).static
source
theorem parser.static.fix_core {α : Type} {F : parser α → parser α} (hF : ∀ (p : parser α), p.static → (F p).static) (max_depth : ℕ) :
(parser.fix_core F max_depth).static
source
theorem parser.static.digit  :
¬parser.digit.static
source
theorem parser.static.nat  :
¬parser.nat.static
source
theorem parser.static.fix {α : Type} {F : parser α → parser α} (hF : ∀ (p : parser α), p.static → (F p).static) :
(parser.fix F).static
source
theorem parser.bounded.done_of_unbounded {α : Type} {p : parser α} (h : ¬p.bounded) :
∃ (cb : char_buffer) (n n' : ℕ) (a : α), p cb n = parse_result.done n' a ∧ buffer.size cb ≤ n
source
theorem parser.bounded.pure {α : Type} {a : α} :
¬(has_pure.pure a).bounded
source
@[protected, instance]
def parser.bounded.bind {α β : Type} {p : parser α} {f : α → parser β} [p.bounded] :
(p >>= f).bounded
source
@[protected, instance]
def parser.bounded.and_then {α β : Type} {p : parser α} {q : parser β} [p.bounded] :
(p >> q).bounded
source
@[protected, instance]
def parser.bounded.map {α β : Type} {p : parser α} [p.bounded] {f : α → β} :
parser.bounded (f <$> p)
source
@[protected, instance]
def parser.bounded.seq {α β : Type} {p : parser α} {f : parser (α → β)} [f.bounded] :
(f <*> p).bounded
source
@[protected, instance]
def parser.bounded.mmap {α β : Type} {a : α} {l : list α} {f : α → parser β} [∀ (a : α), (f a).bounded] :
(list.mmap f (a :: l)).bounded
source
@[protected, instance]
def parser.bounded.mmap' {α β : Type} {a : α} {l : list α} {f : α → parser β} [∀ (a : α), (f a).bounded] :
(list.mmap' f (a :: l)).bounded
source
@[protected, instance]
def parser.bounded.failure {α : Type} :
failure.bounded
source
theorem parser.bounded.guard_iff {p : Prop} [decidable p] :
(guard p).bounded ↔ ¬p
source
@[protected, instance]
def parser.bounded.orelse {α : Type} {p q : parser α} [p.bounded] [q.bounded] :
(p <|> q).bounded
source
@[protected, instance]
def parser.bounded.decorate_errors {α : Type} {msgs : thunk (list string)} {p : parser α} [p.bounded] :
(parser.decorate_errors msgs p).bounded
source
theorem parser.bounded.decorate_errors_iff {α : Type} {msgs : thunk (list string)} {p : parser α} :
(parser.decorate_errors msgs p).bounded ↔ p.bounded
source
@[protected, instance]
def parser.bounded.decorate_error {α : Type} {msg : thunk string} {p : parser α} [p.bounded] :
(parser.decorate_error msg p).bounded
source
theorem parser.bounded.decorate_error_iff {α : Type} {msg : thunk string} {p : parser α} :
(parser.decorate_error msg p).bounded ↔ p.bounded
source
@[protected, instance]
def parser.bounded.any_char  :
parser.any_char.bounded
source
@[protected, instance]
def parser.bounded.sat {p : char → Prop} [decidable_pred p] :
(parser.sat p).bounded
source
theorem parser.bounded.eps  :
¬parser.eps.bounded
source
@[protected, instance]
def parser.bounded.ch {c : char} :
(parser.ch c).bounded
source
theorem parser.bounded.char_buf_iff {cb' : char_buffer} :
(parser.char_buf cb').bounded ↔ cb' ≠ buffer.nil
source
@[protected, instance]
def parser.bounded.one_of {cs : list char} :
(parser.one_of cs).bounded
source
@[protected, instance]
def parser.bounded.one_of' {cs : list char} :
(parser.one_of' cs).bounded
source
theorem parser.bounded.str_iff {s : string} :
(parser.str s).bounded ↔ s ≠ ""
source
theorem parser.bounded.remaining  :
¬parser.remaining.bounded
source
theorem parser.bounded.eof  :
¬parser.eof.bounded
source
@[protected, instance]
def parser.bounded.foldr_core_zero {α β : Type} {p : parser α} {b : β} {f : α → β → β} :
(parser.foldr_core f p b 0).bounded
source
@[protected, instance]
def parser.bounded.foldl_core_zero {α β : Type} {p : parser α} {f : β → α → β} {b : β} :
(parser.foldl_core f b p 0).bounded
source
theorem parser.bounded.foldr_core {α β : Type} {p : parser α} {b : β} {reps : ℕ} [hpb : p.bounded] (he : ∀ (cb : char_buffer) (n n' : ℕ) (err : dlist string), p cb n = parse_result.fail n' err → n ≠ n') {f : α → β → β} :
(parser.foldr_core f p b reps).bounded
source
theorem parser.bounded.foldr {α β : Type} {p : parser α} {b : β} [hpb : p.bounded] (he : ∀ (cb : char_buffer) (n n' : ℕ) (err : dlist string), p cb n = parse_result.fail n' err → n ≠ n') {f : α → β → β} :
(parser.foldr f p b).bounded
source
theorem parser.bounded.foldl_core {α β : Type} {p : parser α} {b : β} {reps : ℕ} [hpb : p.bounded] (he : ∀ (cb : char_buffer) (n n' : ℕ) (err : dlist string), p cb n = parse_result.fail n' err → n ≠ n') {f : β → α → β} :
(parser.foldl_core f b p reps).bounded
source
theorem parser.bounded.foldl {α β : Type} {p : parser α} {b : β} [hpb : p.bounded] (he : ∀ (cb : char_buffer) (n n' : ℕ) (err : dlist string), p cb n = parse_result.fail n' err → n ≠ n') {f : β → α → β} :
(parser.foldl f b p).bounded
source
theorem parser.bounded.many {α : Type} {p : parser α} [hpb : p.bounded] (he : ∀ (cb : char_buffer) (n n' : ℕ) (err : dlist string), p cb n = parse_result.fail n' err → n ≠ n') :
p.many.bounded
source
theorem parser.bounded.many_char {pc : parser char} [pc.bounded] (he : ∀ (cb : char_buffer) (n n' : ℕ) (err : dlist string), pc cb n = parse_result.fail n' err → n ≠ n') :
pc.many_char.bounded
source
theorem parser.bounded.many' {α : Type} {p : parser α} [hpb : p.bounded] (he : ∀ (cb : char_buffer) (n n' : ℕ) (err : dlist string), p cb n = parse_result.fail n' err → n ≠ n') :
p.many'.bounded
source
@[protected, instance]
def parser.bounded.many1 {α : Type} {p : parser α} [p.bounded] :
p.many1.bounded
source
@[protected, instance]
def parser.bounded.many_char1 {p : parser char} [p.bounded] :
p.many_char1.bounded
source
@[protected, instance]
def parser.bounded.sep_by1 {α : Type} {p : parser α} {sep : parser unit} [p.bounded] :
(sep.sep_by1 p).bounded
source
theorem parser.bounded.fix_core {α : Type} {F : parser α → parser α} (hF : ∀ (p : parser α), p.bounded → (F p).bounded) (max_depth : ℕ) :
(parser.fix_core F max_depth).bounded
source
@[protected, instance]
def parser.bounded.digit  :
parser.digit.bounded
source
@[protected, instance]
def parser.bounded.nat  :
parser.nat.bounded
source
theorem parser.bounded.fix {α : Type} {F : parser α → parser α} (hF : ∀ (p : parser α), p.bounded → (F p).bounded) :
(parser.fix F).bounded
source
theorem parser.unfailing.of_bounded {α : Type} {p : parser α} [p.bounded] :
¬p.unfailing
source
@[protected, instance]
def parser.unfailing.pure {α : Type} {a : α} :
(has_pure.pure a).unfailing
source
@[protected, instance]
def parser.unfailing.bind {α β : Type} {p : parser α} {f : α → parser β} [p.unfailing] [∀ (a : α), (f a).unfailing] :
(p >>= f).unfailing
source
@[protected, instance]
def parser.unfailing.and_then {α β : Type} {p : parser α} {q : parser β} [p.unfailing] [q.unfailing] :
(p >> q).unfailing
source
@[protected, instance]
def parser.unfailing.map {α β : Type} {p : parser α} [p.unfailing] {f : α → β} :
parser.unfailing (f <$> p)
source
@[protected, instance]
def parser.unfailing.seq {α β : Type} {p : parser α} {f : parser (α → β)} [f.unfailing] [p.unfailing] :
(f <*> p).unfailing
source
@[protected, instance]
def parser.unfailing.mmap {α β : Type} {l : list α} {f : α → parser β} [∀ (a : α), (f a).unfailing] :
(list.mmap f l).unfailing
source
@[protected, instance]
def parser.unfailing.mmap' {α β : Type} {l : list α} {f : α → parser β} [∀ (a : α), (f a).unfailing] :
(list.mmap' f l).unfailing
source
theorem parser.unfailing.failure {α : Type} :
¬failure.unfailing
source
@[protected, instance]
def parser.unfailing.guard_true  :
(guard true).unfailing
source
theorem parser.unfailing.guard  :
¬(guard false).unfailing
source
@[protected, instance]
def parser.unfailing.orelse {α : Type} {p q : parser α} [p.unfailing] :
(p <|> q).unfailing
source
@[protected, instance]
def parser.unfailing.decorate_errors {α : Type} {p : parser α} {msgs : thunk (list string)} [p.unfailing] :
(parser.decorate_errors msgs p).unfailing
source
@[protected, instance]
def parser.unfailing.decorate_error {α : Type} {p : parser α} {msg : thunk string} [p.unfailing] :
(parser.decorate_error msg p).unfailing
source
@[protected, instance]
def parser.unfailing.any_char  :
parser.any_char.conditionally_unfailing
source
theorem parser.unfailing.sat  :
(parser.sat (λ (_x : char), true)).conditionally_unfailing
source
@[protected, instance]
def parser.unfailing.eps  :
parser.eps.unfailing
source
@[protected, instance]
def parser.unfailing.remaining  :
parser.remaining.unfailing
source
theorem parser.unfailing.foldr_core_zero {α β : Type} {p : parser α} {f : α → β → β} {b : β} :
¬(parser.foldr_core f p b 0).unfailing
source
@[protected, instance]
def parser.unfailing.foldr_core_of_static {α β : Type} {p : parser α} {f : α → β → β} {b : β} {reps : ℕ} [p.static] [p.unfailing] :
(parser.foldr_core f p b (reps + 1)).unfailing
source
@[protected, instance]
def parser.unfailing.foldr_core_one_of_err_static {α β : Type} {p : parser α} {f : α → β → β} {b : β} [p.static] [p.err_static] :
(parser.foldr_core f p b 1).unfailing
source
theorem parser.unfailing.digit  :
¬parser.digit.unfailing
source
theorem parser.unfailing.nat  :
¬parser.nat.unfailing
source
theorem parser.err_static.not_of_ne {α : Type} {p : parser α} {cb : char_buffer} {n' n : ℕ} {err : dlist string} (h : p cb n = parse_result.fail n' err) (hne : n ≠ n') :
¬p.err_static
source
@[protected, instance]
def parser.err_static.pure {α : Type} {a : α} :
(has_pure.pure a).err_static
source
@[protected, instance]
def parser.err_static.bind {α β : Type} {p : parser α} {f : α → parser β} [p.static] [p.err_static] [∀ (a : α), (f a).err_static] :
(p >>= f).err_static
source
@[protected, instance]
def parser.err_static.bind_of_unfailing {α β : Type} {p : parser α} {f : α → parser β} [p.err_static] [∀ (a : α), (f a).unfailing] :
(p >>= f).err_static
source
@[protected, instance]
def parser.err_static.and_then {α β : Type} {p : parser α} {q : parser β} [p.static] [p.err_static] [q.err_static] :
(p >> q).err_static
source
@[protected, instance]
def parser.err_static.and_then_of_unfailing {α β : Type} {p : parser α} {q : parser β} [p.err_static] [q.unfailing] :
(p >> q).err_static
source
@[protected, instance]
def parser.err_static.map {α β : Type} {p : parser α} [p.err_static] {f : α → β} :
parser.err_static (f <$> p)
source
@[protected, instance]
def parser.err_static.seq {α β : Type} {p : parser α} {f : parser (α → β)} [f.static] [f.err_static] [p.err_static] :
(f <*> p).err_static
source
@[protected, instance]
def parser.err_static.seq_of_unfailing {α β : Type} {p : parser α} {f : parser (α → β)} [f.err_static] [p.unfailing] :
(f <*> p).err_static
source
@[protected, instance]
def parser.err_static.mmap {α β : Type} {l : list α} {f : α → parser β} [∀ (a : α), (f a).static] [∀ (a : α), (f a).err_static] :
(list.mmap f l).err_static
source
@[protected, instance]
def parser.err_static.mmap_of_unfailing {α β : Type} {l : list α} {f : α → parser β} [∀ (a : α), (f a).unfailing] [∀ (a : α), (f a).err_static] :
(list.mmap f l).err_static
source
@[protected, instance]
def parser.err_static.mmap' {α β : Type} {l : list α} {f : α → parser β} [∀ (a : α), (f a).static] [∀ (a : α), (f a).err_static] :
(list.mmap' f l).err_static
source
@[protected, instance]
def parser.err_static.mmap'_of_unfailing {α β : Type} {l : list α} {f : α → parser β} [∀ (a : α), (f a).unfailing] [∀ (a : α), (f a).err_static] :
(list.mmap' f l).err_static
source
@[protected, instance]
def parser.err_static.failure {α : Type} :
failure.err_static
source
@[protected, instance]
def parser.err_static.guard {p : Prop} [decidable p] :
(guard p).err_static
source
@[protected, instance]
def parser.err_static.orelse {α : Type} {p q : parser α} [p.err_static] [q.mono] :
(p <|> q).err_static
source
@[protected, instance]
def parser.err_static.decorate_errors {α : Type} {p : parser α} {msgs : thunk (list string)} :
(parser.decorate_errors msgs p).err_static
source
@[protected, instance]
def parser.err_static.decorate_error {α : Type} {p : parser α} {msg : thunk string} :
(parser.decorate_error msg p).err_static
source
@[protected, instance]
def parser.err_static.any_char  :
parser.any_char.err_static
source
@[protected, instance]
def parser.err_static.sat_iff {p : char → Prop} [decidable_pred p] :
(parser.sat p).err_static
source
@[protected, instance]
def parser.err_static.eps  :
parser.eps.err_static
source
@[protected, instance]
def parser.err_static.ch (c : char) :
(parser.ch c).err_static
source
@[protected, instance]
def parser.err_static.char_buf {cb' : char_buffer} :
(parser.char_buf cb').err_static
source
@[protected, instance]
def parser.err_static.one_of {cs : list char} :
(parser.one_of cs).err_static
source
@[protected, instance]
def parser.err_static.one_of' {cs : list char} :
(parser.one_of' cs).err_static
source
@[protected, instance]
def parser.err_static.str {s : string} :
(parser.str s).err_static
source
@[protected, instance]
def parser.err_static.remaining  :
parser.remaining.err_static
source
@[protected, instance]
def parser.err_static.eof  :
parser.eof.err_static
source
theorem parser.err_static.fix_core {α : Type} {F : parser α → parser α} (hF : ∀ (p : parser α), p.err_static → (F p).err_static) (max_depth : ℕ) :
(parser.fix_core F max_depth).err_static
source
@[protected, instance]
def parser.err_static.digit  :
parser.digit.err_static
source
@[protected, instance]
def parser.err_static.nat  :
parser.nat.err_static
source
theorem parser.err_static.fix {α : Type} {F : parser α → parser α} (hF : ∀ (p : parser α), p.err_static → (F p).err_static) :
(parser.fix F).err_static
source
theorem parser.step.not_step_of_static_done {α : Type} {p : parser α} [p.static] (h : ∃ (cb : char_buffer) (n n' : ℕ) (a : α), p cb n = parse_result.done n' a) :
¬p.step
source
theorem parser.step.pure {α : Type} (a : α) :
¬(has_pure.pure a).step
source
@[protected, instance]
def parser.step.bind {α β : Type} {p : parser α} {f : α → parser β} [p.step] [∀ (a : α), (f a).static] :
(p >>= f).step
source
@[protected, instance]
def parser.step.bind' {α β : Type} {p : parser α} {f : α → parser β} [p.static] [∀ (a : α), (f a).step] :
(p >>= f).step
source
@[protected, instance]
def parser.step.and_then {α β : Type} {p : parser α} {q : parser β} [p.step] [q.static] :
(p >> q).step
source
@[protected, instance]
def parser.step.and_then' {α β : Type} {p : parser α} {q : parser β} [p.static] [q.step] :
(p >> q).step
source
@[protected, instance]
def parser.step.map {α β : Type} {p : parser α} [p.step] {f : α → β} :
parser.step (f <$> p)
source
@[protected, instance]
def parser.step.seq {α β : Type} {p : parser α} {f : parser (α → β)} [f.step] [p.static] :
(f <*> p).step
source
@[protected, instance]
def parser.step.seq' {α β : Type} {p : parser α} {f : parser (α → β)} [f.static] [p.step] :
(f <*> p).step
source
@[protected, instance]
def parser.step.mmap {α β : Type} {a : α} {f : α → parser β} [(f a).step] :
(list.mmap f [a]).step
source
@[protected, instance]
def parser.step.mmap' {α β : Type} {a : α} {f : α → parser β} [(f a).step] :
(list.mmap' f [a]).step
source
@[protected, instance]
def parser.step.failure {α : Type} :
failure.step
source
theorem parser.step.guard_true  :
¬(guard true).step
source
@[protected, instance]
def parser.step.guard  :
(guard false).step
source
@[protected, instance]
def parser.step.orelse {α : Type} {p q : parser α} [p.step] [q.step] :
(p <|> q).step
source
theorem parser.step.decorate_errors_iff {α : Type} {p : parser α} {msgs : thunk (list string)} :
(parser.decorate_errors msgs p).step ↔ p.step
source
@[protected, instance]
def parser.step.decorate_errors {α : Type} {p : parser α} {msgs : thunk (list string)} [p.step] :
(parser.decorate_errors msgs p).step
source
theorem parser.step.decorate_error_iff {α : Type} {p : parser α} {msg : thunk string} :
(parser.decorate_error msg p).step ↔ p.step
source
@[protected, instance]
def parser.step.decorate_error {α : Type} {p : parser α} {msg : thunk string} [p.step] :
(parser.decorate_error msg p).step
source
@[protected, instance]
def parser.step.any_char  :
parser.any_char.step
source
@[protected, instance]
def parser.step.sat {p : char → Prop} [decidable_pred p] :
(parser.sat p).step
source
theorem parser.step.eps  :
¬parser.eps.step
source
@[protected, instance]
def parser.step.ch {c : char} :
(parser.ch c).step
source
theorem parser.step.char_buf_iff {cb' : char_buffer} :
(parser.char_buf cb').step ↔ buffer.size cb' = 1
source
@[protected, instance]
def parser.step.one_of {cs : list char} :
(parser.one_of cs).step
source
@[protected, instance]
def parser.step.one_of' {cs : list char} :
(parser.one_of' cs).step
source
theorem parser.step.str_iff {s : string} :
(parser.str s).step ↔ s.length = 1
source
theorem parser.step.remaining  :
¬parser.remaining.step
source
theorem parser.step.eof  :
¬parser.eof.step
source
theorem parser.step.fix_core {α : Type} {F : parser α → parser α} (hF : ∀ (p : parser α), p.step → (F p).step) (max_depth : ℕ) :
(parser.fix_core F max_depth).step
source
@[protected, instance]
def parser.step.digit  :
parser.digit.step
source
theorem parser.step.fix {α : Type} {F : parser α → parser α} (hF : ∀ (p : parser α), p.step → (F p).step) :
(parser.fix F).step
source
theorem parser.many1_eq_done_iff_many_eq_done {α : Type} {p : parser α} {cb : char_buffer} {n' n : ℕ} [p.step] [p.bounded] {x : α} {xs : list α} :
p.many1 cb n = parse_result.done n' (x :: xs) ↔ p.many cb n = parse_result.done n' (x :: xs)
source
@[protected, instance]
def parser.prog.of_step {α : Type} {p : parser α} [p.step] :
p.prog
source
theorem parser.prog.pure {α : Type} (a : α) :
¬(has_pure.pure a).prog
source
@[protected, instance]
def parser.prog.bind {α β : Type} {p : parser α} {f : α → parser β} [p.prog] [∀ (a : α), (f a).mono] :
(p >>= f).prog
source
@[protected, instance]
def parser.prog.and_then {α β : Type} {p : parser α} {q : parser β} [p.prog] [q.mono] :
(p >> q).prog
source
@[protected, instance]
def parser.prog.map {α β : Type} {p : parser α} [p.prog] {f : α → β} :
parser.prog (f <$> p)
source
@[protected, instance]
def parser.prog.seq {α β : Type} {p : parser α} {f : parser (α → β)} [f.prog] [p.mono] :
(f <*> p).prog
source
@[protected, instance]
def parser.prog.mmap {α β : Type} {a : α} {l : list α} {f : α → parser β} [(f a).prog] [∀ (a : α), (f a).mono] :
(list.mmap f (a :: l)).prog
source
@[protected, instance]
def parser.prog.mmap' {α β : Type} {a : α} {l : list α} {f : α → parser β} [(f a).prog] [∀ (a : α), (f a).mono] :
(list.mmap' f (a :: l)).prog
source
@[protected, instance]
def parser.prog.failure {α : Type} :
failure.prog
source
theorem parser.prog.guard_true  :
¬(guard true).prog
source
@[protected, instance]
def parser.prog.guard  :
(guard false).prog
source
@[protected, instance]
def parser.prog.orelse {α : Type} {p q : parser α} [p.prog] [q.prog] :
(p <|> q).prog
source
theorem parser.prog.decorate_errors_iff {α : Type} {p : parser α} {msgs : thunk (list string)} :
(parser.decorate_errors msgs p).prog ↔ p.prog
source
@[protected, instance]
def parser.prog.decorate_errors {α : Type} {p : parser α} {msgs : thunk (list string)} [p.prog] :
(parser.decorate_errors msgs p).prog
source
theorem parser.prog.decorate_error_iff {α : Type} {p : parser α} {msg : thunk string} :
(parser.decorate_error msg p).prog ↔ p.prog
source
@[protected, instance]
def parser.prog.decorate_error {α : Type} {p : parser α} {msg : thunk string} [p.prog] :
(parser.decorate_error msg p).prog
source
@[protected, instance]
def parser.prog.any_char  :
parser.any_char.prog
source
@[protected, instance]
def parser.prog.sat {p : char → Prop} [decidable_pred p] :
(parser.sat p).prog
source
theorem parser.prog.eps  :
¬parser.eps.prog
source
@[protected, instance]
def parser.prog.ch {c : char} :
(parser.ch c).prog
source
theorem parser.prog.char_buf_iff {cb' : char_buffer} :
(parser.char_buf cb').prog ↔ cb' ≠ buffer.nil
source
@[protected, instance]
def parser.prog.one_of {cs : list char} :
(parser.one_of cs).prog
source
@[protected, instance]
def parser.prog.one_of' {cs : list char} :
(parser.one_of' cs).prog
source
theorem parser.prog.str_iff {s : string} :
(parser.str s).prog ↔ s ≠ ""
source
theorem parser.prog.remaining  :
¬parser.remaining.prog
source
theorem parser.prog.eof  :
¬parser.eof.prog
source
@[protected, instance]
def parser.prog.many1 {α : Type} {p : parser α} [p.mono] [p.prog] :
p.many1.prog
source
theorem parser.prog.fix_core {α : Type} {F : parser α → parser α} (hF : ∀ (p : parser α), p.prog → (F p).prog) (max_depth : ℕ) :
(parser.fix_core F max_depth).prog
source
@[protected, instance]
def parser.prog.digit  :
parser.digit.prog
source
@[protected, instance]
def parser.prog.nat  :
parser.nat.prog
source
theorem parser.prog.fix {α : Type} {F : parser α → parser α} (hF : ∀ (p : parser α), p.prog → (F p).prog) :
(parser.fix F).prog
source
theorem parser.many_sublist_of_done {α : Type} {p : parser α} {cb : char_buffer} {n n' : ℕ} [p.step] [p.bounded] {l : list α} (h : p.many cb n = parse_result.done n' l) (k : ℕ) (H : k < n' - n) :
p.many cb (n + k) = parse_result.done n' (list.drop k l)
source
theorem parser.many_eq_nil_of_done {α : Type} {p : parser α} {cb : char_buffer} {n n' : ℕ} [p.step] [p.bounded] {l : list α} (h : p.many cb n = parse_result.done n' l) :
p.many cb n' = parse_result.done n' list.nil
source
theorem parser.many_eq_nil_of_out_of_bound {α : Type} {p : parser α} {cb : char_buffer} {n n' : ℕ} [p.bounded] {l : list α} (h : p.many cb n = parse_result.done n' l) (hn : buffer.size cb < n) :
n' = n ∧ l = list.nil
source
theorem parser.many1_length_of_done {α : Type} {p : parser α} {cb : char_buffer} {n n' : ℕ} [p.mono] [p.step] [p.bounded] {l : list α} (h : p.many1 cb n = parse_result.done n' l) :
l.length = n' - n
source
theorem parser.many1_bounded_of_done {α : Type} {p : parser α} {cb : char_buffer} {n n' : ℕ} [p.step] [p.bounded] {l : list α} (h : p.many1 cb n = parse_result.done n' l) :
n' ≤ buffer.size cb
source
theorem parser.nat_of_done {cb : char_buffer} {n n' val : ℕ} (h : parser.nat cb n = parse_result.done n' val) :
val = nat.of_digits 10 (list.map (λ (c : char), c.to_nat - '0'.to_nat) (list.take (n' - n) (list.drop n (buffer.to_list cb))).reverse)

The val : ℕ produced by a successful parse of a cb : char_buffer is the numerical value represented by the string of decimal digits (possibly padded with 0s on the left) starting from the parsing position n and ending at position n'. The number of characters parsed in is necessarily n' - n.

This is one of the directions of nat_eq_done.

source
theorem parser.nat_of_done_as_digit {cb : char_buffer} {n n' val : ℕ} (h : parser.nat cb n = parse_result.done n' val) (hn : n' ≤ buffer.size cb) (k : ℕ) (hk : k < n') :
n ≤ k → '0' ≤ buffer.read cb ⟨k, _⟩ ∧ buffer.read cb ⟨k, _⟩ ≤ '9'

If we know that parser.nat was successful, starting at position n and ending at position n', then it must be the case that for all k : ℕ, n ≤ k, k < n', the character at the kth position in cb : char_buffer is "numeric", that is, is between '0' and '9' inclusive.

This is a necessary part of proving one of the directions of nat_eq_done.

source
theorem parser.nat_of_done_bounded {cb : char_buffer} {n n' val : ℕ} (h : parser.nat cb n = parse_result.done n' val) (hn : n' < buffer.size cb) :
'0' ≤ buffer.read cb ⟨n', hn⟩ → '9' < buffer.read cb ⟨n', hn⟩

If we know that parser.nat was successful, starting at position n and ending at position n', then it must be the case that for the ending position n', either it is beyond the end of the cb : char_buffer, or the character at that position is not "numeric", that is, between '0' and '9' inclusive.

This is a necessary part of proving one of the directions of nat_eq_done.

source
theorem parser.nat_eq_done {cb : char_buffer} {n n' val : ℕ} :
parser.nat cb n = parse_result.done n' val ↔ ∃ (hn : n < n'), val = nat.of_digits 10 (list.map (λ (c : char), c.to_nat - '0'.to_nat) (list.take (n' - n) (list.drop n (buffer.to_list cb))).reverse) ∧ (∀ (hn' : n' < buffer.size cb), '0' ≤ buffer.read cb ⟨n', hn'⟩ → '9' < buffer.read cb ⟨n', hn'⟩) ∧ ∃ (hn'' : n' ≤ buffer.size cb), ∀ (k : ℕ) (hk : k < n'), n ≤ k → '0' ≤ buffer.read cb ⟨k, _⟩ ∧ buffer.read cb ⟨k, _⟩ ≤ '9'

The val : ℕ produced by a successful parse of a cb : char_buffer is the numerical value represented by the string of decimal digits (possibly padded with 0s on the left) starting from the parsing position n and ending at position n', where n < n'. The number of characters parsed in is necessarily n' - n. Additionally, all of the characters in the cb starting at position n (inclusive) up to position n' (exclusive) are "numeric", in that they are between '0' and '9' inclusive. Such a char_buffer would produce the ℕ value encoded by its decimal characters.