Lean.Data.Json.Basic

Lean.JsonNumber.normalize x = match x with | { mantissa := m, exponent := e } => Id.run (if m = 0 then (0, 0, 0) else let sign := if m > 0 then 1 else -1; let mAbs := Int.natAbs m; let nDigits := Lean.JsonNumber.countDigits mAbs; do let r ← let col := { start := 0, stop := nDigits, step := 1 }; forIn col mAbs fun x r => let mAbs := r; if mAbs % 10 = 0 then let mAbs := mAbs / 10; do pure PUnit.unit pure (ForInStep.yield mAbs) else pure (ForInStep.done mAbs) let x : Nat := r let mAbs : Nat := x (sign, mAbs, -Int.ofNat e + Int.ofNat nDigits))

source

def Lean.JsonNumber.lt (a : Lean.JsonNumber) (b : Lean.JsonNumber) :

Bool

Equations

Lean.JsonNumber.lt a b = let x := Lean.JsonNumber.normalize a; match x with | (as, am, ae) => let x := Lean.JsonNumber.normalize b; match x with | (bs, bm, be) => match (as, bs) with | (Int.negSucc 0, Int.ofNat 1) => true | (Int.ofNat 1, Int.negSucc 0) => false | x => let x := if (decide (as = -1) && decide (bs = -1)) = true then ((bm, be), am, ae) else ((am, ae), bm, be); match x with | ((am, ae), bm, be) => let amDigits := Lean.JsonNumber.countDigits am; let bmDigits := Lean.JsonNumber.countDigits bm; let x := if amDigits < bmDigits then (am * 10 ^ (bmDigits - amDigits), bm) else (am, bm * 10 ^ (amDigits - bmDigits)); match x with | (am, bm) => if ae < be then true else if ae > be then false else decide (am < bm)

source

def Lean.JsonNumber.ltProp :

LT Lean.JsonNumber

Equations

Lean.JsonNumber.ltProp = { lt := fun a b => Lean.JsonNumber.lt a b = true }

source

instance Lean.JsonNumber.instLTJsonNumber :

LT Lean.JsonNumber

Equations

Lean.JsonNumber.instLTJsonNumber = Lean.JsonNumber.ltProp

source

instance Lean.JsonNumber.instDecidableLtJsonNumberInstLTJsonNumber (a : Lean.JsonNumber) (b : Lean.JsonNumber) :

Decidable (a < b)

Equations

Lean.JsonNumber.instDecidableLtJsonNumberInstLTJsonNumber a b = inferInstanceAs (Decidable (Lean.JsonNumber.lt a b = true))

source

instance Lean.JsonNumber.instOrdJsonNumber :

Ord Lean.JsonNumber

Equations

Lean.JsonNumber.instOrdJsonNumber = { compare := fun x y => if x < y then Ordering.lt else if x > y then Ordering.gt else Ordering.eq }

source

def Lean.JsonNumber.toString :

Lean.JsonNumber → String

Equations

Lean.JsonNumber.toString x = match x with | { mantissa := m, exponent := 0 } => Int.repr m | { mantissa := m, exponent := e } => let sign := if m ≥ 0 then "" else "-"; let m := Int.natAbs m; let exp := 9 + Int.ofNat (Lean.JsonNumber.countDigits m) - Int.ofNat e; let exp := if exp < 0 then exp else 0; let e' := 10 ^ (e - Int.natAbs exp); let left := Int.repr (Int.ofNat m / e'); let right := Substring.toString (Substring.dropRightWhile (Substring.drop (String.toSubstring (Int.repr (e' + Int.ofNat m % e'))) 1) fun c => decide (c = Char.ofNat 48)); let exp := if exp = 0 then "" else "e" ++ Int.repr exp; toString "" ++ toString sign ++ toString "" ++ toString left ++ toString "." ++ toString right ++ toString "" ++ toString exp ++ toString ""

source

def Lean.JsonNumber.shiftl :

Lean.JsonNumber → Nat → Lean.JsonNumber

Equations

Lean.JsonNumber.shiftl x x = match x, x with | { mantissa := m, exponent := e }, s => { mantissa := m * Int.ofNat (10 ^ (s - e)), exponent := e - s }

source

def Lean.JsonNumber.shiftr :

Lean.JsonNumber → Nat → Lean.JsonNumber

Equations

Lean.JsonNumber.shiftr x x = match x, x with | { mantissa := m, exponent := e }, s => { mantissa := m, exponent := e + s }

source

instance Lean.JsonNumber.instToStringJsonNumber :

ToString Lean.JsonNumber

Equations

Lean.JsonNumber.instToStringJsonNumber = { toString := Lean.JsonNumber.toString }

source

instance Lean.JsonNumber.instReprJsonNumber :

Repr Lean.JsonNumber

Equations

Lean.JsonNumber.instReprJsonNumber = { reprPrec := fun x x_1 => match x, x_1 with | { mantissa := m, exponent := e }, x => Lean.Format.bracket "⟨" (repr m ++ Std.Format.text "," ++ repr e) "⟩" }

source

def Lean.strLt (a : String) (b : String) :

Bool

Equations

Lean.strLt a b = decide (a < b)

source

inductive Lean.Json :

Type

null: Lean.Json
bool: Bool → Lean.Json
num: Lean.JsonNumber → Lean.Json
str: String → Lean.Json
arr: Array Lean.Json → Lean.Json
obj: (Std.RBNode String fun x => Lean.Json) → Lean.Json

source

instance Lean.instInhabitedJson :

Inhabited Lean.Json

Equations

Lean.instInhabitedJson = { default := Lean.Json.null }

