Zenn
Open5

Lean4のマクロで、文字列リテラルを、Lean4のコードとしてパースして展開する

lean4
denjirydenjiry

文字列リテラル "∀a b, a → b → a ∧ b" に対して、

theorem propA : myterm["∀a b, a → b → a ∧ b"] := 
  fun {a b : Prop} (ha : a) (hb : b) => ⟨ha,hb⟩

と定義することで、propAの型が∀a b, a → b → a ∧ bとなるようなマクロ（すなわち、文字列リテラルをLeanのコードとしてパースして展開するマクロmyterm["ここにLeanのコードを書く"]）をつくった。

denjirydenjiry

実装したコードは

elab "myterm[" s:str "]" : term => do
  let env ← getEnv
  let parsedSyntax ← match Lean.Parser.runParserCategory env `term s.getString with
                      | Except.ok stx => pure stx
                      | Except.error errmsg => throwError errmsg
  let prop ← elabTerm parsedSyntax none
  pure prop

https://github.com/denjiry/str2term

denjirydenjiry

背景

大目標は、文字列リテラルの中の日本語をLeanで証明すること。
日本語を自然言語処理して論理式に変換するソフトウェアはすでに存在するので、
残す作業は

  1. 外部のプロセスとの通信を行う方法
  2. Leanのコードが書いてある文字列リテラルをパースして、その場に展開する方法
  3. 上記２つをビルド前に行い、定理証明のときには出力された論理式を扱えるようにする方法

だった。いろいろ調べた結果、1. はIOモナド、2. はコンパイラの実装に使われている内部の関数たち、3. はElaboration（いわゆるマクロのうちの一つ）によって実現できることがわかった。
Elaboration（今回使用したのはTermElabMというモナド）はマクロのようなもので、IOモナドを含む様々な関数の実行をコンパイル前に行うため、定理証明のときには実行結果が利用できる。
2. を切り出すと表題のような処理になる。

denjirydenjiry

このコードの大半は2. の部分の処理で、Lean.Parser.runParserCategoryによって文字列リテラルをLean.Syntax（原始的な構文木）にパースしたあと、Lean.Elab.elabTermによってLean.Expr（マクロの展開などのメタプログラミングに関する処理が終了した、Leanのコアが処理可能な構文木）に変換する。