エラボレーション

エラボレータは、ユーザが目にする Syntax をコンパイラの他の部分がそれを処理できるようなものに変換するコンポーネントです。ほとんどの場合、これは Syntax を Expr に変換することを意味しますが、#check や #eval のような他の使用例もあります。このためエラボレータは非常に大きなコードとなっており、ここ に格納されています。

コマンドのエラボレーション

コマンドは Syntax の最上位レベルであり、Lean ファイルはコマンドのリストで構成されます。最もよく使われるコマンドは宣言であり、例えば以下です：

  • def
  • inductive
  • structure

しかし、これ以外にもコマンドは存在しており、特筆すべきなものとして #check や #eval などのタイプです。すべてのコマンドは command という構文カテゴリに属しているため、カスタムコマンドを宣言するには、その構文をそのカテゴリに登録する必要があります。

コマンドに意味を与える

次のステップは構文にセマンティクスを与えることです。コマンドの場合、これはいわゆるコマンドエラボレータを登録することで行われます。

コマンドエラボレータは CommandElab という型を持っており、これは Syntax → CommandElabM Unit という型のエイリアスです。これがすることは、コマンドが呼ばれた際に期待されるものを表現した Syntax を取り、CommandElabM モナド上の副作用を生み出します。最終的な戻り値は Unit です。CommandElabM モナドには主に4種類の副作用があります：

  1. Monad を拡張した MonadLog と AddMessageContext を使って #check のようにユーザにメッセージをログ出力する。これは Lean.Elab.Log にある関数で行われ、特に有名なものは logInfo・logWarning・logError です。
  2. Monad を拡張した MonadEnv を使って Environment とやり取りする。これはコンパイラに関連するすべての情報が格納される場所であり、すべての既知の宣言・その型・ドキュメント文字列・値などが格納されています。現在の環境は getEnv で取得でき、更新は setEnv で設定できます。ここで Environment に情報を追加するにあたっては setEnv のラッパーである addDecl などを用いることが大体において正しい方法であることに注意してください。
  3. IO の実行。CommandElabM はあらゆる IO 操作を実行することができます。例えば、ファイルを読み込んでその内容に基づいて宣言を行うことができます。
  4. 例外の送出。このモナドはどんな IO でも実行できるため、例外を throwError で投げることは自然です。

さらに、CommandElabM がサポートする Monad の拡張はほかにもたくさんあります：

  • マクロと同じような Syntax quotation 用の MonadRef と MonadQuotation
  • オプションのフレームワークとのやり取りのための MonadOptions
  • デバッグトレースの情報のための MonadTrace
  • TODO: 関連性があるかどうかはわかりませんが、他にもいくつかあります。Lean.Elab.Command のインスタンスを参照してください。

コマンドのエラボレーション

さて、コマンドエラボレータの種類を理解したところで、エラボレーションのプロセスが実際にどのように機能するのかを簡単に見てみましょう。

  1. 現在の Syntax に適用できるマクロがあるかどうかをチェックする。適用可能なマクロがあり、例外が投げられなければ、結果の Syntax がコマンドとして再帰的にエラボレートされます。
  2. マクロを適用できない場合は、エラボレートする Syntax の SyntaxKind に対して登録されているすべての CommandElab を検索する。これは command_elab 属性を使用して登録されています。
  3. これらの CommandElab はすべて unsupportedSyntaxException を投げるものが出現するまで順番に試行されます。これは、そのエラボレータがこの特定の Syntax の構築に対して「責任を負っている」ことを示す Lean 流の方法です。これらのエラボレータは何かが間違っていることをユーザに示すために通常の例外を投げうることに注意してください。責任を持つエラボレータが見つからない場合、コマンドのエラボレーションは unexpected syntax エラーメッセージとともに中断されます。

見てわかるように、この手順の背後にある一般的な考え方は通常のマクロ展開とよく似ています。

自分用のものを作る

これで CommandElab とは何か、そしてそれがどのように使われるかわかったので、次は自分用のものを作る方法に着目します。そのための手順は上で学んだとおりです：

  1. 構文を定義する
  2. エラボレータを定義する
  3. command_elab 属性を用いて、構文を担当するエラボレータを登録する。

これがどのように実現されるか見てみましょう：

import Lean

open Lean Elab Command Term Meta

syntax (name := mycommand1) "#mycommand1" : command -- declare the syntax

@[command_elab mycommand1]
def mycommand1Impl : CommandElab := fun stx => do -- declare and register the elaborator
  logInfo "Hello World"

#mycommand1 -- Hello World

これは少々ボイラープレート的だと思われるかもしれませんが、Lean の開発者もそう思っていたようです。そこで彼らはこれのためのマクロを追加しました！

