parser.lean

import data.buffer.parser
open parser

inductive res
| str : string → res
| int : int → res
| ch : char → res

instance res_repr : has_repr res :=
⟨λ x, match x with
| res.str s := sformat! "\"{s}\""
| res.int x := to_string x
| res.ch c := sformat! "'{c}'"
end⟩

def reserved := ['\\', '(', ')', '[', ']', '^', '+']

def Char : parser char :=
sat (λ c, reserved.all (≠ c))

def ReservedSymbol : parser char := sat (∈ reserved)

def Num : parser nat :=
list.foldl (λ p n, (str (to_string n) >> pure n) <|> p)
  (parser.fail "?") (list.range 10)

def SingleToken {α : Type} (view : string) (p : parser α) (to_res : α → res) :
  parser (list res → parser (list res)) :=
str view >> pure (λ x, p >>= λ y, pure (x ++ [to_res y]))

def SortsOfCharacters : parser (list res → parser (list res)) :=
(SingleToken "\\d" Num (res.int ∘ int.of_nat)) <|>
(SingleToken "\\w+" (many_char1 $ sat char.is_alpha) res.str) <|>
(SingleToken "\\w" (sat char.is_alpha) res.ch) <|>
(SingleToken "\\u" Char res.ch)

def CharsEnumeration : parser (list res → parser (list res)) :=
(str "[^" >> many1 Char <* ch ']' >>=
  λ chs, pure (λ x, sat (∉ chs) >>= λ c, pure (x ++ [res.ch c]))) <|>
(ch '[' >> many1 Char <* ch ']' >>=
  λ chs, pure (λ x, sat (∈ chs) >>= λ c, pure (x ++ [res.ch c])))

def RegToken : parser (list res → parser (list res)) :=
SortsOfCharacters <|>
CharsEnumeration <|>
(ch '\\' >> ReservedSymbol >>= λ c, pure (λ x, ch c >> pure x)) <|>
(Char >>= λ c, pure (λ x, ch c >> pure x))

def Reg := list.foldl (>>=) (pure []) <$> many1 RegToken

def parse (expr : string) (s : string) : string ⊕ list res :=
sum.rec_on (run_string Reg expr) sum.inl
  (λ p, sum.rec_on (run_string p s) sum.inl sum.inr)

def DateTime : parser (list res) :=
sum.rec_on (run_string Reg "\\d\\d:\\d\\d \\([AP]M\\)") parser.fail id

#eval run_string DateTime "11:24 (PM)" -- ok
#eval run_string DateTime "12:12 (AM)" -- ok
#eval run_string DateTime "11:24 test" -- error