module Generic.ReflectionTermNativeJson where

open import Generic.Core hiding (natAtom; stringAtom)
open import Generic.NativeJson
open import Generic.CanonicalJson
open import Generic.CanonicalNativeJson
import Generic.Json as GenericJson
import Generic.ReflectionTerm as RT
import FF.Json as Json
import FF.Json.Native as Native

open import Cubical.Data.Maybe.Base using (Maybe; just; nothing)
import Cubical.Data.Maybe.Properties as MaybeProperties
import Agda.Builtin.Reflection as R
import Agda.Builtin.Word as Word
import Agda.Builtin.Float as Float
import Agda.Builtin.Char as Char
import Agda.Builtin.UUID as UUID

toTermAtomCodeIndex : RT.TermAtomCode → ℕ
toTermAtomCodeIndex RT.natAtom = zero
toTermAtomCodeIndex RT.nameAtom = suc zero
toTermAtomCodeIndex RT.metaAtom = suc (suc zero)
toTermAtomCodeIndex RT.literalAtom = suc (suc (suc zero))
toTermAtomCodeIndex RT.stringAtom = suc (suc (suc (suc zero)))

fromTermAtomCodeIndex : ℕ → Maybe RT.TermAtomCode
fromTermAtomCodeIndex zero = just RT.natAtom
fromTermAtomCodeIndex (suc zero) = just RT.nameAtom
fromTermAtomCodeIndex (suc (suc zero)) = just RT.metaAtom
fromTermAtomCodeIndex (suc (suc (suc zero))) = just RT.literalAtom
fromTermAtomCodeIndex (suc (suc (suc (suc zero)))) = just RT.stringAtom
fromTermAtomCodeIndex (suc (suc (suc (suc (suc _))))) = nothing

fromTermAtomCodeIndex-toIndex :
  (a : RT.TermAtomCode) →
  fromTermAtomCodeIndex (toTermAtomCodeIndex a) ≡ just a
fromTermAtomCodeIndex-toIndex RT.natAtom = refl
fromTermAtomCodeIndex-toIndex RT.nameAtom = refl
fromTermAtomCodeIndex-toIndex RT.metaAtom = refl
fromTermAtomCodeIndex-toIndex RT.literalAtom = refl
fromTermAtomCodeIndex-toIndex RT.stringAtom = refl

fromTermAtomCodeIndex-index : ∀ {k a} →
                              fromTermAtomCodeIndex k ≡ just a →
                              toTermAtomCodeIndex a ≡ k
fromTermAtomCodeIndex-index {k = zero} {a} p =
  cong toTermAtomCodeIndex
    (sym (MaybeProperties.just-inj RT.natAtom a p))
fromTermAtomCodeIndex-index {k = suc zero} {a} p =
  cong toTermAtomCodeIndex
    (sym (MaybeProperties.just-inj RT.nameAtom a p))
fromTermAtomCodeIndex-index {k = suc (suc zero)} {a} p =
  cong toTermAtomCodeIndex
    (sym (MaybeProperties.just-inj RT.metaAtom a p))
fromTermAtomCodeIndex-index {k = suc (suc (suc zero))} {a} p =
  cong toTermAtomCodeIndex
    (sym (MaybeProperties.just-inj RT.literalAtom a p))
fromTermAtomCodeIndex-index {k = suc (suc (suc (suc zero)))} {a} p =
  cong toTermAtomCodeIndex
    (sym (MaybeProperties.just-inj RT.stringAtom a p))
fromTermAtomCodeIndex-index {k = suc (suc (suc (suc (suc k))))} p =
  nothing≡just-elim p

termAtomCodeToNativeJSON : Native.ToJSON RT.TermAtomCode
termAtomCodeToNativeJSON =
  Native.mkToJSON λ a → Native.jnumber (toTermAtomCodeIndex a)

termAtomCodeFromNativeJSON : Native.FromJSON RT.TermAtomCode
termAtomCodeFromNativeJSON =
  Native.mkFromJSON λ j →
    GenericJson.maybeBind
      (fromNativeJSON Native.numberFromJson j)
      fromTermAtomCodeIndex

termAtomCodeNativeRoundtrip :
  (a : RT.TermAtomCode) →
  Json.fromJSON termAtomCodeFromNativeJSON
    (Json.toJSON termAtomCodeToNativeJSON a)
    ≡ just a
termAtomCodeNativeRoundtrip a =
  fromTermAtomCodeIndex-toIndex a

termAtomCodeFromToNativeJSON : Native.FromToJSON RT.TermAtomCode
termAtomCodeFromToNativeJSON =
  Native.mkFromToJSON
    termAtomCodeToNativeJSON
    termAtomCodeFromNativeJSON
    termAtomCodeNativeRoundtrip

