module Generic.CorrectnessTests where

open import Generic.Core hiding (natAtom; stringAtom; boolAtom)
open import Generic.Certified
open import Generic.Family
open import Generic.Default
open import Generic.CanonicalJson
open import Generic.CanonicalNativeJson
open import Generic.PrimAtom
open import Generic.PrimAtom.WebEditor
open import Generic.Macro.Family

open import Cubical.Data.Maybe.Base using (just)

import FF.Json as Json
import FF.Json.Native as Native
import Generic.Json as GenericJson

data Sample : Type₀ where
  sample-stop : Sample
  sample-step : String → Sample → Sample

sampleFamily : GenericFamily PrimAtoms
sampleFamily = deriveGenericFamilyBundleIn1 PrimAtoms Sample

genericSample : Generic PrimAtoms Sample
genericSample = genericAt sampleFamily Fin.zero

certifiedSample : CertifiedGeneric PrimAtoms Sample
certifiedSample = deriveCertifiedGenericFamilyIn1 PrimAtoms Sample

sample-encode-exact :
  Generic.encode genericSample (sample-step "x" sample-stop) ≡
  rootDataIx
    (ν₂ ι₁
      (atomIx "x")
      (recIx (ν₀ ι₀)))
sample-encode-exact = refl

sample-family-roundtrip : (x : Sample) →
  GenericFamily.decodeAt sampleFamily Fin.zero
    (GenericFamily.encodeAt sampleFamily Fin.zero x) ≡ x
sample-family-roundtrip = GenericFamily.decode-encodeAt sampleFamily Fin.zero

sample-constructor-name : String
sample-constructor-name =
  CertifiedGeneric.constructorName certifiedSample Fin.zero ι₁

sample-productivity :
  ProductiveAtBound primAtomDefaults (Generic.desc genericSample) Fin.zero
sample-productivity =
  defaultableData (defaultableHere defaultable[])

sample-default-complete :
  Σ[ code ∈ CodeIx PrimAtoms (Generic.desc genericSample)
      (Generic.desc genericSample Fin.zero) ]
    defaultCodes primAtomDefaults (Generic.desc genericSample) Fin.zero ≡ just code
sample-default-complete =
  defaultCodes-complete
    primAtomDefaults (Generic.desc genericSample) Fin.zero sample-productivity

sample-default-exact :
  defaultCodes primAtomDefaults (Generic.desc genericSample) Fin.zero ≡
    just (ν₀ ι₀)
sample-default-exact = refl

sampleCanonicalCodec : CanonicalFromToJSON Sample
sampleCanonicalCodec =
  canonicalGenericFromToNativeJSON canonicalPrimAtomValueCodecs genericSample

sample-json-roundtrip : (x : Sample) →
  Json.fromJSON (Json.FromToJSON'.from (codec sampleCanonicalCodec))
    (Json.toJSON (Json.FromToJSON'.to (codec sampleCanonicalCodec)) x) ≡ just x
sample-json-roundtrip =
  Json.FromToJSON'.roundtrip (codec sampleCanonicalCodec)

sample-json-canonical :
  (j : Json.JsonValue) → (x : Sample) →
  Json.fromJSON (Json.FromToJSON'.from (codec sampleCanonicalCodec)) j ≡ just x →
  Json.toJSON (Json.FromToJSON'.to (codec sampleCanonicalCodec)) x ≡ j
sample-json-canonical = canonical sampleCanonicalCodec

sample-json-exact :
  Json.toJSON (Json.FromToJSON'.to (codec sampleCanonicalCodec))
    (sample-step "x" sample-stop) ≡
  Native.jarray
    ( GenericJson.toNatJSON (suc zero)
    ∷ Native.jarray
        ( Native.jstring "x"
        ∷ Native.jarray
            ( GenericJson.toNatJSON zero
            ∷ Native.jarray []
            ∷ []
            )
        ∷ []
        )
    ∷ []
    )
sample-json-exact = refl

sample-source-is-certified :
  RootSourceDenotes certifiedSample
    (Generic.encode (base certifiedSample) (sample-step "x" sample-stop))
    (sourceExprOfValue certifiedSample (sample-step "x" sample-stop))
sample-source-is-certified =
  sourceExprOfValue-correct certifiedSample (sample-step "x" sample-stop)