import data.string.basic

import data.buffer.basic

import data.nat.digits

import data.buffer.parser

open parser parse_result

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

| (done n _) := n

| (fail n _) := n

namespace parser

section defn_lemmas

variables {α β : Type} (msgs : thunk (list string)) (msg : thunk string)

variables (p q : parser α) (cb : char_buffer) (n n' : ℕ) {err : dlist string}

variables {a : α} {b : β}

class mono : Prop :=

(le' : ∀ (cb : char_buffer) (n : ℕ), n ≤ (p cb n).pos)

lemma mono.le [p.mono] : n ≤ (p cb n).pos := mono.le' cb n

class static : Prop :=

(of_done : ∀ {cb : char_buffer} {n n' : ℕ} {a : α}, p cb n = done n' a → n = n')

class err_static : Prop :=

(of_fail : ∀ {cb : char_buffer} {n n' : ℕ} {err : dlist string}, p cb n = fail n' err → n = n')

class step : Prop :=

(of_done : ∀ {cb : char_buffer} {n n' : ℕ} {a : α}, p cb n = done n' a → n' = n + 1)

class prog : Prop :=

(of_done : ∀ {cb : char_buffer} {n n' : ℕ} {a : α}, p cb n = done n' a → n < n')

class bounded : Prop :=

(ex' : ∀ {cb : char_buffer} {n : ℕ}, cb.size ≤ n → ∃ (n' : ℕ) (err : dlist string),

p cb n = fail n' err)

lemma bounded.exists (p : parser α) [p.bounded] {cb : char_buffer} {n : ℕ} (h : cb.size ≤ n) :

∃ (n' : ℕ) (err : dlist string), p cb n = fail n' err :=

bounded.ex' h

class unfailing : Prop :=

(ex' : ∀ (cb : char_buffer) (n : ℕ), ∃ (n' : ℕ) (a : α), p cb n = done n' a)

class conditionally_unfailing : Prop :=

(ex' : ∀ {cb : char_buffer} {n : ℕ}, n < cb.size → ∃ (n' : ℕ) (a : α), p cb n = done n' a)

lemma fail_iff :

(∀ pos' result, p cb n ≠ done pos' result) ↔

∃ (pos' : ℕ) (err : dlist string), p cb n = fail pos' err :=

by cases p cb n; simp

lemma success_iff :

(∀ pos' err, p cb n ≠ fail pos' err) ↔ ∃ (pos' : ℕ) (result : α), p cb n = done pos' result :=

by cases p cb n; simp

variables {p q cb n n' msgs msg}

lemma mono.of_done [p.mono] (h : p cb n = done n' a) : n ≤ n' :=

by simpa [h] using mono.le p cb n

lemma mono.of_fail [p.mono] (h : p cb n = fail n' err) : n ≤ n' :=

by simpa [h] using mono.le p cb n

lemma bounded.of_done [p.bounded] (h : p cb n = done n' a) : n < cb.size :=

contrapose! h,

obtain ⟨np, err, hp⟩ := bounded.exists p h,

simp [hp]

lemma static.iff :

static p ↔ (∀ (cb : char_buffer) (n n' : ℕ) (a : α), p cb n = done n' a → n = n') :=

⟨λ h _ _ _ _ hp, by { haveI := h, exact static.of_done hp}, λ h, ⟨h⟩⟩

lemma exists_done (p : parser α) [p.unfailing] (cb : char_buffer) (n : ℕ) :

∃ (n' : ℕ) (a : α), p cb n = done n' a :=

unfailing.ex' cb n

lemma unfailing.of_fail [p.unfailing] (h : p cb n = fail n' err) : false :=

obtain ⟨np, a, hp⟩ := p.exists_done cb n,

simpa [hp] using h

@[priority 100] -- see Note [lower instance priority]

instance conditionally_unfailing_of_unfailing [p.unfailing] : conditionally_unfailing p :=

⟨λ _ _ _, p.exists_done _ _⟩

lemma exists_done_in_bounds (p : parser α) [p.conditionally_unfailing] {cb : char_buffer} {n : ℕ}

(h : n < cb.size) : ∃ (n' : ℕ) (a : α), p cb n = done n' a :=

conditionally_unfailing.ex' h

lemma conditionally_unfailing.of_fail [p.conditionally_unfailing] (h : p cb n = fail n' err)

(hn : n < cb.size) : false :=

obtain ⟨np, a, hp⟩ := p.exists_done_in_bounds hn,

simpa [hp] using h

lemma decorate_errors_fail (h : p cb n = fail n' err) :

@decorate_errors α msgs p cb n = fail n ((dlist.lazy_of_list (msgs ()))) :=

by simp [decorate_errors, h]

lemma decorate_errors_success (h : p cb n = done n' a) :

@decorate_errors α msgs p cb n = done n' a :=

by simp [decorate_errors, h]

lemma decorate_error_fail (h : p cb n = fail n' err) :

@decorate_error α msg p cb n = fail n ((dlist.lazy_of_list ([msg ()]))) :=

decorate_errors_fail h

lemma decorate_error_success (h : p cb n = done n' a) :

@decorate_error α msg p cb n = done n' a :=

decorate_errors_success h

@[simp] lemma decorate_errors_eq_done :

@decorate_errors α msgs p cb n = done n' a ↔ p cb n = done n' a :=

by cases h : p cb n; simp [decorate_errors, h]

@[simp] lemma decorate_error_eq_done :

@decorate_error α msg p cb n = done n' a ↔ p cb n = done n' a :=

decorate_errors_eq_done

@[simp] lemma decorate_errors_eq_fail :

@decorate_errors α msgs p cb n = fail n' err ↔

n = n' ∧ err = dlist.lazy_of_list (msgs ()) ∧ ∃ np err', p cb n = fail np err' :=

by cases h : p cb n; simp [decorate_errors, h, eq_comm]

@[simp] lemma decorate_error_eq_fail :

@decorate_error α msg p cb n = fail n' err ↔

n = n' ∧ err = dlist.lazy_of_list ([msg ()]) ∧ ∃ np err', p cb n = fail np err' :=

decorate_errors_eq_fail

@[simp] lemma return_eq_pure : (@return parser _ _ a) = pure a := rfl

lemma pure_eq_done : (@pure parser _ _ a) = λ _ n, done n a := rfl

@[simp] lemma pure_ne_fail : (pure a : parser α) cb n ≠ fail n' err := by simp [pure_eq_done]

section bind

variable (f : α → parser β)

@[simp] lemma bind_eq_bind : p.bind f = p >>= f := rfl

variable {f}

@[simp] lemma bind_eq_done :

(p >>= f) cb n = done n' b ↔

∃ (np : ℕ) (a : α), p cb n = done np a ∧ f a cb np = done n' b :=

by cases hp : p cb n; simp [hp, ←bind_eq_bind, parser.bind, and_assoc]

@[simp] lemma bind_eq_fail :

(p >>= f) cb n = fail n' err ↔

(p cb n = fail n' err) ∨ (∃ (np : ℕ) (a : α), p cb n = done np a ∧ f a cb np = fail n' err) :=

by cases hp : p cb n; simp [hp, ←bind_eq_bind, parser.bind, and_assoc]

@[simp] lemma and_then_eq_bind {α β : Type} {m : Type → Type} [monad m] (a : m α) (b : m β) :

a >> b = a >>= (λ _, b) := rfl

lemma and_then_fail :

(p >> return ()) cb n = parse_result.fail n' err ↔ p cb n = fail n' err :=

by simp [pure_eq_done]

lemma and_then_success :

(p >> return ()) cb n = parse_result.done n' () ↔ ∃ a, p cb n = done n' a:=

by simp [pure_eq_done]

end bind

section map

variable {f : α → β}

@[simp] lemma map_eq_done : (f <$> p) cb n = done n' b ↔

∃ (a : α), p cb n = done n' a ∧ f a = b :=

by cases hp : p cb n; simp [←is_lawful_monad.bind_pure_comp_eq_map, hp, and_assoc, pure_eq_done]

@[simp] lemma map_eq_fail : (f <$> p) cb n = fail n' err ↔ p cb n = fail n' err :=

by simp [←bind_pure_comp_eq_map, pure_eq_done]

@[simp] lemma map_const_eq_done {b'} : (b <$ p) cb n = done n' b' ↔

∃ (a : α), p cb n = done n' a ∧ b = b' :=

by simp [map_const_eq]

@[simp] lemma map_const_eq_fail : (b <$ p) cb n = fail n' err ↔ p cb n = fail n' err :=

by simp only [map_const_eq, map_eq_fail]

lemma map_const_rev_eq_done {b'} : (p $> b) cb n = done n' b' ↔

∃ (a : α), p cb n = done n' a ∧ b = b' :=

map_const_eq_done

lemma map_rev_const_eq_fail : (p $> b) cb n = fail n' err ↔ p cb n = fail n' err :=

map_const_eq_fail

end map

@[simp] lemma orelse_eq_orelse : p.orelse q = (p <|> q) := rfl

@[simp] lemma orelse_eq_done : (p <|> q) cb n = done n' a ↔

(p cb n = done n' a ∨ (q cb n = done n' a ∧ ∃ err, p cb n = fail n err)) :=

cases hp : p cb n with np resp np errp,

{ simp [hp, ←orelse_eq_orelse, parser.orelse] },

{ by_cases hn : np = n,

{ cases hq : q cb n with nq resq nq errq,

{ simp [hp, hn, hq, ←orelse_eq_orelse, parser.orelse] },

{ rcases lt_trichotomy nq n with H|rfl|H;

simp [hp, hn, hq, H, not_lt_of_lt H, lt_irrefl, ←orelse_eq_orelse, parser.orelse] <|>

simp [hp, hn, hq, lt_irrefl, ←orelse_eq_orelse, parser.orelse] } },

{ simp [hp, hn, ←orelse_eq_orelse, parser.orelse] } }

@[simp] lemma orelse_eq_fail_eq : (p <|> q) cb n = fail n err ↔

(p cb n = fail n err ∧ ∃ (nq errq), n < nq ∧ q cb n = fail nq errq) ∨

(∃ (errp errq), p cb n = fail n errp ∧ q cb n = fail n errq ∧ errp ++ errq = err)

:=

cases hp : p cb n with np resp np errp,

{ simp [hp, ←orelse_eq_orelse, parser.orelse] },

{ by_cases hn : np = n,

{ cases hq : q cb n with nq resq nq errq,

{ simp [hp, hn, hq, ←orelse_eq_orelse, parser.orelse] },

{ rcases lt_trichotomy nq n with H|rfl|H;

simp [hp, hq, hn, ←orelse_eq_orelse, parser.orelse, H,

ne_of_gt H, ne_of_lt H, not_lt_of_lt H] <|>

simp [hp, hq, hn, ←orelse_eq_orelse, parser.orelse, lt_irrefl] } },

{ simp [hp, hn, ←orelse_eq_orelse, parser.orelse] } }

lemma orelse_eq_fail_not_mono_lt (hn : n' < n) : (p <|> q) cb n = fail n' err ↔

(p cb n = fail n' err) ∨

(q cb n = fail n' err ∧ (∃ (errp), p cb n = fail n errp)) :=

cases hp : p cb n with np resp np errp,

{ simp [hp, ←orelse_eq_orelse, parser.orelse] },

{ by_cases h : np = n,

{ cases hq : q cb n with nq resq nq errq,

{ simp [hp, h, hn, hq, ne_of_gt hn, ←orelse_eq_orelse, parser.orelse] },

{ rcases lt_trichotomy nq n with H|H|H,

{ simp [hp, hq, h, H, ne_of_gt hn, not_lt_of_lt H, ←orelse_eq_orelse, parser.orelse] },

{ simp [hp, hq, h, H, ne_of_gt hn, lt_irrefl, ←orelse_eq_orelse, parser.orelse] },

{ simp [hp, hq, h, H, ne_of_gt (hn.trans H), ←orelse_eq_orelse, parser.orelse] } } },

{ simp [hp, h, ←orelse_eq_orelse, parser.orelse] } }

lemma orelse_eq_fail_of_mono_ne [q.mono] (hn : n ≠ n') :

(p <|> q) cb n = fail n' err ↔ p cb n = fail n' err :=

cases hp : p cb n with np resp np errp,

{ simp [hp, ←orelse_eq_orelse, parser.orelse] },

{ by_cases h : np = n,

{ cases hq : q cb n with nq resq nq errq,

{ simp [hp, h, hn, hq, hn, ←orelse_eq_orelse, parser.orelse] },

{ have : n ≤ nq := mono.of_fail hq,

rcases eq_or_lt_of_le this with rfl|H,

{ simp [hp, hq, h, hn, lt_irrefl, ←orelse_eq_orelse, parser.orelse] },

{ simp [hp, hq, h, hn, H, ←orelse_eq_orelse, parser.orelse] } } },

{ simp [hp, h, ←orelse_eq_orelse, parser.orelse] } },

@[simp] lemma failure_eq_failure : @parser.failure α = failure := rfl

@[simp] lemma failure_def : (failure : parser α) cb n = fail n dlist.empty := rfl

lemma not_failure_eq_done : ¬ (failure : parser α) cb n = done n' a :=

by simp

lemma failure_eq_fail : (failure : parser α) cb n = fail n' err ↔ n = n' ∧ err = dlist.empty :=

by simp [eq_comm]

lemma seq_eq_done {f : parser (α → β)} {p : parser α} : (f <*> p) cb n = done n' b ↔

∃ (nf : ℕ) (f' : α → β) (a : α), f cb n = done nf f' ∧ p cb nf = done n' a ∧ f' a = b :=

by simp [seq_eq_bind_map]

lemma seq_eq_fail {f : parser (α → β)} {p : parser α} : (f <*> p) cb n = fail n' err ↔

(f cb n = fail n' err) ∨ (∃ (nf : ℕ) (f' : α → β), f cb n = done nf f' ∧ p cb nf = fail n' err) :=

by simp [seq_eq_bind_map]

lemma seq_left_eq_done {p : parser α} {q : parser β} : (p <* q) cb n = done n' a ↔

∃ (np : ℕ) (b : β), p cb n = done np a ∧ q cb np = done n' b :=

have : ∀ (p q : ℕ → α → Prop),

(∃ (np : ℕ) (x : α), p np x ∧ q np x ∧ x = a) ↔ ∃ (np : ℕ), p np a ∧ q np a :=

λ _ _, ⟨λ ⟨np, x, hp, hq, rfl⟩, ⟨np, hp, hq⟩, λ ⟨np, hp, hq⟩, ⟨np, a, hp, hq, rfl⟩⟩,

simp [seq_left_eq, seq_eq_done, map_eq_done, this]

lemma seq_left_eq_fail {p : parser α} {q : parser β} : (p <* q) cb n = fail n' err ↔

(p cb n = fail n' err) ∨ (∃ (np : ℕ) (a : α), p cb n = done np a ∧ q cb np = fail n' err) :=

by simp [seq_left_eq, seq_eq_fail]

lemma seq_right_eq_done {p : parser α} {q : parser β} : (p *> q) cb n = done n' b ↔

∃ (np : ℕ) (a : α), p cb n = done np a ∧ q cb np = done n' b :=

by simp [seq_right_eq, seq_eq_done, map_eq_done, and.comm, and.assoc]

lemma seq_right_eq_fail {p : parser α} {q : parser β} : (p *> q) cb n = fail n' err ↔

(p cb n = fail n' err) ∨ (∃ (np : ℕ) (a : α), p cb n = done np a ∧ q cb np = fail n' err) :=

by simp [seq_right_eq, seq_eq_fail]

lemma mmap_eq_done {f : α → parser β} {a : α} {l : list α} {b : β} {l' : list β} :

(a :: l).mmap f cb n = done n' (b :: l') ↔

∃ (np : ℕ), f a cb n = done np b ∧ l.mmap f cb np = done n' l' :=

by simp [mmap, and.comm, and.assoc, and.left_comm, pure_eq_done]

lemma mmap'_eq_done {f : α → parser β} {a : α} {l : list α} :

(a :: l).mmap' f cb n = done n' () ↔

∃ (np : ℕ) (b : β), f a cb n = done np b ∧ l.mmap' f cb np = done n' () :=

by simp [mmap']

lemma guard_eq_done {p : Prop} [decidable p] {u : unit} :

@guard parser _ p _ cb n = done n' u ↔ p ∧ n = n' :=

by { by_cases hp : p; simp [guard, hp, pure_eq_done] }

lemma guard_eq_fail {p : Prop} [decidable p] :

@guard parser _ p _ cb n = fail n' err ↔ (¬ p) ∧ n = n' ∧ err = dlist.empty :=

by { by_cases hp : p; simp [guard, hp, eq_comm, pure_eq_done] }

namespace mono

variables {sep : parser unit}

instance pure : mono (pure a) :=

⟨λ _ _, by simp [pure_eq_done]⟩

instance bind {f : α → parser β} [p.mono] [∀ a, (f a).mono] :

(p >>= f).mono :=

constructor,

intros cb n,

cases hx : (p >>= f) cb n,

{ obtain ⟨n', a, h, h'⟩ := bind_eq_done.mp hx,

refine le_trans (of_done h) _,

simpa [h'] using of_done h' },

{ obtain h | ⟨n', a, h, h'⟩ := bind_eq_fail.mp hx,

{ simpa [h] using of_fail h },

{ refine le_trans (of_done h) _,

simpa [h'] using of_fail h' } }

instance and_then {q : parser β} [p.mono] [q.mono] : (p >> q).mono := mono.bind

instance map [p.mono] {f : α → β} : (f <$> p).mono := mono.bind

instance seq {f : parser (α → β)} [f.mono] [p.mono] : (f <*> p).mono := mono.bind

instance mmap : Π {l : list α} {f : α → parser β} [∀ a ∈ l, (f a).mono],

(l.mmap f).mono

| [] _ _ := mono.pure

| (a :: l) f h := begin

convert mono.bind,

{ exact h _ (list.mem_cons_self _ _) },

{ intro,

convert mono.map,

convert mmap,

exact (λ _ ha, h _ (list.mem_cons_of_mem _ ha)) }

instance mmap' : Π {l : list α} {f : α → parser β} [∀ a ∈ l, (f a).mono],

(l.mmap' f).mono

| [] _ _ := mono.pure

| (a :: l) f h := begin

convert mono.and_then,

{ exact h _ (list.mem_cons_self _ _) },

{ convert mmap',

exact (λ _ ha, h _ (list.mem_cons_of_mem _ ha)) }

instance failure : (failure : parser α).mono :=

⟨by simp [le_refl]⟩

instance guard {p : Prop} [decidable p] : mono (guard p) :=

⟨by { by_cases h : p; simp [h, pure_eq_done, le_refl] }⟩

instance orelse [p.mono] [q.mono] : (p <|> q).mono :=

constructor,

intros cb n,

cases hx : (p <|> q) cb n with posx resx posx errx,

{ obtain h | ⟨h, -, -⟩ := orelse_eq_done.mp hx;

simpa [h] using of_done h },

{ by_cases h : n = posx,

{ simp [hx, h] },

{ simp only [orelse_eq_fail_of_mono_ne h] at hx,

exact of_fail hx } }

instance decorate_errors [p.mono] :

(@decorate_errors α msgs p).mono :=

constructor,

intros cb n,

cases h : p cb n,

{ simpa [decorate_errors, h] using of_done h },

{ simp [decorate_errors, h] }

instance decorate_error [p.mono] : (@decorate_error α msg p).mono :=

mono.decorate_errors

instance any_char : mono any_char :=

constructor,

intros cb n,

by_cases h : n < cb.size;

simp [any_char, h],

instance sat {p : char → Prop} [decidable_pred p] : mono (sat p) :=

constructor,

intros cb n,

simp only [sat],

split_ifs;

simp

instance eps : mono eps := mono.pure

instance ch {c : char} : mono (ch c) := mono.decorate_error

instance char_buf {s : char_buffer} : mono (char_buf s) :=

mono.decorate_error

instance one_of {cs : list char} : (one_of cs).mono :=

mono.decorate_errors

instance one_of' {cs : list char} : (one_of' cs).mono :=

mono.and_then

instance str {s : string} : (str s).mono :=

mono.decorate_error

instance remaining : remaining.mono :=

⟨λ _ _, le_rfl⟩

instance eof : eof.mono :=

mono.decorate_error

instance foldr_core {f : α → β → β} {b : β} [p.mono] :

∀ {reps : ℕ}, (foldr_core f p b reps).mono

| 0 := mono.failure

| (reps + 1) := begin

convert mono.orelse,

{ convert mono.bind,

{ apply_instance },

{ exact λ _, @mono.bind _ _ _ _ foldr_core _ } },

{ exact mono.pure }

instance foldr {f : α → β → β} [p.mono] : mono (foldr f p b) :=

⟨λ _ _, by { convert mono.le (foldr_core f p b _) _ _, exact mono.foldr_core }⟩

instance foldl_core {f : α → β → α} {p : parser β} [p.mono] :

∀ {a : α} {reps : ℕ}, (foldl_core f a p reps).mono

| _ 0 := mono.failure

| _ (reps + 1) := begin

convert mono.orelse,

{ convert mono.bind,

{ apply_instance },

{ exact λ _, foldl_core } },

{ exact mono.pure }

instance foldl {f : α → β → α} {p : parser β} [p.mono] : mono (foldl f a p) :=

⟨λ _ _, by { convert mono.le (foldl_core f a p _) _ _, exact mono.foldl_core }⟩

instance many [p.mono] : p.many.mono :=

mono.foldr

instance many_char {p : parser char} [p.mono] : p.many_char.mono :=

mono.map

instance many' [p.mono] : p.many'.mono :=

mono.and_then

instance many1 [p.mono] : p.many1.mono :=

mono.seq

instance many_char1 {p : parser char} [p.mono] : p.many_char1.mono :=

mono.map

instance sep_by1 [p.mono] [sep.mono] : mono (sep_by1 sep p) :=

mono.seq

instance sep_by [p.mono] [hs : sep.mono] : mono (sep_by sep p) :=

mono.orelse

lemma fix_core {F : parser α → parser α} (hF : ∀ (p : parser α), p.mono → (F p).mono) :

∀ (max_depth : ℕ), mono (fix_core F max_depth)

| 0 := mono.failure

| (max_depth + 1) := hF _ (fix_core _)

instance digit : digit.mono :=

mono.decorate_error

instance nat : nat.mono :=

mono.decorate_error

lemma fix {F : parser α → parser α} (hF : ∀ (p : parser α), p.mono → (F p).mono) :

mono (fix F) :=

⟨λ _ _, by { convert mono.le (parser.fix_core F _) _ _, exact fix_core hF _ }⟩

end mono

@[simp] lemma orelse_pure_eq_fail : (p <|> pure a) cb n = fail n' err ↔

p cb n = fail n' err ∧ n ≠ n' :=

by_cases hn : n = n',

{ simp [hn, pure_eq_done] },

{ simp [orelse_eq_fail_of_mono_ne, hn] }

end defn_lemmas

section done

variables {α β : Type} {cb : char_buffer} {n n' : ℕ} {a a' : α} {b : β} {c : char} {u : unit}

{err : dlist string}

lemma any_char_eq_done : any_char cb n = done n' c ↔

∃ (hn : n < cb.size), n' = n + 1 ∧ cb.read ⟨n, hn⟩ = c :=

simp_rw [any_char],

split_ifs with h;

simp [h, eq_comm]

lemma any_char_eq_fail : any_char cb n = fail n' err ↔ n = n' ∧ err = dlist.empty ∧ cb.size ≤ n :=

simp_rw [any_char],

split_ifs with h;

simp [←not_lt, h, eq_comm]

lemma sat_eq_done {p : char → Prop} [decidable_pred p] : sat p cb n = done n' c ↔

∃ (hn : n < cb.size), p c ∧ n' = n + 1 ∧ cb.read ⟨n, hn⟩ = c :=

by_cases hn : n < cb.size,

{ by_cases hp : p (cb.read ⟨n, hn⟩),

{ simp only [sat, hn, hp, dif_pos, if_true, exists_prop_of_true],

split,

{ rintro ⟨rfl, rfl⟩, simp [hp] },

{ rintro ⟨-, rfl, rfl⟩, simp } },

{ simp only [sat, hn, hp, dif_pos, false_iff, not_and, exists_prop_of_true, if_false],

rintro H - rfl,

exact hp H } },

{ simp [sat, hn] }

lemma sat_eq_fail {p : char → Prop} [decidable_pred p] : sat p cb n = fail n' err ↔

n = n' ∧ err = dlist.empty ∧ ∀ (h : n < cb.size), ¬ p (cb.read ⟨n, h⟩) :=

dsimp only [sat],

split_ifs;

simp [*, eq_comm]

lemma eps_eq_done : eps cb n = done n' u ↔ n = n' := by simp [eps, pure_eq_done]

lemma ch_eq_done : ch c cb n = done n' u ↔ ∃ (hn : n < cb.size), n' = n + 1 ∧ cb.read ⟨n, hn⟩ = c :=

by simp [ch, eps_eq_done, sat_eq_done, and.comm, @eq_comm _ n']

lemma char_buf_eq_done {cb' : char_buffer} : char_buf cb' cb n = done n' u ↔

n + cb'.size = n' ∧ cb'.to_list <+: (cb.to_list.drop n) :=

simp only [char_buf, decorate_error_eq_done, ne.def, ←buffer.length_to_list],

induction cb'.to_list with hd tl hl generalizing cb n n',

{ simp [pure_eq_done, mmap'_eq_done, -buffer.length_to_list, list.nil_prefix] },

{ simp only [ch_eq_done, and.comm, and.assoc, and.left_comm, hl, mmap', and_then_eq_bind,

bind_eq_done, list.length, exists_and_distrib_left, exists_const],

split,

{ rintro ⟨np, h, rfl, rfl, hn, rfl⟩,

simp only [add_comm, add_left_comm, h, true_and, eq_self_iff_true, and_true],

have : n < cb.to_list.length := by simpa using hn,

rwa [←buffer.nth_le_to_list _ this, ←list.cons_nth_le_drop_succ this, list.prefix_cons_inj] },

{ rintro ⟨h, rfl⟩,

by_cases hn : n < cb.size,

{ have : n < cb.to_list.length := by simpa using hn,

rw [←list.cons_nth_le_drop_succ this, list.cons_prefix_iff] at h,

use [n + 1, h.right],

simpa [buffer.nth_le_to_list, add_comm, add_left_comm, add_assoc, hn] using h.left.symm },

{ have : cb.to_list.length ≤ n := by simpa using hn,

rw list.drop_eq_nil_of_le this at h,

simpa using h } } }

lemma one_of_eq_done {cs : list char} : one_of cs cb n = done n' c ↔

∃ (hn : n < cb.size), c ∈ cs ∧ n' = n + 1 ∧ cb.read ⟨n, hn⟩ = c :=

by simp [one_of, sat_eq_done]

lemma one_of'_eq_done {cs : list char} : one_of' cs cb n = done n' u ↔

∃ (hn : n < cb.size), cb.read ⟨n, hn⟩ ∈ cs ∧ n' = n + 1 :=

simp only [one_of', one_of_eq_done, eps_eq_done, and.comm, and_then_eq_bind, bind_eq_done,

exists_eq_left, exists_and_distrib_left],

split,

{ rintro ⟨c, hc, rfl, hn, rfl⟩,

exact ⟨rfl, hn, hc⟩ },

{ rintro ⟨rfl, hn, hc⟩,

exact ⟨cb.read ⟨n, hn⟩, hc, rfl, hn, rfl⟩ }

lemma str_eq_char_buf (s : string) : str s = char_buf s.to_list.to_buffer :=

ext cb n,

rw [str, char_buf],

congr,

{ simp [buffer.to_string, string.as_string_inv_to_list] },

{ simp }

lemma str_eq_done {s : string} : str s cb n = done n' u ↔

n + s.length = n' ∧ s.to_list <+: (cb.to_list.drop n) :=

by simp [str_eq_char_buf, char_buf_eq_done]

lemma remaining_eq_done {r : ℕ} : remaining cb n = done n' r ↔ n = n' ∧ cb.size - n = r :=

by simp [remaining]

lemma remaining_ne_fail : remaining cb n ≠ fail n' err :=

by simp [remaining]

lemma eof_eq_done {u : unit} : eof cb n = done n' u ↔ n = n' ∧ cb.size ≤ n :=

by simp [eof, guard_eq_done, remaining_eq_done, tsub_eq_zero_iff_le, and_comm, and_assoc]

@[simp] lemma foldr_core_zero_eq_done {f : α → β → β} {p : parser α} {b' : β} :

foldr_core f p b 0 cb n ≠ done n' b' :=

by simp [foldr_core]

lemma foldr_core_eq_done {f : α → β → β} {p : parser α} {reps : ℕ} {b' : β} :

foldr_core f p b (reps + 1) cb n = done n' b' ↔

(∃ (np : ℕ) (a : α) (xs : β), p cb n = done np a ∧ foldr_core f p b reps cb np = done n' xs

∧ f a xs = b') ∨

(n = n' ∧ b = b' ∧ ∃ (err), (p cb n = fail n err) ∨

(∃ (np : ℕ) (a : α), p cb n = done np a ∧ foldr_core f p b reps cb np = fail n err)) :=

by simp [foldr_core, and.comm, and.assoc, pure_eq_done]

@[simp] lemma foldr_core_zero_eq_fail {f : α → β → β} {p : parser α} {err : dlist string} :

foldr_core f p b 0 cb n = fail n' err ↔ n = n' ∧ err = dlist.empty :=

by simp [foldr_core, eq_comm]

lemma foldr_core_succ_eq_fail {f : α → β → β} {p : parser α} {reps : ℕ} {err : dlist string} :

foldr_core f p b (reps + 1) cb n = fail n' err ↔ n ≠ n' ∧

(p cb n = fail n' err ∨

∃ (np : ℕ) (a : α), p cb n = done np a ∧ foldr_core f p b reps cb np = fail n' err) :=

by simp [foldr_core, and_comm]

lemma foldr_eq_done {f : α → β → β} {p : parser α} {b' : β} :

foldr f p b cb n = done n' b' ↔

((∃ (np : ℕ) (a : α) (x : β), p cb n = done np a ∧

foldr_core f p b (cb.size - n) cb np = done n' x ∧ f a x = b') ∨

(n = n' ∧ b = b' ∧ (∃ (err), p cb n = parse_result.fail n err ∨

∃ (np : ℕ) (x : α), p cb n = done np x ∧ foldr_core f p b (cb.size - n) cb np = fail n err))) :=

by simp [foldr, foldr_core_eq_done]

lemma foldr_eq_fail_iff_mono_at_end {f : α → β → β} {p : parser α} {err : dlist string}

[p.mono] (hc : cb.size ≤ n) : foldr f p b cb n = fail n' err ↔

n < n' ∧ (p cb n = fail n' err ∨ ∃ (a : α), p cb n = done n' a ∧ err = dlist.empty) :=

have : cb.size - n = 0 := tsub_eq_zero_iff_le.mpr hc,

simp only [foldr, foldr_core_succ_eq_fail, this, and.left_comm, foldr_core_zero_eq_fail,

ne_iff_lt_iff_le, exists_and_distrib_right, exists_eq_left, and.congr_left_iff,

exists_and_distrib_left],

rintro (h | ⟨⟨a, h⟩, rfl⟩),

{ exact mono.of_fail h },

{ exact mono.of_done h }

lemma foldr_eq_fail {f : α → β → β} {p : parser α} {err : dlist string} :

foldr f p b cb n = fail n' err ↔ n ≠ n' ∧ (p cb n = fail n' err ∨

∃ (np : ℕ) (a : α), p cb n = done np a ∧ foldr_core f p b (cb.size - n) cb np = fail n' err) :=

by simp [foldr, foldr_core_succ_eq_fail]

@[simp] lemma foldl_core_zero_eq_done {f : β → α → β} {p : parser α} {b' : β} :

foldl_core f b p 0 cb n = done n' b' ↔ false :=

by simp [foldl_core]

lemma foldl_core_eq_done {f : β → α → β} {p : parser α} {reps : ℕ} {b' : β} :

foldl_core f b p (reps + 1) cb n = done n' b' ↔

(∃ (np : ℕ) (a : α), p cb n = done np a ∧ foldl_core f (f b a) p reps cb np = done n' b') ∨

(n = n' ∧ b = b' ∧ ∃ (err), (p cb n = fail n err) ∨

(∃ (np : ℕ) (a : α), p cb n = done np a ∧ foldl_core f (f b a) p reps cb np = fail n err)) :=

by simp [foldl_core, and.assoc, pure_eq_done]

@[simp] lemma foldl_core_zero_eq_fail {f : β → α → β} {p : parser α} {err : dlist string} :

foldl_core f b p 0 cb n = fail n' err ↔ n = n' ∧ err = dlist.empty :=

by simp [foldl_core, eq_comm]

lemma foldl_core_succ_eq_fail {f : β → α → β} {p : parser α} {reps : ℕ} {err : dlist string} :

foldl_core f b p (reps + 1) cb n = fail n' err ↔ n ≠ n' ∧

(p cb n = fail n' err ∨

∃ (np : ℕ) (a : α), p cb n = done np a ∧ foldl_core f (f b a) p reps cb np = fail n' err) :=

by simp [foldl_core, and_comm]

lemma foldl_eq_done {f : β → α → β} {p : parser α} {b' : β} :

foldl f b p cb n = done n' b' ↔

(∃ (np : ℕ) (a : α), p cb n = done np a ∧

foldl_core f (f b a) p (cb.size - n) cb np = done n' b') ∨

(n = n' ∧ b = b' ∧ ∃ (err), (p cb n = fail n err) ∨

(∃ (np : ℕ) (a : α), p cb n = done np a ∧

foldl_core f (f b a) p (cb.size - n) cb np = fail n err)) :=

by simp [foldl, foldl_core_eq_done]

lemma foldl_eq_fail {f : β → α → β} {p : parser α} {err : dlist string} :

foldl f b p cb n = fail n' err ↔ n ≠ n' ∧ (p cb n = fail n' err ∨

∃ (np : ℕ) (a : α), p cb n = done np a ∧

foldl_core f (f b a) p (cb.size - n) cb np = fail n' err) :=

by simp [foldl, foldl_core_succ_eq_fail]

lemma foldl_eq_fail_iff_mono_at_end {f : β → α → β} {p : parser α} {err : dlist string}

[p.mono] (hc : cb.size ≤ n) : foldl f b p cb n = fail n' err ↔

n < n' ∧ (p cb n = fail n' err ∨ ∃ (a : α), p cb n = done n' a ∧ err = dlist.empty) :=

have : cb.size - n = 0 := tsub_eq_zero_iff_le.mpr hc,

simp only [foldl, foldl_core_succ_eq_fail, this, and.left_comm, ne_iff_lt_iff_le, exists_eq_left,

exists_and_distrib_right, and.congr_left_iff, exists_and_distrib_left,

foldl_core_zero_eq_fail],

rintro (h | ⟨⟨a, h⟩, rfl⟩),

{ exact mono.of_fail h },

{ exact mono.of_done h }

lemma many_eq_done_nil {p : parser α} : many p cb n = done n' (@list.nil α) ↔ n = n' ∧

∃ (err), p cb n = fail n err ∨ ∃ (np : ℕ) (a : α), p cb n = done np a ∧

foldr_core list.cons p [] (cb.size - n) cb np = fail n err :=

by simp [many, foldr_eq_done]

lemma many_eq_done {p : parser α} {x : α} {xs : list α} :

many p cb n = done n' (x :: xs) ↔ ∃ (np : ℕ), p cb n = done np x

∧ foldr_core list.cons p [] (cb.size - n) cb np = done n' xs :=

by simp [many, foldr_eq_done, and.comm, and.assoc, and.left_comm]

lemma many_eq_fail {p : parser α} {err : dlist string} :

many p cb n = fail n' err ↔ n ≠ n' ∧ (p cb n = fail n' err ∨

∃ (np : ℕ) (a : α), p cb n = done np a ∧

foldr_core list.cons p [] (cb.size - n) cb np = fail n' err) :=

by simp [many, foldr_eq_fail]

lemma many_char_eq_done_empty {p : parser char} : many_char p cb n = done n' string.empty ↔ n = n' ∧

∃ (err), p cb n = fail n err ∨ ∃ (np : ℕ) (c : char), p cb n = done np c ∧

foldr_core list.cons p [] (cb.size - n) cb np = fail n err :=

by simp [many_char, many_eq_done_nil, map_eq_done, list.as_string_eq]

lemma many_char_eq_done_not_empty {p : parser char} {s : string} (h : s ≠ "") :

many_char p cb n = done n' s ↔ ∃ (np : ℕ), p cb n = done np s.head ∧

foldr_core list.cons p list.nil (buffer.size cb - n) cb np = done n' (s.popn 1).to_list :=

by simp [many_char, list.as_string_eq, string.to_list_nonempty h, many_eq_done]

lemma many_char_eq_many_of_to_list {p : parser char} {s : string} :

many_char p cb n = done n' s ↔ many p cb n = done n' s.to_list :=

by simp [many_char, list.as_string_eq]

lemma many'_eq_done {p : parser α} : many' p cb n = done n' u ↔

many p cb n = done n' [] ∨ ∃ (np : ℕ) (a : α) (l : list α), many p cb n = done n' (a :: l)

∧ p cb n = done np a ∧ foldr_core list.cons p [] (buffer.size cb - n) cb np = done n' l :=

simp only [many', eps_eq_done, many, foldr, and_then_eq_bind, exists_and_distrib_right,

bind_eq_done, exists_eq_right],

split,

{ rintro ⟨_ | ⟨hd, tl⟩, hl⟩,

{ exact or.inl hl },

{ have hl2 := hl,

simp only [foldr_core_eq_done, or_false, exists_and_distrib_left, and_false, false_and,

exists_eq_right_right] at hl,

obtain ⟨np, hp, h⟩ := hl,

refine or.inr ⟨np, _, _, hl2, hp, h⟩ } },

{ rintro (h | ⟨np, a, l, hp, h⟩),

{ exact ⟨[], h⟩ },

{ refine ⟨a :: l, hp⟩ } }

@[simp] lemma many1_ne_done_nil {p : parser α} : many1 p cb n ≠ done n' [] :=

by simp [many1, seq_eq_done]

lemma many1_eq_done {p : parser α} {l : list α} : many1 p cb n = done n' (a :: l) ↔

∃ (np : ℕ), p cb n = done np a ∧ many p cb np = done n' l :=

by simp [many1, seq_eq_done, map_eq_done]

lemma many1_eq_fail {p : parser α} {err : dlist string} : many1 p cb n = fail n' err ↔

p cb n = fail n' err ∨ (∃ (np : ℕ) (a : α), p cb n = done np a ∧ many p cb np = fail n' err) :=

by simp [many1, seq_eq_fail]

@[simp] lemma many_char1_ne_empty {p : parser char} : many_char1 p cb n ≠ done n' "" :=

by simp [many_char1, ←string.nil_as_string_eq_empty]

lemma many_char1_eq_done {p : parser char} {s : string} (h : s ≠ "") :

many_char1 p cb n = done n' s ↔

∃ (np : ℕ), p cb n = done np s.head ∧ many_char p cb np = done n' (s.popn 1) :=

by simp [many_char1, list.as_string_eq, string.to_list_nonempty h, many1_eq_done,

many_char_eq_many_of_to_list]

@[simp] lemma sep_by1_ne_done_nil {sep : parser unit} {p : parser α} :

sep_by1 sep p cb n ≠ done n' [] :=

by simp [sep_by1, seq_eq_done]

lemma sep_by1_eq_done {sep : parser unit} {p : parser α} {l : list α} :

sep_by1 sep p cb n = done n' (a :: l) ↔ ∃ (np : ℕ), p cb n = done np a ∧

(sep >> p).many cb np = done n' l :=

by simp [sep_by1, seq_eq_done]

lemma sep_by_eq_done_nil {sep : parser unit} {p : parser α} :

sep_by sep p cb n = done n' [] ↔ n = n' ∧ ∃ (err), sep_by1 sep p cb n = fail n err :=

by simp [sep_by, pure_eq_done]

@[simp] lemma fix_core_ne_done_zero {F : parser α → parser α} :

fix_core F 0 cb n ≠ done n' a :=

by simp [fix_core]

lemma fix_core_eq_done {F : parser α → parser α} {max_depth : ℕ} :

fix_core F (max_depth + 1) cb n = done n' a ↔ F (fix_core F max_depth) cb n = done n' a :=

by simp [fix_core]

lemma digit_eq_done {k : ℕ} : digit cb n = done n' k ↔ ∃ (hn : n < cb.size), n' = n + 1 ∧ k ≤ 9 ∧

(cb.read ⟨n, hn⟩).to_nat - '0'.to_nat = k ∧ '0' ≤ cb.read ⟨n, hn⟩ ∧ cb.read ⟨n, hn⟩ ≤ '9' :=

have c9 : '9'.to_nat - '0'.to_nat = 9 := rfl,

have l09 : '0'.to_nat ≤ '9'.to_nat := dec_trivial,

have le_iff_le : ∀ {c c' : char}, c ≤ c' ↔ c.to_nat ≤ c'.to_nat := λ _ _, iff.rfl,

split,

{ simp only [digit, sat_eq_done, pure_eq_done, decorate_error_eq_done, bind_eq_done, ←c9],

rintro ⟨np, c, ⟨hn, ⟨ge0, le9⟩, rfl, rfl⟩, rfl, rfl⟩,

simpa [hn, ge0, le9, true_and, and_true, eq_self_iff_true, exists_prop_of_true,

tsub_le_tsub_iff_right, l09] using (le_iff_le.mp le9) },

{ simp only [digit, sat_eq_done, pure_eq_done, decorate_error_eq_done, bind_eq_done, ←c9,

le_iff_le],

rintro ⟨hn, rfl, -, rfl, ge0, le9⟩,

use [n + 1, cb.read ⟨n, hn⟩],

simp [hn, ge0, le9] }

lemma digit_eq_fail : digit cb n = fail n' err ↔ n = n' ∧ err = dlist.of_list ["<digit>"] ∧

∀ (h : n < cb.size), ¬ ((λ c, '0' ≤ c ∧ c ≤ '9') (cb.read ⟨n, h⟩)) :=

by simp [digit, sat_eq_fail]

end done

namespace static

variables {α β : Type} {p q : parser α} {msgs : thunk (list string)} {msg : thunk string}

{cb : char_buffer} {n' n : ℕ} {err : dlist string} {a : α} {b : β} {sep : parser unit}

lemma not_of_ne (h : p cb n = done n' a) (hne : n ≠ n') : ¬ static p :=

by { introI, exact hne (of_done h) }

instance pure : static (pure a) :=

⟨λ _ _ _ _, by { simp_rw pure_eq_done, rw [and.comm], simp }⟩

instance bind {f : α → parser β} [p.static] [∀ a, (f a).static] :

(p >>= f).static :=

⟨λ _ _ _ _, by { rw bind_eq_done, rintro ⟨_, _, hp, hf⟩, exact trans (of_done hp) (of_done hf) }⟩

instance and_then {q : parser β} [p.static] [q.static] : (p >> q).static := static.bind

instance map [p.static] {f : α → β} : (f <$> p).static :=

⟨λ _ _ _ _, by { simp_rw map_eq_done, rintro ⟨_, hp, _⟩, exact of_done hp }⟩

instance seq {f : parser (α → β)} [f.static] [p.static] : (f <*> p).static := static.bind

instance mmap : Π {l : list α} {f : α → parser β} [∀ a, (f a).static], (l.mmap f).static

| [] _ _ := static.pure

| (a :: l) _ h := begin

convert static.bind,

{ exact h _ },

{ intro,

convert static.bind,

{ convert mmap,

exact h },

{ exact λ _, static.pure } }

instance mmap' : Π {l : list α} {f : α → parser β} [∀ a, (f a).static], (l.mmap' f).static

| [] _ _ := static.pure

| (a :: l) _ h := begin

convert static.and_then,

{ exact h _ },

{ convert mmap',

exact h }

instance failure : @parser.static α failure :=

⟨λ _ _ _ _, by simp⟩

instance guard {p : Prop} [decidable p] : static (guard p) :=

⟨λ _ _ _ _, by simp [guard_eq_done]⟩

instance orelse [p.static] [q.static] : (p <|> q).static :=

⟨λ _ _ _ _, by { simp_rw orelse_eq_done, rintro (h | ⟨h, -⟩); exact of_done h }⟩

instance decorate_errors [p.static] :

(@decorate_errors α msgs p).static :=

⟨λ _ _ _ _, by { rw decorate_errors_eq_done, exact of_done }⟩

instance decorate_error [p.static] : (@decorate_error α msg p).static :=

static.decorate_errors

lemma any_char : ¬ static any_char :=

have : any_char "s".to_char_buffer 0 = done 1 's',

{ have : 0 < "s".to_char_buffer.size := dec_trivial,

simpa [any_char_eq_done, this] },

exact not_of_ne this zero_ne_one

lemma sat_iff {p : char → Prop} [decidable_pred p] : static (sat p) ↔ ∀ c, ¬ p c :=

split,

{ introI,

intros c hc,

have : sat p [c].to_buffer 0 = done 1 c := by simp [sat_eq_done, hc],

exact zero_ne_one (of_done this) },

{ contrapose!,

simp only [iff, sat_eq_done, and_imp, exists_prop, exists_and_distrib_right,

exists_and_distrib_left, exists_imp_distrib, not_forall],

rintros _ _ _ a h hne rfl hp -,

exact ⟨a, hp⟩ }

instance sat : static (sat (λ _, false)) :=

by { apply sat_iff.mpr, simp }

instance eps : static eps := static.pure

lemma ch (c : char) : ¬ static (ch c) :=

have : ch c [c].to_buffer 0 = done 1 (),

{ have : 0 < [c].to_buffer.size := dec_trivial,

simp [ch_eq_done, this] },

exact not_of_ne this zero_ne_one

lemma char_buf_iff {cb' : char_buffer} : static (char_buf cb') ↔ cb' = buffer.nil :=

rw ←buffer.size_eq_zero_iff,