parser.lean

def parser (α : Type) :=
list char → list (list char × α)

namespace parser
variables {α β : Type}

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

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

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

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

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
| [] := []
| (c::input) := do guard (pred c), pure ⟨input, c⟩

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 eof : parser unit
| [] := [⟨[], ⟨⟩⟩]
| _ := failure

private def fix_core (f : parser α → parser α) : ℕ → parser α
| 0 := failure
| (limit + 1) := f (fix_core limit)

def fix (f : parser α → parser α) : parser α :=
λ input, fix_core f (input.length + 1) input

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

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

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 ℕ :=
list.foldl (λn digit, n * 10 + digit) 0 <$> some digit

def run (p : parser α) (input : string) : option α :=
prod.snd <$> ((p <* eof) input.to_list).nth 0

end parser

section
  open parser
  
  def op : ℕ → char → ℕ → ℕ
  | a '+' b := a + b
  | a '-' b := a - b
  | a '*' b := a * b
  | _ _ _ := 0

  def term : parser ℕ := fix $ λ term,
  (ch '(' *> term <* ch ')') <|>
  (op <$> term <*> one_of ['+', '-', '*'] <*> term) <|>
  nat

  #eval term.run "11*(2+3+4)-(10)"
end