module Generic.PrimAtom where

open import Generic.Core hiding (natAtom; stringAtom; boolAtom)
open import Generic.NativeJson
open import Generic.CanonicalJson
open import Generic.CanonicalNativeJson
open import Generic.Default

import Cubical.Data.Int.Base as IntBase
import Cubical.Data.Maybe.Properties as MaybeProperties
open IntBase public using (pos; negsuc)
open import Cubical.Data.Maybe.Base using (Maybe; just; nothing)
import FF.Json as Json
import FF.Json.Native as Native
import Generic.Json as GenericJson

Int : Type₀
Int = IntBase.ℤ

data PrimAtomCode : Type₀ where
  stringAtom natAtom intAtom boolAtom : PrimAtomCode

PrimAtom : PrimAtomCode → Type₀
PrimAtom stringAtom = String
PrimAtom natAtom = ℕ
PrimAtom intAtom = Int
PrimAtom boolAtom = Bool

PrimAtoms : AtomUniverse ℓ-zero
PrimAtoms = atomUniverse PrimAtomCode PrimAtom

primAtomDefaults : AtomDefaults PrimAtoms
primAtomDefaults stringAtom = ""
primAtomDefaults natAtom = zero
primAtomDefaults intAtom = pos zero
primAtomDefaults boolAtom = false

primAtomCodeToNativeJSON : Native.ToJSON PrimAtomCode
primAtomCodeToNativeJSON =
  Native.mkToJSON λ
    { stringAtom → Native.jstring "string"
    ; natAtom → Native.jstring "nat"
    ; intAtom → Native.jstring "int"
    ; boolAtom → Native.jstring "bool"
    }

primAtomCodeFromNativeJSON : Native.FromJSON PrimAtomCode
primAtomCodeFromNativeJSON =
  Native.mkFromJSON λ
    { (Json.atom Native.string "string") → just stringAtom
    ; (Json.atom Native.string "nat") → just natAtom
    ; (Json.atom Native.string "int") → just intAtom
    ; (Json.atom Native.string "bool") → just boolAtom
    ; _ → nothing
    }

primAtomCodeRoundtrip :
  (a : PrimAtomCode) →
  Json.fromJSON primAtomCodeFromNativeJSON
    (Json.toJSON primAtomCodeToNativeJSON a)
    ≡ just a
primAtomCodeRoundtrip stringAtom = refl
primAtomCodeRoundtrip natAtom = refl
primAtomCodeRoundtrip intAtom = refl
primAtomCodeRoundtrip boolAtom = refl

primAtomCodeFromToNativeJSON : Native.FromToJSON PrimAtomCode
primAtomCodeFromToNativeJSON =
  Native.mkFromToJSON
    primAtomCodeToNativeJSON
    primAtomCodeFromNativeJSON
    primAtomCodeRoundtrip

primAtomCodeIndex : PrimAtomCode → ℕ
primAtomCodeIndex stringAtom = zero
primAtomCodeIndex natAtom = suc zero
primAtomCodeIndex intAtom = suc (suc zero)
primAtomCodeIndex boolAtom = suc (suc (suc zero))

fromPrimAtomCodeIndex : ℕ → Maybe PrimAtomCode
fromPrimAtomCodeIndex zero = just stringAtom
fromPrimAtomCodeIndex (suc zero) = just natAtom
fromPrimAtomCodeIndex (suc (suc zero)) = just intAtom
fromPrimAtomCodeIndex (suc (suc (suc zero))) = just boolAtom
fromPrimAtomCodeIndex (suc (suc (suc (suc _)))) = nothing

fromPrimAtomCodeIndex-roundtrip :
  (a : PrimAtomCode) → fromPrimAtomCodeIndex (primAtomCodeIndex a) ≡ just a
fromPrimAtomCodeIndex-roundtrip stringAtom = refl
fromPrimAtomCodeIndex-roundtrip natAtom = refl
fromPrimAtomCodeIndex-roundtrip intAtom = refl
fromPrimAtomCodeIndex-roundtrip boolAtom = refl

