From dc81915da6d5e4ce4e778799e46d3f33b10fd9ff Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Mon, 12 Jun 2017 16:32:35 +0200 Subject: [PATCH] refactor(library): unify char.to_string and char.has_to_string --- leanpkg/leanpkg/toml.lean | 2 +- library/init/data/string/basic.lean | 8 ++++---- library/init/data/to_string.lean | 5 ++++- library/init/meta/interactive_base.lean | 4 ++-- library/tools/debugger/util.lean | 2 +- tests/lean/char_lits.lean | 2 +- tests/lean/char_lits.lean.expected.out | 2 +- tests/lean/format_to_buffer.lean.expected.out | 2 +- 8 files changed, 15 insertions(+), 12 deletions(-) diff --git a/leanpkg/leanpkg/toml.lean b/leanpkg/leanpkg/toml.lean index 73e5b86eec..b622b933fe 100644 --- a/leanpkg/leanpkg/toml.lean +++ b/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) diff --git a/library/init/data/string/basic.lean b/library/init/data/string/basic.lean index 5cbf0c47b9..655f3cb424 100644 --- a/library/init/data/string/basic.lean +++ b/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 \ No newline at end of file diff --git a/library/init/data/to_string.lean b/library/init/data/to_string.lean index ce41bb4484..4e8ae12c63 100644 --- a/library/init/data/to_string.lean +++ b/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 diff --git a/library/init/meta/interactive_base.lean b/library/init/meta/interactive_base.lean index 8f7d1486c4..70743f486d 100644 --- a/library/init/meta/interactive_base.lean +++ b/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] diff --git a/library/tools/debugger/util.lean b/library/tools/debugger/util.lean index 89d0ac32a2..ddb3a99d4e 100644 --- a/library/tools/debugger/util.lean +++ b/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 := [] diff --git a/tests/lean/char_lits.lean b/tests/lean/char_lits.lean index 710326ab7c..2ea38d07fb 100644 --- a/tests/lean/char_lits.lean +++ b/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 '\'') diff --git a/tests/lean/char_lits.lean.expected.out b/tests/lean/char_lits.lean.expected.out index 5949b9a59d..edcfc5093b 100644 --- a/tests/lean/char_lits.lean.expected.out +++ b/tests/lean/char_lits.lean.expected.out @@ -3,6 +3,6 @@ '\n' '\\' aaa\ - +'\n' aaa' diff --git a/tests/lean/format_to_buffer.lean.expected.out b/tests/lean/format_to_buffer.lean.expected.out index 7f99f7d936..20dc559156 100644 --- a/tests/lean/format_to_buffer.lean.expected.out +++ b/tests/lean/format_to_buffer.lean.expected.out @@ -1 +1 @@ -[f, o, o, b, a, r] +['f', 'o', 'o', 'b', 'a', 'r']