付録：オプション

オプションはメタプログラムと Lean のコンパイラの両方に特別な設定を伝える機能です。基本的にこれは KVMap であり、Name から Lean.DataValue への単純なマップです。現在、6種類のデータ値を有します：

  • String
  • Bool
  • Name
  • Nat
  • Int
  • Syntax

set_option コマンドを使うことで、とても簡単に Lean コンパイラにプログラムに対して何か違うことを行うように指示するオプションを設定することができます：

import Lean
open Lean

#check 1 + 1 -- 1 + 1 : Nat

set_option pp.explicit true -- No custom syntax in pretty printing

#check 1 + 1 -- @HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) 1 1 : Nat

set_option pp.explicit false

さらに、オプションの値をすぐ次のコマンドや項だけに限定することもできます：

set_option pp.explicit true in
#check 1 + 1 -- @HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) 1 1 : Nat

#check 1 + 1 -- 1 + 1 : Nat

#check set_option trace.Meta.synthInstance true in 1 + 1 -- the trace of the type class synthesis for `OfNat` and `HAdd`

もし今すぐ利用可能なオプションを取り出したい場合は、set_option コマンドを実行し、カーソルをその名前が書かれている場所に移動するだけで、自動補完の候補としてそれらのオプションのリストが表示されるでしょう。メタ関連でデバッグをしているときに最も役に立つオプションは trace. から始まるものです。

メタプログラミングにおけるオプション

これでオプションを設定する方法がわかったので、メタプログラムがオプションにアクセスする方法を見てみましょう。最も一般的な方法は MonadOptions 型クラスを通じたもので、これは Monad に関数 getOptions : m Options を拡張したものです。現時点でこれは以下に対して実装されています：

  • CoreM
  • CommandElabM
  • LevelElabM
  • 上記のいずれかの操作を持ち上げることができるすべてのモナド（例えば、CoreM から MetaM）

一度 Options オブジェクトを取得すれば、Options.get を使って情報を照会することができます。これを示すために、pp.explicit の値を表示するコマンドを書いてみましょう。

elab "#getPPExplicit" : command => do
  let opts ← getOptions
  -- defValue = default value
  logInfo s!"pp.explicit : {opts.get pp.explicit.name pp.explicit.defValue}"

#getPPExplicit -- pp.explicit : false

set_option pp.explicit true in
#getPPExplicit -- pp.explicit : true

pp.explicit を取得するた実際の実装である Lean.getPPExplicit は代わりに pp.all がデフォルト値として設定されているかどうかを使用することに注意してください。

独自のオプションを作る

独自のオプションを宣言するのも非常に簡単です。Lean コンパイラはこのために register_option というマクロを用意しています。実際に使ってみましょう：

register_option book.myGreeting : String := {
  defValue := "Hello World"
  group := "pp"
  descr := "just a friendly greeting"
}

しかし、初期化の制約があるため、宣言したオプションをそのまま同じファイルで使うことはできません。