json.lean

class has_range (α : Type) :=
(range : α → α → list α)

infix `..`:50 := has_range.range

instance : has_range ℕ :=
{ range := λ a b, (+ a) <$> list.range (b + 1 - a) }

instance : has_range char :=
{ range := λ a b, char.of_nat <$> (a.to_nat .. b.to_nat) }

#eval 'a'..'z'
#eval 'A'..'z'
#eval 10..20
#eval 1..2

def list.asum {m α} [alternative m] : list (m α) → m α :=
list.foldr (<|>) failure

----------------------------------------------------------------
-- parser

def parser (α : Type) :=
list char → list (list char × α)

namespace parser
  variables {α β : Type}

  protected def pure (value : α) : parser α :=
  λ input, [⟨input, value⟩]

  protected def bind (p : parser α) (f : α → parser β) : parser β :=
  λ input₁, do ⟨input₂, value⟩ ← p input₁, f value input₂

  protected def failure : parser α :=
  λ _, []

  protected def orelse (p q : parser α) : parser α :=
  λ input, p input ++ q input

  instance : monad parser :=
  { pure := @parser.pure, bind := @parser.bind }

  instance : alternative parser :=
  { failure := @parser.failure, orelse := @parser.orelse }

  def sat (pred : char → Prop) [decidable_pred pred] : parser char
  | [] := []
  | (c::input) := do guard (pred c), pure ⟨input, c⟩

  def sat_option (pred : char → option α) : parser α
  | [] := []
  | (c::input) :=
    match pred c with
    | some x := [⟨input, x⟩]
    | none := []
    end

  def any_char : parser char :=
  sat (λ_, tt)

  def ch (c : char) : parser char :=
  sat (= c)

  def ch' (c : char) : parser unit :=
  ch c $> ⟨⟩

  def one_of (cs : list char) : parser char :=
  sat (∈ cs)

  def str (s : string) : parser unit :=
  s.to_list.mmap' ch

  def eof : parser unit
  | [] := [⟨[], ⟨⟩⟩]
  | _ := failure

  private def fix_core (f : parser α → parser α) : ℕ → parser α
  | 0 := failure
  | (n + 1) := f (fix_core n)

  def fix (f : parser α → parser α) : parser α :=
  λ input, fix_core f (input.length + 1) input

  private def foldr_core (f : α → β → β) (p : parser α) (b : β) : ℕ → parser β
  | 0 := failure
  | (n + 1) := (do x ← p, xs ← foldr_core n, pure (f x xs)) <|> pure b

  def foldr (f : α → β → β) (p : parser α) (b : β) : parser β :=
  λ input, foldr_core f p b (input.length + 1) input

  def many (p : parser α) : parser (list α) :=
  foldr (::) p []

  def some (p : parser α) : parser (list α) :=
  do x ← p, xs ← many p, pure (x :: xs)

  def sep_by1 (sep : parser unit) (p : parser α) : parser (list α) :=
  do x ← p, xs ← many (sep >> p), pure (x :: xs)

  def sep_by (sep : parser unit) (p : parser α) : parser (list α) :=
  sep_by1 sep p <|> pure []

  def between (before after : parser β) (p : parser α) : parser α :=
    before *> p <* after

  def digit : parser ℕ :=
  do c ← sat char.is_digit, pure (c.to_nat - '0'.to_nat)

  def nat : parser ℕ :=
  list.foldl (λn digit, n * 10 + digit) 0 <$> some digit

  def void {m α} [functor m] : m α → m unit :=
  ($> ⟨⟩)

  def run (p : parser α) (input : string) : option α :=
  prod.snd <$> ((p <* eof) input.to_list).nth 0

end parser

----------------------------------------------------------------
-- json

def from_digits (base : ℕ) : list ℕ → ℕ :=
list.foldl (λ n d, n * base + d) 0

#check option.get_or_else

