Monadic parser combinators, in Lean

This repository contains an implementation in Lean 3 of monadic parser combinators, as described in the paper Monadic parsing in Haskell (Hutton-Meijer, 1998).

We make some modifications: parsers are a special case of state_t and we replace the list monad with the tactic monad.

Examples

Parsing arithmetic expressions

For comparison, here is the final example from the paper (a parser for evaluating arithmetic expressions), redone in Lean:

meta mutual def parse_addop,parse_mulop,parse_digit,parse_factor,parse_term,parse_expr
with parse_addop                : string → tactic ((ℤ → ℤ → ℤ) × string)
| arg := (symb "+" >> return (+) <|> symb "-" >> return (λ x y : ℤ, x - y)).run arg
with parse_mulop                : string → tactic ((ℤ → ℤ → ℤ) × string)
| arg := (symb "*" >> return (*) <|> symb "/" >> return (λ x y : ℤ, x / y)).run arg
with parse_digit                : string → tactic (ℤ × string)
| arg := (token $ digit').run arg
with parse_factor               : string → tactic (ℤ × string)
| arg := (mk parse_digit <|> do symb "(", e <- (mk parse_expr), symb ")", return e).run arg
with parse_term                 : string → tactic (ℤ × string)
| arg := (chainl1 (mk parse_factor) (mk parse_mulop)).run arg
with parse_expr                 : string → tactic (ℤ × string)
| arg := (chainl1 (mk parse_term) (mk parse_addop)).run arg

meta def calculator : parser_tactic ℤ := mk parse_expr

run_cmd calculator.run' "(2 * (3 + 5 + (2 * 2)))"
-- 24

run_cmd calculator.run' "9 - 9 * 0 * 3 + 4 - 7"
-- 6

Parsing lists into trees

To demonstrate the flexibility of parser combinators, it’s quite easy to adapt the technique in the previous example to build a parser which constructs a labelled tree from an arbitrarily nested list:

inductive my_tree : Type
| node : option string → my_tree
| join : list my_tree → option string → my_tree
open my_tree

meta instance : has_to_format my_tree := ⟨my_tree_format⟩

meta mutual def my_tree_parser₁,my_tree_parser₂
with my_tree_parser₁ : string → tactic (my_tree × string)
| arg := ((do int <- (fail_if_nil $ delimiter'' "(" ")"),
               ts  <- (run_parser (mk my_tree_parser₂) int),
               return (my_tree.join ts none))
            <|>
           (do x <- not_str ",",
               return $ my_tree.node x)).run arg
with my_tree_parser₂ : string → tactic (list my_tree × string)
| arg := (sepby (mk my_tree_parser₁) (symb ",")).run arg

meta def my_tree_parser : parser_tactic my_tree := mk my_tree_parser₁

run_cmd my_tree_parser.run' "(a, b, c)"
/- {• || a   |  b   |  c } -/

run_cmd my_tree_parser.run' "(a,(b,c))"
/- {• || a   |  {• || b   |  c }} -/

run_cmd my_tree_parser.run' "((a,b),c)"
/- {• || {• || a   |  b }  |  c } -/

run_cmd my_tree_parser.run' "(a, b, c, (d, e), f)"
/- {• || a   |  b   |  c   |  {• || d   |  e }  |  f } -/