module FF.Json.Native where

open import Agda.Builtin.String
  using (String)
open import Agda.Builtin.Unit
  using (⊤; tt)

open import Cubical.Foundations.Prelude
  using (Type; _≡_; refl; ℓ-zero)
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 (ℕ)
open import Cubical.Data.Sigma.Base
  using (_×_; _,_)

open import FF.Json.Base

data NativeCode : Type ℓ-zero where
  string number boolean null : NativeCode

NativeEl : NativeCode → Type ℓ-zero
NativeEl string = String
NativeEl number = ℕ
NativeEl boolean = Bool
NativeEl null = ⊤

renderNativeAtom : (c : NativeCode) → NativeEl c → String
renderNativeAtom string s = quoteString s
renderNativeAtom number n = showNat n
renderNativeAtom boolean true = "true"
renderNativeAtom boolean false = "false"
renderNativeAtom null tt = "null"

Native : AtomUniverse _
Native = mkAtomUniverse NativeCode NativeEl renderNativeAtom

JsonValue : Type ℓ-zero
JsonValue = Json Native

ToJSON : ∀ {ℓA} → Type ℓA → Type ℓA
ToJSON = ToJSON' Native

FromJSON : ∀ {ℓA} → Type ℓA → Type ℓA
FromJSON = FromJSON' Native

FromToJSON : ∀ {ℓA} → Type ℓA → Type ℓA
FromToJSON = FromToJSON' Native

mkToJSON : ∀ {ℓA} {A : Type ℓA} → (A → JsonValue) → ToJSON A
mkToJSON = mkToJSON'

mkFromJSON : ∀ {ℓA} {A : Type ℓA} → (JsonValue → Maybe A) → FromJSON A
mkFromJSON = mkFromJSON'

mkFromToJSON : ∀ {ℓA} {A : Type ℓA} →
               (to : ToJSON A) → (from : FromJSON A) →
               ((x : A) → fromJSON from (toJSON to x) ≡ just x) →
               FromToJSON A
mkFromToJSON = mkFromToJSON'

jstring : String → JsonValue
jstring = atom string

jnumber : ℕ → JsonValue
jnumber = atom number

jbool : Bool → JsonValue
jbool = atom boolean

jnull : JsonValue
jnull = atom null tt

jarray : List JsonValue → JsonValue
jarray = array

jobject : List (String × JsonValue) → JsonValue
jobject = object

stringToJson : ToJSON String
stringToJson = mkToJSON jstring

stringFromJson : FromJSON String
stringFromJson = mkFromJSON fromString
  where
  fromString : JsonValue → Maybe String
  fromString (atom string s) = just s
  fromString _ = nothing

stringFromToJson : FromToJSON String
stringFromToJson = mkFromToJSON stringToJson stringFromJson (λ _ → refl)

boolToJson : ToJSON Bool
boolToJson = mkToJSON jbool

boolFromJson : FromJSON Bool
boolFromJson = mkFromJSON fromBool
  where
  fromBool : JsonValue → Maybe Bool
  fromBool (atom boolean b) = just b
  fromBool _ = nothing

boolFromToJson : FromToJSON Bool
boolFromToJson = mkFromToJSON boolToJson boolFromJson (λ _ → refl)

jsonToJson : ToJSON JsonValue
jsonToJson = mkToJSON (λ x → x)

jsonFromJson : FromJSON JsonValue
jsonFromJson = mkFromJSON just

jsonFromToJson : FromToJSON JsonValue
jsonFromToJson = mkFromToJSON jsonToJson jsonFromJson (λ _ → refl)

numberToJson : ToJSON ℕ
numberToJson = mkToJSON jnumber

numberFromJson : FromJSON ℕ
numberFromJson = mkFromJSON fromNumber
  where
  fromNumber : JsonValue → Maybe ℕ
  fromNumber (atom number n) = just n
  fromNumber _ = nothing

numberFromToJson : FromToJSON ℕ
numberFromToJson = mkFromToJSON numberToJson numberFromJson (λ _ → refl)