module FF.HTML.Spec.Safe.Tag where

open import Agda.Builtin.String using (String)
open import Agda.Primitive using (lzero) renaming (Set to Type)

-- MDN element reference:
-- https://developer.mozilla.org/en-US/docs/Web/HTML/Reference/Elements
-- MDN content categories:
-- https://developer.mozilla.org/en-US/docs/Web/HTML/Guides/Content_categories
data TagName : Type lzero where
  htmlTag headTag titleTag baseTag linkTag metaTag styleTag bodyTag : TagName
  addressTag articleTag asideTag footerTag headerTag h1Tag h2Tag h3Tag h4Tag h5Tag h6Tag hgroupTag mainTag navTag sectionTag searchTag : TagName
  blockquoteTag ddTag divTag dlTag dtTag figcaptionTag figureTag hrTag liTag menuTag olTag pTag preTag ulTag : TagName
  aTag abbrTag bTag bdiTag bdoTag brTag citeTag codeTag dataTag dfnTag emTag iTag kbdTag markTag qTag rpTag rtTag rubyTag sTag sampTag smallTag spanTag strongTag subTag supTag timeTag uTag varTag wbrTag : TagName
  areaTag audioTag imgTag imageMapTag trackTag videoTag : TagName
  embedTag fencedframeTag iframeTag objectTag pictureTag sourceTag : TagName
  canvasTag noscriptTag scriptTag : TagName
  delTag insTag : TagName
  captionTag colTag colgroupTag tableTag tbodyTag tdTag tfootTag thTag theadTag trTag : TagName
  buttonTag datalistTag fieldsetTag formTag inputTag labelTag legendTag meterTag optgroupTag optionTag outputTag progressTag selectTag selectedcontentTag textareaTag : TagName
  detailsTag dialogTag geolocationTag summaryTag : TagName
  slotTag templateTag : TagName

tagString : TagName -> String
tagString htmlTag = "html"
tagString headTag = "head"
tagString titleTag = "title"
tagString baseTag = "base"
tagString linkTag = "link"
tagString metaTag = "meta"
tagString styleTag = "style"
tagString bodyTag = "body"
tagString addressTag = "address"
tagString articleTag = "article"
tagString asideTag = "aside"
tagString footerTag = "footer"
tagString headerTag = "header"
tagString h1Tag = "h1"
tagString h2Tag = "h2"
tagString h3Tag = "h3"
tagString h4Tag = "h4"
tagString h5Tag = "h5"
tagString h6Tag = "h6"
tagString hgroupTag = "hgroup"
tagString mainTag = "main"
tagString navTag = "nav"
tagString sectionTag = "section"
tagString searchTag = "search"
tagString blockquoteTag = "blockquote"
tagString ddTag = "dd"
tagString divTag = "div"
tagString dlTag = "dl"
tagString dtTag = "dt"
tagString figcaptionTag = "figcaption"
tagString figureTag = "figure"
tagString hrTag = "hr"
tagString liTag = "li"
tagString menuTag = "menu"
tagString olTag = "ol"
tagString pTag = "p"
tagString preTag = "pre"
tagString ulTag = "ul"
tagString aTag = "a"
tagString abbrTag = "abbr"
tagString bTag = "b"
tagString bdiTag = "bdi"
tagString bdoTag = "bdo"
tagString brTag = "br"
tagString citeTag = "cite"
tagString codeTag = "code"
tagString dataTag = "data"
tagString dfnTag = "dfn"
tagString emTag = "em"
tagString iTag = "i"
tagString kbdTag = "kbd"
tagString markTag = "mark"
tagString qTag = "q"
tagString rpTag = "rp"
tagString rtTag = "rt"
tagString rubyTag = "ruby"
tagString sTag = "s"
tagString sampTag = "samp"
tagString smallTag = "small"
tagString spanTag = "span"
tagString strongTag = "strong"
tagString subTag = "sub"
tagString supTag = "sup"
tagString timeTag = "time"
tagString uTag = "u"
tagString varTag = "var"
tagString wbrTag = "wbr"
tagString areaTag = "area"
tagString audioTag = "audio"
tagString imgTag = "img"
tagString imageMapTag = "map"
tagString trackTag = "track"
tagString videoTag = "video"
tagString embedTag = "embed"
tagString fencedframeTag = "fencedframe"
tagString iframeTag = "iframe"
tagString objectTag = "object"
tagString pictureTag = "picture"
tagString sourceTag = "source"
tagString canvasTag = "canvas"
tagString noscriptTag = "noscript"
tagString scriptTag = "script"
tagString delTag = "del"
tagString insTag = "ins"
tagString captionTag = "caption"
tagString colTag = "col"
tagString colgroupTag = "colgroup"
tagString tableTag = "table"
tagString tbodyTag = "tbody"
tagString tdTag = "td"
tagString tfootTag = "tfoot"
tagString thTag = "th"
tagString theadTag = "thead"
tagString trTag = "tr"
tagString buttonTag = "button"
tagString datalistTag = "datalist"
tagString fieldsetTag = "fieldset"
tagString formTag = "form"
tagString inputTag = "input"
tagString labelTag = "label"
tagString legendTag = "legend"
tagString meterTag = "meter"
tagString optgroupTag = "optgroup"
tagString optionTag = "option"
tagString outputTag = "output"
tagString progressTag = "progress"
tagString selectTag = "select"
tagString selectedcontentTag = "selectedcontent"
tagString textareaTag = "textarea"
tagString detailsTag = "details"
tagString dialogTag = "dialog"
tagString geolocationTag = "geolocation"
tagString summaryTag = "summary"
tagString slotTag = "slot"
tagString templateTag = "template"