termAtomCodeCanonical :
  (j : JsonValue) → (a : RT.TermAtomCode) →
  fromNativeJSON termAtomCodeFromNativeJSON j ≡ just a →
  toNativeJSON termAtomCodeToNativeJSON a ≡ j
termAtomCodeCanonical j a p with inspect (fromNativeJSON Native.numberFromJson j)
... | nothing , natEq =
  nothing≡just-elim
    (sym (cong (λ m → GenericJson.maybeBind m fromTermAtomCodeIndex) natEq) ∙ p)
... | just k , natEq with inspect (fromTermAtomCodeIndex k)
...   | nothing , codeEq =
  nothing≡just-elim
    (sym
      (cong (λ m → GenericJson.maybeBind m fromTermAtomCodeIndex) natEq ∙ codeEq)
    ∙ p)
...   | just a' , codeEq =
  cong Native.jnumber
    ( cong toTermAtomCodeIndex
        (sym (MaybeProperties.just-inj a' a
          (sym
            (cong (λ m → GenericJson.maybeBind m fromTermAtomCodeIndex) natEq ∙ codeEq)
          ∙ p)))
    ∙ fromTermAtomCodeIndex-index codeEq )
  ∙ canonical canonicalNatFromToJSON j k natEq

canonicalTermAtomCodeFromToNativeJSON :
  CanonicalFromToJSON RT.TermAtomCode
canonicalTermAtomCodeFromToNativeJSON =
  canonicalFromToJSON'
    termAtomCodeFromToNativeJSON
    termAtomCodeCanonical

natToNativeJSON : Native.ToJSON ℕ
natToNativeJSON = Native.numberToJson

natFromNativeJSON : Native.FromJSON ℕ
natFromNativeJSON = Native.numberFromJson

natFromToNativeJSON : Native.FromToJSON ℕ
natFromToNativeJSON = Native.numberFromToJson

nameToNativeJSON : Native.ToJSON R.Name
nameToNativeJSON =
  Native.mkToJSON λ x → Native.jstring (R.primShowQName x)

metaToNativeJSON : Native.ToJSON R.Meta
metaToNativeJSON =
  Native.mkToJSON λ x → Native.jstring (R.primShowMeta x)

literalToNativeJSONValue : R.Literal → JsonValue
literalToNativeJSONValue (R.nat n) =
  Native.jarray (Native.jstring "nat" ∷ Native.jnumber n ∷ [])
literalToNativeJSONValue (R.word64 n) =
  Native.jarray (Native.jstring "word64" ∷ Native.jnumber (Word.primWord64ToNat n) ∷ [])
literalToNativeJSONValue (R.float x) =
  Native.jarray (Native.jstring "float" ∷ Native.jstring (Float.primShowFloat x) ∷ [])
literalToNativeJSONValue (R.char c) =
  Native.jarray (Native.jstring "char" ∷ Native.jnumber (Char.primCharToNat c) ∷ [])
literalToNativeJSONValue (R.string s) =
  Native.jarray (Native.jstring "string" ∷ Native.jstring s ∷ [])
literalToNativeJSONValue (R.uuid u) =
  Native.jarray (Native.jstring "uuid" ∷ Native.jstring (UUID.primUUIDToString u) ∷ [])
literalToNativeJSONValue (R.name x) =
  Native.jarray (Native.jstring "name" ∷ Native.jstring (R.primShowQName x) ∷ [])
literalToNativeJSONValue (R.meta x) =
  Native.jarray (Native.jstring "meta" ∷ Native.jstring (R.primShowMeta x) ∷ [])

literalToNativeJSON : Native.ToJSON R.Literal
literalToNativeJSON =
  Native.mkToJSON literalToNativeJSONValue

termAtomValueNativeToCodecs :
  NativeAtomValueToCodecs RT.TermAtoms
termAtomValueNativeToCodecs RT.natAtom = natToNativeJSON
termAtomValueNativeToCodecs RT.nameAtom = nameToNativeJSON
termAtomValueNativeToCodecs RT.metaAtom = metaToNativeJSON
termAtomValueNativeToCodecs RT.literalAtom = literalToNativeJSON
termAtomValueNativeToCodecs RT.stringAtom = Native.stringToJson

record ReflectionLeafNativeCodecs : Type₀ where
  constructor reflectionLeafNativeCodecs
  field
    nameCodec    : Native.FromToJSON R.Name
    metaCodec    : Native.FromToJSON R.Meta
    literalCodec : Native.FromToJSON R.Literal

open ReflectionLeafNativeCodecs public