fromPrimAtomCodeIndex-index : ∀ {k a} →
                              fromPrimAtomCodeIndex k ≡ just a →
                              primAtomCodeIndex a ≡ k
fromPrimAtomCodeIndex-index {k = zero} {a} p =
  cong primAtomCodeIndex (sym (MaybeProperties.just-inj stringAtom a p))
fromPrimAtomCodeIndex-index {k = suc zero} {a} p =
  cong primAtomCodeIndex (sym (MaybeProperties.just-inj natAtom a p))
fromPrimAtomCodeIndex-index {k = suc (suc zero)} {a} p =
  cong primAtomCodeIndex (sym (MaybeProperties.just-inj intAtom a p))
fromPrimAtomCodeIndex-index {k = suc (suc (suc zero))} {a} p =
  cong primAtomCodeIndex (sym (MaybeProperties.just-inj boolAtom a p))
fromPrimAtomCodeIndex-index {k = suc (suc (suc (suc k)))} p =
  nothing≡just-elim p

canonicalPrimAtomCodeToNativeJSON : Native.ToJSON PrimAtomCode
canonicalPrimAtomCodeToNativeJSON =
  Native.mkToJSON (λ a → GenericJson.toNatJSON (primAtomCodeIndex a))

canonicalPrimAtomCodeFromNativeJSON : Native.FromJSON PrimAtomCode
canonicalPrimAtomCodeFromNativeJSON =
  Native.mkFromJSON λ j →
    GenericJson.maybeBind (GenericJson.fromNatJSON j) fromPrimAtomCodeIndex

canonicalPrimAtomCodeRoundtrip :
  (a : PrimAtomCode) →
  Json.fromJSON canonicalPrimAtomCodeFromNativeJSON
    (Json.toJSON canonicalPrimAtomCodeToNativeJSON a) ≡ just a
canonicalPrimAtomCodeRoundtrip a =
  cong (λ m → GenericJson.maybeBind m fromPrimAtomCodeIndex)
    (GenericJson.natJSONRoundtrip (primAtomCodeIndex a))
  ∙ fromPrimAtomCodeIndex-roundtrip a

primAtomCodeCanonical :
  (j : Json.JsonValue) → (a : PrimAtomCode) →
  Json.fromJSON canonicalPrimAtomCodeFromNativeJSON j ≡ just a →
  Json.toJSON canonicalPrimAtomCodeToNativeJSON a ≡ j
primAtomCodeCanonical j a p with inspect (GenericJson.fromNatJSON j)
... | nothing , natEq =
  nothing≡just-elim
    (sym (cong (λ m → GenericJson.maybeBind m fromPrimAtomCodeIndex) natEq) ∙ p)
... | just k , natEq with inspect (fromPrimAtomCodeIndex k)
...   | nothing , codeEq =
  nothing≡just-elim
    (sym
      (cong (λ m → GenericJson.maybeBind m fromPrimAtomCodeIndex) natEq ∙ codeEq)
    ∙ p)
...   | just a' , codeEq =
  cong GenericJson.toNatJSON
    ( cong primAtomCodeIndex
        (sym (MaybeProperties.just-inj a' a
          (sym
            (cong (λ m → GenericJson.maybeBind m fromPrimAtomCodeIndex) natEq ∙ codeEq)
          ∙ p)))
    ∙ fromPrimAtomCodeIndex-index codeEq )
  ∙ Generic.CanonicalJson.natJSONCanonical j k natEq

canonicalPrimAtomCodeFromToNativeJSON : CanonicalFromToJSON PrimAtomCode
canonicalPrimAtomCodeFromToNativeJSON =
  canonicalFromToJSON'
    (Native.mkFromToJSON
      canonicalPrimAtomCodeToNativeJSON
      canonicalPrimAtomCodeFromNativeJSON
      canonicalPrimAtomCodeRoundtrip)
    primAtomCodeCanonical

natToNativeJSON : Native.ToJSON ℕ
natToNativeJSON = Native.numberToJson

natFromNativeJSON : Native.FromJSON ℕ
natFromNativeJSON = Native.numberFromJson

