抽象構文木

Lean の parser は，文字列を Syntax 型の木に変換します． これはまだ「意味づけ」されていません． たとえば x + y という構文だけを見ても，自然数の足し算か，群の演算か，行列の足し算かは分かりません． この段階では，記号の並びとその木構造が分かっているだけです．

Lean では parser や syntax がユーザー拡張可能です． notation，syntax，macro によって新しい表面構文を追加できます．

各 syntax node には kind があり，エラボレータやマクロ展開器はこの kind を手がかりに処理を選びます． また，parser から直接作られた syntax には元のソース位置や空白に関する情報も残るため， エラー表示，hover，ジャンプ，pretty printing などの基礎にもなります．

#check Lean.Syntax.getKind
#check Lean.Parser.runParserCategory

#eval show CoreM Unit from do
  let result := Lean.Parser.runParserCategory (← getEnv) `term "x + y"
  match result with
  | .ok stx =>
      IO.println s!"kind = {Syntax.getKind stx}"
  | .error e =>
      IO.println e

Syntax.getKind は syntax node の種類を取り出す関数です． Parser.runParserCategory は，指定した parser category で文字列を解析するための関数です． 通常の証明では直接使いませんが，Lean のフロントエンドが「文字列から syntax tree を作る」ことを確認できます． 上の例では，term category として "x + y" を解析し，得られた syntax node の kind を表示しています． 木全体を見たい場合は，IO.println (repr stx) のように repr を出力すると，Syntax.node，Syntax.ident，Syntax.atom などの構造が見えます．