The canonical number spelling (CONFORMANCE §5.5.3.1)
- An integer prints plainly,
-for a negative one. - A decimal prints its digits positionally when its decimal exponent
e10is in[-4, 5](0.000123456,999999.5), and otherwise in scientific notationd.f…e<exp>with at least one fraction digit, a lowercasee, and-but never+on the exponent (1.0e-9,1.0000005e6).
print
writes the spelling, parse
reads a number token, and parse_print
is the
round trip: parsing the printed spelling, followed by anything that does not continue a
number token, gives back the number and the rest.
parse
reads any decimal spelling of a number, not only the canonical one, and
returns it in canonical form: 1.0 and 1.0e0 are the integer 1, 0.0e10 is the
integer 0, 2.50 is 2.5 (§5.5.3.1 rules 1 and 3). It rejects what has no
canonical form or is not a JSON number: an integer outside Int64 (§5.5.3.1 rule 1),
and a leading zero (007, 01.5). parse_wf
: whatever parse
returns is well
formed.
Digits
def natDigits (n : Nat) : List Nat
The big-endian decimal digits of n ([0] for zero).
def leadZero (ip : List Nat) : Bool
More than one digit, the first of them 0: a leading zero, which JSON forbids.
def readDigits : List Char → List Nat × List Char
The maximal run of digit characters at the front, as digits.
def parseNat (input : List Char) : Option (Nat × List Char)
A natural number token.
def parseInt (input : List Char) : Option (Int × List Char)
An integer token: an optional -, then digits.
Decimals
def fracDigits (fp : List Nat) : List Nat
The fraction digits printed after the point: at least one.
def decBody (ds : List Nat) (e10 : Int) : List Char
The unsigned spelling of the decimal d₁.d₂… × 10^e10.
def print : JNum → List Char
The canonical spelling of a number (CONFORMANCE §5.5.3.1).
def mkDec (neg : Bool) (ds : List Nat) (e10 : Int) : JNum
The decimal with digits ds (any leading or trailing zeros dropped) whose first
listed digit sits at decimal exponent e10.
def finishDec (neg : Bool) (ds : List Nat) (e10 : Int) (r : List Char) :
Option (JNum × List Char)
After the fraction digits of a decimal: an optional e exponent.
def afterInt (neg : Bool) (ip : List Nat) (r : List Char) : Option (JNum × List Char)
After the integer digits ip: a . and fraction digits make a decimal, anything
else ends an integer.
def parseRaw (input : List Char) : Option (JNum × List Char)
A number token as written: -?, digits with no leading zero, then either nothing
(an integer) or ., digits, and an optional e exponent (a decimal). Not yet in
canonical form (see parse
).
def canonize : JNum → JNum
The canonical form of a number read as written: a decimal whose digits are all
zero is the integer 0, and an integral decimal in Int64 is that integer
(§5.5.3.1 rules 1 and 3).
def parse (input : List Char) : Option (JNum × List Char)
A number token, in canonical form; none for one that has none (an integer
outside Int64).
theorem parse_wf {input rest : List Char} {n : JNum} (h : parse input = some (n, rest)) :
n.WF
What parse
reads is well formed.
theorem canonize_wf (n : JNum) (hn : n.WF) : canonize n = n
A well-formed number is already canonical.
def NumStop (rest : List Char) : Prop
What may follow a number token: anything that does not start with a digit, . or
e.
mkDec
undoes the padding the printer adds
The round trip
theorem parse_digits (neg : Bool) (ip : List Nat) (rest : List Char)
(hip : ip ≠ []) (hi : ∀ d ∈ ip, d < 10) (hl : leadZero ip = false) (hr : NoDigit rest) :
parseRaw ((if neg then ['-'] else []) ++ (ip.map digitChar ++ rest)) = afterInt neg ip rest
Parsing -? digits, followed by rest.
theorem parse_shape (neg : Bool) (ip fp : List Nat) (rest : List Char)
(hip : ip ≠ []) (hfp : fp ≠ []) (hi : ∀ d ∈ ip, d < 10) (hf : ∀ d ∈ fp, d < 10)
(hl : leadZero ip = false) (hr : NoDigit rest) :
parseRaw ((if neg then ['-'] else []) ++ (ip.map digitChar ++ '.' :: (fp.map digitChar ++ rest))) =
finishDec neg (ip ++ fp) (ip.length - 1) rest
Parsing -? digits . digits, followed by rest.
theorem parse_dec (neg : Bool) (ip fp : List Nat) (rest : List Char) (n : JNum)
(hip : ip ≠ []) (hfp : fp ≠ []) (hi : ∀ d ∈ ip, d < 10) (hf : ∀ d ∈ fp, d < 10)
(hl : leadZero ip = false) (hr : NumStop rest) (hm : mkDec neg (ip ++ fp) (ip.length - 1) = n) :
parseRaw ((if neg then ['-'] else []) ++ (ip.map digitChar ++ '.' :: (fp.map digitChar ++ rest))) =
some (n, rest)
A decimal spelling whose digits normalize to n, followed by a number stop.
theorem parse_print (n : JNum) (rest : List Char) (hn : n.WF) (hr : NumStop rest) :
parse (print n ++ rest) = some (n, rest)
The number round trip.
Canonical form of what parse
reads
def NumHead (c : Char) : Prop
The first character of a printed number: - or a digit.
theorem NumHead.of_fin {P : Char → Prop} (h1 : P '-') (h2 : ∀ d : Fin 10, P (digitChar d.val))
{c : Char} (hc : NumHead c) : P c
A fact about every possible first character of a number, checked character by character.
theorem print_head (n : JNum) (hn : n.WF) : ∃ c t, print n = c :: t ∧ NumHead c
A printed number starts with - or a digit.
theorem print_neg_head (n : JNum) (hn : n.WF) (t : List Char) (h : print n = '-' :: t) :
∃ d t', d < 10 ∧ t = digitChar d :: t'
After a leading -, a printed number continues with a digit.