module FF.Json.ValidateSamples where

open import Agda.Builtin.String
  using (String)
open import Agda.Builtin.Unit
  using (⊤)

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

open import FF.Json
open import FF.Json.Validate.Jq

renderedStringToJson : String
renderedStringToJson =
  renderCompact (toJSON stringToJson "quote: \" slash: \\ newline:\n tab:\t")

renderedBoolToJson : String
renderedBoolToJson = renderCompact (toJSON boolToJson true)

renderedNumberToJson : String
renderedNumberToJson =
  renderCompact (toJSON numberToJson )

renderedJsonToJson : String
renderedJsonToJson =
  renderCompact
    (toJSON jsonToJson
      (jobject
        ( ("nested" , jarray (jbool true ∷ jbool false ∷ jnull ∷ []))
        ∷ ("empty-object" , jobject [])
        ∷ ("empty-array" , jarray [])
        ∷ [] )))

renderedPrettyJsonToJson : String
renderedPrettyJsonToJson =
  renderPrettyWith jsonToJson
    (jobject
      ( ("a" , jarray [])
      ∷ ("b" , jobject [])
      ∷ ("c" , jstring "")
      ∷ [] ))

renderedValidationSamples : List String
renderedValidationSamples =
  renderedStringToJson ∷
  renderedBoolToJson ∷
  renderedNumberToJson ∷
  renderedJsonToJson ∷
  renderedPrettyJsonToJson ∷
  []

validateStringToJson : ⊤
validateStringToJson = validateJsonWithJq renderedStringToJson

validateBoolToJson : ⊤
validateBoolToJson = validateJsonWithJq renderedBoolToJson

validateNumberToJson : ⊤
validateNumberToJson = validateJsonWithJq renderedNumberToJson

validateJsonToJson : ⊤
validateJsonToJson = validateJsonWithJq renderedJsonToJson

validatePrettyJsonToJson : ⊤
validatePrettyJsonToJson = validateJsonWithJq renderedPrettyJsonToJson