学习在 Lean4 中使用 Parser Combinator

此时对于我那幽默的《编译原理》课程还在用 C 语言写编译器的不满达到了顶峰。

你说得对，但是《编译原理》是由 Alfred V. Aho, Monica S. Lam, Ravi Sethi 和 Jeffrey D. Ullman 等人自主研发的一款全旧计算机世界编程游戏。游戏发生在一个被称作「C–」的简化语言，在这里，选择这门课的人将被迫享受「GCC 7.5.0」，没有一点 5202 年该有的体验。玩家将扮演一位名为「C 程序员」的神秘角色，在自由的编码中邂逅各种各样、时机诡异的 Segment Fault 们，和他们一起泄露内存，感受 C 语言的恶心之处——同时，逐步发掘「都 5202 年了这帮人还在拿 39 年前的书教文法分析」的真相。

但跑远了。总而言之这里介绍一种叫 parser combinator —— 解析器组合子的函数式手段，为您带来哪怕是手写递归下降也很舒适的体验（并非）

0. 介绍 ¶

Parser combinator（解析器组合子）是一种函数式编程中的技术，用于构建复杂语法分析器的工具。它的核心思想是：用小的、可组合的解析器函数构建更复杂的解析器。

一个 parser combinator 就是一个函数，它接受一些解析器作为输入，返回一个新的、更复杂的解析器。它是一种“组合模式”，非常适合处理递归文法。

一个经典的 Parser 可以是：

abbrev Parser (α : Type) := List Char → Option (α × List Char)

也就是说，一个 parser 就是是一个函数，接受 List Char 作为参数，如果解析成功，返回 .some (α × List Char) 为解析结果和剩余内容。如果失败，返回 .none.

在这里，为了一步到位地解决报错，我们把返回类型改成 Except

abbrev Parser (α : Type) := List Char → Except String (α × List Char)

这样，如果报错就能看到一个字符串作为错误信息。

对于不熟悉函数式写法的人，这是它的类似的 Rust 代码（懒得配平生命周期了）：

#![feature(type_alias_impl_trait)]

struct Parser<T>(Box<dyn FnOnce(&'static str) -> Result<(T, &'static str), String>>)
where
    T: 'static;

impl<T> Parser<T> {
    fn parse(self, input: &'static str) -> Result<(T, &'static str), String> {
        self.0(input)
    }
    fn chain<U>(self, other: Parser<U>) -> Parser<(T, U)>
    {
        let f = self.0;
        let g = other.0;
        (move |input: &'static str| {
            let (t, input) = f(input)?;
            let (u, input) = g(input)?;
            Ok(((t, u), input))
        })
        .into()
    }
}

impl<T, F> From<F> for Parser<T>
where
    F: FnOnce(&'static str) -> Result<(T, &'static str), String> + 'static
{
    fn from(value: F) -> Self {
        Parser(Box::new(value))
    }
}

fn char(c: char) -> Parser<char> {
    (move |input: &'static str| {
        if input.is_empty() {
            return Err("Input is empty".to_string());
        }
        if input.chars().next().unwrap() == c {
            Ok((c, &input[c.len_utf8()..]))
        } else {
            Err(format!("Expected '{}', found '{}'", c, input.chars().next().unwrap()))
        }
    })
    .into()
}

fn main() {
    let res = char('a').parse("anc");
    println!("Result: {:?}", res);
    let res = char('a').chain(char('b')).parse("anc");
    println!("Result: {:?}", res);
    let res = char('a').chain(char('b')).parse("abc");
    println!("Result: {:?}", res);

    // Result: Ok(('a', "nc"))
    // Result: Err("Expected 'b', found 'n'")
    // Result: Ok((('a', 'b'), "c"))
}

其中，chain 就是一个 combinator，它用两个小的 parser 合成了一个大的 parser。

1. 抽象 ¶

让我们再次请出万能的 Monad 来。关于 Monad 是什么，不妨看看所以这个 Monads 到底是什么啊之让我学学

