結合優先度の取得

概要

Lean 4 で、infix、infixl、infixr によって定義された二項演算子の優先順位を、Lean のコードから取得する方法のメモです。
重要な点は、演算子の優先順位は、その演算を実装する関数ではなく、演算子の構文宣言である Lean.ParserDescr に記録されていることです。

優先順位を取得する

infix 系のコマンドによって生成された構文宣言は、通常 Lean.ParserDescr.trailingNode です。
その第2引数に演算子自身の優先順位が格納されています。

import Lean
open Lean
def infixPrecedence? : ParserDescr → Option Nat
  | .trailingNode _ precedence _ _ => some precedence
  | _ => none

組み込みの演算子に対して実行すると、次のようになります。

#eval infixPrecedence? «term_+_»
-- some 65
#eval infixPrecedence? «term_*_»
-- some 70
#eval infixPrecedence? «term_^_»
-- some 80

ParserDescr.trailingNode の引数は、概略として次のように解釈できます。

trailingNode 構文ノード名 演算子の優先順位 左辺の優先順位 残りのパーサ

したがって、上の関数では第2引数を取り出しています。

独自演算子の場合

独自演算子について同じ処理を行う場合は、構文宣言に明示的な名前を付けておくと扱いやすくなります。

import Lean
open Lean
def combine (x y : Nat) : Nat :=
  x + y
infixl:57 (name := combineOp) " ⊛ " => combine
def infixPrecedence? : ParserDescr → Option Nat
  | .trailingNode _ precedence _ _ => some precedence
  | _ => none
#eval infixPrecedence? combineOp
-- some 57

ここで combineOp は、演算を実装する関数 combine の名前ではなく、演算子のパーサ拡張に付けた名前です。
名前を省略した場合、Lean は次のような名前を自動生成します。

«term_⊛_»

ただし、自動生成される名前の具体的な規則には依存しない方がよいため、メタプログラミングから参照する演算子には (name := ...) を指定するのが安全です。

結合性について

infix、infixl、infixr の違いは、演算子自身の優先順位に加えて、左辺と右辺に要求される優先順位として表現されます。
優先順位を p とすると、それぞれ概略として次のように展開されます。

宣言	左辺の優先順位	右辺の優先順位
infix:p	p + 1	p + 1
infixl:p	p	p + 1
infixr:p	p + 1	p
例えば、左結合の + は次のような構造です。

演算子の優先順位: 65
左辺の優先順位:   65
右辺の優先順位:   66

一方、右結合の ^ は次のような構造です。

演算子の優先順位: 80
左辺の優先順位:   81
右辺の優先順位:   80

この情報まで調べれば、通常の infix 系宣言については結合性も判定できます。
ただし、右辺の優先順位は ParserDescr の本体部分を解析する必要があります。任意の syntax や複雑な notation が常に同じ構造になるとは限らないため、一般的な構文宣言を対象とする場合は注意が必要です。

注意点

演算を実装する関数からは取得できない

例えば + は通常 HAdd.hAdd に展開されますが、優先順位は HAdd.hAdd 自体の情報ではありません。
同じ関数に対して、異なる優先順位を持つ複数の記法を定義することもできます。
そのため、次のような問い合わせは一般には定義できません。

-- HAdd.hAdd の優先順位を取得する

問い合わせの対象にする必要があるのは関数ではなく、演算子の構文宣言です。

演算子の文字列だけでは一意に決まらない

Lean では、同じ演算子文字列に対して複数の構文宣言を定義できます。
例えば、既存の + と同じ文字列を使った別の演算子を追加することも可能です。
したがって、単なる文字列 "+" から一意の優先順位を取得することは一般にはできません。構文宣言の名前、または ParserDescr 自体を指定する必要があります。

まとめ

二項演算子の優先順位をコードから取得する場合は、その演算を実装する関数ではなく、infix 系コマンドが生成した Lean.ParserDescr を調べます。
最小限の実装は次のとおりです。

import Lean
open Lean
def infixPrecedence? : ParserDescr → Option Nat
  | .trailingNode _ precedence _ _ => some precedence
  | _ => none
#eval infixPrecedence? «term_+_»
-- some 65

独自演算子を後からメタプログラミングで参照する場合は、宣言時に構文名を明示しておくのがよさそうです。

infixl:57 (name := combineOp) " ⊛ " => combine

参考資料

• Lean Language Reference: Custom Operators
• Lean API Documentation

The issue contains a Japanese memo about retrieving Lean operator precedence from Lean.ParserDescr, but it names no target file, test, or documentation entry point. Start by locating the repository’s documentation structure and checking how such articles are incorporated; done should mean the memo is placed in the appropriate location and its examples and reference links are verified.