Merge pull request #1327 from lean-ja/Seasawher/issue1318

`ToString` の例が不適切

Author: Seasawher

LeanByExample/TypeClass/ToString.lean

@@ -1,64 +1,62 @@
 /-
 # ToString
-`ToString` は、文字列への変換を行う型クラスです。
+`ToString` は、文字列 `String` への変換方法を提供する型クラスです。`ToString` のインスタンスになっている型の項は、`toString` 関数で文字列に変換することができます。
 -/
-namespace ToString --#
+import Lean --#
 
-structure Point (α : Type) where
-  x : α
-  y : α
+/-- 標準ライブラリの `List` を真似て作った自前のリスト -/
+inductive MyList (α : Type) where
+  | nil : MyList α
+  | cons (hd : α) (tl : MyList α) : MyList α
 
-def origin : Point Int := ⟨0, 0⟩
+namespace MyList
 
--- 文字列補完により文字列に変換しようとしても、
--- 最初はどう変換したらいいのかわからないのでエラーになる
-/--
-error: failed to synthesize
-  ToString (Point Int)
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
--/
-#guard_msgs (error) in #check s!"{origin}"
-
-/-- `ToString` のインスタンスを登録する -/
-instance : ToString (Point Int) where
-  toString p := s!"Point: ({p.x}, {p.y})"
+  variable {α : Type}
 
--- これで文字列に変換できる
-/-- info: "Point: (0, 0)" -/
-#guard_msgs in #eval s!"{origin}"
+  /-- リストをリストらしく `"[a₁, a₂, ..., aₙ]"` という文字列に変換する
+  **注意**: `ToString.toString` と紛らわしいことがあるので `protected` で修飾している
+  -/
+  protected def toString [ToString α] : MyList α → String
+    | nil => "[]"
+    | ls@(cons _hd _tail) =>
+      "[" ++ helper ls ++ "]"
+  where
+    /-- 外側の括弧抜きでリストの中身を `,` でつないで表示する -/
+    helper : MyList α → String
+      | nil => ""
+      | cons hd .nil => toString hd
+      | cons hd tail => toString hd ++ ", " ++ helper tail
 
-/- ## Repr と ToString
+  instance [ToString α] : ToString (MyList α) where
+    toString := MyList.toString
 
-[`Repr`](./Repr.md) のインスタンスはないが、`ToString` のインスタンスはあるという状態で `#eval` しようとすると、`Repr` の代わりに `ToString` のインスタンスが使用されます。`Repr` のインスタンスを与えればそちらが優先して使用されます。-/
+  -- `toString` が正しく動作しているかテスト
+  #guard (toString <| MyList.cons 1 (MyList.nil)) = "[1]"
+  #guard (toString <| MyList.cons 1 (MyList.cons 2 (MyList.nil))) = "[1, 2]"
 
-/-- info: Point: (0, 0) -/
-#guard_msgs in #eval origin
+end MyList
 
--- `Repr` のインスタンスを自動生成して登録する
--- 以降は、`#eval` 時には `Repr` のインスタンスが使用される
-deriving instance Repr for Point
 
-/-- info: { x := 0, y := 0 } -/
-#guard_msgs in #eval origin
 
-/- 逆に、`Repr` のインスタンスはあるが、`ToString` のインスタンスがないとき、`ToString` の代わりに `Repr` が呼び出されることはありません。エラーになります。-/
+/- ## Repr と ToString の違い
 
-structure Person where
-  name : String
-  age : Nat
-deriving Repr
+[`Repr`](#{root}/TypeClass/Repr.md) と [`ToString`](#{root}/TypeClass/ToString.md) はどちらも項の表示に関わる型クラスですが、使い分けのルールが存在しており、それは `Repr` のドキュメントコメントに書かれています。
+-/
 
-def david := Person.mk "David" 42
+open Lean Elab Command in
 
--- #eval はできる
-#eval david
+/-- ドキュメントコメントを取得して表示するコマンド -/
+elab "#doc " x:ident : command => do
+  let name ← liftCoreM do realizeGlobalConstNoOverload x
+  if let some s ← findDocString? (← getEnv) name then
+  logInfo m!"{s}"
 
--- `ToString` のインスタンスがないのでエラーになる
 /--
-error: failed to synthesize
-  ToString Person
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+info: A typeclass that specifies the standard way of turning values of some type into `Format`.
+
+When rendered this `Format` should be as close as possible to something that can be parsed as the
+input value.
 -/
-#guard_msgs (error) in #check s!"{david}"
+#guard_msgs in #doc Repr
 
-end ToString --#
+/- `Repr` の出力は Lean のコードとしてパース可能なものに可能な限り近くなければならない、つまり Lean のコードとして実行可能であることが期待されます。一方で、`ToString` は単なる `String` への変換であってそのような制約はありません。 -/