declare_syntax_cat

declare_syntax_cat コマンドは、新しい構文カテゴリを宣言するためのコマンドです。構文カテゴリを宣言することで、宣言した構文を再利用可能にして冗長な構文宣言を減らすことができます。

例として、集合の内包表記 {x : T | P x} を定義するコードを示します。

universe u

/-- `α` を全体集合とする部分集合の全体 -/
def Set (α : Type u) := α → Prop

variable {α : Type u}

/-- 項 `x : α` が `X : Set α` に属する -/
def Set.mem (X : Set α) (x : α) : Prop := X x

/-- `x ∈ X` と書けるようにする -/
instance : Membership α (Set α) where
  mem := Set.mem

/-- 述語 `p : α → Prop` から構成される集合 -/
def setOf (p : α → Prop) : Set α := p

/-- binder という構文カテゴリ。
これは変数束縛を表していて、
`{x : X | P x}` の `x : X` の部分とか
`{x ∈ X | P x}` の `x ∈ X` の部分とかを表している -/
declare_syntax_cat binder

/-- `{x : T | P x}` の `: T` の部分。
あってもなくても良いので `( )?` で囲う -/
syntax ident (" : " term)? : binder

/-- `{x ∈ T | P x}` の `∈ T` の部分。
あってもなくても良いので `( )?` で囲う -/
syntax ident (" ∈ " term)? : binder

/-- 集合の内包表記 -/
syntax "{" binder "|" term "}" : term

-- 合法な構文として認識される
-- 実装は与えていないのでエラーにはなる
#check_failure { x | x = 0}
#check_failure { x : Nat | x > 0 }
#check_failure { x ∈ T | x = 0}

/-- `{x : T | P x}` と `{x ∈ T | P x}` の形の式を `setOf` の式に変換する -/
macro_rules
  | `({ $var:ident | $body:term }) => `(setOf (fun $var => $body))
  | `({ $var:ident : $ty:term | $body:term }) => `(setOf (fun ($var : $ty) => $body))
  | `({ $var:ident ∈ $s:term | $body:term }) => `(setOf (fun $var => $var ∈ $s ∧ $body))

-- 内包表記が使えるようになった
#check { x : Nat | x > 0 }

#check
  let Even := { x : Nat | x % 2 = 0 }
  { x ∈ Even | x > 0 }