max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: Json.num

Browse source 
Handle negative numbers correctly.
This commit is contained in:
Joe Hendrix 2021-02-17 14:57:08 -08:00 • committed by Sebastian Ullrich
parent 51771d5d07
commit ffef5635bb
2 changed files with 4 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/Lean/Data/Json/Parser.lean
View file

@ -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

2
tests/lean/json.lean.expected.out
View file

@ -2,7 +2,7 @@
"false"
"true"
"0.0000123456"
"1000000"
"-1000000"
"\"\""
"\"abc\""
"[true, 123, \"foo\", []]"