elab "#mycommand2" : command =>
  logInfo "Hello World"

#mycommand2 -- Hello World

コマンドのエラボレーションは同じ構文に対して複数のエラボレータの登録をサポートしているため、必要な時には実は構文のオーバーロードが可能である点に注意してください。

@[command_elab mycommand1]
def myNewImpl : CommandElab := fun stx => do
  logInfo "new!"

#mycommand1 -- new!

さらに、unsupportedSyntaxException を投げることで、構文の一部だけをオーバーロードすることも可能で、その場合はデフォルトのハンドラに処理させるか、elab コマンドに処理を処理をまかせます。

以下の例では、元の #check 構文を拡張しているのではなく、この特定の構文のために新しい SyntaxKind を追加しています。しかし利用者からすれば、このコマンドの効果は基本的に同じです。

elab "#check" "mycheck" : command => do
  logInfo "Got ya!"

これは実際にはオリジナルの #check を拡張したものです。

@[command_elab Lean.Parser.Command.check] def mySpecialCheck : CommandElab := fun stx => do
  if let some str := stx[1].isStrLit? then
    logInfo s!"Specially elaborated string literal!: {str} : String"
  else
    throwUnsupportedSyntax

#check mycheck -- Got ya!
#check "Hello" -- Specially elaborated string literal!: Hello : String
#check Nat.add -- Nat.add : Nat → Nat → Nat

ミニプロジェクト

この節の最後のミニプロジェクトとして、実際に役立つコマンドエラボレータを作ってみましょう。これはコマンドを受け取り、elabCommand（コマンドのエラボレーションのエントリポイント）と同じメカニズムを使って、与えたコマンドに関連するマクロやエラボレータを教えてくれます。

しかし、実際に elabCommand を再実装する労力は省きます。

elab "#findCElab " c:command : command => do
  let macroRes ← liftMacroM <| expandMacroImpl? (←getEnv) c
  match macroRes with
  | some (name, _) => logInfo s!"Next step is a macro: {name.toString}"
  | none =>
    let kind := c.raw.getKind
    let elabs := commandElabAttribute.getEntries (←getEnv) kind
    match elabs with
    | [] => logInfo s!"There is no elaborators for your syntax, looks like its bad :("
    | _ => logInfo s!"Your syntax may be elaborated by: {elabs.map (fun el => el.declName.toString)}"

#findCElab def lala := 12 -- Your syntax may be elaborated by: [Lean.Elab.Command.elabDeclaration]
#findCElab abbrev lolo := 12 -- Your syntax may be elaborated by: [Lean.Elab.Command.elabDeclaration]
#findCElab #check foo -- even our own syntax!: Your syntax may be elaborated by: [mySpecialCheck, Lean.Elab.Command.elabCheck]
#findCElab open Hi -- Your syntax may be elaborated by: [Lean.Elab.Command.elabOpen]
#findCElab namespace Foo -- Your syntax may be elaborated by: [Lean.Elab.Command.elabNamespace]
#findCElab #findCElab open Bar -- even itself!: Your syntax may be elaborated by: [«_aux_lean_elaboration___elabRules_command#findCElab__1»]

TODO: 今すぐには何も思い浮かばないが、# スタイルではないコマンド、つまり宣言を示すミニプロジェクトも追加すべきかもしれない。 TODO: lemma/theorem に似ているが、自動的に sorry してくれる conjecture 宣言を定義する。sorry は「推測」が真であると予想されることを反映するために、カスタムのものにすることもできる。

項のエラボレーション

項はある種の Expr を表す Syntax オブジェクトです。項エラボレータは私たちが書くコードのほとんどを処理するものです。特に、定義や型（これらも単なる Expr であるため）など、すべての値をエラボレートします。

すべての項は term 構文カテゴリに属しています（この動作はマクロの章ですでに見ています）。したがって、カスタムの項を宣言するには、その構文をこのカテゴリに登録する必要があります。

項に意味を与える

コマンドのエラボレーションと同様に、次のステップは構文にセマンティクスを与えることです。項の場合、これはいわゆる項エラボレータを登録することで行われます。

項エラボレータは TermElab という型を持っており、これは Syntax → Option Expr → TermElabM Expr という型のエイリアスです。この型の時点ですでにコマンドのエラボレーションとはかなり異なっています：

  • コマンドのエラボレーションと同様に、この Syntax はユーザがこの項を作成するために使用したものです。
  • Option Expr は期待される項の型ですが、これは常にわかるとは限らないため、Option 引数となっています。
  • コマンドのエラボレーションとは異なり、項のエラボレーションはその副作用によって実行されるだけでなく、TermElabM Expr が戻り値には実際の興味の対象、つまりその Syntax オブジェクトを表す Expr を含んでいます。