一个 parser 的合成过程经常需要前面的 parse 都 ok，一旦其中某一个不是 ok 的了，就短路返回 error。这是典型的 monad 行为

instance : Monad Parser where
  pure := fun a =>
    fun input => .ok (a, input)
  bind := fun parser f =>
    fun input => do
      let (a, rest) ← parser input
      f a rest

实现了 monad 的特征以后，我们就能方便的使用 do-记号，如

def symbol : Parser $ Int :=
  fun input =>
    match input with
    | '+' :: xs => .ok (1, xs)
    | '-' :: xs => .ok (-1, xs)
    | xs => .ok (1, xs)

def digits : Parser $ List Char :=
  fun input =>
    .ok $ input.span (·.isDigit)

def parseInt : Parser Json := do
  let symbol ← symbol
  let numStr ← digits
  match numStr.asString.toInt? with
  | some n => return Json.int $ symbol * n
  | none   => fail "expected an integer, but got non-digit characters"

#eval parseInt "12345abced12345".data
-- Except.ok (Json.int 12345, ['a', 'b', 'c', 'e', 'd', '1', '2', '3', '4', '5'])

其次，一个 parser 还能实现 Alternative（选择子）。字面意义上地，

An Alternative functor is an Applicative functor that can “fail” or be “empty” and a binary operation <|> that “collects values” or finds the “left-most success”.

Important instances include

• Option, where failure := none and <|> returns the left-most some.
• Parser combinators typically provide an Applicative instance for error-handling and backtracking.

Error recovery and state can interact subtly. For example, the implementation of Alternative for OptionT (StateT σ Id) keeps modifications made to the state while recovering from failure, while StateT σ (OptionT Id) discards them.

关于函子 functor 的概念我推荐阅读图解 Functor、Applicative、Monad。这样，我们用

parser1 <|> parser2

就能描述“第一个解析成功的 parser”。

或许 parser 还适用一些别的抽象，但我也是刚学，想到写什么就放些什么了（）总而言之，让我们又双叒叕开启愉快的 JSON 解析之旅。

2. 实践：JSON 解析器 ¶

还是熟悉的 JSON

inductive Json where
  | null
  | bool (x: Bool)
  | int  (x: Int)
  | float(x: Float)
  | str  (x: String)
  | arr  (x: List Json)
  | obj  (x: List (String × Json))
deriving Repr

这次我们要正确地解析数字，所以引入了 int 和 float 类型。然后是准备工作：

abbrev Parser (α : Type) := List Char → Except String (α × List Char)

def fail (reason : String) : Parser α :=
  fun _ => .error reason
-- 无论如何总是返回失败原因的函数

instance : Monad Parser where
  pure := fun a =>
    fun input => .ok (a, input)
  bind := fun p f =>
    fun input => do
      let (a, rest) ← p input
      f a rest

instance : Alternative Parser where
  failure := fail "unknown error"
  orElse p₁ p₂ := fun input =>
      match p₁ input with
      | .ok    r => .ok r
      | .error _ => p₂ () input

接下来可以实践写几个辅助函数

-- 返回一个拿一个 char 的 parser
def char (c : Char) : Parser Char :=
   fun input =>
    match input with
    | x :: xs =>
      if x == c then
        .ok (c, xs)
      else .error s!"Expected '{c}', got '{x}'"
    | [] => .error s!"Unexpected EOF, expected character '{c}'"

-- 返回一个拿走前面的 whitespace 的 parser
def whitespaces : Parser Unit :=
  fun input =>
    .ok ((), input.dropWhile (·.isWhitespace))

-- 返回一个拿一个 + 或者 - 符号的 parser
def symbol : Parser $ Int :=
  fun input =>
    match input with
    | '+' :: xs => .ok (1, xs)
    | '-' :: xs => .ok (-1, xs)
    | xs => .ok (1, xs)

-- 返回一个拿数字的 parser
def digits : Parser $ List Char :=
  fun input =>
    .ok $ input.span (·.isDigit)

