refactor(library): unify char.to_string and char.has_to_string

leanpkg/leanpkg/toml.lean

@@ -28,7 +28,7 @@ private def escapec : char → string
 | '\t' := "\\t"
 | '\n' := "\\n"
 | '\\' := "\\\\"
-| c    := c.to_string
+| c    := string.singleton c
 
 private def escape (s : string) : string :=
 s.fold "" (λ s c, s ++ escapec c)

library/init/data/string/basic.lean

@@ -69,6 +69,9 @@ def backn : string → nat → string
 def join (l : list string) : string :=
 l.foldl (λ r s, r ++ s) ""
 
+def singleton (c : char) : string :=
+str empty c
+
 end string
 
 open list string
@@ -97,7 +100,4 @@ private def to_nat_core : list char → nat → nat
   to_nat_core cs (char.to_nat c - char.to_nat '0' + r*10)
 
 def string.to_nat (s : string) : nat :=
-to_nat_core s.to_list 0
-
-def char.to_string (c : char) : string :=
-str empty c
+to_nat_core s.to_list 0

library/init/data/to_string.lean

@@ -82,7 +82,7 @@ else if  c = '\t' then "\\t"
 else if  c = '\\' then "\\\\"
 else if  c = '\"' then "\\\""
 else if  char.to_nat c <= 31 then "\\x" ++ char_to_hex c
-else c.to_string
+else string.singleton c
 
 instance : has_to_string char :=
 ⟨λ c, "'" ++ char.quote_core c ++ "'"⟩
@@ -103,3 +103,6 @@ instance (n : nat) : has_to_string (fin n) :=
 
 instance : has_to_string unsigned :=
 ⟨λ n, to_string (fin.val n)⟩
+
+def char.to_string (c : char) : string :=
+to_string c

library/init/meta/interactive_base.lean

@@ -157,7 +157,7 @@ do (e, s) ← with_input (lean.parser.pexpr 0) s.as_string,
    '}'::s ← return s.to_list | fail "'}' expected",
    f ← parse_format "" s,
    pure ``(to_fmt %%(reflect acc) ++ to_fmt %%e ++ %%f)
-| acc (c::s) := parse_format (acc ++ c.to_string) s
+| acc (c::s) := parse_format (acc.str c) s
 
 reserve prefix `format! `:100
 @[user_notation]
@@ -172,7 +172,7 @@ do (e, s) ← with_input (lean.parser.pexpr 0) s.as_string,
    '}'::s ← return s.to_list | fail "'}' expected",
    f ← parse_sformat "" s,
    pure ``(%%(reflect acc) ++ to_string %%e ++ %%f)
-| acc (c::s) := parse_sformat (acc ++ c.to_string) s
+| acc (c::s) := parse_sformat (acc.str c) s
 
 reserve prefix `sformat! `:100
 @[user_notation]

library/tools/debugger/util.lean

@@ -9,7 +9,7 @@ if c = ' ' ∨ c = char.of_nat 11 ∨ c = '\n' then tt else ff
 
 private def split_core : list char → option string → list string
 | (c::cs) none     :=
-  if is_space c then split_core cs none else split_core cs (some c.to_string)
+  if is_space c then split_core cs none else split_core cs (some $ string.singleton c)
 | (c::cs) (some s) :=
   if is_space c then s :: split_core cs none else split_core cs (s.str c)
 | []      none     := []

tests/lean/char_lits.lean

@@ -8,5 +8,5 @@ open io
 variable [io.interface]
 #eval put_str ("aaa".str '\\')
 #eval put_str '\n'.to_string
-#eval put_str '\n'.to_string
+#eval put_str $ string.singleton '\n'
 #eval put_str ("aaa".str '\'')

tests/lean/char_lits.lean.expected.out

@@ -3,6 +3,6 @@
 '\n'
 '\\'
 aaa\
-
+'\n'
 
 aaa'

tests/lean/format_to_buffer.lean.expected.out

@@ -1 +1 @@
-[f, o, o, b, a, r]
+['f', 'o', 'o', 'b', 'a', 'r']