Repr
Repr
は、その型の項をどのように表示するかを指示する型クラスです。
たとえば、以下のように新しく構造体 Point
を定義したとき、特に何も指定しなければ Point
の項を #eval
で表示することはできません。
-- 平面上の点を表す構造体
structure Point (α : Type) : Type where
x : α
y : α
-- 原点
def origin : Point Nat := ⟨0, 0⟩
/--
error: expression
origin
has type
Point Nat
but instance
Lean.Eval (Point Nat)
failed to be synthesized, this instance instructs Lean on how to display the resulting value,
recall that any type implementing the `Repr` class also implements the `Lean.Eval` class
-/
#guard_msgs in #eval origin
エラーメッセージが示すように、これは Point
が型クラス Lean.Eval
のインスタンスではないからです。エラーメッセージには、Repr
クラスのインスタンスであれば自動的に Lean.Eval
のインスタンスにもなることが書かれています。通常、Lean.Eval
のインスタンスを手で登録することはなく、Repr
インスタンスによって自動生成させます。
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
あるいは、ToString
クラスのインスタンスがあればそこから Lean.Eval
クラスのインスタンスも生成されて、表示に使われるので、それを利用しても良いでしょう。
-- `ToString` クラスのインスタンスがあれば、`Lean.Eval` のインスタンスが生成できる
example {α : Type} [ToString α] : Lean.Eval α := inferInstance
/-- `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