chore: don't include redundant empty strings in string interpolation (#10269)

This PR changes the string interpolation procedure to omit redundant
empty parts. For example `s!"{1}{2}"` previously elaborated to `toString
"" ++ toString 1 ++ toString "" ++ toString 2 ++ toString ""` and now
elaborates to `toString 1 ++ toString 2`.

src/Init/Meta.lean

@@ -8,8 +8,8 @@ Additional goodies for writing macros
 module
 
 prelude
-public import Init.Prelude  -- for unfolding `Name.beq`
-import all Init.Prelude  -- for unfolding `Name.beq`
+public import Init.Prelude
+import all Init.Prelude -- for unfolding `Name.beq`
 public import Init.MetaTypes
 public import Init.Syntax
 public import Init.Data.Array.GetLit
@@ -1519,18 +1519,21 @@ end Syntax
 namespace TSyntax
 
 def expandInterpolatedStrChunks (chunks : Array Syntax) (mkAppend : Syntax → Syntax → MacroM Syntax) (mkElem : Syntax → MacroM Syntax) : MacroM Syntax := do
-  let mut i := 0
   let mut result := Syntax.missing
   for elem in chunks do
-    let elem ← withRef elem <| match elem.isInterpolatedStrLit? with
-      | none     => mkElem elem
-      | some str => mkElem (Syntax.mkStrLit str)
-    if i == 0 then
+    let elem ← match elem.isInterpolatedStrLit? with
+      | none     => withRef elem <| mkElem elem
+      | some str =>
+        if String.Internal.isEmpty str then continue
+        else withRef elem <| mkElem (Syntax.mkStrLit str)
+    if result.isMissing then
       result := elem
     else
       result ← mkAppend result elem
-    i := i+1
-  return result
+  if result.isMissing then
+    mkElem (Syntax.mkStrLit "")
+  else
+    return result
 
 open TSyntax.Compat in
 def expandInterpolatedStr (interpStr : TSyntax interpolatedStrKind) (type : Term) (toTypeFn : Term) : MacroM Term := do

tests/lean/run/strInterpolation.lean

@@ -1,10 +1,20 @@
+/-!
+Tests the behavior of string interpolation literals
+-/
 
+/-!
+Constant values are correctly interpolated.
+-/
 
 #eval s!"hello {1+1}"
 
+/-!
+Values with variables are correctly interpolated.
+-/
+
 def tst (x : Nat) : IO Unit := do
-IO.println s!"x: {x}"
-IO.println s!"x+1: {x+1}"
+  IO.println s!"x: {x}"
+  IO.println s!"x+1: {x+1}"
 
 /--
 info: x: 10
@@ -13,26 +23,37 @@ x+1: 11
 #guard_msgs in
 #eval tst 10
 
-/-- info: "1+1" -/
-#guard_msgs in
-#eval s!"{1}+{1}"
+/-!
+Opening braces (`{`) can be escaped, closing braces (`}`) don't need to be.
+-/
 
 /-- info: "{2}" -/
 #guard_msgs in
 #eval s!"\{{1+1}}"
 
+/-!
+String interpolation doesn't add any spaces.
+-/
+
+/-- info: "1+1" -/
+#guard_msgs in
+#eval s!"{1}+{1}"
+
 /-- info: "a1" -/
 #guard_msgs in
 #eval s!"a{1}"
 
+/-!
+String interpolation works correctly with monadic computations.
+-/
+
 def g (x : Nat) : StateRefT Nat IO Nat := do
-modify (· + x)
-get
+  modify (· + x)
+  get
 
 def ex : StateRefT Nat IO Unit := do
-IO.println s!">> hello {(←g 1)}"
-IO.println s!">> world {(←g 1)}"
-pure ()
+  IO.println s!">> hello {← g 1}"
+  IO.println s!">> world {← g 1}"
 
 /--
 info: >> hello 1
@@ -40,3 +61,22 @@ info: >> hello 1
 -/
 #guard_msgs in
 #eval ex.run' 0
+
+/-!
+String interpolation elaborates to the individual components wrapped in `toString` and combined
+using `++`.
+-/
+
+/--
+info: toString "he" ++ toString "llo" ++ toString ", " ++ toString "wo" ++ toString "rld" : String
+-/
+#guard_msgs in
+#check s!"he{"llo"}, {"wo"}rld"
+
+/-!
+Redundant parts are omitted.
+-/
+
+/-- info: toString 1 ++ toString 2 : String -/
+#guard_msgs in
+#check s!"{1}{2}"