JSON values of an ESM document, in canonical form

Lean module Esm.Document.Json, formal/Esm/Document/Json.lean at 184aa13d35e5
Imports Mathlib.Data.List.Nodup

The value type the document codecs (Esm.Document.Yaml , Esm.Document.TypstDict ) print and read. Numbers are already in the canonical form of CONFORMANCE §5.5.3.1:

rule 1 and rule 3: a number whose value is integral and representable in Int64 is the integer literal (1.0 IS the integer 1), so it is JNum.int;
rule 2: every other finite number is JNum.dec, its shortest round-trip decimal digits and the decimal exponent of the first digit. Binary64 is not modelled; the shortest digits are given data.

Object key order is part of the value (the codecs preserve it; they never sort).

inductive JNum source

inductive JNum where
  | int (z : Int)
  | dec (neg : Bool) (digits : List Nat) (e10 : Int)
  deriving DecidableEq, Repr

A JSON number in canonical form.

int z: an integer literal (well formed when z fits in Int64).
dec neg ds e10: the value ±d₁.d₂d₃… × 10^e10, - when neg, with ds the shortest round-trip digits.

def InInt64 source

def InInt64 (z : Int) : Prop

z is representable in Int64.

def digitsVal source

def digitsVal (ds : List Nat) : Nat

The value of a big-endian decimal digit list.

def decInt? source

def decInt? (neg : Bool) (ds : List Nat) (e10 : Int) : Option Int

The integer a decimal denotes, when the decimal is integral (its last digit sits at or left of the units place), else none.

def WF source

def WF : JNum → Prop

Canonical form of a number:

an int fits in Int64;
a dec has nonempty digits, each below 10, with no leading and no trailing zero, and is not an integral Int64 value (that number is an int, §5.5.3.1 rule 1).

def wfb source

def wfb : JNum → Bool

WF , as a check.

inductive Json source

inductive Json where
  | null
  | bool (b : Bool)
  | num (n : JNum)
  | str (s : String)
  | arr (xs : List Json)
  | obj (kvs : List (String × Json))
  deriving Repr

A JSON value. Strings and keys are arbitrary Lean strings (any Unicode scalar values); object entries keep their order.

def WF source

def WF : Json → Prop

Well formed: every number is canonical and every object has distinct keys.

def WFList source

def WFList : List Json → Prop

Every element is well formed.

def WFObj source

def WFObj : List (String × Json) → Prop

Every entry’s value is well formed.

def wfb source

def wfb : Json → Bool

WF , as a check.

def size source

def size : Json → Nat

A size measure: the parsers’ fuel is bounded below by it.

This module also proves 4 lemmas without doc comments; they are in the source.