simple-parser.lean

import data.buffer data.dlist system.io

def parser (α : Type) :=
∀ (input : char_buffer) (start : ℕ), list (ℕ × α)

namespace parser
variables {α β : Type}

protected def pure (value : α) : parser α :=
λ input pos, [⟨pos, value⟩]

protected def bind (p : parser α) (f : α → parser β) : parser β :=
λ input pos, do ⟨pos₂, value⟩ ← p input pos, f value input pos₂

protected def failure : parser α :=
λ _ _, []

protected def orelse (p q : parser α) : parser α :=
λ input pos, p input pos ++ q input pos

instance : monad parser :=
{ pure := @parser.pure, bind := @parser.bind }

instance : alternative parser :=
{ failure := @parser.failure, orelse := @parser.orelse }

def sat (pred : char → Prop) [decidable_pred pred] : parser char :=
λ input pos,
if h : pos < input.size then
  do let c := input.read ⟨pos, h⟩,
     guard (pred c),
     pure ⟨pos + 1, c⟩
else []

def any_char : parser char :=
sat (λ_, tt)

def ch (c : char) : parser unit :=
sat (= c) $> ⟨⟩

def one_of (cs : list char) : parser char :=
sat (∈ cs)

def str (s : string) : parser unit :=
s.to_list.mmap' ch

def remaining : parser ℕ :=
λ input pos, [⟨pos, input.size - pos⟩]

def eof : parser unit :=
do n ← remaining, guard (n = 0)

private def foldr_core (f : α → β → β) (p : parser α) (b : β) : ∀ (reps : ℕ), parser β
| 0 := failure
| (reps + 1) := (do x ← p, xs ← foldr_core reps, pure (f x xs)) <|> pure b

def foldr (f : α → β → β) (p : parser α) (b : β) : parser β :=
λ input pos, foldr_core f p b (input.size - pos + 1) input pos

def many (p : parser α) : parser (list α) :=
foldr (::) p []

def some (p : parser α) : parser (list α) :=
do x ← p, xs ← many p, pure (x :: xs)

def sep_by1 (sep : parser unit) (p : parser α) : parser (list α) :=
do x ← p, xs ← many (sep >> p), pure (x :: xs)

def sep_by (sep : parser unit) (p : parser α) : parser (list α) :=
sep_by1 sep p <|> pure []

def digit : parser ℕ :=
do c ← sat char.is_digit,
   pure (c.to_nat - '0'.to_nat)

def nat : parser ℕ :=
do digits ← some digit,
   pure (digits.foldl (λn digit, n * 10 + digit) 0)

def run (p : parser α) (input : string) : option α :=
let input_buffer := input.to_char_buffer in
match (p <* eof) input.to_char_buffer 0 with
| [] := none
| (⟨_, value⟩::_) := option.some value
end

end parser

section
  open parser
  
  def term : ℕ → parser ℕ
  | 0 := failure
  | (n + 1) :=
    (ch '(' *> term n <* ch ')') <|>
    ((+) <$> term n <* ch '+' <*> term n) <|>
    nat

  def test (p : ℕ → parser ℕ) (source : string) := do
    match (p 20).run source with
    | none := io.put_str_ln "none"
    | option.some x := io.print x
    end

  #eval test term "11+(2+3+4)+(110)"
end