natFromToNativeJSON : Native.FromToJSON ℕ
natFromToNativeJSON = Native.numberFromToJson

intToNativeJSONValue : Int → Json.JsonValue
intToNativeJSONValue (pos n) =
  Native.jarray (Native.jstring "pos" ∷ Native.jnumber n ∷ [])
intToNativeJSONValue (negsuc n) =
  Native.jarray (Native.jstring "negsuc" ∷ Native.jnumber n ∷ [])

intToNativeJSON : Native.ToJSON Int
intToNativeJSON =
  Native.mkToJSON intToNativeJSONValue

intFromNativeJSONValue : Json.JsonValue → Maybe Int
intFromNativeJSONValue
  (Json.array (Json.atom Native.string "pos" ∷ n ∷ [])) =
  GenericJson.maybeMap pos (fromNativeJSON Native.numberFromJson n)
intFromNativeJSONValue
  (Json.array (Json.atom Native.string "negsuc" ∷ n ∷ [])) =
  GenericJson.maybeMap negsuc (fromNativeJSON Native.numberFromJson n)
intFromNativeJSONValue _ =
  nothing

intFromNativeJSON : Native.FromJSON Int
intFromNativeJSON =
  Native.mkFromJSON intFromNativeJSONValue

intNativeJSONRoundtrip :
  (x : Int) →
  Json.fromJSON intFromNativeJSON
    (Json.toJSON intToNativeJSON x)
    ≡ just x
intNativeJSONRoundtrip (pos n) =
  refl
intNativeJSONRoundtrip (negsuc n) =
  refl

intFromToNativeJSON : Native.FromToJSON Int
intFromToNativeJSON =
  Native.mkFromToJSON
    intToNativeJSON
    intFromNativeJSON
    intNativeJSONRoundtrip

canonicalIntToNativeJSONValue : Int → Json.JsonValue
canonicalIntToNativeJSONValue (pos n) =
  Native.jarray (GenericJson.toNatJSON zero ∷ Native.jnumber n ∷ [])
canonicalIntToNativeJSONValue (negsuc n) =
  Native.jarray (GenericJson.toNatJSON (suc zero) ∷ Native.jnumber n ∷ [])

canonicalIntFromTag : Json.JsonValue → ℕ → Maybe Int
canonicalIntFromTag j zero =
  GenericJson.maybeMap pos (fromNativeJSON Native.numberFromJson j)
canonicalIntFromTag j (suc zero) =
  GenericJson.maybeMap negsuc (fromNativeJSON Native.numberFromJson j)
canonicalIntFromTag j (suc (suc _)) = nothing

canonicalIntFromNativeJSONValue : Json.JsonValue → Maybe Int
canonicalIntFromNativeJSONValue (Json.array (tag ∷ j ∷ [])) =
  GenericJson.maybeBind (GenericJson.fromNatJSON tag) (canonicalIntFromTag j)
canonicalIntFromNativeJSONValue _ = nothing

canonicalIntToNativeJSON : Native.ToJSON Int
canonicalIntToNativeJSON = Native.mkToJSON canonicalIntToNativeJSONValue

canonicalIntFromNativeJSON : Native.FromJSON Int
canonicalIntFromNativeJSON = Native.mkFromJSON canonicalIntFromNativeJSONValue

canonicalIntRoundtrip :
  (x : Int) →
  Json.fromJSON canonicalIntFromNativeJSON
    (Json.toJSON canonicalIntToNativeJSON x) ≡ just x
canonicalIntRoundtrip (pos n) = refl
canonicalIntRoundtrip (negsuc n) = refl

canonicalIntTag :
  (tag j : Json.JsonValue) → (k : ℕ) →
  GenericJson.fromNatJSON tag ≡ just k →
  (x : Int) → canonicalIntFromTag j k ≡ just x →
  Json.toJSON canonicalIntToNativeJSON x ≡ Json.array (tag ∷ j ∷ [])
canonicalIntTag tag j zero tagEq x p with inspect (fromNativeJSON Native.numberFromJson j)
... | nothing , valueEq =
  nothing≡just-elim (sym (cong (GenericJson.maybeMap pos) valueEq) ∙ p)
