module FF.HTML.Spec.Safe.Attribute where

open import Agda.Builtin.String using (String)
open import Agda.Primitive using (lzero) renaming (Set to Type)
open import Cubical.Data.Bool.Base using (Bool)

open import FF.HTML.Spec.Safe.Tag
open import FF.HTML.Spec.Safe.Value

-- MDN global attributes:
-- https://developer.mozilla.org/en-US/docs/Web/HTML/Reference/Global_attributes
-- MDN attribute reference:
-- https://developer.mozilla.org/en-US/docs/Web/HTML/Reference/Attributes

data HrefElement : TagName -> Type lzero where
  hrefA : HrefElement aTag
  hrefArea : HrefElement areaTag
  hrefBase : HrefElement baseTag
  hrefLink : HrefElement linkTag

data TargetElement : TagName -> Type lzero where
  targetA : TargetElement aTag
  targetArea : TargetElement areaTag
  targetBase : TargetElement baseTag
  targetForm : TargetElement formTag

data RelElement : TagName -> Type lzero where
  relA : RelElement aTag
  relArea : RelElement areaTag
  relLink : RelElement linkTag
  relForm : RelElement formTag

data LinkLanguageElement : TagName -> Type lzero where
  langA : LinkLanguageElement aTag
  langLink : LinkLanguageElement linkTag

data AttributionSrcElement : TagName -> Type lzero where
  attributionA : AttributionSrcElement aTag
  attributionImg : AttributionSrcElement imgTag
  attributionScript : AttributionSrcElement scriptTag

data InterestForElement : TagName -> Type lzero where
  interestA : InterestForElement aTag
  interestArea : InterestForElement areaTag

data DownloadElement : TagName -> Type lzero where
  downloadA : DownloadElement aTag
  downloadArea : DownloadElement areaTag

data PingElement : TagName -> Type lzero where
  pingA : PingElement aTag
  pingArea : PingElement areaTag

data AcceptElement : TagName -> Type lzero where
  acceptForm : AcceptElement formTag
  acceptInput : AcceptElement inputTag

data MediaQueryElement : TagName -> Type lzero where
  mediaA : MediaQueryElement aTag
  mediaArea : MediaQueryElement areaTag
  mediaLink : MediaQueryElement linkTag
  mediaMeta : MediaQueryElement metaTag
  mediaSource : MediaQueryElement sourceTag
  mediaStyle : MediaQueryElement styleTag

data SourceElement : TagName -> Type lzero where
  srcAudio : SourceElement audioTag
  srcEmbed : SourceElement embedTag
  srcIframe : SourceElement iframeTag
  srcImg : SourceElement imgTag
  srcInput : SourceElement inputTag
  srcScript : SourceElement scriptTag
  srcSource : SourceElement sourceTag
  srcTrack : SourceElement trackTag
  srcVideo : SourceElement videoTag

data SourceSetElement : TagName -> Type lzero where
  srcsetImg : SourceSetElement imgTag
  srcsetSource : SourceSetElement sourceTag

data SizesElement : TagName -> Type lzero where
  sizesLink : SizesElement linkTag
  sizesImg : SizesElement imgTag
  sizesSource : SizesElement sourceTag

data ShapeElement : TagName -> Type lzero where
  shapeA : ShapeElement aTag
  shapeArea : ShapeElement areaTag

data AltElement : TagName -> Type lzero where
  altArea : AltElement areaTag
  altImg : AltElement imgTag
  altInput : AltElement inputTag

data SizeElement : TagName -> Type lzero where
  sizeCanvas : SizeElement canvasTag
  sizeEmbed : SizeElement embedTag
  sizeFencedframe : SizeElement fencedframeTag
  sizeIframe : SizeElement iframeTag
  sizeImg : SizeElement imgTag
  sizeInput : SizeElement inputTag
  sizeObject : SizeElement objectTag
  sizeSource : SizeElement sourceTag
  sizeVideo : SizeElement videoTag

data LoadingElement : TagName -> Type lzero where
  loadingAudio : LoadingElement audioTag
  loadingIframe : LoadingElement iframeTag
  loadingImg : LoadingElement imgTag
  loadingVideo : LoadingElement videoTag

data FetchPriorityElement : TagName -> Type lzero where
  fetchPriorityImg : FetchPriorityElement imgTag
  fetchPriorityLink : FetchPriorityElement linkTag
  fetchPriorityScript : FetchPriorityElement scriptTag

data BlockingElement : TagName -> Type lzero where
  blockingLink : BlockingElement linkTag
  blockingScript : BlockingElement scriptTag
  blockingStyle : BlockingElement styleTag

data CrossOriginElement : TagName -> Type lzero where
  corsAudio : CrossOriginElement audioTag
  corsImg : CrossOriginElement imgTag
  corsLink : CrossOriginElement linkTag
  corsScript : CrossOriginElement scriptTag
  corsVideo : CrossOriginElement videoTag

data ReferrerPolicyElement : TagName -> Type lzero where
  refA : ReferrerPolicyElement aTag
  refArea : ReferrerPolicyElement areaTag
  refIframe : ReferrerPolicyElement iframeTag
  refImg : ReferrerPolicyElement imgTag
  refLink : ReferrerPolicyElement linkTag
  refScript : ReferrerPolicyElement scriptTag

data ElementTimingElement : TagName -> Type lzero where
  timingImg : ElementTimingElement imgTag
  timingP : ElementTimingElement pTag
  timingVideo : ElementTimingElement videoTag

data IntegrityElement : TagName -> Type lzero where
  integrityLink : IntegrityElement linkTag
  integrityScript : IntegrityElement scriptTag

data MimeTypedElement : TagName -> Type lzero where
  mimeA : MimeTypedElement aTag
  mimeEmbed : MimeTypedElement embedTag
  mimeLink : MimeTypedElement linkTag
  mimeObject : MimeTypedElement objectTag
  mimeSource : MimeTypedElement sourceTag
  mimeStyle : MimeTypedElement styleTag

data NameElement : TagName -> Type lzero where
  nameButton : NameElement buttonTag
  nameDetails : NameElement detailsTag
  nameFieldset : NameElement fieldsetTag
  nameForm : NameElement formTag
  nameIframe : NameElement iframeTag
  nameInput : NameElement inputTag
  nameMap : NameElement imageMapTag
  nameMeta : NameElement metaTag
  nameObject : NameElement objectTag
  nameOutput : NameElement outputTag
  nameSelect : NameElement selectTag
  nameSlot : NameElement slotTag
  nameTextarea : NameElement textareaTag