record CanonicalReflectionLeafNativeCodecs : Type₀ where
  constructor canonicalReflectionLeafNativeCodecs
  field
    canonicalNameCodec    : CanonicalFromToJSON R.Name
    canonicalMetaCodec    : CanonicalFromToJSON R.Meta
    canonicalLiteralCodec : CanonicalFromToJSON R.Literal

open CanonicalReflectionLeafNativeCodecs public

termAtomValueNativeCodecs :
  ReflectionLeafNativeCodecs →
  NativeAtomValueCodecs RT.TermAtoms
termAtomValueNativeCodecs codecs RT.natAtom = natFromToNativeJSON
termAtomValueNativeCodecs codecs RT.nameAtom = nameCodec codecs
termAtomValueNativeCodecs codecs RT.metaAtom = metaCodec codecs
termAtomValueNativeCodecs codecs RT.literalAtom = literalCodec codecs
termAtomValueNativeCodecs codecs RT.stringAtom = Native.stringFromToJson

canonicalTermAtomValueNativeCodecs :
  CanonicalReflectionLeafNativeCodecs →
  CanonicalNativeAtomValueCodecs RT.TermAtoms
canonicalTermAtomValueNativeCodecs codecs RT.natAtom = canonicalNatFromToJSON
canonicalTermAtomValueNativeCodecs codecs RT.nameAtom = canonicalNameCodec codecs
canonicalTermAtomValueNativeCodecs codecs RT.metaAtom = canonicalMetaCodec codecs
canonicalTermAtomValueNativeCodecs codecs RT.literalAtom = canonicalLiteralCodec codecs
canonicalTermAtomValueNativeCodecs codecs RT.stringAtom = canonicalStringFromToJSON

termSpecificationFromToNativeJSON :
  Native.FromToJSON (GenericSpecification RT.TermAtoms)
termSpecificationFromToNativeJSON =
  genericSpecificationFromToNativeJSON termAtomCodeFromToNativeJSON

canonicalTermSpecificationFromToNativeJSON :
  CanonicalFromToJSON (GenericSpecification RT.TermAtoms)
canonicalTermSpecificationFromToNativeJSON =
  canonicalGenericSpecificationFromToNativeJSON
    canonicalTermAtomCodeFromToNativeJSON

termSpecificationNativeJSON : JsonValue
termSpecificationNativeJSON =
  toSpecificationNativeJSON
    termAtomCodeFromToNativeJSON
    (specificationOf RT.genericTerm)

termFromToNativeJSON :
  ReflectionLeafNativeCodecs →
  Native.FromToJSON R.Term
termFromToNativeJSON codecs =
  genericFromToNativeJSON
    (termAtomValueNativeCodecs codecs)
    RT.genericTerm

canonicalTermFromToNativeJSON :
  CanonicalReflectionLeafNativeCodecs →
  CanonicalFromToJSON R.Term
canonicalTermFromToNativeJSON codecs =
  canonicalGenericFromToNativeJSON
    (canonicalTermAtomValueNativeCodecs codecs)
    RT.genericTerm

termToNativeJSONCodec : Native.ToJSON R.Term
termToNativeJSONCodec =
  genericToNativeJSON
    termAtomValueNativeToCodecs
    RT.genericTerm

termToNativeJSON : R.Term → JsonValue
termToNativeJSON =
  toNativeJSON termToNativeJSONCodec

termToNativeJSONWithCodecs :
  ReflectionLeafNativeCodecs →
  R.Term →
  JsonValue
termToNativeJSONWithCodecs codecs =
  toNativeJSON (Json.FromToJSON'.to (termFromToNativeJSON codecs))

termFromNativeJSON :
  ReflectionLeafNativeCodecs →
  JsonValue →
  Maybe R.Term
termFromNativeJSON codecs =
  fromNativeJSON (Json.FromToJSON'.from (termFromToNativeJSON codecs))

renderTermNativeJSON : R.Term → String
renderTermNativeJSON =
  renderNativeJSON termToNativeJSONCodec

renderTermNativeJSONWithCodecs :
  ReflectionLeafNativeCodecs →
  R.Term →
  String
renderTermNativeJSONWithCodecs codecs =
  renderNativeJSON (Json.FromToJSON'.to (termFromToNativeJSON codecs))

renderTermPrettyNativeJSON : R.Term → String
renderTermPrettyNativeJSON =
  renderPrettyNativeJSON termToNativeJSONCodec

renderTermPrettyNativeJSONWithCodecs :
  ReflectionLeafNativeCodecs →
  R.Term →
  String
renderTermPrettyNativeJSONWithCodecs codecs =
  renderPrettyNativeJSON (Json.FromToJSON'.to (termFromToNativeJSON codecs))