module FF.Json.Base where

open import Agda.Builtin.String
  using (String; primStringAppend; primShowNat; primShowString)

open import Cubical.Foundations.Prelude
  using (Level; Type; _≡_; ℓ-max; ℓ-suc)
open import Cubical.Data.Bool.Base
  using (Bool; true; false)
open import Cubical.Data.List.Base
  using (List; []; _∷_; _++_)
open import Cubical.Data.Maybe.Base
  using (Maybe; just; nothing)
open import Cubical.Data.Nat.Base
  using (ℕ; zero; suc)
open import Cubical.Data.Sigma.Base
  using (_×_; _,_)

infixr  _<>_

_<>_ : String → String → String
_<>_ = primStringAppend

record AtomUniverse (ℓ : Level) : Type (ℓ-suc ℓ) where
  constructor mkAtomUniverse
  field
    Code       : Type ℓ
    El         : Code → Type ℓ
    renderAtom : (c : Code) → El c → String

open AtomUniverse public

data Json {ℓ : Level} (U : AtomUniverse ℓ) : Type ℓ where
  atom   : (c : Code U) → El U c → Json U
  array  : List (Json U) → Json U
  object : List (String × Json U) → Json U

quoteString : String → String
quoteString = primShowString

showNat : ℕ → String
showNat = primShowNat

join : String → List String → String
join sep [] = ""
join sep (x ∷ []) = x
join sep (x ∷ y ∷ xs) = x <> sep <> join sep (y ∷ xs)

indent : ℕ → String
indent zero = ""
indent (suc n) = "  " <> indent n

mutual
  renderCompact : ∀ {ℓ} {U : AtomUniverse ℓ} → Json U → String
  renderCompact {U = U} (atom c x) = renderAtom U c x
  renderCompact (array xs) = "[" <> renderCompactList xs <> "]"
  renderCompact (object xs) = "{" <> renderCompactFields xs <> "}"

  renderCompactList : ∀ {ℓ} {U : AtomUniverse ℓ} → List (Json U) → String
  renderCompactList [] = ""
  renderCompactList (x ∷ []) = renderCompact x
  renderCompactList (x ∷ y ∷ xs) =
    renderCompact x <> "," <> renderCompactList (y ∷ xs)

  renderCompactFields : ∀ {ℓ} {U : AtomUniverse ℓ} →
                        List (String × Json U) → String
  renderCompactFields [] = ""
  renderCompactFields ((k , v) ∷ []) =
    quoteString k <> ":" <> renderCompact v
  renderCompactFields ((k , v) ∷ y ∷ xs) =
    quoteString k <> ":" <> renderCompact v <> "," <> renderCompactFields (y ∷ xs)

mutual
  renderPrettyAt : ∀ {ℓ} {U : AtomUniverse ℓ} → ℕ → Json U → String
  renderPrettyAt {U = U} depth (atom c x) = renderAtom U c x
  renderPrettyAt depth (array []) = "[]"
  renderPrettyAt depth (array (x ∷ xs)) =
    "[\n"
    <> renderPrettyItems depth (x ∷ xs)
    <> "\n"
    <> indent depth
    <> "]"
  renderPrettyAt depth (object []) = "{}"
  renderPrettyAt depth (object (x ∷ xs)) =
    "{\n"
    <> renderPrettyFields depth (x ∷ xs)
    <> "\n"
    <> indent depth
    <> "}"

  renderPrettyItems : ∀ {ℓ} {U : AtomUniverse ℓ} → ℕ → List (Json U) → String
  renderPrettyItems depth [] = ""
  renderPrettyItems depth (x ∷ []) =
    indent (suc depth) <> renderPrettyAt (suc depth) x
  renderPrettyItems depth (x ∷ y ∷ xs) =
    indent (suc depth) <> renderPrettyAt (suc depth) x
    <> ",\n"
    <> renderPrettyItems depth (y ∷ xs)

  renderPrettyFields : ∀ {ℓ} {U : AtomUniverse ℓ} →
                       ℕ → List (String × Json U) → String
  renderPrettyFields depth [] = ""
  renderPrettyFields depth ((k , v) ∷ []) =
    indent (suc depth) <> quoteString k <> ": " <> renderPrettyAt (suc depth) v
  renderPrettyFields depth ((k , v) ∷ y ∷ xs) =
    indent (suc depth) <> quoteString k <> ": " <> renderPrettyAt (suc depth) v
    <> ",\n"
    <> renderPrettyFields depth (y ∷ xs)

renderPretty : ∀ {ℓ} {U : AtomUniverse ℓ} → Json U → String
renderPretty = renderPrettyAt zero

record ToJSON' {ℓA ℓU : Level} (U : AtomUniverse ℓU)
               (A : Type ℓA) : Type (ℓ-max ℓA ℓU) where
  constructor mkToJSON'
  field
    toJSON : A → Json U

open ToJSON' public

record FromJSON' {ℓA ℓU : Level} (U : AtomUniverse ℓU)
                 (A : Type ℓA) : Type (ℓ-max ℓA ℓU) where
  constructor mkFromJSON'
  field
    fromJSON : Json U → Maybe A

open FromJSON' public

record FromToJSON' {ℓA ℓU : Level} (U : AtomUniverse ℓU)
                   (A : Type ℓA) : Type (ℓ-max ℓA ℓU) where
  constructor mkFromToJSON'
  field
    to   : ToJSON' U A
    from : FromJSON' U A
    roundtrip : (x : A) → fromJSON from (toJSON to x) ≡ just x

open FromToJSON' public

encodeWith : ∀ {ℓA ℓU} {U : AtomUniverse ℓU} {A : Type ℓA} →
             ToJSON' U A → A → Json U
encodeWith codec x = toJSON codec x

decodeWith : ∀ {ℓA ℓU} {U : AtomUniverse ℓU} {A : Type ℓA} →
             FromJSON' U A → Json U → Maybe A
decodeWith codec x = fromJSON codec x

renderWith : ∀ {ℓA ℓU} {U : AtomUniverse ℓU} {A : Type ℓA} →
             ToJSON' U A → A → String
renderWith codec x = renderCompact (encodeWith codec x)

renderPrettyWith : ∀ {ℓA ℓU} {U : AtomUniverse ℓU} {A : Type ℓA} →
                   ToJSON' U A → A → String
renderPrettyWith codec x = renderPretty (encodeWith codec x)