module FF.CSS.Metadata where

open import Agda.Builtin.String using (String)
open import Agda.Primitive using (lzero) renaming (Set to Type)
open import Cubical.Data.List.Base using ([]; _∷_)
open import Cubical.Data.Sigma.Base using (_×_; _,_)

import FF.Json as Json

-- MDN CSS data repository:
-- https://github.com/mdn/data/tree/main/css
record PropertyMetadata : Type lzero where
  constructor propertyMetadata
  field
    name    : String
    formalSyntax : String
    status  : String
    group   : String
    initial : String

open PropertyMetadata public

propertyMetadataToJson : PropertyMetadata -> Json.JsonValue
propertyMetadataToJson metadata =
  Json.jobject
    ( ("name" , Json.jstring (name metadata))
    ∷ ("syntax" , Json.jstring (formalSyntax metadata))
    ∷ ("status" , Json.jstring (status metadata))
    ∷ ("group" , Json.jstring (group metadata))
    ∷ ("initial" , Json.jstring (initial metadata))
    ∷ []
    )

displayMetadata : PropertyMetadata
displayMetadata =
  propertyMetadata
    "display"
    "[ <display-outside> || <display-inside> ] | <display-listitem> | <display-internal> | <display-box> | <display-legacy>"
    "standard"
    "CSS Display"
    "inline"

displayMetadataJson : Json.JsonValue
displayMetadataJson = propertyMetadataToJson displayMetadata

renderDisplayMetadataJson : String
renderDisplayMetadataJson = Json.renderCompact displayMetadataJson