data FormAssociatedElement : TagName -> Type lzero where
  formButton : FormAssociatedElement buttonTag
  formFieldset : FormAssociatedElement fieldsetTag
  formInput : FormAssociatedElement inputTag
  formObject : FormAssociatedElement objectTag
  formOutput : FormAssociatedElement outputTag
  formSelect : FormAssociatedElement selectTag
  formTextarea : FormAssociatedElement textareaTag

data DisableableElement : TagName -> Type lzero where
  disableButton : DisableableElement buttonTag
  disableFieldset : DisableableElement fieldsetTag
  disableInput : DisableableElement inputTag
  disableLink : DisableableElement linkTag
  disableOptgroup : DisableableElement optgroupTag
  disableOption : DisableableElement optionTag
  disableSelect : DisableableElement selectTag
  disableTextarea : DisableableElement textareaTag

data ReadonlyElement : TagName -> Type lzero where
  readonlyInput : ReadonlyElement inputTag
  readonlyTextarea : ReadonlyElement textareaTag

data RequiredElement : TagName -> Type lzero where
  requiredInput : RequiredElement inputTag
  requiredSelect : RequiredElement selectTag
  requiredTextarea : RequiredElement textareaTag

data MultipleElement : TagName -> Type lzero where
  multipleInput : MultipleElement inputTag
  multipleSelect : MultipleElement selectTag

data PlaceholderElement : TagName -> Type lzero where
  placeholderInput : PlaceholderElement inputTag
  placeholderTextarea : PlaceholderElement textareaTag

data LengthElement : TagName -> Type lzero where
  lengthInput : LengthElement inputTag
  lengthTextarea : LengthElement textareaTag

data ValueElement : TagName -> Type lzero where
  valueButton : ValueElement buttonTag
  valueData : ValueElement dataTag
  valueInput : ValueElement inputTag
  valueLi : ValueElement liTag
  valueMeter : ValueElement meterTag
  valueOption : ValueElement optionTag
  valueProgress : ValueElement progressTag

data ForElement : TagName -> Type lzero where
  forLabel : ForElement labelTag
  forOutput : ForElement outputTag

data AutocompleteElement : TagName -> Type lzero where
  autocompleteInput : AutocompleteElement inputTag
  autocompleteSelect : AutocompleteElement selectTag
  autocompleteTextarea : AutocompleteElement textareaTag

data FormOverrideElement : TagName -> Type lzero where
  overrideButton : FormOverrideElement buttonTag
  overrideInput : FormOverrideElement inputTag

data DirNameElement : TagName -> Type lzero where
  dirnameInput : DirNameElement inputTag
  dirnameTextarea : DirNameElement textareaTag

data PopoverControlElement : TagName -> Type lzero where
  popoverButton : PopoverControlElement buttonTag
  popoverInput : PopoverControlElement inputTag

data UseMapElement : TagName -> Type lzero where
  usemapImg : UseMapElement imgTag
  usemapInput : UseMapElement inputTag
  usemapObject : UseMapElement objectTag

data MediaElement : TagName -> Type lzero where
  mediaAudio : MediaElement audioTag
  mediaVideo : MediaElement videoTag

data CitableElement : TagName -> Type lzero where
  citeBlockquote : CitableElement blockquoteTag
  citeQ : CitableElement qTag
  citeDel : CitableElement delTag
  citeIns : CitableElement insTag

data DateTimeElement : TagName -> Type lzero where
  datetimeTime : DateTimeElement timeTag
  datetimeDel : DateTimeElement delTag
  datetimeIns : DateTimeElement insTag

data OpenElement : TagName -> Type lzero where
  openDetails : OpenElement detailsTag
  openDialog : OpenElement dialogTag

data AllowElement : TagName -> Type lzero where
  allowIframe : AllowElement iframeTag
  allowFencedframe : AllowElement fencedframeTag

data TableCellElement : TagName -> Type lzero where
  cellTd : TableCellElement tdTag
  cellTh : TableCellElement thTag

data SpanElement : TagName -> Type lzero where
  spanCol : SpanElement colTag
  spanColgroup : SpanElement colgroupTag

-- Legacy/presentational MDN attribute rows. These are typed by element so they
-- remain safe to render, but their values intentionally stay simple because the
-- historical value languages vary by element and browser.
data AlignElement : TagName -> Type lzero where
  alignCaption : AlignElement captionTag
  alignCol : AlignElement colTag
  alignColgroup : AlignElement colgroupTag
  alignHr : AlignElement hrTag
  alignIframe : AlignElement iframeTag
  alignImg : AlignElement imgTag
  alignTable : AlignElement tableTag
  alignTbody : AlignElement tbodyTag
  alignTd : AlignElement tdTag
  alignTfoot : AlignElement tfootTag
  alignTh : AlignElement thTag
  alignThead : AlignElement theadTag
  alignTr : AlignElement trTag

data BackgroundElement : TagName -> Type lzero where
  backgroundBody : BackgroundElement bodyTag
  backgroundTable : BackgroundElement tableTag
  backgroundTd : BackgroundElement tdTag
  backgroundTh : BackgroundElement thTag

data BgColorElement : TagName -> Type lzero where
  bgColorBody : BgColorElement bodyTag
  bgColorCol : BgColorElement colTag
  bgColorColgroup : BgColorElement colgroupTag
  bgColorTable : BgColorElement tableTag
  bgColorTbody : BgColorElement tbodyTag
  bgColorTfoot : BgColorElement tfootTag
  bgColorTd : BgColorElement tdTag
  bgColorTh : BgColorElement thTag
  bgColorTr : BgColorElement trTag

data BorderElement : TagName -> Type lzero where
  borderImg : BorderElement imgTag
  borderObject : BorderElement objectTag
  borderTable : BorderElement tableTag

data ColorElement : TagName -> Type lzero where
  colorHr : ColorElement hrTag

