From ffef5635bb49a7221b36c0f56a4ae9fe93d2cb85 Mon Sep 17 00:00:00 2001
From: Joe Hendrix <jhendrix@galois.com>
Date: Wed, 17 Feb 2021 14:57:08 -0800
Subject: [PATCH] fix: Json.num

Handle negative numbers correctly.
---
 src/Lean/Data/Json/Parser.lean    | 7 +++----
 tests/lean/json.lean.expected.out | 2 +-
 2 files changed, 4 insertions(+), 5 deletions(-)

diff --git a/src/Lean/Data/Json/Parser.lean b/src/Lean/Data/Json/Parser.lean
index 904e81a90c..a243aaa8bb 100644
--- a/src/Lean/Data/Json/Parser.lean
+++ b/src/Lean/Data/Json/Parser.lean
@@ -197,18 +197,17 @@ def num : Quickparse JsonNumber := do
       pure 0
     else
       natNonZero
-  let res := JsonNumber.fromInt (sign * res)
   let c? ← peek?
   let res : JsonNumber ←
     if c? = some '.' then
       skip
       let (n, d) ← natNumDigits
       if d > USize.size then fail "too many decimals"
-      let mantissa' := res.mantissa * (10^d : Nat) + n
-      let exponent' := res.exponent + d
+      let mantissa' := sign * (res * (10^d : Nat) + n)
+      let exponent' := d
       JsonNumber.mk mantissa' exponent'
     else
-      res
+      JsonNumber.fromInt (sign * res)
   let c? ← peek?
   if c? = some 'e' ∨ c? = some 'E' then
     skip
diff --git a/tests/lean/json.lean.expected.out b/tests/lean/json.lean.expected.out
index 5069244378..df40979117 100644
--- a/tests/lean/json.lean.expected.out
+++ b/tests/lean/json.lean.expected.out
@@ -2,7 +2,7 @@
 "false"
 "true"
 "0.0000123456"
-"1000000"
+"-1000000"
 "\"\""
 "\"abc\""
 "[true, 123, \"foo\", []]"