source

instance Lean.Json.instBEqJson :

BEq Lean.Json

Equations

Lean.Json.instBEqJson = { beq := Lean.Json.beq' }

source

def Lean.Json.mkObj (o : List (String × Lean.Json)) :

Lean.Json

Equations

Lean.Json.mkObj o = Lean.Json.obj (Id.run (let kvPairs := Std.RBNode.leaf; do let r ← forIn o kvPairs fun x r => match x with | (k, v) => let kvPairs := r; let kvPairs := Std.RBNode.insert compare kvPairs k v; do pure PUnit.unit pure (ForInStep.yield kvPairs) let x : Std.RBNode String fun x => Lean.Json := r let kvPairs : Std.RBNode String fun x => Lean.Json := x kvPairs))

source

instance Lean.Json.instCoeNatJson :

Coe Nat Lean.Json

Equations

Lean.Json.instCoeNatJson = { coe := fun n => Lean.Json.num (Lean.JsonNumber.fromNat n) }

source

instance Lean.Json.instCoeIntJson :

Coe Int Lean.Json

Equations

Lean.Json.instCoeIntJson = { coe := fun n => Lean.Json.num (Lean.JsonNumber.fromInt n) }

source

instance Lean.Json.instCoeStringJson :

Coe String Lean.Json

Equations

Lean.Json.instCoeStringJson = { coe := Lean.Json.str }

source

instance Lean.Json.instCoeBoolJson :

Coe Bool Lean.Json

Equations

Lean.Json.instCoeBoolJson = { coe := Lean.Json.bool }

source

instance Lean.Json.instOfNatJson {n : Nat} :

OfNat Lean.Json n

Equations

Lean.Json.instOfNatJson = { ofNat := Lean.Json.num (Lean.JsonNumber.fromNat n) }

source

def Lean.Json.isNull :

Lean.Json → Bool

Equations

Lean.Json.isNull x = match x with | Lean.Json.null => true | x => false

source

def Lean.Json.getObj? :

Lean.Json → Except String (Std.RBNode String fun x => Lean.Json)

Equations

Lean.Json.getObj? x = match x with | Lean.Json.obj kvs => pure kvs | x => throw "object expected"

source

def Lean.Json.getArr? :

Lean.Json → Except String (Array Lean.Json)

Equations

Lean.Json.getArr? x = match x with | Lean.Json.arr a => pure a | x => throw "array expected"

source

def Lean.Json.getStr? :

Lean.Json → Except String String

Equations

Lean.Json.getStr? x = match x with | Lean.Json.str s => pure s | x => throw "String expected"

source

def Lean.Json.getNat? :

Lean.Json → Except String Nat

Equations

Lean.Json.getNat? x = match x with | Lean.Json.num { mantissa := Int.ofNat n, exponent := 0 } => pure n | x => throw "Natural number expected"

source

def Lean.Json.getInt? :

Lean.Json → Except String Int

Equations

Lean.Json.getInt? x = match x with | Lean.Json.num { mantissa := i, exponent := 0 } => pure i | x => throw "Integer expected"

source

def Lean.Json.getBool? :

Lean.Json → Except String Bool

Equations

Lean.Json.getBool? x = match x with | Lean.Json.bool b => pure b | x => throw "Bool expected"

source

def Lean.Json.getNum? :

Lean.Json → Except String Lean.JsonNumber

Equations

Lean.Json.getNum? x = match x with | Lean.Json.num n => pure n | x => throw "number expected"

source

def Lean.Json.getObjVal? :

Lean.Json → String → Except String Lean.Json

Equations

Lean.Json.getObjVal? x x = match x, x with | Lean.Json.obj kvs, k => match Std.RBNode.find compare kvs k with | some v => pure v | none => throw (toString "property not found: " ++ toString k ++ toString "") | x, x_1 => throw "object expected"

source

def Lean.Json.getArrVal? :

Lean.Json → Nat → Except String Lean.Json

Equations

Lean.Json.getArrVal? x x = match x, x with | Lean.Json.arr a, i => match Array.get? a i with | some v => pure v | none => throw (toString "index out of bounds: " ++ toString i ++ toString "") | x, x_1 => throw "array expected"

source

def Lean.Json.getObjValD (j : Lean.Json) (k : String) :

Lean.Json

Equations

Lean.Json.getObjValD j k = Option.getD (Except.toOption (Lean.Json.getObjVal? j k)) Lean.Json.null

source

def Lean.Json.setObjVal! :

Lean.Json → String → Lean.Json → Lean.Json

Equations

Lean.Json.setObjVal! x x x = match x, x, x with | Lean.Json.obj kvs, k, v => Lean.Json.obj (Std.RBNode.insert compare kvs k v) | j, x, x_1 => panicWithPosWithDecl "Lean.Data.Json.Basic" "Lean.Json.setObjVal!" 232 21 "Json.setObjVal!: not an object: {j}"

source

inductive Lean.Json.Structured :

Type

arr: Array Lean.Json → Lean.Json.Structured
obj: (Std.RBNode String fun x => Lean.Json) → Lean.Json.Structured

source

instance Lean.Json.instCoeArrayJsonStructured :

Coe (Array Lean.Json) Lean.Json.Structured

Equations

Lean.Json.instCoeArrayJsonStructured = { coe := Lean.Json.Structured.arr }

source

instance Lean.Json.instCoeRBNodeStringJsonStructured :

Coe (Std.RBNode String fun x => Lean.Json) Lean.Json.Structured

Equations

Lean.Json.instCoeRBNodeStringJsonStructured = { coe := Lean.Json.Structured.obj }