这样， number 的 parse 工作就变得很简单，只需要分两种情况：

def parseInt : Parser Json := do
  let symbol ← symbol
  let numStr ← digits
  match numStr.asString.toInt? with
  | some n => return Json.int $ symbol * n
  | none   => fail "expected an integer, but got non-digit characters"

def toFloat (num : List Char) (fraction : List Char) : Option Float := do
  let num ← num.asString.toNat?
  let fra ← fraction.asString.toNat?
  let exp := 0.1 ^ fraction.length.toFloat
  return num.toFloat + (fra.toFloat * exp)

def parseFloat : Parser Json := do
  let symbol ← symbol
  let num ← digits
  let _ ← char '.'
  let fraction ← digits
  match toFloat num fraction with
  | .some num => return Json.float $ if symbol == -1 then -num else num
  | .none => fail "expected a float"

def parseNumber : Parser Json := do
  parseFloat <|> parseInt

现在我们的 paserNumber 就是一个既可以解析整数又可以解析浮点数的 parser 了！

随后我们一鼓作气，把几个简单的 parser 写掉。先写字符串：

def quotedString : Parser $ List Char := do
  _ ← char '"'
  fun input =>
    let (str, last) := input.span (· != '"')
    .ok (str, last.drop 1)

def parseString : Parser Json := do
  let str ← quotedString
   return (Json.str str.asString)

为什么要分 quoted string 和 string 呢？因为后者直接得到了一个 Json，但我们还要在 object 那里复用获得字符串的 parser。

随后是几个关键字，异常简单：

def keyword (kw : String) (val : Json) : Parser Json :=
  fun input =>
    if input.asString.startsWith kw then
      .ok (val, input.drop kw.length)
    else .error s!"Expected keyword '{kw}', but got '{input.asString}'"

def parseTrue := keyword "true" $ Json.bool true
def parseFalse := keyword "false" $ Json.bool false
def parseNull := keyword "null" Json.null

现在是三个递归结构：

