fix(library/string): unicode char literals

library/init/data/repr.lean

@@ -108,7 +108,7 @@ 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 if  c.to_nat <= 31 ∨ c = '\x7f' then "\\x" ++ char_to_hex c
 else string.singleton c
 
 instance : has_repr char :=

src/library/string.cpp

@@ -29,16 +29,18 @@ static expr * g_fin_mk               = nullptr;
 
 expr from_string_core(std::string const & s);
 
-static void display_char_literal_core(std::ostream & out, unsigned char c, bool in_string) {
+static void display_char_literal_utf8(std::ostream & out, unsigned char c, bool in_string) {
     if (c == '\n') {
         out << "\\n";
     } else if (c == '\t') {
         out << "\\t";
+    } else if (c == '\\') {
+        out << "\\\\";
     } else if (in_string && c == '\"') {
         out << "\\\"";
     } else if (!in_string && c == '\'') {
         out << "\\'";
-    } else if (32 <= c && c <= 126) {
+    } else if (c >= 32 && c != 127) {
         out << c;
     } else {
         out << "\\x";
@@ -47,16 +49,20 @@ static void display_char_literal_core(std::ostream & out, unsigned char c, bool
     }
 }
 
-static void display_char_literal(std::ostream & out, char c) {
+static void display_char_literal(std::ostream & out, unsigned c) {
     out << "'";
-    display_char_literal_core(out, c, false);
+    std::string s;
+    push_unicode_scalar(s, c);
+    for (unsigned i = 0; i < s.size(); i++) {
+        display_char_literal_utf8(out, s[i], false);
+    }
     out << "'";
 }
 
 static void display_string_literal(std::ostream & out, std::string const & s) {
     out << "\"";
     for (unsigned i = 0; i < s.size(); i++) {
-        display_char_literal_core(out, s[i], true);
+        display_char_literal_utf8(out, s[i], true);
     }
     out << "\"";
 }
@@ -67,7 +73,7 @@ format pp_string_literal(std::string const & s) {
     return format(out.str());
 }
 
-format pp_char_literal(char c) {
+format pp_char_literal(unsigned c) {
     std::ostringstream out;
     display_char_literal(out, c);
     return format(out.str());

src/library/string.h

@@ -29,7 +29,7 @@ optional<unsigned> to_char(abstract_type_context & ctx, expr const & e);
 bool is_char_value(abstract_type_context & ctx, expr const & e);
 
 format pp_string_literal(std::string const & s);
-format pp_char_literal(char c);
+format pp_char_literal(unsigned c);
 
 void initialize_string();
 void finalize_string();

tests/lean/char_lits.lean

@@ -1,6 +1,8 @@
 import system.io
 open io
 #check 'a'
+#check '\\'
+#check 'α'
 
 #eval 'a'
 #eval '\n'
@@ -11,7 +13,7 @@ variable [io.interface]
 #eval put_str $ string.singleton '\n'
 #eval put_str ("aaa".str '\'')
 
-#check ['\x7f', '\x00', '\x11', '\xff']
+#check ['\x7f', '\x00', '\x11']
 -- ^^ all characters should be pretty-printed using \x escapes
 
 #eval 'α'

tests/lean/char_lits.lean.expected.out

@@ -1,4 +1,6 @@
 'a' : char
+'\\' : char
+'α' : char
 'a'
 '\n'
 '\\'
@@ -6,7 +8,7 @@ aaa\
 '\n'
 
 aaa'
-['\x7f', '\x00', '\x11', '\xff'] : list char
+['\x7f', '\x00', '\x11'] : list char
 'α'
 'β'
 'α'