From 749e2063cf6a063dff57d136f7de47285dc8a3d7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 9 Oct 2020 14:37:56 -0700
Subject: [PATCH] feat: add interpolated string for `toString`

---
 src/Init/Control/Except.lean         |   2 +-
 src/Init/Data.lean                   |   1 +
 src/Init/Data/Array/Basic.lean       |   2 +-
 src/Init/Data/Basic.lean             |   2 +-
 src/Init/Data/Float.lean             |   2 +-
 src/Init/Data/Int/Basic.lean         |   2 +-
 src/Init/Data/ToString.lean          |  98 +------------------------
 src/Init/Data/ToString/Basic.lean    | 102 +++++++++++++++++++++++++++
 src/Init/Data/ToString/Macro.lean    |  17 +++++
 src/Init/System/IOError.lean         |   2 +-
 src/Init/Util.lean                   |   2 +-
 tests/lean/run/strInterpolation.lean |  12 ----
 12 files changed, 129 insertions(+), 115 deletions(-)
 create mode 100644 src/Init/Data/ToString/Basic.lean
 create mode 100644 src/Init/Data/ToString/Macro.lean

diff --git a/src/Init/Control/Except.lean b/src/Init/Control/Except.lean
index 7b40b0e916..bb8924fdf0 100644
--- a/src/Init/Control/Except.lean
+++ b/src/Init/Control/Except.lean
@@ -6,7 +6,7 @@ Authors: Jared Roesch, Sebastian Ullrich
 The Except monad transformer.
 -/
 prelude
-import Init.Data.ToString
+import Init.Data.ToString.Basic
 import Init.Control.Alternative
 import Init.Control.MonadControl
 import Init.Control.Id
diff --git a/src/Init/Data.lean b/src/Init/Data.lean
index faed6c9aad..a1baaba130 100644
--- a/src/Init/Data.lean
+++ b/src/Init/Data.lean
@@ -18,3 +18,4 @@ import Init.Data.UInt
 import Init.Data.Float
 import Init.Data.Option
 import Init.Data.Random
+import Init.Data.ToString
diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index ce205184f0..8a7530fc11 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -8,7 +8,7 @@ import Init.Data.Nat.Basic
 import Init.Data.Fin.Basic
 import Init.Data.UInt
 import Init.Data.Repr
-import Init.Data.ToString
+import Init.Data.ToString.Basic
 import Init.Control.Id
 import Init.Util
 universes u v w
diff --git a/src/Init/Data/Basic.lean b/src/Init/Data/Basic.lean
index e849e784b1..ea963f66b3 100644
--- a/src/Init/Data/Basic.lean
+++ b/src/Init/Data/Basic.lean
@@ -12,5 +12,5 @@ import Init.Data.String.Basic
 import Init.Data.Option.Basic
 import Init.Data.UInt
 import Init.Data.Repr
-import Init.Data.ToString
+import Init.Data.ToString.Basic
 import Init.Data.String.Extra
diff --git a/src/Init/Data/Float.lean b/src/Init/Data/Float.lean
index 77bb3294d3..6ed526daab 100644
--- a/src/Init/Data/Float.lean
+++ b/src/Init/Data/Float.lean
@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Core
-import Init.Data.ToString
+import Init.Data.ToString.Basic
 
 structure FloatSpec :=
 (float : Type)
diff --git a/src/Init/Data/Int/Basic.lean b/src/Init/Data/Int/Basic.lean
index 530bc98332..62ef3c9387 100644
--- a/src/Init/Data/Int/Basic.lean
+++ b/src/Init/Data/Int/Basic.lean
@@ -9,7 +9,7 @@ prelude
 import Init.Data.Nat.Basic
 import Init.Data.List
 import Init.Data.Repr
-import Init.Data.ToString
+import Init.Data.ToString.Basic
 open Nat
 
 /- the Type, coercions, and notation -/