-- MDN <a>: https://developer.mozilla.org/en-US/docs/Web/HTML/Reference/Elements/a
-- MDN <link>: https://developer.mozilla.org/en-US/docs/Web/HTML/Reference/Elements/link
-- MDN <img>: https://developer.mozilla.org/en-US/docs/Web/HTML/Reference/Elements/img
-- MDN <form>: https://developer.mozilla.org/en-US/docs/Web/HTML/Reference/Elements/form
-- MDN <input>: https://developer.mozilla.org/en-US/docs/Web/HTML/Reference/Elements/input
-- MDN <button>: https://developer.mozilla.org/en-US/docs/Web/HTML/Reference/Elements/button
-- MDN <select>: https://developer.mozilla.org/en-US/docs/Web/HTML/Reference/Elements/select
-- MDN <textarea>: https://developer.mozilla.org/en-US/docs/Web/HTML/Reference/Elements/textarea
-- MDN <table>: https://developer.mozilla.org/en-US/docs/Web/HTML/Reference/Elements/table
-- MDN <script>: https://developer.mozilla.org/en-US/docs/Web/HTML/Reference/Elements/script
data AttributeKey : TagName -> Type lzero where
  idAttr classAttr titleAttr langAttr dirAttr hiddenAttr tabindexAttr accesskeyAttr
    draggableAttr spellcheckAttr translateAttr styleAttr roleAttr partAttr slotAttr nonceGlobalAttr
    contenteditableAttr inertAttr autofocusAttr popoverAttr anchorAttr autocapitalizeAttr
    autocorrectAttr enterkeyhintAttr exportpartsAttr inputmodeAttr isAttr itemidAttr
    itempropAttr itemrefAttr itemscopeAttr itemtypeAttr virtualkeyboardpolicyAttr
    writingsuggestionsAttr : {tagName : TagName} -> AttributeKey tagName
  dataAttr ariaAttr eventHandlerAttr : {tagName : TagName} -> String -> AttributeKey tagName

  hrefAttr : {tagName : TagName} -> HrefElement tagName -> AttributeKey tagName
  targetAttr : {tagName : TagName} -> TargetElement tagName -> AttributeKey tagName
  relAttr : {tagName : TagName} -> RelElement tagName -> AttributeKey tagName
  hreflangAttr : {tagName : TagName} -> LinkLanguageElement tagName -> AttributeKey tagName
  attributionsrcAttr : {tagName : TagName} -> AttributionSrcElement tagName -> AttributeKey tagName
  interestforAttr : {tagName : TagName} -> InterestForElement tagName -> AttributeKey tagName
  downloadAttr : {tagName : TagName} -> DownloadElement tagName -> AttributeKey tagName
  pingAttr : {tagName : TagName} -> PingElement tagName -> AttributeKey tagName
  mediaAttr : {tagName : TagName} -> MediaQueryElement tagName -> AttributeKey tagName
  asAttr : AttributeKey linkTag
  imagesizesAttr : AttributeKey linkTag
  imagesrcsetAttr : AttributeKey linkTag

  coordsAttr : AttributeKey areaTag
  shapeAttr : {tagName : TagName} -> ShapeElement tagName -> AttributeKey tagName
  srcAttr : {tagName : TagName} -> SourceElement tagName -> AttributeKey tagName
  srcsetAttr : {tagName : TagName} -> SourceSetElement tagName -> AttributeKey tagName
  sizesAttr : {tagName : TagName} -> SizesElement tagName -> AttributeKey tagName
  altAttr : {tagName : TagName} -> AltElement tagName -> AttributeKey tagName
  usemapAttr : {tagName : TagName} -> UseMapElement tagName -> AttributeKey tagName
  ismapAttr : AttributeKey imgTag
  elementtimingAttr : {tagName : TagName} -> ElementTimingElement tagName -> AttributeKey tagName
  widthAttr heightAttr : {tagName : TagName} -> SizeElement tagName -> AttributeKey tagName
  loadingAttr : {tagName : TagName} -> LoadingElement tagName -> AttributeKey tagName
  decodingAttr : AttributeKey imgTag
  fetchpriorityAttr : {tagName : TagName} -> FetchPriorityElement tagName -> AttributeKey tagName
  blockingAttr : {tagName : TagName} -> BlockingElement tagName -> AttributeKey tagName
  crossoriginAttr : {tagName : TagName} -> CrossOriginElement tagName -> AttributeKey tagName
  referrerpolicyAttr : {tagName : TagName} -> ReferrerPolicyElement tagName -> AttributeKey tagName
  integrityAttr : {tagName : TagName} -> IntegrityElement tagName -> AttributeKey tagName
  typeAttr : {tagName : TagName} -> MimeTypedElement tagName -> AttributeKey tagName

  charsetAttr : AttributeKey metaTag
  contentAttr : AttributeKey metaTag
  httpEquivAttr : AttributeKey metaTag
  languageAttr : AttributeKey scriptTag

  nameAttr : {tagName : TagName} -> NameElement tagName -> AttributeKey tagName
  formAttr : {tagName : TagName} -> FormAssociatedElement tagName -> AttributeKey tagName
  disabledAttr : {tagName : TagName} -> DisableableElement tagName -> AttributeKey tagName
  readonlyAttr : {tagName : TagName} -> ReadonlyElement tagName -> AttributeKey tagName
  requiredAttr : {tagName : TagName} -> RequiredElement tagName -> AttributeKey tagName
  multipleAttr : {tagName : TagName} -> MultipleElement tagName -> AttributeKey tagName
  placeholderAttr : {tagName : TagName} -> PlaceholderElement tagName -> AttributeKey tagName
  maxlengthAttr minlengthAttr : {tagName : TagName} -> LengthElement tagName -> AttributeKey tagName
  valueAttr : {tagName : TagName} -> ValueElement tagName -> AttributeKey tagName
  forAttr : {tagName : TagName} -> ForElement tagName -> AttributeKey tagName

  actionAttr : AttributeKey formTag
  acceptCharsetAttr : AttributeKey formTag
  methodAttr : AttributeKey formTag
  enctypeAttr : AttributeKey formTag
  autocompleteAttr : {tagName : TagName} -> AutocompleteElement tagName -> AttributeKey tagName
  formAutocompleteAttr : AttributeKey formTag
  novalidateAttr : AttributeKey formTag
  formactionAttr : {tagName : TagName} -> FormOverrideElement tagName -> AttributeKey tagName
  formenctypeAttr : {tagName : TagName} -> FormOverrideElement tagName -> AttributeKey tagName
  formmethodAttr : {tagName : TagName} -> FormOverrideElement tagName -> AttributeKey tagName
  formnovalidateAttr : {tagName : TagName} -> FormOverrideElement tagName -> AttributeKey tagName
  formtargetAttr : {tagName : TagName} -> FormOverrideElement tagName -> AttributeKey tagName
  dirnameAttr : {tagName : TagName} -> DirNameElement tagName -> AttributeKey tagName
  popovertargetAttr : {tagName : TagName} -> PopoverControlElement tagName -> AttributeKey tagName
  popovertargetactionAttr : {tagName : TagName} -> PopoverControlElement tagName -> AttributeKey tagName

  inputTypeAttr : AttributeKey inputTag
  alphaAttr switchAttr : AttributeKey inputTag
  buttonTypeAttr : AttributeKey buttonTag
  commandAttr commandforAttr : AttributeKey buttonTag
  checkedAttr : AttributeKey inputTag
  listAttr : AttributeKey inputTag
  patternAttr : AttributeKey inputTag
  acceptAttr : {tagName : TagName} -> AcceptElement tagName -> AttributeKey tagName
  captureAttr : AttributeKey inputTag
  colorspaceAttr : AttributeKey inputTag
  minAttr maxAttr stepAttr : AttributeKey inputTag
  inputSizeAttr : AttributeKey inputTag
  selectSizeAttr : AttributeKey selectTag

  colsAttr rowsAttr : AttributeKey textareaTag
  wrapAttr : AttributeKey textareaTag

  selectedAttr : AttributeKey optionTag
  optionLabelAttr : AttributeKey optionTag
  optgroupLabelAttr : AttributeKey optgroupTag

  objectDataAttr : AttributeKey objectTag

  controlsAttr autoplayAttr loopAttr mutedAttr : {tagName : TagName} -> MediaElement tagName -> AttributeKey tagName
  controlslistAttr disableremoteplaybackAttr : {tagName : TagName} -> MediaElement tagName -> AttributeKey tagName
  preloadAttr : {tagName : TagName} -> MediaElement tagName -> AttributeKey tagName
  posterAttr playsinlineAttr disablepictureinpictureAttr : AttributeKey videoTag
  kindAttr srclangAttr trackLabelAttr defaultAttr : AttributeKey trackTag

  sandboxAttr : AttributeKey iframeTag
  allowAttr : {tagName : TagName} -> AllowElement tagName -> AttributeKey tagName
  allowfullscreenAttr allowpaymentrequestAttr browsingtopicsAttr credentiallessAttr srcdocAttr cspAttr privateTokenAttr : AttributeKey iframeTag
  closedbyAttr : AttributeKey dialogTag
  autolocateAttr watchAttr : AttributeKey geolocationTag

  scriptTypeAttr asyncAttr deferAttr nonceAttr nomoduleAttr : AttributeKey scriptTag

  reversedAttr startAttr olTypeAttr : AttributeKey olTag

  citeAttr : {tagName : TagName} -> CitableElement tagName -> AttributeKey tagName
  datetimeAttr : {tagName : TagName} -> DateTimeElement tagName -> AttributeKey tagName
  openAttr : {tagName : TagName} -> OpenElement tagName -> AttributeKey tagName

  colspanAttr rowspanAttr headersAttr : {tagName : TagName} -> TableCellElement tagName -> AttributeKey tagName
  scopeAttr : AttributeKey thTag
  abbrAttr : AttributeKey thTag
  spanAttr : {tagName : TagName} -> SpanElement tagName -> AttributeKey tagName

  minMeterAttr maxMeterAttr lowAttr highAttr optimumAttr : AttributeKey meterTag
  maxProgressAttr : AttributeKey progressTag

  alignAttr : {tagName : TagName} -> AlignElement tagName -> AttributeKey tagName
  backgroundAttr : {tagName : TagName} -> BackgroundElement tagName -> AttributeKey tagName
  bgcolorAttr : {tagName : TagName} -> BgColorElement tagName -> AttributeKey tagName
  borderAttr : {tagName : TagName} -> BorderElement tagName -> AttributeKey tagName
  colorAttr : {tagName : TagName} -> ColorElement tagName -> AttributeKey tagName
  summaryAttr : AttributeKey tableTag

  shadowrootmodeAttr shadowrootclonableAttr shadowrootcustomelementregistryAttr shadowrootdelegatesfocusAttr shadowrootreferencetargetAttr shadowrootserializableAttr shadowrootslotassignmentAttr : AttributeKey templateTag