TermElabM は基本的にすべての点で CommandElabM をアップグレードしたものです：これは上述したものをすべてに加えてさらに2つの機能をサポートしています。一つ目は非常にシンプルです：IO コードを実行することに加えて、MetaM のコードも実行することができるため、Expr をうまく構築することができます。2つ目はエラボレーションのループという項に特化したものです。

項のエラボレーション

項のエラボレーションの基本的なアイデアはコマンドのエラボレーションと同じです：マクロを展開し、term_elab 属性によって Syntax に登録された項エラボレータを全て完了するまで再帰的に実行します（term_elab 属性が項のエラボレーションを実行することもあります）。しかし、項エラボレータが実行中にできる特別なアクションが1つあります。

項エラボレータは Except.postpone を投げることがあります。これは項エラボレータが作業を続けるためにさらなる情報を必要としていることを示します。この不足している情報を表現するために、Lean はいわゆる synthetic metavariable を使用します。以前からご存じのように、メタ変数は埋められることを待っている Expr の穴です。synthetic metavariable はそれを解決するための特別なメソッドを持っている点で異なっており、SyntheticMVarKind に登録されています。現時点では4種類あります：

  • typeClass、メタ変数は型クラスの統合で解決される
  • coe、メタ変数は強制によって解決される（型クラスの特殊なケース）
  • tactic、メタ変数はタクティクの項であり、タクティクを実行することで解決される
  • postponed、Except.postpone で生成される

このような synthetic metavariable が作成されると、次の上位レベルの項エラボレータが継続されます。ある時点で延期されたメタ変数の実行は、その実行が完了できる望みができた時に項エラボレータによって再開されます。次の例でこれを実際に見てみましょう：

#check set_option trace.Elab.postpone true in List.foldr .add 0 [1,2,3] -- [Elab.postpone] .add : ?m.5695 → ?m.5696 → ?m.5696

ここで起こったことは、関数適用のエラボレータがジェネリックな関数である List.foldr に対して開始し、暗黙の型パラメータのメタ変数を作成したことです。そして最初の引数 .add をエラボレートしようとしました。

.name がどのように機能するかご存じでない方のために説明しておくと、基本的な考え方は大体（今回のケースのように）Lean が関数（今回の場合は Nat.add）の出力型（今回の場合は Nat）を推測できるべきというものです。このような場合、.name 機能は名前空間 Nat で name という名前の関数を単純に検索します。これはある型のコンストラクタをその名前空間を参照したり開いたりすることなく使用したい場合に特に便利ですが、上記のように使用することもできます。

さて、例に戻ると Lean はこの時点で .add が型 ?m1 → ?m2 → ?m2（ここで ?x はメタ変数の記法です）を持つ必要があることを知っています。.add のエラボレータは ?m2 の実際の値を知る必要があるため、項エラボレータは実行を延期します（これは .add の代わりに内部的に synthetic metavariable を作成することで行われます）。他の2つの引数のエラボレーションによって ?m2 が Nat でなければならないという事実が得られるため、.add のエラボレータが続行されると、この情報を使ってエラボレーションを完了することができます。

また、これがうまくいかないケースを引き起こすことも簡単にできます。例えば：

#check_failure set_option trace.Elab.postpone true in List.foldr .add
-- [Elab.postpone] .add : ?m.5808 → ?m.5809 → ?m.5809
-- invalid dotted identifier notation, expected type is not of the form (... → C ...) where C is a constant
  -- ?m.5808 → ?m.5809 → ?m.5809

この場合、.add はまず実行を延期し、その後再び呼び出されましたが、エラボレーションを終えるのに十分な情報を持っていなかったことで失敗しました。

自分用のものを作る

新しい項エラボレータの追加は、新しいコマンドエラボレータの追加と基本的に同じように機能するため、ごく簡単に見ておきましょう：

syntax (name := myterm1) "myterm 1" : term

def mytermValues := [1, 2]

@[term_elab myterm1]
def myTerm1Impl : TermElab := fun stx type? =>
  mkAppM ``List.get! #[.const ``mytermValues [], mkNatLit 0] -- `MetaM` code

#eval myterm 1 -- 1

-- `elab` も機能する
elab "myterm 2" : term => do
  mkAppM ``List.get! #[.const ``mytermValues [], mkNatLit 1] -- `MetaM` code

#eval myterm 2 -- 2

小さなプロジェクト

