From df91ae37388d9802407667290abf4eab8e5060f8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 11 Jan 2017 23:44:33 -0800 Subject: [PATCH] fix(library/string,library/init/data/to_string): handle ASCII control characters --- library/init/data/to_string.lean | 34 ++++++++++++++----- src/frontends/lean/scanner.cpp | 4 ++- src/library/string.cpp | 19 ++++++----- .../interactive/field_info.lean.expected.out | 2 +- tests/lean/pp_char_bug.lean | 16 +++++++++ tests/lean/pp_char_bug.lean.expected.out | 9 +++++ 6 files changed, 65 insertions(+), 19 deletions(-) diff --git a/library/init/data/to_string.lean b/library/init/data/to_string.lean index 7d1a46b9ed..dac98ebbb4 100644 --- a/library/init/data/to_string.lean +++ b/library/init/data/to_string.lean @@ -5,7 +5,7 @@ Author: Leonardo de Moura -/ prelude import init.data.string.basic init.data.bool.basic init.data.subtype.basic -import init.data.unsigned init.data.prod init.data.sum.basic +import init.data.unsigned init.data.prod init.data.sum.basic init.data.nat.div open sum subtype nat universe variables u v @@ -53,10 +53,35 @@ instance {α : Type u} {β : α → Type v} [has_to_string α] [s : ∀ x, has_t instance {α : Type u} {p : α → Prop} [has_to_string α] : has_to_string (subtype p) := ⟨λ s, to_string (elt_of s)⟩ +/- Remark: the code generator replaces this definition with one that display natural numbers in decimal notation -/ +protected def nat.to_string : nat → string +| 0 := "zero" +| (succ a) := "(succ " ++ nat.to_string a ++ ")" + +instance : has_to_string nat := +⟨nat.to_string⟩ + +def hex_digit_to_string (n : nat) : string := +if n ≤ 9 then to_string n +else if n = 10 then "a" +else if n = 11 then "b" +else if n = 12 then "c" +else if n = 13 then "d" +else if n = 14 then "e" +else "f" + +def char_to_hex (c : char) : string := +let n := char.to_nat c, + d2 := div n 16, + d1 := n % 16 +in hex_digit_to_string d2 ++ hex_digit_to_string d1 + def char.quote_core (c : char) : string := if c = #"\n" then "\\n" +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] instance : has_to_string char := @@ -73,13 +98,6 @@ def string.quote : string → string instance : has_to_string string := ⟨string.quote⟩ -/- Remark: the code generator replaces this definition with one that display natural numbers in decimal notation -/ -protected def nat.to_string : nat → string -| 0 := "zero" -| (succ a) := "(succ " ++ nat.to_string a ++ ")" - -instance : has_to_string nat := -⟨nat.to_string⟩ instance (n : nat) : has_to_string (fin n) := ⟨λ f, to_string (fin.val f)⟩ diff --git a/src/frontends/lean/scanner.cpp b/src/frontends/lean/scanner.cpp index df4bd9bc3f..b43823f02b 100644 --- a/src/frontends/lean/scanner.cpp +++ b/src/frontends/lean/scanner.cpp @@ -142,10 +142,12 @@ char scanner::read_quoted_char(char const * error_msg) { next(); check_not_eof(error_msg); char c = curr(); - if (c != '\\' && c != '\"' && c != 'n' && c != '\'' && c != 'x') + if (c != '\\' && c != '\"' && c != 'n' && c != 't' && c != '\'' && c != 'x') throw_exception("invalid escape sequence"); if (c == 'n') { return '\n'; + } else if (c == 't') { + return '\t'; } else if (c == 'x') { next(); char c = curr(); diff --git a/src/library/string.cpp b/src/library/string.cpp index f862bc4ed9..87db1c0514 100644 --- a/src/library/string.cpp +++ b/src/library/string.cpp @@ -31,20 +31,21 @@ static expr * g_list_nil_char = nullptr; expr from_string_core(std::string const & s); static void display_char_literal_core(std::ostream & out, char c, bool in_string) { - if (c == '\n') + if (c == '\n') { out << "\\n"; - else if (c == '\t') + } else if (c == '\t') { out << "\\t"; - else if (c == '\r') - out << "\\r"; - else if (c == 0) - out << "\\0"; - else if (in_string && c == '\"') + } else if (in_string && c == '\"') { out << "\\\""; - else if (!in_string && c == '\'') + } else if (!in_string && c == '\'') { out << "\\'"; - else + } else if (0 <= c && c <= 31) { + out << "\\x"; + if (c < 16) out << "0"; + out << std::hex << static_cast(c); + } else { out << c; + } } static void display_char_literal(std::ostream & out, char c) { diff --git a/tests/lean/interactive/field_info.lean.expected.out b/tests/lean/interactive/field_info.lean.expected.out index 936d4d027d..71fa6169d1 100644 --- a/tests/lean/interactive/field_info.lean.expected.out +++ b/tests/lean/interactive/field_info.lean.expected.out @@ -1,2 +1,2 @@ {"message":"file invalidated","response":"ok","seq_num":0} -{"record":{"full-id":"nat.to_string","source":{"column":14,"file":"/library/init/data/to_string.lean","line":77},"type":"ℕ → string"},"response":"ok","seq_num":2} +{"record":{"full-id":"nat.to_string","source":{"column":14,"file":"/library/init/data/to_string.lean","line":57},"type":"ℕ → string"},"response":"ok","seq_num":2} diff --git a/tests/lean/pp_char_bug.lean b/tests/lean/pp_char_bug.lean index 7868eba4a7..c3cddd6935 100644 --- a/tests/lean/pp_char_bug.lean +++ b/tests/lean/pp_char_bug.lean @@ -4,3 +4,19 @@ check #"a" check to_string #"a" vm_eval to_string #"a" vm_eval #"a" + +vm_eval char.of_nat 1 +vm_eval char.of_nat 1 +vm_eval char.of_nat 20 + +check char.of_nat 1 +check char.of_nat 20 +check char.of_nat 15 +check char.of_nat 16 +vm_eval char.of_nat 15 +vm_eval char.of_nat 16 + +example : char.of_nat 1 = #"\x01" := +rfl +example : char.of_nat 20 = #"\x14" := +rfl diff --git a/tests/lean/pp_char_bug.lean.expected.out b/tests/lean/pp_char_bug.lean.expected.out index d16fe890c5..bec8d544d2 100644 --- a/tests/lean/pp_char_bug.lean.expected.out +++ b/tests/lean/pp_char_bug.lean.expected.out @@ -4,3 +4,12 @@ fin.mk 1 (of_as_true trivial) : fin 3 to_string #"a" : string "#\"a\"" #"a" +#"\x01" +#"\x01" +#"\x14" +#"\x01" : char +#"\x14" : char +#"\x0f" : char +#"\x10" : char +#"\x0f" +#"\x10"