chore: do not use internal append in ToString instances for basic types (#12885)

This PR shifts some material in `Init` to make sure that the `ToString`
instances of basic types don't rely on `String.Internal.append`.

src/Init/Data/Array/Basic.lean

@@ -2151,7 +2151,4 @@ protected def repr {α : Type u} [Repr α] (xs : Array α) : Std.Format :=
 instance {α : Type u} [Repr α] : Repr (Array α) where
   reprPrec xs _ := Array.repr xs
 
-instance [ToString α] : ToString (Array α) where
-  toString xs := String.Internal.append "#" (toString xs.toList)
-
 end Array

src/Init/Data/ByteArray/Basic.lean

@@ -469,5 +469,3 @@ def prevn : Iterator → Nat → Iterator
 
 end Iterator
 end ByteArray
-
-instance : ToString ByteArray := ⟨fun bs => bs.toList.toString⟩

src/Init/Data/FloatArray/Basic.lean

@@ -9,6 +9,7 @@ prelude
 public import Init.Data.Float
 import Init.Ext
 public import Init.GetElem
+public import Init.Data.ToString.Extra
 
 public section
 universe u

src/Init/Data/Rat/Basic.lean

@@ -11,6 +11,7 @@ public import Init.Data.OfScientific
 public import Init.Data.Int.DivMod.Basic
 public import Init.Data.String.Defs
 public import Init.Data.ToString.Macro
+public import Init.Data.ToString.Extra
 import Init.Data.Hashable
 import Init.Data.Int.DivMod.Bootstrap
 import Init.Data.Int.DivMod.Lemmas

src/Init/Data/SInt/Basic.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Data.UInt.Basic
+public import Init.Data.ToString.Extra
 
 @[expose] public section
 

src/Init/Data/Slice/Array/Iterator.lean

@@ -10,6 +10,7 @@ public import Init.Data.Slice.Operations
 import all Init.Data.Range.Polymorphic.Basic
 import Init.Omega
 public import Init.Data.Array.Subarray
+public import Init.Data.ToString.Extra
 
 public section
 

src/Init/Data/Slice/List/Iterator.lean

@@ -11,6 +11,7 @@ public import Init.Data.Iterators.Producers.List
 public import Init.Data.Iterators.Combinators.Take
 import all Init.Data.Range.Polymorphic.Basic
 public import Init.Data.Slice.Operations
+public import Init.Data.ToString.Extra
 
 public section
 

src/Init/Data/ToString.lean

@@ -9,3 +9,4 @@ prelude
 public import Init.Data.ToString.Basic
 public import Init.Data.ToString.Macro
 public import Init.Data.ToString.Name
+public import Init.Data.ToString.Extra

src/Init/Data/ToString/Basic.lean

@@ -51,29 +51,6 @@ instance {p : Prop} : ToString (Decidable p) := ⟨fun h =>
   | Decidable.isTrue _  => "true"
   | Decidable.isFalse _ => "false"⟩
 
-/--
-Converts a list into a string, using `ToString.toString` to convert its elements.
-
-The resulting string resembles list literal syntax, with the elements separated by `", "` and
-enclosed in square brackets.
-
-The resulting string may not be valid Lean syntax, because there's no such expectation for
-`ToString` instances.
-
-Examples:
-* `[1, 2, 3].toString = "[1, 2, 3]"`
-* `["cat", "dog"].toString = "[cat, dog]"`
-* `["cat", "dog", ""].toString = "[cat, dog, ]"`
--/
-protected def List.toString [ToString α] : List α → String
-  | [] => "[]"
-  | [x] => String.Internal.append (String.Internal.append "[" (toString x)) "]"
-  | x::xs => String.push (xs.foldl (fun l r => String.Internal.append (String.Internal.append l ", ") (toString r))
-      (String.Internal.append "[" (toString x))) ']'
-
-instance {α : Type u} [ToString α] : ToString (List α) :=
-  ⟨List.toString⟩
-
 instance : ToString PUnit.{u+1} :=
   ⟨fun _ => "()"⟩
 
@@ -89,11 +66,6 @@ instance : ToString Nat :=
 instance : ToString String.Pos.Raw :=
   ⟨fun p => Nat.repr p.byteIdx⟩
 
-instance : ToString Int where
-  toString
-    | Int.ofNat m   => toString m
-    | Int.negSucc m => String.Internal.append "-" (toString (succ m))
-
 instance (n : Nat) : ToString (Fin n) :=
   ⟨fun f => toString (Fin.val f)⟩
 

src/Init/Data/ToString/Extra.lean

@@ -0,0 +1,43 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Leonardo de Moura
+-/
+module
+
+prelude
+public import Init.Data.String.Defs
+
+public section
+
+/--
+Converts a list into a string, using `ToString.toString` to convert its elements.
+
+The resulting string resembles list literal syntax, with the elements separated by `", "` and
+enclosed in square brackets.
+
+The resulting string may not be valid Lean syntax, because there's no such expectation for
+`ToString` instances.
+
+Examples:
+* `[1, 2, 3].toString = "[1, 2, 3]"`
+* `["cat", "dog"].toString = "[cat, dog]"`
+* `["cat", "dog", ""].toString = "[cat, dog, ]"`
+-/
+protected def List.toString [ToString α] : List α → String
+  | [] => "[]"
+  | [x] => "[" ++ toString x ++ "]"
+  | x::xs => String.push (xs.foldl (fun l r => l ++ ", " ++ toString r) ("[" ++ (toString x))) ']'
+
+instance {α : Type u} [ToString α] : ToString (List α) :=
+  ⟨List.toString⟩
+
+instance [ToString α] : ToString (Array α) where
+  toString xs := "#" ++ (toString xs.toList)
+
+instance : ToString ByteArray := ⟨fun bs => bs.toList.toString⟩
+
+instance : ToString Int where
+  toString
+    | Int.ofNat m   => toString m
+    | Int.negSucc m => "-" ++ toString (m + 1)

src/Init/Omega/Constraint.lean

@@ -52,6 +52,11 @@ namespace Constraint
 private local instance : Append String where
   append := String.Internal.append
 
+private local instance : ToString Int where
+  toString
+    | Int.ofNat m   => toString m
+    | Int.negSucc m => "-" ++ toString (m + 1)
+
 instance : ToString Constraint where
   toString := private fun
   | ⟨none, none⟩ => "(-∞, ∞)"

src/Init/Omega/LinearCombo.lean

@@ -41,6 +41,14 @@ private def join (l : List String) : String :=
 private local instance : Append String where
   append := String.Internal.append
 
+private local instance : ToString Int where
+  toString
+    | Int.ofNat m   => toString m
+    | Int.negSucc m => "-" ++ toString (m + 1)
+
+private local instance : Append String where
+  append := String.Internal.append
+
 instance : ToString LinearCombo where
   toString lc := private
     s!"{lc.const}{join <| lc.coeffs.toList.zipIdx.map fun ⟨c, i⟩ => s!" + {c} * x{i+1}"}"

src/Lean/Data/KVMap.lean

@@ -8,6 +8,7 @@ module
 prelude
 public import Init.Data.Format.Syntax
 public import Init.Data.ToString.Name
+public import Init.Data.ToString.Extra
 
 public section
 

src/Lean/Data/OpenDecl.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Data.ToString.Name
+public import Init.Data.ToString.Extra
 
 public section