本章の最後のミニプロジェクトとして、最もよく使われる Lean の構文糖衣の1つである ⟨a,b,c⟩ 記法を単一コンストラクタ型のショートハンドとして再現します：

-- オリジナルと紛らわしくならないようにちょっとだけ変えている
syntax (name := myanon) "⟨⟨" term,* "⟩⟩" : term

def getCtors (typ : Name) : MetaM (List Name) := do
  let env ← getEnv
  match env.find? typ with
  | some (ConstantInfo.inductInfo val) =>
    pure val.ctors
  | _ => pure []

@[term_elab myanon]
def myanonImpl : TermElab := fun stx typ? => do
  -- 型がわからないメタ変数である場合、実行を延期しようとする。
  -- メタ変数は関数のエラボレータのように、それらが何であるか解明するための情報が
  -- まだ十分手に入れられない際に暗黙のパラメータの値を埋めるために用いられる。
  -- 項エラボレータが実行を延期できるのは一度だけであるため、エラボレータが無限ループに陥ることはない。
  -- 従って、ここでは実行の延期だけを試みるが、そうしないと例外を引き起こすかもしれない。
  tryPostponeIfNoneOrMVar typ?
  -- もし延期しても型が見つからなかった場合はエラーとなる。
  let some typ := typ? | throwError "expected type must be known"
  if typ.isMVar then
    throwError "expected type must be known"
  let Expr.const base .. := typ.getAppFn | throwError s!"type is not of the expected form: {typ}"
  let [ctor] ← getCtors base | throwError "type doesn't have exactly one constructor"
  let args := TSyntaxArray.mk stx[1].getSepArgs
  let stx ← `($(mkIdent ctor) $args*) -- syntax quotations
  elabTerm stx typ -- call term elaboration recursively

#check (⟨⟨1, sorry⟩⟩ : Fin 12) -- { val := 1, isLt := (_ : 1 < 12) } : Fin 12
#check_failure ⟨⟨1, sorry⟩⟩ -- expected type must be known
#check_failure (⟨⟨0⟩⟩ : Nat) -- type doesn't have exactly one constructor
#check_failure (⟨⟨⟩⟩ : Nat → Nat) -- type is not of the expected form: Nat -> Nat

最後の注釈として、elab 構文の糖衣構文を代わりに使うことで、延期の動作を短くすることができます：

-- この `t` 構文は `myanonImpl` の最初の2行を効果的に実行する。
elab "⟨⟨" args:term,* "⟩⟩" : term <= t => do
  sorry

演習問題

  1. 以下のコードについて考えてみましょう。syntax + @[term_elab hi]... : TermElab の組み合わせの代わりに elab だけを使って書き換えてください。

    syntax (name := hi) term " ♥ " " ♥ "? " ♥ "? : term

@[term_elab hi]
def heartElab : TermElab := fun stx tp =>
  match stx with
    | `($l:term ♥) => do
      let nExpr ← elabTermEnsuringType l (mkConst `Nat)
      return Expr.app (Expr.app (Expr.const `Nat.add []) nExpr) (mkNatLit 1)
    | `($l:term ♥♥) => do
      let nExpr ← elabTermEnsuringType l (mkConst `Nat)
      return Expr.app (Expr.app (Expr.const `Nat.add []) nExpr) (mkNatLit 2)
    | `($l:term ♥♥♥) => do
      let nExpr ← elabTermEnsuringType l (mkConst `Nat)
      return Expr.app (Expr.app (Expr.const `Nat.add []) nExpr) (mkNatLit 3)
    | _ =>
      throwUnsupportedSyntax

  2. 以下は実際の mathlib のコマンド alias から抜粋した構文です。

    syntax (name := our_alias) (docComment)? "our_alias " ident " ← " ident* : command

    これについて alias hi ← hello yes で ← の牛との識別子、つまり「hello」と「yes」を出力するようにしたいです。

    これらのセマンティクスを追加してください：

    a) syntax + @[command_elab alias] def elabOurAlias : CommandElab を使用する b) syntax + elab_rules を使用する c) elab を使用する

  3. 以下は実際の mathlib の nth_rewrite から抜粋した構文です。

    open Parser.Tactic
syntax (name := nthRewriteSeq) "nth_rewrite " (config)? num rwRuleSeq (ppSpace location)? : tactic

    これについて nth_rewrite 5 [←add_zero a] at h でユーザが場所を指定した場合は "rewrite location!" を、場所を指定しなかった場合は "rewrite target!" を出力するようにしたいです。

    これらのセマンティクスを追加してください：

    a) syntax + @[command_elab alias] def elabOurAlias : CommandElab を使用する b) syntax + elab_rules を使用する c) elab を使用する