module Generic.CanonicalNativeJson where

open import Generic.Core
open import Generic.NativeJson
open import Generic.CanonicalJson

open import Cubical.Data.Maybe.Base using (just)
import Cubical.Data.Maybe.Properties as MaybeProperties
import FF.Json as Json
import FF.Json.Native as Native

CanonicalFromToJSON : ∀ {ℓ} → Type ℓ → Type ℓ
CanonicalFromToJSON A = CanonicalFromToJSON' Native.Native A

CanonicalNativeAtomCodeCodec : ∀ {ℓ} → AtomUniverse ℓ → Type₀
CanonicalNativeAtomCodeCodec U = CanonicalFromToJSON (AtomCode U)

CanonicalNativeAtomValueCodecs : ∀ {ℓ} → AtomUniverse ℓ → Type ℓ
CanonicalNativeAtomValueCodecs U =
  (a : AtomCode U) → CanonicalFromToJSON (Atom U a)

canonicalStringFromToJSON : CanonicalFromToJSON String
canonicalStringFromToJSON =
  canonicalFromToJSON' Native.stringFromToJson canonicalString
  where
  canonicalString : (j : Json.JsonValue) → (x : String) →
                    Json.fromJSON Native.stringFromJson j ≡ just x →
                    Json.toJSON Native.stringToJson x ≡ j
  canonicalString (Json.atom Native.string s) x p =
    cong Native.jstring (sym (MaybeProperties.just-inj s x p))
  canonicalString (Json.atom Native.number n) x p = nothing≡just-elim p
  canonicalString (Json.atom Native.boolean b) x p = nothing≡just-elim p
  canonicalString (Json.atom Native.null u) x p = nothing≡just-elim p
  canonicalString (Json.array xs) x p = nothing≡just-elim p
  canonicalString (Json.object xs) x p = nothing≡just-elim p

canonicalNatFromToJSON : CanonicalFromToJSON ℕ
canonicalNatFromToJSON =
  canonicalFromToJSON' Native.numberFromToJson canonicalNat
  where
  canonicalNat : (j : Json.JsonValue) → (x : ℕ) →
                 Json.fromJSON Native.numberFromJson j ≡ just x →
                 Json.toJSON Native.numberToJson x ≡ j
  canonicalNat (Json.atom Native.string s) x p = nothing≡just-elim p
  canonicalNat (Json.atom Native.number n) x p =
    cong Native.jnumber (sym (MaybeProperties.just-inj n x p))
  canonicalNat (Json.atom Native.boolean b) x p = nothing≡just-elim p
  canonicalNat (Json.atom Native.null u) x p = nothing≡just-elim p
  canonicalNat (Json.array xs) x p = nothing≡just-elim p
  canonicalNat (Json.object xs) x p = nothing≡just-elim p

canonicalBoolFromToJSON : CanonicalFromToJSON Bool
canonicalBoolFromToJSON =
  canonicalFromToJSON' Native.boolFromToJson canonicalBool
  where
  canonicalBool : (j : Json.JsonValue) → (x : Bool) →
                  Json.fromJSON Native.boolFromJson j ≡ just x →
                  Json.toJSON Native.boolToJson x ≡ j
  canonicalBool (Json.atom Native.string s) x p = nothing≡just-elim p
  canonicalBool (Json.atom Native.number n) x p = nothing≡just-elim p
  canonicalBool (Json.atom Native.boolean b) x p =
    cong Native.jbool (sym (MaybeProperties.just-inj b x p))
  canonicalBool (Json.atom Native.null u) x p = nothing≡just-elim p
  canonicalBool (Json.array xs) x p = nothing≡just-elim p
  canonicalBool (Json.object xs) x p = nothing≡just-elim p

canonicalJsonValueFromToJSON : CanonicalFromToJSON JsonValue
canonicalJsonValueFromToJSON =
  canonicalFromToJSON' Native.jsonFromToJson λ j x p →
    sym (MaybeProperties.just-inj j x p)

canonicalGenericSpecificationFromToNativeJSON :
  ∀ {ℓ} {U : AtomUniverse ℓ} →
  CanonicalNativeAtomCodeCodec U →
  CanonicalFromToJSON (GenericSpecification U)
canonicalGenericSpecificationFromToNativeJSON atomCodeCodec =
  canonicalGenericSpecificationFromToJSON
    Native.Native canonicalStringFromToJSON atomCodeCodec

canonicalGenericFromToNativeJSON :
  ∀ {ℓ} {U : AtomUniverse ℓ} {A : Type ℓ} →
  CanonicalNativeAtomValueCodecs U →
  Generic U A →
  CanonicalFromToJSON A
canonicalGenericFromToNativeJSON =
  genericCanonicalFromToJSON Native.Native