Lean.Data.Json.Parser

source

@[inline]

def Lean.Json.Parser.hexChar :

Lean.Parsec Nat

Equations

Lean.Json.Parser.hexChar = do let c ← Lean.Parsec.anyChar if Char.ofNat 48 ≤ c ∧ c ≤ Char.ofNat 57 then pure (UInt32.toNat c.val - UInt32.toNat (Char.ofNat 48).val) else if Char.ofNat 97 ≤ c ∧ c ≤ Char.ofNat 102 then pure (UInt32.toNat c.val - UInt32.toNat (Char.ofNat 97).val) else if Char.ofNat 65 ≤ c ∧ c ≤ Char.ofNat 70 then pure (UInt32.toNat c.val - UInt32.toNat (Char.ofNat 65).val) else Lean.Parsec.fail "invalid hex character"

source

def Lean.Json.Parser.escapedChar :

Lean.Parsec Char

Equations

Lean.Json.Parser.escapedChar = do let c ← Lean.Parsec.anyChar match c with | Char.ofNat 92 => pure (Char.ofNat 92) | Char.ofNat 34 => pure (Char.ofNat 34) | Char.ofNat 47 => pure (Char.ofNat 47) | Char.ofNat 98 => pure (Char.ofNat 8) | Char.ofNat 102 => pure (Char.ofNat 12) | Char.ofNat 110 => pure (Char.ofNat 10) | Char.ofNat 114 => pure (Char.ofNat 13) | Char.ofNat 116 => pure (Char.ofNat 9) | Char.ofNat 117 => do let u1 ← Lean.Json.Parser.hexChar let u2 ← Lean.Json.Parser.hexChar let u3 ← Lean.Json.Parser.hexChar let u4 ← Lean.Json.Parser.hexChar pure (Char.ofNat (4096 * u1 + 256 * u2 + 16 * u3 + u4)) | x => Lean.Parsec.fail "illegal \\u escape"

source

partial def Lean.Json.Parser.strCore (acc : String) :

Lean.Parsec String

source

def Lean.Json.Parser.str :

Lean.Parsec String

Equations

Lean.Json.Parser.str = Lean.Json.Parser.strCore ""

source

partial def Lean.Json.Parser.natCore (acc : Nat) (digits : Nat) :

Lean.Parsec (Nat × Nat)

source

@[inline]

def Lean.Json.Parser.lookahead (p : Char → Prop) (desc : String) [inst : DecidablePred p] :

Lean.Parsec Unit

Equations

Lean.Json.Parser.lookahead p desc = do let c ← Lean.Parsec.peek! if p c then pure () else Lean.Parsec.fail ("expected " ++ desc)

source

@[inline]

def Lean.Json.Parser.natNonZero :

Lean.Parsec Nat

Equations

Lean.Json.Parser.natNonZero = do Lean.Json.Parser.lookahead (fun c => Char.ofNat 49 ≤ c ∧ c ≤ Char.ofNat 57) "1-9" let discr ← Lean.Json.Parser.natCore 0 0 let x : Nat × Nat := discr match x with | (n, x) => pure n

source

@[inline]

def Lean.Json.Parser.natNumDigits :

Lean.Parsec (Nat × Nat)

Equations

Lean.Json.Parser.natNumDigits = do Lean.Json.Parser.lookahead (fun c => Char.ofNat 48 ≤ c ∧ c ≤ Char.ofNat 57) "digit" Lean.Json.Parser.natCore 0 0

source

@[inline]

def Lean.Json.Parser.natMaybeZero :

Lean.Parsec Nat

Equations

Lean.Json.Parser.natMaybeZero = do let discr ← Lean.Json.Parser.natNumDigits let x : Nat × Nat := discr match x with | (n, x) => pure n

source

def Lean.Json.Parser.num :

Lean.Parsec Lean.JsonNumber

Equations

Lean.Json.Parser.num = do let c ← Lean.Parsec.peek! let _do_jp : Int → Lean.Parsec Lean.JsonNumber := fun sign => do let c ← Lean.Parsec.peek! let _do_jp : Nat → Lean.Parsec Lean.JsonNumber := fun res => do let c? ← Lean.Parsec.peek? let _do_jp : Lean.JsonNumber → Lean.Parsec Lean.JsonNumber := fun res => do let c? ← Lean.Parsec.peek? if c? = some (Char.ofNat 101) ∨ c? = some (Char.ofNat 69) then do Lean.Parsec.skip let c ← Lean.Parsec.peek! if c = Char.ofNat 45 then do Lean.Parsec.skip let n ← Lean.Json.Parser.natMaybeZero pure (Lean.JsonNumber.shiftr res n) else let _do_jp := fun y => do let n ← Lean.Json.Parser.natMaybeZero let _do_jp : PUnit → Lean.Parsec Lean.JsonNumber := fun y => pure (Lean.JsonNumber.shiftl res n) if n > USize.size then do let y ← Lean.Parsec.fail "exp too large" _do_jp y else do let y ← pure PUnit.unit _do_jp y; if c = Char.ofNat 43 then do let y ← Lean.Parsec.skip _do_jp y else do let y ← pure PUnit.unit _do_jp y else pure res if c? = some (Char.ofNat 46) then do Lean.Parsec.skip let discr ← Lean.Json.Parser.natNumDigits let x : Nat × Nat := discr match x with | (n, d) => let _do_jp := fun y => let mantissa' := sign * (Int.ofNat res * Int.ofNat (10 ^ d) + Int.ofNat n); let exponent' := d; do let y ← pure { mantissa := mantissa', exponent := exponent' } _do_jp y; if d > USize.size then do let y ← Lean.Parsec.fail "too many decimals" _do_jp y else do let y ← pure PUnit.unit _do_jp y else do let y ← pure (Lean.JsonNumber.fromInt (sign * Int.ofNat res)) _do_jp y if c = Char.ofNat 48 then do Lean.Parsec.skip let y ← pure 0 _do_jp y else do let y ← Lean.Json.Parser.natNonZero _do_jp y if c = Char.ofNat 45 then do Lean.Parsec.skip let y ← pure (-1) _do_jp y else do let y ← pure 1 _do_jp y

source

partial def Lean.Json.Parser.arrayCore (anyCore : Unit → Lean.Parsec Lean.Json) (acc : Array Lean.Json) :

Lean.Parsec (Array Lean.Json)

source

partial def Lean.Json.Parser.objectCore (anyCore : Unit → Lean.Parsec Lean.Json) :

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

source

partial def Lean.Json.Parser.anyCore (u : Unit) :

Lean.Parsec Lean.Json

source

def Lean.Json.Parser.any :

Lean.Parsec Lean.Json

Equations

Lean.Json.Parser.any = do Lean.Parsec.ws let res ← Lean.Json.Parser.anyCore () Lean.Parsec.eof pure res

source

def Lean.Json.parse (s : String) :

Except String Lean.Json

Equations

Lean.Json.parse s = match Lean.Json.Parser.any (String.mkIterator s) with | Lean.Parsec.ParseResult.success x res => Except.ok res | Lean.Parsec.ParseResult.error it err => Except.error (toString "offset " ++ toString (Nat.repr it.i) ++ toString ": " ++ toString err ++ toString "")