fix(library/string,library/init/data/to_string): handle ASCII control characters

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

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

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<int>(c);
+    } else {
         out << c;
+    }
 }
 
 static void display_char_literal(std::ostream & out, char c) {

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}

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

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"