module Generic.NativeJson where

open import Generic.Core
open import Cubical.Data.Maybe.Base using (Maybe)
import Generic.Json as GenericJson
import FF.Json as Json
import FF.Json.Native as Native

open GenericJson public
  using
    ( DescVec
    ; GenericSpecification
    ; specificationOf
    ; descOfSpecification
    ; typeNameOfSpecification
    ; constructorNamesOfSpecification
    )

JsonValue : Type₀
JsonValue = Native.JsonValue

ToJSON : ∀ {ℓ} → Type ℓ → Type ℓ
ToJSON = Native.ToJSON

FromJSON : ∀ {ℓ} → Type ℓ → Type ℓ
FromJSON = Native.FromJSON

FromToJSON : ∀ {ℓ} → Type ℓ → Type ℓ
FromToJSON = Native.FromToJSON

NativeAtomCodeCodec : ∀ {ℓ} → AtomUniverse ℓ → Type₀
NativeAtomCodeCodec U = Native.FromToJSON (AtomCode U)

NativeAtomValueCodecs : ∀ {ℓ} → AtomUniverse ℓ → Type ℓ
NativeAtomValueCodecs U = (a : AtomCode U) → Native.FromToJSON (Atom U a)

NativeAtomValueToCodecs : ∀ {ℓ} → AtomUniverse ℓ → Type ℓ
NativeAtomValueToCodecs U = (a : AtomCode U) → Native.ToJSON (Atom U a)

toSpecificationNativeJSON :
  ∀ {ℓ} {U : AtomUniverse ℓ} →
  NativeAtomCodeCodec U →
  GenericSpecification U →
  JsonValue
toSpecificationNativeJSON =
  GenericJson.toSpecificationJSON Native.stringFromToJson

fromSpecificationNativeJSON :
  ∀ {ℓ} {U : AtomUniverse ℓ} →
  NativeAtomCodeCodec U →
  JsonValue →
  Maybe (GenericSpecification U)
fromSpecificationNativeJSON =
  GenericJson.fromSpecificationJSON Native.stringFromToJson

genericSpecificationFromToNativeJSON :
  ∀ {ℓ} {U : AtomUniverse ℓ} →
  NativeAtomCodeCodec U →
  Native.FromToJSON (GenericSpecification U)
genericSpecificationFromToNativeJSON =
  GenericJson.genericSpecificationFromToJSON Native.Native Native.stringFromToJson

toRootCodeNativeJSON :
  ∀ {ℓ n} {U : AtomUniverse ℓ}
  (atomCodecs : NativeAtomValueCodecs U) →
  (D : Fin n → TyDesc U n) →
  (r : RootDesc U n) →
  RootCodeIx U D r →
  JsonValue
toRootCodeNativeJSON =
  GenericJson.toRootCodeJSON

toRootCodeNativeJSONWith :
  ∀ {ℓ n} {U : AtomUniverse ℓ}
  (atomCodecs : NativeAtomValueToCodecs U) →
  (D : Fin n → TyDesc U n) →
  (r : RootDesc U n) →
  RootCodeIx U D r →
  JsonValue
toRootCodeNativeJSONWith =
  GenericJson.toRootCodeJSONWith

fromRootCodeNativeJSON :
  ∀ {ℓ n} {U : AtomUniverse ℓ}
  (atomCodecs : NativeAtomValueCodecs U) →
  (D : Fin n → TyDesc U n) →
  (r : RootDesc U n) →
  JsonValue →
  Maybe (RootCodeIx U D r)
fromRootCodeNativeJSON =
  GenericJson.fromRootCodeJSON

genericFromToNativeJSON :
  ∀ {ℓ} {U : AtomUniverse ℓ} {A : Type ℓ} →
  NativeAtomValueCodecs U →
  Generic U A →
  Native.FromToJSON A
genericFromToNativeJSON =
  GenericJson.genericFromToJSON Native.Native

genericToNativeJSON :
  ∀ {ℓ} {U : AtomUniverse ℓ} {A : Type ℓ} →
  NativeAtomValueToCodecs U →
  Generic U A →
  Native.ToJSON A
genericToNativeJSON =
  GenericJson.genericToJSON Native.Native

toNativeJSON :
  ∀ {ℓ} {A : Type ℓ} →
  Native.ToJSON A →
  A →
  JsonValue
toNativeJSON =
  Json.toJSON

fromNativeJSON :
  ∀ {ℓ} {A : Type ℓ} →
  Native.FromJSON A →
  JsonValue →
  Maybe A
fromNativeJSON =
  Json.fromJSON

renderNativeJSON :
  ∀ {ℓ} {A : Type ℓ} →
  Native.ToJSON A →
  A →
  String
renderNativeJSON =
  Json.renderWith

renderPrettyNativeJSON :
  ∀ {ℓ} {A : Type ℓ} →
  Native.ToJSON A →
  A →
  String
renderPrettyNativeJSON =
  Json.renderPrettyWith