---
tags: lean
---
# `Lean.Data.Parsec` 使用

首先關鍵是了解 `Parsec` 型別的定義

abbrev Parsec a := String.Iterator -> Parsec.ParseResult a

## `tryP`

然後就可以了解要讓 parser 不一定運行的方式就是套用上一個 `Iterator`

def tryP (p : Parsec a) : Parsec (Option a) := λ it =>
  match p it with
  | .success rem a => .success rem a
  | .error _ _ => .success it .none

這裡運行 `p` 之後要是失敗就還是給 `.success` 但是

1. 把 `a` 包裝成 `Option a`，好在失敗之後使用 `.none` 表示嘗試失敗
2. 用原本的 `it` 而非運算後的 `rem` 流，等於復原到套用 `p` 之前的狀態

## 優先級運算式解析問題

在遞歸下降分析器裡面解析二元運算式的第一個問題就是左遞迴，傳統上我們把 expression 語法分成 term 跟 expr 等等不同層級來解決這個問題。這裡的解決方式並無不同，`binary` 需要多取用一個 `tm` parser 來解析比較優先的層級。而解析有優先級的運算子恰恰就需要一樣的結構，於是我們可以抽象出以下函數

def binary (opList : List $ Parsec (α → α → α)) (tm : Parsec α)
  : Parsec α := do
  let l ← tm
  let rs ← many opRhs
  return rs.foldl (fun lhs (bin, rhs) => (bin lhs rhs)) l
  where
    opRhs : Parsec $ (α → α → α) × α := do
      for findOp in opList do
        match ← tryP findOp with
        | .some f => return ⟨ f, ← tm ⟩
        | .none => continue
      fail "cannot match operator"

partial def mexpr : Parsec MExpr :=
  mterm
  |> binary [keyword "*" *> return .bin .mul, keyword "/" *> return .bin .div]
  |> binary [keyword "+" *> return .bin .add, keyword "-" *> return .bin .sub]

而具體解釋就是先 parse 一個 lhs term 然後再嘗試多次 operator + rhs（7 到 12 行）。最後使用 `foldl` 把多個的 operator + rhs 跟 lhs 合併成單一 expression。

使用的 API 善用了 `|>`，所以每個 operator 都會回傳自己用來組合出對應 expression 的構造函數

> 這裡 `.bin` 是 `MOp -> MExpr -> MExpr -> MExpr`，所以要給的就是 `return .bin op`

最方便的地方就是套用順序就是解析優先度，越上方越優先。此外這個方法容易擴展，在這裡就有前綴運算子的實現，基本上就是試試所有 operator 並使用第一個。其後解析一個 term 再根據是否有遇到運算子進行構造

> 註：也有可能 `opList` 全部不 match 故最後還是要檢查 `op.isSome`

def «prefix» (opList : List $ Parsec (α → α)) (tm : Parsec α)
  : Parsec α := do
  let mut op := .none
  for findOp in opList do
    op ← tryP findOp
    if op.isSome then break
  let e ← tm
  match op with
  | .none => return e
  | .some f => return f e