... | just n , valueEq =
  cong (Json.toJSON canonicalIntToNativeJSON)
    (sym (MaybeProperties.just-inj (pos n) x
      (sym (cong (GenericJson.maybeMap pos) valueEq) ∙ p)))
  ∙ (λ q → Json.array
      ( Generic.CanonicalJson.natJSONCanonical tag zero tagEq q
      ∷ canonical canonicalNatFromToJSON j n valueEq q
      ∷ [] ))
canonicalIntTag tag j (suc zero) tagEq x p with
  inspect (fromNativeJSON Native.numberFromJson j)
... | nothing , valueEq =
  nothing≡just-elim (sym (cong (GenericJson.maybeMap negsuc) valueEq) ∙ p)
... | just n , valueEq =
  cong (Json.toJSON canonicalIntToNativeJSON)
    (sym (MaybeProperties.just-inj (negsuc n) x
      (sym (cong (GenericJson.maybeMap negsuc) valueEq) ∙ p)))
  ∙ (λ q → Json.array
      ( Generic.CanonicalJson.natJSONCanonical tag (suc zero) tagEq q
      ∷ canonical canonicalNatFromToJSON j n valueEq q
      ∷ [] ))
canonicalIntTag tag j (suc (suc k)) tagEq x p = nothing≡just-elim p

intNativeJSONCanonical :
  (j : Json.JsonValue) → (x : Int) →
  Json.fromJSON canonicalIntFromNativeJSON j ≡ just x →
  Json.toJSON canonicalIntToNativeJSON x ≡ j
intNativeJSONCanonical (Json.atom c a) x p = nothing≡just-elim p
intNativeJSONCanonical (Json.object fields) x p = nothing≡just-elim p
intNativeJSONCanonical (Json.array []) x p = nothing≡just-elim p
intNativeJSONCanonical (Json.array (j ∷ [])) x p = nothing≡just-elim p
intNativeJSONCanonical (Json.array (tag ∷ j ∷ [])) x p with
  inspect (GenericJson.fromNatJSON tag)
... | nothing , tagEq =
  nothing≡just-elim
    (sym (cong (λ m → GenericJson.maybeBind m (canonicalIntFromTag j)) tagEq) ∙ p)
... | just k , tagEq =
  canonicalIntTag tag j k tagEq x
    (sym (cong (λ m → GenericJson.maybeBind m (canonicalIntFromTag j)) tagEq) ∙ p)
intNativeJSONCanonical (Json.array (j ∷ j' ∷ j'' ∷ js)) x p = nothing≡just-elim p

canonicalIntFromToNativeJSON : CanonicalFromToJSON Int
canonicalIntFromToNativeJSON =
  canonicalFromToJSON'
    (Native.mkFromToJSON
      canonicalIntToNativeJSON canonicalIntFromNativeJSON canonicalIntRoundtrip)
    intNativeJSONCanonical

primAtomValueCodecs : NativeAtomValueCodecs PrimAtoms
primAtomValueCodecs stringAtom = Native.stringFromToJson
primAtomValueCodecs natAtom = natFromToNativeJSON
primAtomValueCodecs intAtom = intFromToNativeJSON
primAtomValueCodecs boolAtom = Native.boolFromToJson

canonicalPrimAtomValueCodecs : CanonicalNativeAtomValueCodecs PrimAtoms
canonicalPrimAtomValueCodecs stringAtom = canonicalStringFromToJSON
canonicalPrimAtomValueCodecs natAtom = canonicalNatFromToJSON
canonicalPrimAtomValueCodecs intAtom = canonicalIntFromToNativeJSON
canonicalPrimAtomValueCodecs boolAtom = canonicalBoolFromToJSON

primAtomValueToCodecs : NativeAtomValueToCodecs PrimAtoms
primAtomValueToCodecs stringAtom = Native.stringToJson
primAtomValueToCodecs natAtom = natToNativeJSON
primAtomValueToCodecs intAtom = intToNativeJSON
primAtomValueToCodecs boolAtom = Native.boolToJson