syntax
syntax
コマンドは新しい構文を定義することができます。
import Lean
open Lean Parser
/-- `s : String` をパースして `Syntax` の項を得る。`cat` は構文カテゴリ。-/
def parse (cat : Name) (s : String) : MetaM Syntax := do
ofExcept <| runParserCategory (← getEnv) cat s
-- 最初は `#greet` などというコマンドは定義されていないので
-- そもそも Lean の合法な構文として認められない。
/- error: <input>:1:0: expected command -/
#eval parse `command "#greet"
-- `#greet` というコマンドのための構文を定義
syntax "#greet" : command
-- まだエラーになるが、少なくとも `#greet` というコマンドが Lean に認識されるようにはなった。
-- エラーメッセージは、`#greet` コマンドの解釈方法がないと言っている。
/- error: elaboration function for `«command#greet»` has not been implemented -/
#greet
Lean に構文を認識させるだけでなく、解釈させるには macro_rules
などの別のコマンドが必要です。
-- `#greet` コマンドの解釈方法を定める
macro_rules
| `(command| #greet) => `(#eval "Hello, Lean!")
/- info: "Hello, Lean!" -/
#greet
パース優先順位
syntax
コマンドは Lean に新しい構文解析ルールを追加しますが、導入した構文が意図通りに解釈されないことがあります。
section
/-- `a = b as T` という構文を定義 -/
local syntax term " = " term " as " term : term
/-- `a = b as T` という構文を、型 `T` 上で `a = b` が成り立つと解釈させる -/
local macro_rules
| `(term| $a = $b as $c) => `(@Eq (α := $c) $a $b)
-- メタ変数の番号を表示しない
set_option pp.mvars false
-- `1 + (1 = 2)` だと認識されてしまっている
/- info: 1 + (1 = 2) : ?_ -/
#check (1 + 1 = 2 as Nat)
end
パース優先順位(parsing precedence) を設定することで、どの構文から順に解釈されるかを指定することができ、問題を修正できることがあります。このあたりは notation
コマンドと同様です。
section
-- 十分低いパース優先順位を設定する
local syntax:10 term:10 " = " term:10 " as " term:10 : term
local macro_rules
| `(term| $a = $b as $c) => `(@Eq (α := $c) $a $b)
-- 意図通りに構文解析が通るようになる
#guard (1 + 1 = 2 as Nat)
#guard (3 - 5 + 4 = 2 as Int)
-- Nat だと 3 - 5 = 0 となるので結果が変わる
#guard (3 - 5 + 4 = 4 as Nat)
end
name 構文
(name := ...)
という構文により、名前を付けることができます。名前を付けると、その名前で Lean.ParserDescr
の項が生成されます。実際、syntax
コマンドは Lean のパーサーを拡張するコマンドであるといえます。
-- 最初は存在しない
#check_failure (hogeCmd : ParserDescr)
-- `#hoge` というコマンドを定義する
-- `name` 構文で名前を付けることができる
syntax (name := hogeCmd) "#hoge" : command
-- 構文に対して付けた名前で、ParserDescr 型の項が生成されている
#check (hogeCmd : ParserDescr)
パーサー定義
syntax
コマンドや declare_syntax_cat
コマンドで生成された Lean のパーサーを利用して、String
を引数に取るようなパーサーを定義することができます。
具体例を挙げましょう。まず LeanByExample/Declarative/Syntax/Syntax.lean
というファイルを作成して次のように書きます。
/-- 2項演算の集合 -/
inductive Op where
/-- 加法 -/
| add
/-- 乗法 -/
| mul
deriving DecidableEq, Repr
/-- 数式 -/
inductive Arith where
/-- 数値リテラル -/
| val (n : Nat) : Arith
/-- 演算子の適用 -/
| app (op : Op) (lhs rhs : Arith) : Arith
deriving DecidableEq, Inhabited, Repr
section arith_syntax
/-- `Arith` のための構文カテゴリ -/
declare_syntax_cat arith
/-- `Arith` を見やすく定義するための構文 -/
syntax "[arith| " arith "]" : term
-- 数値リテラルは数式
syntax:max num : arith
-- 数式を `+` または `*` で結合したものは数式
-- `+` と `*` のパース優先順位を指定しておく
syntax:30 arith:30 " + " arith:31 : arith
syntax:35 arith:35 " * " arith:36 : arith
-- 数式を括弧でくくったものは数式
syntax:max "(" arith ")" : arith
end arith_syntax
macro_rules
| `([arith| $n:num ]) => `(Arith.val $n)
| `([arith| $l:arith + $r:arith]) => `(Arith.app Op.add [arith| $l] [arith| $r])
| `([arith| $l:arith * $r:arith]) => `(Arith.app Op.mul [arith| $l] [arith| $r])
| `([arith| ($e:arith) ]) => `([arith| $e ])
次に、LeanByExample/Declarative/Syntax/Environment.lean
というファイルを作成して次のように書きます。
import LeanByExample.Declarative.Syntax.Syntax
import Lean
open Lean
/-- import先のファイル名 -/
private def fileName : Name := `LeanByExample.Declarative.Syntax.Syntax
/-- `Arith`のための構文とマクロの定義が終わった直後の状態の`Environment` -/
initialize env_of_arith_stx : Environment ← do
initSearchPath (← findSysroot) -- コンパイル時にLeanにoleanファイルを見つけさせるために必要
importModules #[{module := fileName}] {} (loadExts := true)
そうすると、以下のように Lean のパーサーとマクロ展開ルールを利用して String
上のパーサーを定義することができます。
import LeanByExample.Declarative.Syntax.Environment
open Lean Elab Term Command
/-- Leanのマクロ展開ルールを使って、`input : String` から `Arith` の項を生成する -/
def TermElabM.parseArith (input : String) : TermElabM (Except String Arith) := do
let stx := Parser.runParserCategory env_of_arith_stx `term s!"[arith| {input}]"
match stx with
| .error err => return Except.error err
| .ok stx =>
let result ← unsafe evalTerm Arith (.const ``Arith []) stx
return Except.ok result
/-- `TermElabM` に包まれた値をむりやり取り出す -/
unsafe def TermElabM.unsafeRun {α : Type} [Inhabited α] (env : Environment) (m : TermElabM α) : α :=
let core := liftCommandElabM <| liftTermElabM m
let ctx : ContextInfo := { env := env, fileMap := ⟨"", #[]⟩, ngen := { } }
let io := ContextInfo.runCoreM ctx core
match unsafeIO io with
| .error e => panic! s!"{e}"
| .ok a => a
/-- 文字列をパースして`Arith`の項を生成する -/
def parseArith (s : String) : Except String Arith := unsafe
TermElabM.unsafeRun env_of_arith_stx (TermElabM.parseArith s)
open Arith
-- パーサーのテスト
#guard
let expected := app Op.add (val 1) (val 2)
let actual := parseArith "1 + 2"
match actual with
| Except.error _ => false
| Except.ok actual =>
expected == actual
#guard
let expected := app Op.mul (val 3) (app Op.add (val 4) (val 5))
let actual := parseArith "3 * (4 + 5)"
match actual with
| Except.error _ => false
| Except.ok actual =>
expected == actual