json.lean

-- This module serves as the root of the `Json` library.
-- Import modules here that should be built as part of the library.

import Std

inductive Json where
  | null : Json
  | bool (b: Bool)
  | number (n: Int)
  | array (a: List Json)

def Json.numNodes : Json -> Nat
  | Json.null | Json.bool _ | Json.number _ => 1
  | Json.array as =>
      -- some really cursed `attach` magic to make the termination checker see
      --    that the list nodes are subnodes of Json itself:
      as.attach.foldr (fun ⟨a, _h⟩ n => n + Json.numNodes a) 1

def Json.toString : Json → String
  | Json.null => "null"
  | Json.bool b => if b then "true" else "false"
  | Json.number n => n.repr
  | Json.array as =>
      "["++ ", ".intercalate (as.attach.map fun ⟨ a, _h ⟩ => a.toString ) ++"]"

instance : ToString Json where
  toString := Json.toString

#eval (Json.array [Json.bool true, Json.number 42]).numNodes


/-
Parsing
-/

def Error := String

def Substring.span (s: Substring) (pred: Char -> Bool) : (Substring × Substring) :=
  (s.takeWhile pred, s.dropWhile pred)

def Json.parse (s: Substring) : Except Error (Substring × Json) :=
  let (c, s') := (s.take 1, s.drop 1)
  if c.isEmpty then
    Except.error s!"Unexpected end at {s.startPos}"
  else if c.all Char.isWhitespace then
    let s'' := s'.dropWhile Char.isWhitespace
    have : s''.bsize < s.bsize := sorry
    Json.parse s''
  else if c.isNat then
    let (digits, s') := s.span Char.isDigit
    let n := digits.toString.toInt!
    Except.ok (s', Json.number n)
  else if c.all Char.isAlpha then
    let (letters, s') := s.span Char.isAlpha
    match letters.toString with
    | "null" => Except.ok (s', Json.null)
    | "false" => Except.ok (s', Json.bool false)
    | "true" => Except.ok (s', Json.bool true)
    | _ => Except.error s!"Unknown word at {s.startPos}: {letters}"
  else if c.toString.get? 0 == some '[' then
    let rec loop (s : Substring) (as : List Json) : Except Error (Substring × List Json) :=
      let s1 := s.dropWhile Char.isWhitespace
      let (c, s') := (s1.take 1, s1.drop 1)
      match c.toString with
      | "," =>
        have : s'.bsize < s.bsize := sorry
        match Json.parse s' with
        | .error e => Except.error e
        | .ok res =>
            let (s'', a) := res
            have : s''.bsize < s.bsize := sorry
            loop s'' (a :: as)
      | "]" => Except.ok (s', as)
      | _ => Except.error s!"Expected ',' or ']', found: {c}"
    -- consume '['
    have : s'.bsize < s.bsize := sorry
    let s'' := s'.dropWhile Char.isWhitespace
    let (c, s'') := (s''.take 1, s''.drop 1)
    if c.toString == "]"
      then Except.ok (s'', Json.array [])
      else match Json.parse s' with
        | .error e => Except.error e
        | .ok (s'', a) =>
          have : s''.bsize < s.bsize := sorry
          match loop s'' [a] with
          | .error e => Except.error e
          | .ok (s', as) => Except.ok (s', Json.array as.reverse)
  else
    Except.error s!"Unknown char at {s.startPos}: {c}"
termination_by _ => s.bsize


#eval Json.parse "null"
#eval Json.parse "[ false  ]"
#eval Json.parse "[false , 1,2, [3]]"


#eval ("привіт".toSubstring)
#eval "12".drop 1