module FF.Json.Generate.NodeTests where

open import Agda.Builtin.Nat
  using (zero; suc)
open import Agda.Builtin.Reflection
  using (TC; Term; quoteTC; strErr; typeError; unify)
open import Agda.Builtin.Reflection.External
  using (execTC)
open import Agda.Builtin.String
  using (String)
open import Agda.Builtin.Unit
  using (⊤; tt)

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

open import FF.Json
open import FF.Json.Generate.Node

generatedNull : JsonValue
generatedNull = jsonValueFromNode "null"

generatedNullCorrect : generatedNull ≡ jnull
generatedNullCorrect = refl

generatedArray : JsonValue
generatedArray = jsonValueFromNode "[true,false,null]"

generatedArrayCorrect :
  generatedArray ≡ jarray (jbool true ∷ jbool false ∷ jnull ∷ [])
generatedArrayCorrect = refl

generatedObject : JsonValue
generatedObject =
  jsonValueFromNode
    "{\"name\":\"Ada\",\"score\":42,\"tags\":[\"agda\",\"json\"]}"

generatedObjectCorrect :
  generatedObject ≡
    jobject
      ( ("name" , jstring "Ada")
      ∷ ("score" , jnumber )
      ∷ ("tags" , jarray (jstring "agda" ∷ jstring "json" ∷ []))
      ∷ [] )
generatedObjectCorrect = refl

generatedEscapes : JsonValue
generatedEscapes = jsonValueFromNode "\"a\\n\\t\\\"\\\\\""

generatedEscapesCorrect : generatedEscapes ≡ jstring "a\n\t\"\\"
generatedEscapesCorrect = refl

generatedDuplicateKeys : JsonValue
generatedDuplicateKeys = jsonValueFromNode "{\"x\":1,\"x\":2}"

generatedDuplicateKeysCorrect :
  generatedDuplicateKeys ≡
    jobject (("x" , jnumber ) ∷ ("x" , jnumber ) ∷ [])
generatedDuplicateKeysCorrect = refl

macro
  jsonValueFromNodeFails : String → Term → TC ⊤
  jsonValueFromNodeFails input hole =
    execTC nodeExecutable (scriptPath ∷ []) input >>= λ where
      (zero , _) →
        typeError (strErr "json-to-agda.js unexpectedly accepted input" ∷ [])
      (suc _ , _) →
        quoteTC tt >>= unify hole

generatedRejectsNegativeNumber : ⊤
generatedRejectsNegativeNumber = jsonValueFromNodeFails "-1"

generatedRejectsFractionalNumber : ⊤
generatedRejectsFractionalNumber = jsonValueFromNodeFails "1.25"

generatedRejectsTrailingInput : ⊤
generatedRejectsTrailingInput = jsonValueFromNodeFails "true false"