FF.Json.Tests

module FF.Json.Tests where

open import Agda.Builtin.String
  using (String)

open import Cubical.Foundations.Prelude
  using (_≡_; refl)
open import Cubical.Data.Bool.Base
  using (true; false)
open import Cubical.Data.List.Base
  using (List; []; _∷_)
open import Cubical.Data.Maybe.Base
  using (just; nothing)
open import Cubical.Data.Sigma.Base
  using (_,_)

open import FF.Json

emptyArrayCompact : renderCompact (jarray []) ≡ "[]"
emptyArrayCompact = refl

emptyObjectCompact : renderCompact (jobject []) ≡ "{}"
emptyObjectCompact = refl

nestedEmptyPretty : renderPretty (jobject (("a" , jarray []) ∷ ("o" , jobject []) ∷ []))
  ≡ "{\n  \"a\": [],\n  \"o\": {}\n}"
nestedEmptyPretty = refl

escapedStringCompact : renderCompact (jstring "quote: \" slash: \\ newline:\n")
  ≡ "\"quote: \\\" slash: \\\\ newline:\\n\""
escapedStringCompact = refl

duplicateKeysCompact :
  renderCompact (jobject (("x" , jnumber 1) ∷ ("x" , jnumber 2) ∷ []))
    ≡ "{\"x\":1,\"x\":2}"
duplicateKeysCompact = refl

numberCompact : renderCompact (jnumber 125) ≡ "125"
numberCompact = refl

decodeStringSuccess : fromJSON stringFromJson (jstring "ok") ≡ just "ok"
decodeStringSuccess = refl

decodeStringFailure : fromJSON stringFromJson (jbool true) ≡ nothing
decodeStringFailure = refl

decodeBoolSuccess : fromJSON boolFromJson (jbool false) ≡ just false
decodeBoolSuccess = refl

stringCodecRoundtrip : roundtrip stringFromToJson "round" ≡ refl
stringCodecRoundtrip = refl

numberCodecRoundtrip : roundtrip numberFromToJson 12 ≡ refl
numberCodecRoundtrip = refl

arrayPretty : renderPretty (jarray (jnumber 0 ∷ jstring "" ∷ jnull ∷ []))
  ≡ "[\n  0,\n  \"\",\n  null\n]"
arrayPretty = refl

sampleRenderedValues : List String
sampleRenderedValues =
  renderCompact (jarray []) ∷
  renderCompact (jobject []) ∷
  renderCompact (jstring "quote: \" slash: \\ newline:\n tab:\t") ∷
  renderCompact (jnumber 125) ∷
  renderCompact (jobject (("nested" , jarray (jbool true ∷ jbool false ∷ jnull ∷ [])) ∷ [])) ∷
  renderPretty (jobject (("a" , jarray []) ∷ ("b" , jobject []) ∷ [])) ∷
  []