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 を引数に取るようなパーサーを定義することができます。¹

具体例を挙げましょう。まず 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 ])

次に、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

このコード例を用意するにあたって、伊勢村哲司さんおよび Adam Topaz さんにご助力をいただきました。ありがとうございました。 ↩

Lean by Example

syntax

パース優先順位

name 構文

パーサー定義