diff --git a/src/Init/Data/ToString.lean b/src/Init/Data/ToString.lean
index 77c858f8f1..e5d7e81c79 100644
--- a/src/Init/Data/ToString.lean
+++ b/src/Init/Data/ToString.lean
@@ -4,99 +4,5 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
-import Init.Data.String.Basic
-import Init.Data.UInt
-import Init.Data.Nat.Div
-import Init.Data.Repr
-import Init.Control.Id
-open Sum Subtype Nat
-
-universes u v
-
-class HasToString (α : Type u) :=
-(toString : α → String)
-
-export HasToString (toString)
-
--- This instance is needed because `id` is not reducible
-instance {α} [HasToString α] : HasToString (id α) :=
-inferInstanceAs (HasToString α)
-
-instance {α} [HasToString α] : HasToString (Id α) :=
-inferInstanceAs (HasToString α)
-
-instance : HasToString String :=
-⟨fun s => s⟩
-
-instance : HasToString Substring :=
-⟨fun s => s.toString⟩
-
-instance : HasToString String.Iterator :=
-⟨fun it => it.remainingToString⟩
-
-instance : HasToString Bool :=
-⟨fun b => cond b "true" "false"⟩
-
-instance {p : Prop} : HasToString (Decidable p) :=
-⟨fun h => match h with
-  | Decidable.isTrue _  => "true"
-  | Decidable.isFalse _ => "false"⟩
-
-protected def List.toStringAux {α : Type u} [HasToString α] : Bool → List α → String
-| b,     []    => ""
-| true,  x::xs => toString x ++ List.toStringAux false xs
-| false, x::xs => ", " ++ toString x ++ List.toStringAux false xs
-
-protected def List.toString {α : Type u} [HasToString α] : List α → String
-| []    => "[]"
-| x::xs => "[" ++ List.toStringAux true (x::xs) ++ "]"
-
-instance {α : Type u} [HasToString α] : HasToString (List α) :=
-⟨List.toString⟩
-
-instance : HasToString Unit :=
-⟨fun u => "()"⟩
-
-instance : HasToString Nat :=
-⟨fun n => repr n⟩
-
-instance : HasToString Char :=
-⟨fun c => c.toString⟩
-
-instance (n : Nat) : HasToString (Fin n) :=
-⟨fun f => toString (Fin.val f)⟩
-
-instance : HasToString UInt8 :=
-⟨fun n => toString n.toNat⟩
-
-instance : HasToString UInt16 :=
-⟨fun n => toString n.toNat⟩
-
-instance : HasToString UInt32 :=
-⟨fun n => toString n.toNat⟩
-
-instance : HasToString UInt64 :=
-⟨fun n => toString n.toNat⟩
-
-instance : HasToString USize :=
-⟨fun n => toString n.toNat⟩
-
-def addParenHeuristic (s : String) : String :=
-if "(".isPrefixOf s || "[".isPrefixOf s || "{".isPrefixOf s || "#[".isPrefixOf s then s
-else if !s.any Char.isWhitespace then s
-else "(" ++ s ++ ")"
-
-instance {α : Type u} [HasToString α] : HasToString (Option α) :=
-⟨fun o => match o with | none => "none" | (some a) => "(some " ++ addParenHeuristic (toString a) ++ ")"⟩
-
-instance {α : Type u} {β : Type v} [HasToString α] [HasToString β] : HasToString (Sum α β) :=
-⟨fun s => match s with | (inl a) => "(inl " ++ addParenHeuristic (toString a) ++ ")" | (inr b) => "(inr " ++ addParenHeuristic (toString b) ++ ")"⟩
-
-instance {α : Type u} {β : Type v} [HasToString α] [HasToString β] : HasToString (α × β) :=
-⟨fun ⟨a, b⟩ => "(" ++ toString a ++ ", " ++ toString b ++ ")"⟩
-
-instance {α : Type u} {β : α → Type v} [HasToString α] [s : ∀ x, HasToString (β x)] : HasToString (Sigma β) :=
-⟨fun ⟨a, b⟩ => "⟨"  ++ toString a ++ ", " ++ toString b ++ "⟩"⟩
-
-instance {α : Type u} {p : α → Prop} [HasToString α] : HasToString (Subtype p) :=
-⟨fun s => toString (val s)⟩
+import Init.Data.ToString.Basic
+import Init.Data.ToString.Macro
diff --git a/src/Init/Data/ToString/Basic.lean b/src/Init/Data/ToString/Basic.lean
new file mode 100644
index 0000000000..25ffe204db
--- /dev/null
+++ b/src/Init/Data/ToString/Basic.lean
@@ -0,0 +1,102 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Leonardo de Moura
+-/
+prelude
+import Init.Data.String.Basic
+import Init.Data.UInt
+import Init.Data.Nat.Div
+import Init.Data.Repr
+import Init.Control.Id
+open Sum Subtype Nat
+
+universes u v
+
+class HasToString (α : Type u) :=
+(toString : α → String)
+
+export HasToString (toString)
+
+-- This instance is needed because `id` is not reducible
+instance {α} [HasToString α] : HasToString (id α) :=
+inferInstanceAs (HasToString α)
+
+instance {α} [HasToString α] : HasToString (Id α) :=
+inferInstanceAs (HasToString α)
+
+instance : HasToString String :=
+⟨fun s => s⟩
+
+instance : HasToString Substring :=
+⟨fun s => s.toString⟩
+
+instance : HasToString String.Iterator :=
+⟨fun it => it.remainingToString⟩
+
+instance : HasToString Bool :=
+⟨fun b => cond b "true" "false"⟩
+
+instance {p : Prop} : HasToString (Decidable p) :=
+⟨fun h => match h with
+  | Decidable.isTrue _  => "true"
+  | Decidable.isFalse _ => "false"⟩
+
+protected def List.toStringAux {α : Type u} [HasToString α] : Bool → List α → String
+| b,     []    => ""
+| true,  x::xs => toString x ++ List.toStringAux false xs
+| false, x::xs => ", " ++ toString x ++ List.toStringAux false xs
+
+protected def List.toString {α : Type u} [HasToString α] : List α → String
+| []    => "[]"
+| x::xs => "[" ++ List.toStringAux true (x::xs) ++ "]"
+
+instance {α : Type u} [HasToString α] : HasToString (List α) :=
+⟨List.toString⟩
+
+instance : HasToString Unit :=
+⟨fun u => "()"⟩
+
+instance : HasToString Nat :=
+⟨fun n => repr n⟩
+
+instance : HasToString Char :=
+⟨fun c => c.toString⟩
+
+instance (n : Nat) : HasToString (Fin n) :=
+⟨fun f => toString (Fin.val f)⟩
+
+instance : HasToString UInt8 :=
+⟨fun n => toString n.toNat⟩
+
+instance : HasToString UInt16 :=
+⟨fun n => toString n.toNat⟩
+
+instance : HasToString UInt32 :=
+⟨fun n => toString n.toNat⟩
+
+instance : HasToString UInt64 :=
+⟨fun n => toString n.toNat⟩
+
+instance : HasToString USize :=
+⟨fun n => toString n.toNat⟩
+
+def addParenHeuristic (s : String) : String :=
+if "(".isPrefixOf s || "[".isPrefixOf s || "{".isPrefixOf s || "#[".isPrefixOf s then s
+else if !s.any Char.isWhitespace then s
+else "(" ++ s ++ ")"
+
+instance {α : Type u} [HasToString α] : HasToString (Option α) :=
+⟨fun o => match o with | none => "none" | (some a) => "(some " ++ addParenHeuristic (toString a) ++ ")"⟩
+
+instance {α : Type u} {β : Type v} [HasToString α] [HasToString β] : HasToString (Sum α β) :=
+⟨fun s => match s with | (inl a) => "(inl " ++ addParenHeuristic (toString a) ++ ")" | (inr b) => "(inr " ++ addParenHeuristic (toString b) ++ ")"⟩
+
+instance {α : Type u} {β : Type v} [HasToString α] [HasToString β] : HasToString (α × β) :=
+⟨fun ⟨a, b⟩ => "(" ++ toString a ++ ", " ++ toString b ++ ")"⟩
+
+instance {α : Type u} {β : α → Type v} [HasToString α] [s : ∀ x, HasToString (β x)] : HasToString (Sigma β) :=
+⟨fun ⟨a, b⟩ => "⟨"  ++ toString a ++ ", " ++ toString b ++ "⟩"⟩
+
+instance {α : Type u} {p : α → Prop} [HasToString α] : HasToString (Subtype p) :=
+⟨fun s => toString (val s)⟩
diff --git a/src/Init/Data/ToString/Macro.lean b/src/Init/Data/ToString/Macro.lean
new file mode 100644
index 0000000000..e60e6f0d9f
--- /dev/null
+++ b/src/Init/Data/ToString/Macro.lean
@@ -0,0 +1,17 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Leonardo de Moura
+-/
+prelude
+import Init.LeanInit
+import Init.Data.ToString.Basic
+new_frontend
+
+syntax:max "s!" (interpolatedStr term) : term
+
+macro_rules
+| `(s! $interpStr) => do
+  let chunks := interpStr.getArgs
+  let r ← Lean.Syntax.expandInterpolatedStrChunks chunks (fun a b => `($a ++ $b)) (fun a => `(toString $a))
+  `(($r : String))
diff --git a/src/Init/System/IOError.lean b/src/Init/System/IOError.lean
index 9696c4e412..c8c76c8458 100644
--- a/src/Init/System/IOError.lean
+++ b/src/Init/System/IOError.lean
@@ -7,7 +7,7 @@ Authors: Simon Hudon
 prelude
 import Init.Core
 import Init.Data.UInt
-import Init.Data.ToString
+import Init.Data.ToString.Basic
 import Init.Data.String.Basic
 
 /-
diff --git a/src/Init/Util.lean b/src/Init/Util.lean
index eea7ab3b39..7c4d1c8483 100644
--- a/src/Init/Util.lean
+++ b/src/Init/Util.lean
@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Data.String.Basic
-import Init.Data.ToString
+import Init.Data.ToString.Basic
 
 universes u v
 /- debugging helper functions -/
diff --git a/tests/lean/run/strInterpolation.lean b/tests/lean/run/strInterpolation.lean
index b555f38185..5d348ab557 100644
--- a/tests/lean/run/strInterpolation.lean
+++ b/tests/lean/run/strInterpolation.lean
@@ -1,17 +1,5 @@
 new_frontend
 
-open Lean
-
-def mkToString! (chunks : Array Syntax) : MacroM Syntax :=
-Syntax.expandInterpolatedStrChunks chunks (fun a b => `($a ++ $b)) (fun a => `(toString $a))
-
-syntax:max "s!" (interpolatedStr term) : term
-
-macro_rules
-| `(s! $interpStr) =>
-  let chunks := interpStr.getArgs
-  Syntax.expandInterpolatedStrChunks chunks (fun a b => `($a ++ $b)) (fun a => `(toString $a))
-
 #eval s!"hello {1+1}"
 
 def tst (x : Nat) : IO Unit := do