Monadic parsing in Lean

MonadicParsing.lean

/-
Implementation of monadic parsing in Lean, based on the original
paper's implementation in Haskell.

- FUNCTIONAL PEARL - Monadic parsing in Haskell:
  https://www.cmi.ac.in/~spsuresh/teaching/prgh15/papers/monadic-parsing.pdf
-/

-- ## Parser definition

structure ParserRes (a : Type u) where
  item: a
  str: String
deriving Repr

def res (item: a) (str: String) : ParserRes a :=
  ParserRes.mk item str

structure Parser (a : Type) where
  parse : String -> List (ParserRes a)

-- ## Parser as a monad

instance : Functor Parser where
  map := fun f p => Parser.mk (
    fun str => List.map
      (fun res => {res with item := f res.item})
      (p.parse str))

instance : Monad Parser where
  pure a := Parser.mk fun str => [res a str]
  bind p f := Parser.mk fun str => (p.parse str)
    |> List.map (fun res => (f res.item).parse res.str)
    |> List.foldr (List.foldl List.concat) []

instance : Add (Parser a) where
  add p1 p2 := Parser.mk fun str => p1.parse str ++ p2.parse str

def Parser.zero : Parser a :=
  Parser.mk (fun _str => [])

-- ## Combinators

def item : Parser Char :=
  Parser.mk fun str => match str.data with
    | [] => []
    | (c :: cs) => [res c (String.mk cs)]

#eval item.parse "123"

def sat (p : Char -> Bool) : Parser Char := do
  let c <- item
  if p c then pure c
  else        Parser.zero

#eval (sat $ fun c => c == 'a').parse "ABC"
#eval (sat $ fun c => c == 'a').parse "abc"

def char (c: Char) : Parser Char :=
  sat (fun c' => c == c')

#eval (char 'a').parse "ABC"
#eval (char 'a').parse "abc"
#eval (char 'a' + (pure '?')).parse "ABC"
#eval (char 'a' + (pure '?')).parse "abc"

def chars : List Char -> Parser (List Char)
  | [] => pure []
  | c :: cs => do
    let _ <- char c
    let _ <- chars cs
    pure (c :: cs)

def string (str: String) := String.mk <$> chars str.data

#eval (string "Hello").parse "Hello, world!"

def first (p : Parser a) : Parser a :=
  Parser.mk (fun str => match p.parse str with
    | [] => []
    | r :: _rs => [r])

mutual
  partial def many (p : Parser a) : Parser (List a) :=
    first $ (many1 p) + (pure [])

  partial def many1 (p : Parser a) : Parser (List a) :=
    first $ do
      let x <- p
      let xs <- many p
      return x :: xs
end

#eval (many (char 'a')).parse "ABC"
#eval (many (char 'a')).parse "aaabc"

#eval (many1 (char 'a')).parse "ABC"
#eval (many1 (char 'a')).parse "aaabc"

def sepby1 (p : Parser a) (sep : Parser b) : Parser (List a) := do
  let x <- p
  let xs <- many $ do
    let _ <- sep
    p

  return x :: xs

#eval (sepby1 (char 'a') (char ',')).parse "a,a,b,c"
#eval (sepby1 (char 'a') (char ',')).parse "A,A,B,C"

def sepby (p : Parser a) (sep : Parser b) : Parser (List a) :=
  first $ (sepby1 p sep) + (pure [])

#eval (sepby (char 'a') (char ',')).parse "a,a,b,c"
#eval (sepby (char 'a') (char ',')).parse "A,A,B,C"

mutual
  partial def chainl (p : Parser a) (op : Parser (a -> a -> a)) (x: a) : Parser a :=
    first $ (chainl1 p op) + (pure x)

  partial def chainl1 (p : Parser a) (op: Parser (a -> a -> a)) : Parser a :=
    do
      let x <- p
      rest x 
    where
      rest x := first $ (do
        let f <- op
        let y <- p
        rest $ f x y
      ) + pure x
end

def number := String.toNat! <$> String.mk <$> (many1 $ sat Char.isDigit)

#eval (chainl number ((fun _ => (.+.)) <$> item) 0).parse "10+10"
#eval (chainl number ((fun _ => (.+.)) <$> item) 0).parse "abc"
#eval (chainl1 number ((fun _ => (.+.)) <$> item)).parse "10+10"
#eval (chainl1 number ((fun _ => (.+.)) <$> item)).parse "abc"