14.3. 記法（Notations）🔗

記法 （notation）という用語は Lean では2つの意味で用いられます：アイデアを簡潔に書き記すという一般的な概念を指す場合と、少ないコードで便利に記法を実装できる言語機能の名前です。カスタム演算子のように、Lean の記法は項の文法を新しい形で拡張することができます。しかし、記法はより汎用的です：新しい構文では、必要なキーワードや演算子と下位の項を自由に混在させることができ、優先順位レベルをより正確に制御することができます。記法はまた、結果として得られる部分項のパラメータを並べ替えることができますが、その一方で中置演算子は固定された順序でパラメータを関数項に与えます。記法は前置・中置・後置を混在して使用する演算子を定義することができるため、それらを mixfix 演算子と呼ぶことができます。

command ::= ...
    | A `docComment` parses a "documentation comment" like `/-- foo -/`. This is not treated like
a regular comment (that is, as whitespace); it is parsed and forms part of the syntax tree structure.

A `docComment` node contains a `/--` atom and then the remainder of the comment, `foo -/` in this
example. Use `TSyntax.getDocString` to extract the body text from a doc string syntax node. docComment?
      attributes?
      `attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`. attrKind notation(:prec)? ((name := ident))? ((priority := prio))? notationItem* => term

notationItem ::=
    str

notationItem ::= ...
    | ident(:prec)?

演算子の宣言と同様に、新しい構文を操作している間はドキュメントコメントの内容がユーザに表示されます。 inherit_doc 属性を追加すると、記法が展開される項の先頭にある関数のドキュメントコメントが新しい構文にコピーされます。他の属性を追加して、結果の定義に他のコンパイル時のメタプログラムを呼び出すことができます。

記法は セクションスコープ と属性や演算子と同様に相互作用します。デフォルトでは、記法はそれが確立されたモジュールをインポートした任意のモジュールで遷移的に利用可能です。しかし、scoped または local と宣言することで、それぞれ現在の名前空間が開かれているコンテキストか、現在の セクションスコープ に限定することができます。

演算子と同様に、 ローカル最長一致規則 が記法をパースする際に使用されます。もし複数の記法が最長一致で並んだ場合、宣言された優先順位によってどのパース結果が適用されるかが決定されます。それでもあいまいさが解消されない場合、すべてが保存され、エラボレータはそれらすべてを試行し、ちょうど1つがエラボレートできたときに成功することが期待されます。

単一の演算子についてその配置と字句を示す代わりに、記法の本体の宣言は 記法アイテム （notation item）の列から構成されます。これは新しい アトム （if や #eval などのキーワードと => ・ + ・ ↗ ・ ⟦ ・ ⋉ などの記号の両方を含む）、または項の位置です。演算子と同様に、文字列リテラルはアトムの配置を指定します。文字列の先頭と末尾の空白はパースに影響しませんが、空白を入れた場合 証明状態 やエラーメッセージで構文を表示する時に Lean が対応する位置に空白が挿入されます。識別子は項が予想される位置を示し、対応する項を記法の展開に挿入できるように名前を付けます。

カスタム演算子には単一の優先順位の表記がありますが、記法には多くの優先順位の表記があります。パースされる各項と同様に、記法自体にも優先順位があります。記法の優先順位はどのコンテキストでパースされるかを決定します：パーサは少なくとも現在のコンテキストと同程度の優先順位を持つプロダクションのパースを試みます。例えば、乗算は加算よりも優先順位が高いため、パーサは加算の引数をパースしている間に乗算の中置項のパースを試みますが、その逆は行いません。パースされる各項の優先順位は、その中でどの他のプロダクションが出現するかを決定します。

記法自体に優先順位が与えられていない場合、デフォルト値は記法の形式によって異なります。記法がアトム（文字列リテラルで表される）出は自杏里、アトムで終わる場合、デフォルトの優先順位は max となります。これは1つのアトムだけで構成される記法と、最初と最後のアイテムが両方ともアトムである複数のアイテムを持つ記法にも適用されます。それ以外の場合、記法全体のデフォルトの優先順位は lead となります。項である記法アイテムに対して優先順位が与えられない場合、デフォルトの優先順位は min になります。

必須の二重矢印（ Lean.Parser.Command.notation : command=> ）に続いて記法がその展開される内容と共に提供されます。演算子は常にその関数を演算子の引数に順番に適用することで展開されますが、記法はその項アイテムを展開内の任意の位置に置くことができます。項は名前によって参照されます。項アイテムは展開の中で何度も出現することができます。記法の展開はエラボレーションやコード生成の前に行われる純粋に構文的な処理であるため、展開で項が複製されると、結果の項が評価される時に計算が重複したり、モナドで作業する際には副作用が重複したりする可能性があります。

5

#eval ignore (2 +expected term) 5

<example>:1:17: expected term

def e : Nat × Int :=
(2 + 2, 2 + 2)

展開がグローバル環境で定義された関数の適用で構成され、記法の各項がちょうど1回出現する場合、 unexpander が生成されます。この新しい記法は 証明状態 ・エラーメッセージ・その他の Lean からの出力にて、マッチする関数適用項が表示される場合に表示されます。カスタム演算子と同様に、Lean はもとの項がその記法で使われていたかどうかを追跡しません；これは Lean の出力にていたるところで用いられます。