AttributeValue : {tagName : TagName} -> AttributeKey tagName -> Type lzero
AttributeValue idAttr = String
AttributeValue classAttr = TokenList
AttributeValue titleAttr = String
AttributeValue langAttr = LanguageTag
AttributeValue dirAttr = Direction
AttributeValue hiddenAttr = HiddenState
AttributeValue tabindexAttr = String
AttributeValue accesskeyAttr = String
AttributeValue draggableAttr = Bool
AttributeValue spellcheckAttr = Bool
AttributeValue translateAttr = Translate
AttributeValue styleAttr = InlineStyle
AttributeValue roleAttr = String
AttributeValue partAttr = TokenList
AttributeValue slotAttr = String
AttributeValue nonceGlobalAttr = String
AttributeValue contenteditableAttr = ContentEditable
AttributeValue inertAttr = Presence
AttributeValue autofocusAttr = Presence
AttributeValue popoverAttr = Popover
AttributeValue anchorAttr = IdReference
AttributeValue autocapitalizeAttr = AutoCapitalize
AttributeValue autocorrectAttr = AutoCorrect
AttributeValue enterkeyhintAttr = EnterKeyHint
AttributeValue exportpartsAttr = String
AttributeValue inputmodeAttr = InputMode
AttributeValue isAttr = String
AttributeValue itemidAttr = String
AttributeValue itempropAttr = TokenList
AttributeValue itemrefAttr = IdReferences
AttributeValue itemscopeAttr = Presence
AttributeValue itemtypeAttr = String
AttributeValue virtualkeyboardpolicyAttr = VirtualKeyboardPolicy
AttributeValue writingsuggestionsAttr = WritingSuggestions
AttributeValue (dataAttr _) = String
AttributeValue (ariaAttr _) = String
AttributeValue (eventHandlerAttr _) = JavaScript
AttributeValue (hrefAttr _) = Url
AttributeValue (targetAttr _) = Target
AttributeValue (relAttr _) = RelList
AttributeValue (hreflangAttr _) = LanguageTag
AttributeValue (attributionsrcAttr _) = AttributionSrc
AttributeValue (interestforAttr _) = IdReference
AttributeValue (downloadAttr _) = String
AttributeValue (pingAttr _) = TokenList
AttributeValue (mediaAttr _) = MediaQuery
AttributeValue asAttr = LinkAs
AttributeValue imagesizesAttr = Sizes
AttributeValue imagesrcsetAttr = SourceSet
AttributeValue coordsAttr = Coordinates
AttributeValue (shapeAttr _) = AreaShape
AttributeValue (srcAttr _) = Url
AttributeValue (srcsetAttr _) = SourceSet
AttributeValue (sizesAttr _) = Sizes
AttributeValue (altAttr _) = String
AttributeValue (usemapAttr _) = IdReference
AttributeValue ismapAttr = Presence
AttributeValue (elementtimingAttr _) = String
AttributeValue (widthAttr _) = String
AttributeValue (heightAttr _) = String
AttributeValue (loadingAttr _) = Loading
AttributeValue decodingAttr = Decoding
AttributeValue (fetchpriorityAttr _) = FetchPriority
AttributeValue (blockingAttr _) = Blocking
AttributeValue (crossoriginAttr _) = CrossOrigin
AttributeValue (referrerpolicyAttr _) = ReferrerPolicy
AttributeValue (integrityAttr _) = IntegrityMetadata
AttributeValue (typeAttr _) = MimeType
AttributeValue charsetAttr = String
AttributeValue contentAttr = String
AttributeValue httpEquivAttr = String
AttributeValue languageAttr = String
AttributeValue (nameAttr _) = String
AttributeValue (formAttr _) = IdReference
AttributeValue (disabledAttr _) = Presence
AttributeValue (readonlyAttr _) = Presence
AttributeValue (requiredAttr _) = Presence
AttributeValue (multipleAttr _) = Presence
AttributeValue (placeholderAttr _) = String
AttributeValue (maxlengthAttr _) = String
AttributeValue (minlengthAttr _) = String
AttributeValue (valueAttr _) = String
AttributeValue (forAttr forLabel) = IdReference
AttributeValue (forAttr forOutput) = IdReferences
AttributeValue actionAttr = Url
AttributeValue acceptCharsetAttr = String
AttributeValue methodAttr = FormMethod
AttributeValue enctypeAttr = FormEncoding
AttributeValue (autocompleteAttr _) = Autocomplete
AttributeValue formAutocompleteAttr = Autocomplete
AttributeValue novalidateAttr = Presence
AttributeValue (formactionAttr _) = Url
AttributeValue (formenctypeAttr _) = FormEncoding
AttributeValue (formmethodAttr _) = FormMethod
AttributeValue (formnovalidateAttr _) = Presence
AttributeValue (formtargetAttr _) = Target
AttributeValue (dirnameAttr _) = String
AttributeValue (popovertargetAttr _) = IdReference
AttributeValue (popovertargetactionAttr _) = PopoverTargetAction
AttributeValue inputTypeAttr = InputType
AttributeValue alphaAttr = Presence
AttributeValue switchAttr = Presence
AttributeValue buttonTypeAttr = ButtonType
AttributeValue commandAttr = ButtonCommand
AttributeValue commandforAttr = IdReference
AttributeValue checkedAttr = Presence
AttributeValue listAttr = IdReference
AttributeValue patternAttr = String
AttributeValue (acceptAttr _) = String
AttributeValue captureAttr = Capture
AttributeValue colorspaceAttr = ColorSpace
AttributeValue minAttr = String
AttributeValue maxAttr = String
AttributeValue stepAttr = String
AttributeValue inputSizeAttr = String
AttributeValue selectSizeAttr = String
AttributeValue colsAttr = String
AttributeValue rowsAttr = String
AttributeValue wrapAttr = Wrap
AttributeValue selectedAttr = Presence
AttributeValue optionLabelAttr = String
AttributeValue optgroupLabelAttr = String
AttributeValue objectDataAttr = Url
AttributeValue (controlsAttr _) = Presence
AttributeValue (autoplayAttr _) = Presence
AttributeValue (loopAttr _) = Presence
AttributeValue (mutedAttr _) = Presence
AttributeValue (controlslistAttr _) = ControlsList
AttributeValue (disableremoteplaybackAttr _) = Presence
AttributeValue (preloadAttr _) = Preload
AttributeValue posterAttr = Url
AttributeValue playsinlineAttr = Presence
AttributeValue disablepictureinpictureAttr = Presence
AttributeValue kindAttr = TrackKind
AttributeValue srclangAttr = LanguageTag
AttributeValue trackLabelAttr = String
AttributeValue defaultAttr = Presence
AttributeValue sandboxAttr = Sandbox
AttributeValue (allowAttr _) = String
AttributeValue allowfullscreenAttr = Presence
AttributeValue allowpaymentrequestAttr = Presence
AttributeValue browsingtopicsAttr = Presence
AttributeValue credentiallessAttr = Presence
AttributeValue srcdocAttr = String
AttributeValue cspAttr = ContentSecurityPolicy
AttributeValue privateTokenAttr = PrivateTokenOptions
AttributeValue closedbyAttr = DialogClosedBy
AttributeValue autolocateAttr = Presence
AttributeValue watchAttr = Presence
AttributeValue scriptTypeAttr = ScriptKind
AttributeValue asyncAttr = Presence
AttributeValue deferAttr = Presence
AttributeValue nonceAttr = String
AttributeValue nomoduleAttr = Presence
AttributeValue reversedAttr = Presence
AttributeValue startAttr = String
AttributeValue olTypeAttr = OrderedListType
AttributeValue (citeAttr _) = Url
AttributeValue (datetimeAttr _) = DateTimeString
AttributeValue (openAttr _) = Presence
AttributeValue (colspanAttr _) = String
AttributeValue (rowspanAttr _) = String
AttributeValue (headersAttr _) = IdReferences
AttributeValue scopeAttr = TableScope
AttributeValue abbrAttr = String
AttributeValue (spanAttr _) = String
AttributeValue minMeterAttr = String
AttributeValue maxMeterAttr = String
AttributeValue lowAttr = String
AttributeValue highAttr = String
AttributeValue optimumAttr = String
AttributeValue maxProgressAttr = String
AttributeValue (alignAttr _) = String
AttributeValue (backgroundAttr _) = Url
AttributeValue (bgcolorAttr _) = CssText
AttributeValue (borderAttr _) = String
AttributeValue (colorAttr _) = CssText
AttributeValue summaryAttr = String
AttributeValue shadowrootmodeAttr = ShadowRootMode
AttributeValue shadowrootclonableAttr = Presence
AttributeValue shadowrootcustomelementregistryAttr = Presence
AttributeValue shadowrootdelegatesfocusAttr = Presence
AttributeValue shadowrootreferencetargetAttr = IdReference
AttributeValue shadowrootserializableAttr = Presence
AttributeValue shadowrootslotassignmentAttr = ShadowRootSlotAssignment

