Elaborator

Lean 4でのElaboratorというものについて

Lean 4のコンパイル処理過程でElaborationという過程が出てくる

Leanのソースコードをパースした結果Syntaxオブジェクトが作られて、その結果をElaboratorがEraborationして、Exprオブジェクトが作られる

Elaboratorの訳の候補はいくつかある

精緻化器

推敲器

詳細化器

IdrisでもElaboratorは出てくる

おそらく衛生的マクロや柔軟な構文定義、

code:mermaid

flowchart LR

leanSyntaxObject -->|Elaboration| leanExprObject"Lean Expr object<br>(Abstract Syntax Tree)"

leanExprObject -->|Evaluation| CString"C String <br>"int a = 2;""

CString -->|C Compiler| binaryString"0100100"

構文解析(Parsing)で具象構文木(CST)を生成

Elaborationで抽象構文木(AST)を生成

評価(Evaluation)でC言語のコードを生成

Cコンパイラがバイナリコードを生成

確認用

Q. Elaborator

Q. なぜElaborationの過程が必要か

参考

調査用

Wikipedia.icon

Wikipedia.icon