Lean の処理パイプライン

Lean が .lean ファイルを読むときの流れは，大まかには次のようになります． これは概念図であり，実装が常にこの順にファイル全体を一括処理するという意味ではありません．

文字列としてのソースコード
  ↓ parsing
抽象構文木 Syntax
  ↓ macro expansion
展開後の Syntax
  ↓ elaboration
コア言語の式 Expr
  ↓ kernel checking
カーネルに受理された定義・定理
  ↓ serialization / compilation
.olean, .ilean, C code, native object など

実際には，ファイル全体を一度に処理するというより，トップレベルの command ごとに 「構文解析，マクロ展開，エラボレーション，カーネル検査」が進みます． ある command によって新しい記法や定義が追加されると，次の command はその更新後の環境で解釈されます．

また，マクロ展開はエラボレーションから完全に独立した前処理ではありません． Reference の言い方では，macro expansion は elaboration の一部であり， 外側の構文を展開してからその層をエラボレートし，内側に残ったマクロはエラボレータがそこに到達したときに展開されます． したがって，上の図の「macro expansion -> elaboration」は，学習用に分けて見せた模式的な区分です．

この図の各段階で現れるものは，おおよそ次のように考えるとよいです．

段階	実体	見方
文字列としてのソースコード	.lean ファイルや標準入力から渡される Unicode 文字列です．まだ Lean の構文木ではありません．	エディタで開く，cat LeanMathNote/basic/chapter06.lean で見る，lake env lean --stdin に文字列を渡す．
抽象構文木 Syntax	parser が作る Lean.Syntax 型の値です．記号列の木構造とソース位置は持ちますが，型や意味はまだ決まっていません．	Lean.Parser.runParserCategory を使うと，小さな文字列を Syntax にできます．
展開後の Syntax	macro expansion によって，表面構文をより基本的な構文へ置き換えた後の Syntax です．型づけ済みの式ではなく，まだ構文です．	syntax，macro，macro_rules で自分でマクロを定義できます．全ファイルの展開後構文を普段の開発で直接見ることはあまりありません．
コア言語の式 Expr	term elaborator が作る Lean.Expr 型の値です．暗黙引数，型クラス，overload，tactic などが解決された，カーネルが検査する対象に近い式です．	#check，#reduce，#print，set_option pp.all true で pretty printer 越しに見ることができます．メタプログラムでは Lean.Elab.Term.elabTerm が Expr を返します．
カーネルに受理された定義・定理	Environment に登録された定数情報です．名前，型，定義本体や定理の証明項などが ConstantInfo として保存されます．	#check name，#print name，#print axioms name，メタプログラムでは Environment.find? で調べます．

処理を行う実体も分けておくと，どこをユーザーが拡張できるかが見えやすくなります．

処理	行う実体	ユーザーが触れるもの
parsing	Lean の parser です．parser table は import 済みの構文拡張や開いている namespace の影響を受けます．	syntax，notation で新しい構文を追加できます．小さな例なら Parser.runParserCategory で parser を直接呼べます．
macro expansion	elaborator から呼ばれる macro expander です．syntax kind から macro 実装を探し，Syntax を別の Syntax に変換します．	macro，macro_rules，notation で拡張できます．macro の実装は概念的には Syntax -> MacroM Syntax です．
elaboration	command elaborator，term elaborator，tactic elaborator です．構文を解釈し，環境を更新し，Expr や証明項を作ります．	普通の def，theorem，tactic はここを使います．高度な用途では elab，elab_rules，自作 tactic で拡張できます．
kernel checking	Lean の信頼されるカーネルです．エラボレータが作った定義や証明項がコア型理論の規則に従うか検査します．	ユーザーがカーネル自体を Lean コードから拡張することは通常ありません．def，theorem，inductive を書くと，追加前に検査されます．
serialization	検査済みの環境や対話用情報をファイルへ保存する処理です．module を再利用するための .olean などが作られます．	lake build や lean の実行で発生します．ユーザーは通常，生成物を直接編集せず，import や leanchecker を通して利用します．

#check Lean.Syntax
#check Lean.Expr
#check Lean.Environment

Syntax は parser が作る構文木です． Expr はエラボレータが作る，Lean のコア型理論に近い式です． Environment は，これまでに宣言された定義，定理，記法，型クラスインスタンス，属性などを保持する環境です． 実際の対話環境では，これに加えて proof state，識別子の位置，補完候補などの情報も記録され， VS Code などのフロントエンドがそれを利用します．

ここでいう「コア」は，Lean Language Reference の core type theory や core language に対応する語です． ユーザーが書く Lean コードそのものを指すのではなく，エラボレータが作り，カーネルが検査するための小さな型理論を指します． したがって，def，theorem，match，tactic script，型クラス探索，暗黙引数の補完，記法やマクロなどは，そのままコア型理論の構成要素ではありません． これらはユーザー向けの表面構文やエラボレーションの仕組みであり，最終的には Expr として表されるコア言語の項へ変換されます． また，実行ファイルを作るための compiler intermediate representation や C code，native object も，コア型理論そのものではなく，コンパイルのための別の表現です． この区別により，Lean は便利な表面構文を持ちながら，信頼するカーネルを小さく保てます．