keyString : {tagName : TagName} -> AttributeKey tagName -> String
keyString idAttr = "id"
keyString classAttr = "class"
keyString titleAttr = "title"
keyString langAttr = "lang"
keyString dirAttr = "dir"
keyString hiddenAttr = "hidden"
keyString tabindexAttr = "tabindex"
keyString accesskeyAttr = "accesskey"
keyString draggableAttr = "draggable"
keyString spellcheckAttr = "spellcheck"
keyString translateAttr = "translate"
keyString styleAttr = "style"
keyString roleAttr = "role"
keyString partAttr = "part"
keyString slotAttr = "slot"
keyString nonceGlobalAttr = "nonce"
keyString contenteditableAttr = "contenteditable"
keyString inertAttr = "inert"
keyString autofocusAttr = "autofocus"
keyString popoverAttr = "popover"
keyString anchorAttr = "anchor"
keyString autocapitalizeAttr = "autocapitalize"
keyString autocorrectAttr = "autocorrect"
keyString enterkeyhintAttr = "enterkeyhint"
keyString exportpartsAttr = "exportparts"
keyString inputmodeAttr = "inputmode"
keyString isAttr = "is"
keyString itemidAttr = "itemid"
keyString itempropAttr = "itemprop"
keyString itemrefAttr = "itemref"
keyString itemscopeAttr = "itemscope"
keyString itemtypeAttr = "itemtype"
keyString virtualkeyboardpolicyAttr = "virtualkeyboardpolicy"
keyString writingsuggestionsAttr = "writingsuggestions"
keyString (dataAttr name) = "data-" ++ name
keyString (ariaAttr name) = "aria-" ++ name
keyString (eventHandlerAttr name) = "on" ++ name
keyString (hrefAttr _) = "href"
keyString (targetAttr _) = "target"
keyString (relAttr _) = "rel"
keyString (hreflangAttr _) = "hreflang"
keyString (attributionsrcAttr _) = "attributionsrc"
keyString (interestforAttr _) = "interestfor"
keyString (downloadAttr _) = "download"
keyString (pingAttr _) = "ping"
keyString (mediaAttr _) = "media"
keyString asAttr = "as"
keyString imagesizesAttr = "imagesizes"
keyString imagesrcsetAttr = "imagesrcset"
keyString coordsAttr = "coords"
keyString (shapeAttr _) = "shape"
keyString (srcAttr _) = "src"
keyString (srcsetAttr _) = "srcset"
keyString (sizesAttr _) = "sizes"
keyString (altAttr _) = "alt"
keyString (usemapAttr _) = "usemap"
keyString ismapAttr = "ismap"
keyString (elementtimingAttr _) = "elementtiming"
keyString (widthAttr _) = "width"
keyString (heightAttr _) = "height"
keyString (loadingAttr _) = "loading"
keyString decodingAttr = "decoding"
keyString (fetchpriorityAttr _) = "fetchpriority"
keyString (blockingAttr _) = "blocking"
keyString (crossoriginAttr _) = "crossorigin"
keyString (referrerpolicyAttr _) = "referrerpolicy"
keyString (integrityAttr _) = "integrity"
keyString (typeAttr _) = "type"
keyString charsetAttr = "charset"
keyString contentAttr = "content"
keyString httpEquivAttr = "http-equiv"
keyString languageAttr = "language"
keyString (nameAttr _) = "name"
keyString (formAttr _) = "form"
keyString (disabledAttr _) = "disabled"
keyString (readonlyAttr _) = "readonly"
keyString (requiredAttr _) = "required"
keyString (multipleAttr _) = "multiple"
keyString (placeholderAttr _) = "placeholder"
keyString (maxlengthAttr _) = "maxlength"
keyString (minlengthAttr _) = "minlength"
keyString (valueAttr _) = "value"
keyString (forAttr _) = "for"
keyString actionAttr = "action"
keyString acceptCharsetAttr = "accept-charset"
keyString methodAttr = "method"
keyString enctypeAttr = "enctype"
keyString (autocompleteAttr _) = "autocomplete"
keyString formAutocompleteAttr = "autocomplete"
keyString novalidateAttr = "novalidate"
keyString (formactionAttr _) = "formaction"
keyString (formenctypeAttr _) = "formenctype"
keyString (formmethodAttr _) = "formmethod"
keyString (formnovalidateAttr _) = "formnovalidate"
keyString (formtargetAttr _) = "formtarget"
keyString (dirnameAttr _) = "dirname"
keyString (popovertargetAttr _) = "popovertarget"
keyString (popovertargetactionAttr _) = "popovertargetaction"
keyString inputTypeAttr = "type"
keyString alphaAttr = "alpha"
keyString switchAttr = "switch"
keyString buttonTypeAttr = "type"
keyString commandAttr = "command"
keyString commandforAttr = "commandfor"
keyString checkedAttr = "checked"
keyString listAttr = "list"
keyString patternAttr = "pattern"
keyString (acceptAttr _) = "accept"
keyString captureAttr = "capture"
keyString colorspaceAttr = "colorspace"
keyString minAttr = "min"
keyString maxAttr = "max"
keyString stepAttr = "step"
keyString inputSizeAttr = "size"
keyString selectSizeAttr = "size"
keyString colsAttr = "cols"
keyString rowsAttr = "rows"
keyString wrapAttr = "wrap"
keyString selectedAttr = "selected"
keyString optionLabelAttr = "label"
keyString optgroupLabelAttr = "label"
keyString objectDataAttr = "data"
keyString (controlsAttr _) = "controls"
keyString (autoplayAttr _) = "autoplay"
keyString (loopAttr _) = "loop"
keyString (mutedAttr _) = "muted"
keyString (controlslistAttr _) = "controlslist"
keyString (disableremoteplaybackAttr _) = "disableremoteplayback"
keyString (preloadAttr _) = "preload"
keyString posterAttr = "poster"
keyString playsinlineAttr = "playsinline"
keyString disablepictureinpictureAttr = "disablepictureinpicture"
keyString kindAttr = "kind"
keyString srclangAttr = "srclang"
keyString trackLabelAttr = "label"
keyString defaultAttr = "default"
keyString sandboxAttr = "sandbox"
keyString (allowAttr _) = "allow"
keyString allowfullscreenAttr = "allowfullscreen"
keyString allowpaymentrequestAttr = "allowpaymentrequest"
keyString browsingtopicsAttr = "browsingtopics"
keyString credentiallessAttr = "credentialless"
keyString srcdocAttr = "srcdoc"
keyString cspAttr = "csp"
keyString privateTokenAttr = "privateToken"
keyString closedbyAttr = "closedby"
keyString autolocateAttr = "autolocate"
keyString watchAttr = "watch"
keyString scriptTypeAttr = "type"
keyString asyncAttr = "async"
keyString deferAttr = "defer"
keyString nonceAttr = "nonce"
keyString nomoduleAttr = "nomodule"
keyString reversedAttr = "reversed"
keyString startAttr = "start"
keyString olTypeAttr = "type"
keyString (citeAttr _) = "cite"
keyString (datetimeAttr _) = "datetime"
keyString (openAttr _) = "open"
keyString (colspanAttr _) = "colspan"
keyString (rowspanAttr _) = "rowspan"
keyString (headersAttr _) = "headers"
keyString scopeAttr = "scope"
keyString abbrAttr = "abbr"
keyString (spanAttr _) = "span"
keyString minMeterAttr = "min"
keyString maxMeterAttr = "max"
keyString lowAttr = "low"
keyString highAttr = "high"
keyString optimumAttr = "optimum"
keyString maxProgressAttr = "max"
keyString (alignAttr _) = "align"
keyString (backgroundAttr _) = "background"
keyString (bgcolorAttr _) = "bgcolor"
keyString (borderAttr _) = "border"
keyString (colorAttr _) = "color"
keyString summaryAttr = "summary"
keyString shadowrootmodeAttr = "shadowrootmode"
keyString shadowrootclonableAttr = "shadowrootclonable"
keyString shadowrootcustomelementregistryAttr = "shadowrootcustomelementregistry"
keyString shadowrootdelegatesfocusAttr = "shadowrootdelegatesfocus"
keyString shadowrootreferencetargetAttr = "shadowrootreferencetarget"
keyString shadowrootserializableAttr = "shadowrootserializable"
keyString shadowrootslotassignmentAttr = "shadowrootslotassignment"