-- 这是一个辅助函数，用来把以 sep 分割的 a 生成一个 list parser
partial def sepBy (α : Parser a) (sep : Parser b) : Parser (List a) :=
  fun input =>
    let rec go (acc : List a) (input : List Char) : (List a × List Char) :=
      match α input with
      | .ok (a, rest) =>
        match sep rest with
        | .ok (_, rest') => go (acc.concat a) rest'
        | .error _ => (acc.concat a, rest)
      | .error _ => (acc, input)
    .ok $ go [] input

mutual
  partial def parseArray : Parser Json := do
    _ ← char '['
    _ ← whitespaces
    let elems ← sepBy parseJson (char ',')
    _ ← whitespaces
    _ ← char ']'
    return Json.arr elems

  partial def parseObject : Parser Json := do
    _ ← char '{'
    _ ← whitespaces
    let pairs ← sepBy parsePair (char ',')
    _ ← whitespaces
    _ ← char '}'
    return Json.obj pairs

  partial def parsePair : Parser (String × Json) := do
    _ ← whitespaces
    let key ← quotedString
    _ ← whitespaces
    _ ← char ':'
    let value ← parseJson
    return (key.asString, value)

  partial def parseJson : Parser Json := do
    let _ ← whitespaces
    let json ← fun str => match str with
      | 'n' :: _ => parseNull str
      | 't' :: _ => parseTrue str
      | 'f' :: _ => parseFalse str
      | '[' :: _ => parseArray str
      | '{' :: _ => parseObject str
      | '"' :: _ => parseString str
      | _ => parseNumber str
    let _ ← whitespaces
    return json
end

整个逻辑极其清晰和简单！这就是 parser combinator 的魅力。回顾我们之前写的 lean4 的 json 大概长这样

def parseJsonObject (fuel: Nat) (str: List Char) : Except String (List (String × Json) × List Char) := do
  match fuel with
  | 0 => .error "out of fuel"
  | .succ fuel =>
  let mut xs := trimList str
  let mut ret : List (String × Json) := []
  while true do
    match xs with
    | '"' :: next =>
      let (key, next) ← parseJsonString next
      xs := trimList next
      if xs.head? != some ':' then
        .error "expect `:` but got unexpected token"
      else
        xs := xs.tail
      let (val, next) ← parseJsonValue fuel xs
      ret := ret.append [(key, val)]
      match trimList next with
      | ',' :: next => xs := trimList next
      | '}' :: next =>
        return (ret, next)
      | x => .error $ "expect `,` or `}` but got unexpected token:" ++ String.mk x
    | '}' :: next =>
      return (ret, next)
    | x => .error $ "unexpected token:" ++ String.mk x
  return ([], xs.tail)
termination_by fuel

虽然比起抽象更少的 gleam 还是很不错，但对比 parser combinator 的做法：

partial def parseObject : Parser Json := do
  _ ← char '{'
  _ ← whitespaces
  let pairs ← sepBy parsePair (char ',')
  _ ← whitespaces
  _ ← char '}'
  return Json.obj pairs

partial def parsePair : Parser (String × Json) := do
  _ ← whitespaces
  let key ← quotedString
  _ ← whitespaces
  _ ← char ':'
  let value ← parseJson
  return (key.asString, value)

显然，所有人都看得出来， parser combinator 的做法非常简洁明了，可读性极强。

如果你正在编写一个传统的递归下降解析器来解析 JSON 数组，你可能会尝试在循环中解析语句，当它无法解析中间的逗号时停止。这个过程很难做到复用，除非你其实已经在写一个 parser combinator 了。比如我之前写的 C++ 的解析器：

class Object : public Node {
  using ObjectVT = std::unordered_map<std::string, JSON>;
  ObjectVT value_{};

public:
  Object() {};
  explicit Object(ObjectVT &&val) : value_(std::move(val)) {};
  Object(Object &&) = default;
  Object(const Object &) = delete; // 删掉拷贝构造函数
  Object &operator=(Object &&) = default;
  Object &operator=(const Object &) = delete;

  inline static std::unique_ptr<Object> parse(std::string_view &sv, int dep) {
    assert_depth(sv, dep);
    removeWhiteSpaces(sv);
    if (sv[0] != '{')
      throw getJSONParseError(sv, "object start `{`");
    sv.remove_prefix(1);
    removeWhiteSpaces(sv);
    ObjectVT val;
    bool isTComma = false; // 是不是尾随逗号
    while (sv[0] != '}') {
      auto key = String::parse(sv); // 解析 key
      if (ENABLE_DUMPLICATED_KEY_DETECT && val.contains(key->value())) {
        throw getJSONParseError(
            sv, ("unique key, but got dumplicated key `" + key->value() + "`")
                    .c_str());
      } else {
        removeWhiteSpaces(sv);
        if (sv[0] != ':') // 解析 key :
          throw getJSONParseError(sv, "object spliter `:`");
        sv.remove_prefix(1);
        val.insert({key->take(), JSON(Node::parse(sv, dep + 1))});
        removeWhiteSpaces(sv); // 解析 key : value
        switch (sv[0]) {
        case '}': // 看看结束了没
          sv.remove_prefix(1);
          return std::make_unique<Object>(std::move(val));
        case ',':
          sv.remove_prefix(1);
          isTComma = true;
          continue;
        default:
          throw getJSONParseError(sv, "object spliter `,` or object end `}`");
        }
      }
    }
    if (isTComma && !ENABLE_TRAILING_COMMA)
      throw getJSONParseError(sv, "next json value");
    sv.remove_prefix(1);
    return std::make_unique<Object>(std::move(val));
  }

  // ...
}

但如你所见，使用函数式语言 parser combinator 的话，定义一个复用的解析器极其简单

def arrayElems := sepBy parseJson (char ',')
def urlParams := sepBy (agg3 $ parseVar (char '=') parseVal) (char '&')