FF.Json.Examples

module FF.Json.Examples where

open import Agda.Builtin.String
  using (String)

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

open import FF.Json

profile : JsonValue
profile =
  jobject
    ( ("name" , jstring "Ada")
    ∷ ("admin" , jbool true)
    ∷ ("score" , jnumber 42)
    ∷ ("tags" , jarray (jstring "agda" ∷ jstring "json" ∷ []))
    ∷ ("metadata" , jobject [])
    ∷ [] )

profileCompact : String
profileCompact = renderCompact profile

profilePretty : String
profilePretty = renderPretty profile

record User : Type ℓ-zero where
  constructor mkUser
  field
    name  : String
    admin : Bool

open User public

userToJson : ToJSON User
userToJson = mkToJSON userToValue
  where
  userToValue : User → JsonValue
  userToValue u =
    jobject
      ( ("name" , jstring (name u))
      ∷ ("admin" , jbool (admin u))
      ∷ [] )

fromUserJson : JsonValue → Maybe User
fromUserJson
  (object (("name" , atom string n) ∷ ("admin" , atom boolean a) ∷ [])) =
    just (mkUser n a)
fromUserJson _ = nothing

userFromJson : FromJSON User
userFromJson = mkFromJSON fromUserJson

userCodec : FromToJSON User
userCodec = mkFromToJSON userToJson userFromJson (λ _ → refl)

sampleUser : User
sampleUser = mkUser "Grace" false

sampleUserJson : JsonValue
sampleUserJson = toJSON userToJson sampleUser

sampleUserPretty : String
sampleUserPretty = renderPrettyWith userToJson sampleUser

data HtmlAtomCode : Type ℓ-zero where
  htmlText htmlRawNumber : HtmlAtomCode

HtmlAtomEl : HtmlAtomCode → Type ℓ-zero
HtmlAtomEl htmlText = String
HtmlAtomEl htmlRawNumber = String

renderHtmlAtom : (c : HtmlAtomCode) → HtmlAtomEl c → String
renderHtmlAtom htmlText s = quoteString ("html:" <> s)
renderHtmlAtom htmlRawNumber n = n

HtmlAtoms : AtomUniverse _
HtmlAtoms = mkAtomUniverse HtmlAtomCode HtmlAtomEl renderHtmlAtom

htmlExample : Json HtmlAtoms
htmlExample =
  object
    ( ("node" , atom htmlText "<main>")
    ∷ ("children" , array [])
    ∷ ("weight" , atom htmlRawNumber "1")
    ∷ [] )

htmlExampleRendered : String
htmlExampleRendered = renderPretty htmlExample