Repr
Repr
は、その型の項をどのように表示するかを指示する型クラスです。
たとえば、以下のように新しく構造体 Point
を定義したとき、何も指定しなくても Point
の項を #eval
で表示することはできますが、裏で使用しているのが Repr
インスタンスです。
-- 平面上の点を表す構造体
structure Point (α : Type) : Type where
x : α
y : α
-- 原点
def origin : Point Nat := ⟨0, 0⟩
-- Repr インスタンスを暗黙的に生成しない
set_option eval.derive.repr false
/--
error: could not synthesize a 'Repr' or 'ToString' instance for type
Point Nat
-/
#guard_msgs in #eval origin
エラーメッセージが示すように、Point
が型クラス Repr
または ToString
のインスタンスではないため #eval
が実行できずエラーになります。
Repr
インスタンスの登録方法ですが、通り一遍の表示で構わなければ deriving
コマンドで Lean に自動生成させることができます。
deriving instance Repr for Point
#eval origin
あるいは、Point
の定義時に以下のようにしても構いません。
structure Point (α : Type) : Type where
x : α
y : α
deriving Repr
def origin : Point Nat := ⟨0, 0⟩
#eval origin
deriving を使わない場合
Repr
のインスタンスは deriving
コマンドで生成できますが、手動で作ることもできます。
variable {α : Type}
/-- 入れ子になったリスト -/
inductive NestedList (α : Type) where
| elem : α → NestedList α
| list : List (NestedList α) → NestedList α
open Std
protected partial def NestedList.repr [Repr α] (a : NestedList α) (n : Nat) : Format :=
let _instToFormat : ToFormat (NestedList α) := ⟨(NestedList.repr · 0)⟩
match a, n with
| elem x, _ => reprPrec x n
| list as, _ => Format.bracket "[" (Format.joinSep as ("," ++ Format.line)) "]"
def sample : NestedList Nat :=
.list [.elem 1, .list [.elem 2, .elem 3], .elem 4]
/-- Repr インスタンスを登録 -/
local instance [Repr α] : Repr (NestedList α) where
reprPrec := NestedList.repr
/-- info: [1, [2, 3], 4] -/
#guard_msgs in #eval sample
また、Repr
インスタンスがなくても ToString
クラスのインスタンスがあればそれが表示に使われます。
/-- `NestedList` を文字列に変換 -/
partial def NestedList.toString [ToString α] : NestedList α → String
| NestedList.elem x => ToString.toString x
| NestedList.list xs => "[" ++ String.intercalate ", " (xs.map toString) ++ "]"
/-- `NestedList` の `ToString` インスタンスを宣言 -/
instance [ToString α] : ToString (NestedList α) where
toString nl := NestedList.toString nl
/-- info: [1, [2, 3], 4] -/
#guard_msgs in #eval sample