fix: correctly parse json unicode escapes

leanprover · Dec 24, 2022 · d19033e · d19033e
1 parent 0553b59
commit d19033e
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 2 deletions.
diff --git a/src/Lean/Data/Json/Parser.lean b/src/Lean/Data/Json/Parser.lean
@@ -17,9 +17,9 @@ def hexChar : Parsec Nat := do
   if '0' ≤ c ∧ c ≤ '9' then
     pure $ c.val.toNat - '0'.val.toNat
   else if 'a' ≤ c ∧ c ≤ 'f' then
-    pure $ c.val.toNat - 'a'.val.toNat
+    pure $ c.val.toNat - 'a'.val.toNat + 10
   else if 'A' ≤ c ∧ c ≤ 'F' then
-    pure $ c.val.toNat - 'A'.val.toNat
+    pure $ c.val.toNat - 'A'.val.toNat + 10
   else
     fail "invalid hex character"
 

diff --git a/tests/lean/run/1985.lean b/tests/lean/run/1985.lean
@@ -0,0 +1,14 @@
+import Lean.Data.Json
+open Lean
+
+deriving instance BEq for Except
+
+example : Json.parse "\"\\u7406\\u79d1\"" == .ok "理科" := by native_decide
+example : Json.parse "\"\\u7406\\u79D1\"" == .ok "理科" := by native_decide
+
+example : Json.pretty "\x0b" == "\"\\u000b\"" := by native_decide
+example : Json.pretty "\x1b" == "\"\\u001b\"" := by native_decide
+example : Json.parse "\"\\u000b\"" == .ok "\x0b" := by native_decide
+example : Json.parse "\"\\u001b\"" == .ok "\x1b" := by native_decide
+example : Json.parse "\"\\u000B\"" == .ok "\x0b" := by native_decide
+example : Json.parse "\"\\u001B\"" == .ok "\x1b" := by native_decide