feat: add interpolated string for toString

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

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

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

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

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)

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 -/

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

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)⟩

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))

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
 
 /-

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 -/

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