namespace aeson
  meta inductive value
  | string : string → value
  | object : list (string × value) → value
  | array : list value → value
  | number : ℤ × option ℕ × option ℤ → value
  | bool : bool → value
  | null : value

  meta def value.to_string : value → string
  | (value.string s) := repr s
  | (value.object members) :=
    "{" ++ string.intercalate ", " (((λ ⟨k, v⟩, repr k ++ ": " ++ value.to_string v) : string × value → string) <$> members) ++"}"
  | (value.array elements) :=
    "[" ++ string.intercalate ", " (value.to_string <$> elements) ++ "]"
  | (value.number ⟨i, none, none⟩) := to_string i
  | (value.number ⟨i, some f, none⟩) := to_string i ++ "." ++ to_string f
  | (value.number ⟨i, some f, some e⟩) := to_string i ++ "." ++ to_string f ++ "e" ++ to_string e
  | (value.number ⟨i, none, some e⟩) := to_string i ++ "e" ++ to_string e
  | (value.bool tt) := "true"
  | (value.bool ff) := "false"
  | value.null := "null"

  meta instance : has_to_string value := ⟨value.to_string⟩

  namespace parsers
    open parser

    def ws : parser unit := fix $ λ ws,
    void ∘ optional $
    one_of (char.of_nat <$> [9, 10, 13, 32]) *> ws

    def sign : parser ℤ := list.asum
    [ ch '+' $> 1
    , ch '-' $> -1
    , pure 1 ]

    def onenine : parser ℕ :=
    do c ← one_of ('1'..'9'),
       pure (c.to_nat - '0'.to_nat)

    def digit : parser ℕ := list.asum
    [ (ch '0' $> 0)
    , onenine ]

    def digits : parser (list ℕ) :=
    some digit

    def exponent : parser (option ℤ):=
    optional $
    do one_of ['e', 'E'],
       s ← sign,
       ds ← digits,
       pure (s * from_digits 10 ds)

    def fraction : parser (option ℕ) :=
    optional $
    from_digits 10 <$> (ch '.' *> digits)
    
    def integer : parser ℤ := list.asum
    [ (int.of_nat <$> digit)
    , (do d ← onenine, ds ← digits, pure (from_digits 10 (d::ds)))
    , ((int.neg ∘ int.of_nat) <$> (ch '-' *> digit))
    , (do ch '-', d ← onenine, ds ← digits, pure (int.neg (from_digits 10 (d::ds)))) ]

    def number : parser (ℤ × option ℕ × option ℤ) :=
    do i ← integer, f ← fraction, e ← exponent, pure ⟨i, f, e⟩

    def hex : parser ℕ := list.asum
    [ digit
    , (λ c, char.to_nat c - 'a'.to_nat + 10) <$> one_of ('a'..'f')
    , (λ c, char.to_nat c - 'A'.to_nat + 10) <$> one_of ('A'..'F') ]

    def escape : parser char := list.asum
    [ ch '"'
    , ch '\\'
    , ch '/'
    , ch 'b' $> char.of_nat 0x08
    , ch 'f' $> char.of_nat 0x0C
    , ch 'n' $> '\n'
    , ch 'r' $> char.of_nat 0x0D
    , ch 't' $> '\t'
    , ch 'u' *> (char.of_nat ∘ from_digits 16) <$> monad.sequence [hex, hex, hex, hex] ]

    def character : parser char := list.asum
    [ sat (λ c, c ≠ '"' ∧ c ≠ '\\')
    , ch '\\' *> escape ]

    def characters : parser (list char) :=
    many character

    def string : parser string :=
    list.as_string <$> (ch '"' *> characters <* ch '"')

    def bool : parser bool := list.asum
    [ true <$ str "true"
    , false <$ str "false" ]

    def null : parser unit :=
    str "null"

    meta def element (value : parser aeson.value) : parser aeson.value :=
    ws *> value <* ws

    meta def elements (value : parser aeson.value) : parser (list aeson.value) :=
    sep_by1 (ch' ',') (element value)

    meta def array (value : parser aeson.value) : parser (list aeson.value) := list.asum
    [ ch '[' *> (ws $> []) <* ch ']'
    , ch '[' *> elements value <* ch ']' ]

    meta def member (value : parser aeson.value) : parser (_root_.string × aeson.value) :=
    do k ← ws *> string <* ws, ch ':', v ← element value, pure ⟨k, v⟩

    meta def members (value : parser aeson.value) : parser (list (_root_.string × aeson.value)) :=
    sep_by1 (ch' ',') (member value)

    meta def object (value : parser aeson.value) : parser (list (_root_.string × aeson.value)) := list.asum
    [ ch '{' *> (ws $> []) <* ch '}'
    , ch '{' *> members value <* ch '}' ]

    meta def value : parser aeson.value :=
    λ input, list.asum
    [ aeson.value.object <$> object value
    , aeson.value.array <$> array value
    , aeson.value.string <$> string
    , aeson.value.number <$> number
    , aeson.value.bool <$> bool
    , aeson.value.null <$ null ] input

    meta def json : parser aeson.value := element value
  end parsers
end aeson

#eval has_to_string.to_string <$> aeson.parsers.json.run "[{\"1\": 1}, \"hello world \\u0030\",  1e1, false, null, [[1.1]]]"