valueString : {tagName : TagName} -> (keyName : AttributeKey tagName) -> AttributeValue keyName -> String
valueString idAttr value = value
valueString classAttr value = renderTokenList value
valueString titleAttr value = value
valueString langAttr value = renderLanguageTag value
valueString dirAttr value = renderDirection value
valueString hiddenAttr value = renderHiddenState value
valueString tabindexAttr value = value
valueString accesskeyAttr value = value
valueString draggableAttr value = renderBool value
valueString spellcheckAttr value = renderBool value
valueString translateAttr value = renderTranslate value
valueString styleAttr value = renderInlineStyle value
valueString roleAttr value = value
valueString partAttr value = renderTokenList value
valueString slotAttr value = value
valueString nonceGlobalAttr value = value
valueString contenteditableAttr value = renderContentEditable value
valueString inertAttr value = renderPresence "inert" value
valueString autofocusAttr value = renderPresence "autofocus" value
valueString popoverAttr value = renderPopover value
valueString anchorAttr value = renderIdReference value
valueString autocapitalizeAttr value = renderAutoCapitalize value
valueString autocorrectAttr value = renderAutoCorrect value
valueString enterkeyhintAttr value = renderEnterKeyHint value
valueString exportpartsAttr value = value
valueString inputmodeAttr value = renderInputMode value
valueString isAttr value = value
valueString itemidAttr value = value
valueString itempropAttr value = renderTokenList value
valueString itemrefAttr value = renderIdReferences value
valueString itemscopeAttr value = renderPresence "itemscope" value
valueString itemtypeAttr value = value
valueString virtualkeyboardpolicyAttr value = renderVirtualKeyboardPolicy value
valueString writingsuggestionsAttr value = renderWritingSuggestions value
valueString (dataAttr _) value = value
valueString (ariaAttr _) value = value
valueString (eventHandlerAttr _) value = renderJavaScript value
valueString (hrefAttr _) value = renderUrl value
valueString (targetAttr _) value = renderTarget value
valueString (relAttr _) value = renderRelList value
valueString (hreflangAttr _) value = renderLanguageTag value
valueString (attributionsrcAttr _) value = renderAttributionSrc value
valueString (interestforAttr _) value = renderIdReference value
valueString (downloadAttr _) value = value
valueString (pingAttr _) value = renderTokenList value
valueString (mediaAttr _) value = renderMediaQuery value
valueString asAttr value = renderLinkAs value
valueString imagesizesAttr value = renderSizes value
valueString imagesrcsetAttr value = renderSourceSet value
valueString coordsAttr value = renderCoordinates value
valueString (shapeAttr _) value = renderAreaShape value
valueString (srcAttr _) value = renderUrl value
valueString (srcsetAttr _) value = renderSourceSet value
valueString (sizesAttr _) value = renderSizes value
valueString (altAttr _) value = value
valueString (usemapAttr _) value = renderIdReference value
valueString ismapAttr value = renderPresence "ismap" value
valueString (elementtimingAttr _) value = value
valueString (widthAttr _) value = value
valueString (heightAttr _) value = value
valueString (loadingAttr _) value = renderLoading value
valueString decodingAttr value = renderDecoding value
valueString (fetchpriorityAttr _) value = renderFetchPriority value
valueString (blockingAttr _) value = renderBlocking value
valueString (crossoriginAttr _) value = renderCrossOrigin value
valueString (referrerpolicyAttr _) value = renderReferrerPolicy value
valueString (integrityAttr _) value = renderIntegrityMetadata value
valueString (typeAttr _) value = renderMimeType value
valueString charsetAttr value = value
valueString contentAttr value = value
valueString httpEquivAttr value = value
valueString languageAttr value = value
valueString (nameAttr _) value = value
valueString (formAttr _) value = renderIdReference value
valueString (disabledAttr _) value = renderPresence "disabled" value
valueString (readonlyAttr _) value = renderPresence "readonly" value
valueString (requiredAttr _) value = renderPresence "required" value
valueString (multipleAttr _) value = renderPresence "multiple" value
valueString (placeholderAttr _) value = value
valueString (maxlengthAttr _) value = value
valueString (minlengthAttr _) value = value
valueString (valueAttr _) value = value
valueString (forAttr forLabel) value = renderIdReference value
valueString (forAttr forOutput) value = renderIdReferences value
valueString actionAttr value = renderUrl value
valueString acceptCharsetAttr value = value
valueString methodAttr value = renderFormMethod value
valueString enctypeAttr value = renderFormEncoding value
valueString (autocompleteAttr _) value = renderAutocomplete value
valueString formAutocompleteAttr value = renderAutocomplete value
valueString novalidateAttr value = renderPresence "novalidate" value
valueString (formactionAttr _) value = renderUrl value
valueString (formenctypeAttr _) value = renderFormEncoding value
valueString (formmethodAttr _) value = renderFormMethod value
valueString (formnovalidateAttr _) value = renderPresence "formnovalidate" value
valueString (formtargetAttr _) value = renderTarget value
valueString (dirnameAttr _) value = value
valueString (popovertargetAttr _) value = renderIdReference value
valueString (popovertargetactionAttr _) value = renderPopoverTargetAction value
valueString inputTypeAttr value = renderInputType value
valueString alphaAttr value = renderPresence "alpha" value
valueString switchAttr value = renderPresence "switch" value
valueString buttonTypeAttr value = renderButtonType value
valueString commandAttr value = renderButtonCommand value
valueString commandforAttr value = renderIdReference value
valueString checkedAttr value = renderPresence "checked" value
valueString listAttr value = renderIdReference value
valueString patternAttr value = value
valueString (acceptAttr _) value = value
valueString captureAttr value = renderCapture value
valueString colorspaceAttr value = renderColorSpace value
valueString minAttr value = value
valueString maxAttr value = value
valueString stepAttr value = value
valueString inputSizeAttr value = value
valueString selectSizeAttr value = value
valueString colsAttr value = value
valueString rowsAttr value = value
valueString wrapAttr value = renderWrap value
valueString selectedAttr value = renderPresence "selected" value
valueString optionLabelAttr value = value
valueString optgroupLabelAttr value = value
valueString objectDataAttr value = renderUrl value
valueString (controlsAttr _) value = renderPresence "controls" value
valueString (autoplayAttr _) value = renderPresence "autoplay" value
valueString (loopAttr _) value = renderPresence "loop" value
valueString (mutedAttr _) value = renderPresence "muted" value
valueString (controlslistAttr _) value = renderControlsList value
valueString (disableremoteplaybackAttr _) value = renderPresence "disableremoteplayback" value
valueString (preloadAttr _) value = renderPreload value
valueString posterAttr value = renderUrl value
valueString playsinlineAttr value = renderPresence "playsinline" value
valueString disablepictureinpictureAttr value = renderPresence "disablepictureinpicture" value
valueString kindAttr value = renderTrackKind value
valueString srclangAttr value = renderLanguageTag value
valueString trackLabelAttr value = value
valueString defaultAttr value = renderPresence "default" value
valueString sandboxAttr value = renderSandbox value
valueString (allowAttr _) value = value
valueString allowfullscreenAttr value = renderPresence "allowfullscreen" value
valueString allowpaymentrequestAttr value = renderPresence "allowpaymentrequest" value
valueString browsingtopicsAttr value = renderPresence "browsingtopics" value
valueString credentiallessAttr value = renderPresence "credentialless" value
valueString srcdocAttr value = value
valueString cspAttr value = renderContentSecurityPolicy value
valueString privateTokenAttr value = renderPrivateTokenOptions value
valueString closedbyAttr value = renderDialogClosedBy value
valueString autolocateAttr value = renderPresence "autolocate" value
valueString watchAttr value = renderPresence "watch" value
valueString scriptTypeAttr value = renderScriptKind value
valueString asyncAttr value = renderPresence "async" value
valueString deferAttr value = renderPresence "defer" value
valueString nonceAttr value = value
valueString nomoduleAttr value = renderPresence "nomodule" value
valueString reversedAttr value = renderPresence "reversed" value
valueString startAttr value = value
valueString olTypeAttr value = renderOrderedListType value
valueString (citeAttr _) value = renderUrl value
valueString (datetimeAttr _) value = renderDateTimeString value
valueString (openAttr _) value = renderPresence "open" value
valueString (colspanAttr _) value = value
valueString (rowspanAttr _) value = value
valueString (headersAttr _) value = renderIdReferences value
valueString scopeAttr value = renderTableScope value
valueString abbrAttr value = value
valueString (spanAttr _) value = value
valueString minMeterAttr value = value
valueString maxMeterAttr value = value
valueString lowAttr value = value
valueString highAttr value = value
valueString optimumAttr value = value
valueString maxProgressAttr value = value
valueString (alignAttr _) value = value
valueString (backgroundAttr _) value = renderUrl value
valueString (bgcolorAttr _) value = renderCss value
valueString (borderAttr _) value = value
valueString (colorAttr _) value = renderCss value
valueString summaryAttr value = value
valueString shadowrootmodeAttr value = renderShadowRootMode value
valueString shadowrootclonableAttr value = renderPresence "shadowrootclonable" value
valueString shadowrootcustomelementregistryAttr value = renderPresence "shadowrootcustomelementregistry" value
valueString shadowrootdelegatesfocusAttr value = renderPresence "shadowrootdelegatesfocus" value
valueString shadowrootreferencetargetAttr value = renderIdReference value
valueString shadowrootserializableAttr value = renderPresence "shadowrootserializable" value
valueString shadowrootslotassignmentAttr value = renderShadowRootSlotAssignment value