syntax
syntax
コマンドは新しい構文を定義することができます。
import Lean
open Lean Parser
/-- parse できるかどうかチェックする関数 -/
def checkParse (cat : Name) (s : String) : MetaM Unit := do
if let .error s := runParserCategory (← getEnv) cat s then
throwError s
-- 最初は `#greet` などというコマンドは定義されていないので
-- そもそも Lean の合法な構文として認められない。
/-- error: <input>:1:0: expected command -/
#guard_msgs (error) in
#eval checkParse `command "#greet"
-- `#greet` というコマンドのための構文を定義
syntax "#greet" : command
-- `#greet` というコマンドが Lean に認識されるようになった。
-- エラーメッセージは、`#greet` コマンドの解釈方法がないと言っている。
/-- error: elaboration function for 'Syntax.«command#greet»' has not been implemented -/
#guard_msgs in #greet
Lean に構文を認識させるだけでなく、解釈させるには macro_rules
などの別のコマンドが必要です。
-- `#greet` コマンドの解釈方法を定める
macro_rules
| `(command| #greet) => `(#eval "Hello, Lean!")
パース優先順位
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)
-- `Nat` と `Prop` を足すことはできないというエラーメッセージ。
-- `1 + (1 = 2)` だと認識されてしまっているようだ。
/--
warning: failed to synthesize
HAdd Nat Prop ?_
Additional diagnostic information may be available using the `set_option diagnostics true` command.
-/
#guard_msgs (warning) in
#check_failure (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)
#guard (2 * 3 / 2 = 3 as Rat)
end