From 05d46348c7d0119b272b9dc2fd1ebaf0725b74ce Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <t-wnawrocki@microsoft.com>
Date: Mon, 21 Jun 2021 11:03:32 -0700
Subject: [PATCH] fix: 32-bit Unicode name mangling

---
 src/Lean/Compiler/NameMangling.lean   | 38 +++++++++++++++++----------
 tests/lean/mangling.lean              |  6 +++++
 tests/lean/mangling.lean.expected.out |  4 +++
 3 files changed, 34 insertions(+), 14 deletions(-)
 create mode 100644 tests/lean/mangling.lean
 create mode 100644 tests/lean/mangling.lean.expected.out

diff --git a/src/Lean/Compiler/NameMangling.lean b/src/Lean/Compiler/NameMangling.lean
index f2d22b24b7..64fa0e3d07 100644
--- a/src/Lean/Compiler/NameMangling.lean
+++ b/src/Lean/Compiler/NameMangling.lean
@@ -4,9 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 import Lean.Data.Name
-namespace Lean
 
-private def String.mangleAux : Nat → String.Iterator → String → String
+namespace String
+
+private def mangleAux : Nat → String.Iterator → String → String
   | 0,   it, r => r
   | i+1, it, r =>
     let c := it.curr
@@ -14,25 +15,34 @@ private def String.mangleAux : Nat → String.Iterator → String → String
       mangleAux i it.next (r.push c)
     else if c = '_' then
       mangleAux i it.next (r ++ "__")
-    else if c.toNat < 255 then
+    else if c.toNat < 0x100 then
       let n := c.toNat
       let r := r ++ "_x"
-      let r := r.push $ Nat.digitChar (n / 16)
-      let r := r.push $ Nat.digitChar (n % 16)
+      let r := r.push $ Nat.digitChar (n / 0x10)
+      let r := r.push $ Nat.digitChar (n % 0x10)
+      mangleAux i it.next r
+    else if c.toNat < 0x10000 then
+      let n := c.toNat
+      let r := r ++ "_u"
+      let r := r.push $ Nat.digitChar (n / 0x1000)
+      let n := n % 0x1000
+      let r := r.push $ Nat.digitChar (n / 0x100)
+      let n := n % 0x100
+      let r := r.push $ Nat.digitChar (n / 0x10)
+      let r := r.push $ Nat.digitChar (n % 0x10)
       mangleAux i it.next r
     else
       let n := c.toNat
-      let r := r ++ "_u"
-      let r := r.push $ Nat.digitChar (n / 4096)
-      let n := n % 4096
-      let r := r.push $ Nat.digitChar (n / 256)
-      let n := n % 256
-      let r := r.push $ Nat.digitChar (n / 16)
-      let r := r.push $ Nat.digitChar (n % 16)
+      let r := r ++ "_u32"
+      let r := Nat.toDigits 16 n |>.foldl (fun r c => r.push c) r
       mangleAux i it.next r
 
-def String.mangle (s : String) : String :=
-  String.mangleAux s.length s.mkIterator ""
+def mangle (s : String) : String :=
+  mangleAux s.length s.mkIterator ""
+
+end String
+
+namespace Lean
 
 private def Name.mangleAux : Name → String
   | Name.anonymous => ""
diff --git a/tests/lean/mangling.lean b/tests/lean/mangling.lean
new file mode 100644
index 0000000000..6d30fc07e8
--- /dev/null
+++ b/tests/lean/mangling.lean
@@ -0,0 +1,6 @@
+import Lean.Compiler.NameMangling
+
+#eval "ab12".mangle
+#eval "ÿ".mangle
+#eval "α₁".mangle
+#eval "𝒫".mangle
\ No newline at end of file
diff --git a/tests/lean/mangling.lean.expected.out b/tests/lean/mangling.lean.expected.out
new file mode 100644
index 0000000000..727ded7a4e
--- /dev/null
+++ b/tests/lean/mangling.lean.expected.out
@@ -0,0 +1,4 @@
+"ab12"
+"_xff"
+"_u03b1_u2081"
+"_u321d4ab"