module FF.HTML.Spec.Safe.Value where

open import Agda.Builtin.String using (String; primStringAppend)
open import Agda.Primitive using (lzero) renaming (Set to Type)
open import Cubical.Data.Bool.Base using (Bool; true; false)
import FF.CSS.Render as CSSRender
import FF.CSS.Spec.Safe as CSS

infixr  _++_

_++_ : String -> String -> String
_++_ = primStringAppend

record CssText : Type lzero where
  constructor css
  field rawCss : String

open CssText public

data InlineStyle : Type lzero where
  styleRaw : String -> InlineStyle
  styleOne : CSS.DeclarationT -> InlineStyle
  styleCons : CSS.DeclarationT -> InlineStyle -> InlineStyle

record Url : Type lzero where
  constructor url
  field rawUrl : String

open Url public

record UrlList : Type lzero where
  constructor urls
  field rawUrls : String

open UrlList public

record MimeType : Type lzero where
  constructor mime
  field rawMime : String

open MimeType public

record LanguageTag : Type lzero where
  constructor language
  field rawLanguage : String

open LanguageTag public

record TokenList : Type lzero where
  constructor tokens
  field rawTokens : String

open TokenList public

record IdReference : Type lzero where
  constructor idRef
  field rawIdRef : String

open IdReference public

record IdReferences : Type lzero where
  constructor idRefs
  field rawIdRefs : String

open IdReferences public

record SourceSet : Type lzero where
  constructor srcset
  field rawSourceSet : String

open SourceSet public

record MediaQuery : Type lzero where
  constructor mediaQuery
  field rawMediaQuery : String

open MediaQuery public

record ContentSecurityPolicy : Type lzero where
  constructor csp
  field rawContentSecurityPolicy : String

open ContentSecurityPolicy public

record PrivateTokenOptions : Type lzero where
  constructor privateToken
  field rawPrivateTokenOptions : String

open PrivateTokenOptions public

record Sizes : Type lzero where
  constructor sizes
  field rawSizes : String

open Sizes public

record Coordinates : Type lzero where
  constructor coords
  field rawCoordinates : String

open Coordinates public

record IntegrityMetadata : Type lzero where
  constructor integrity
  field rawIntegrity : String

open IntegrityMetadata public

record JavaScript : Type lzero where
  constructor js
  field rawJavaScript : String

open JavaScript public

record DateTimeString : Type lzero where
  constructor dateTime
  field rawDateTime : String

open DateTimeString public

data Direction : Type lzero where
  ltr rtl autoDir : Direction

data Translate : Type lzero where
  translateYes translateNo : Translate

data ContentEditable : Type lzero where
  editableTrue editableFalse editablePlaintextOnly : ContentEditable

data Presence : Type lzero where
  present : Presence

data HiddenState : Type lzero where
  hiddenPresent hiddenUntilFound : HiddenState

data Popover : Type lzero where
  popoverAuto popoverHint popoverManual : Popover

data PopoverTargetAction : Type lzero where
  hidePopover showPopover togglePopover : PopoverTargetAction

record CustomCommandName : Type lzero where
  constructor customCommandName
  field customCommandSuffix : String

open CustomCommandName public

data ButtonCommand : Type lzero where
  showModalCommand closeCommand requestCloseCommand showPopoverCommand hidePopoverCommand togglePopoverCommand : ButtonCommand
  customCommand : CustomCommandName -> ButtonCommand

data DialogClosedBy : Type lzero where
  closedByAny closedByCloseRequest closedByNone : DialogClosedBy

data AutoCapitalize : Type lzero where
  autoCapitalizeOff autoCapitalizeNone autoCapitalizeOn autoCapitalizeSentences autoCapitalizeWords autoCapitalizeCharacters : AutoCapitalize

data AutoCorrect : Type lzero where
  autoCorrectOn autoCorrectOff : AutoCorrect

data EnterKeyHint : Type lzero where
  enter enterDone enterGo enterNext enterPrevious enterSearch enterSend : EnterKeyHint

data InputMode : Type lzero where
  inputNone inputText inputDecimal inputNumeric inputTel inputSearch inputEmail inputUrl : InputMode

data VirtualKeyboardPolicy : Type lzero where
  vkAuto vkManual : VirtualKeyboardPolicy

data WritingSuggestions : Type lzero where
  writingSuggestionsTrue writingSuggestionsFalse : WritingSuggestions

data CrossOrigin : Type lzero where
  anonymous useCredentials : CrossOrigin

data ReferrerPolicy : Type lzero where
  noReferrer noReferrerWhenDowngrade originPolicy originWhenCrossOrigin
    sameOrigin strictOrigin strictOriginWhenCrossOrigin unsafeUrl : ReferrerPolicy

data Loading : Type lzero where
  eager lazy : Loading

data Decoding : Type lzero where
  sync async autoDecoding : Decoding

data FetchPriority : Type lzero where
  high low autoPriority : FetchPriority

data Target : Type lzero where
  self blank parent top unfencedTop : Target
  targetName : String -> Target

data LinkAs : Type lzero where
  asAudio asAudioWorklet asDocument asEmbed asFetch asFont asImage asJson asObject
    asPaintWorklet asScript asServiceWorker asSharedWorker asStyle asText asTrack
    asVideo asWorker : LinkAs

data Blocking : Type lzero where
  blockRender : Blocking

data AreaShape : Type lzero where
  rect circle poly defaultShape : AreaShape

data AttributionSrc : Type lzero where
  attributionPresent : AttributionSrc
  attributionUrls : UrlList -> AttributionSrc

data RelToken : Type lzero where
  relAlternate relAuthor relBookmark relCanonical relCompressionDictionary
    relDnsPrefetch relExternal relExpect relHelp relIcon relLicense relManifest
    relMe relModulepreload relNext relNofollow relNoopener relNoreferrer
    relOpener relPingback relPreconnect relPrefetch relPreload relPrerender
    relPrev relPrivacyPolicy relSearch relStylesheet relTag relTermsOfService
    : RelToken
  relCustom : String -> RelToken

data RelList : Type lzero where
  relOne : RelToken -> RelList
  relCons : RelToken -> RelList -> RelList
  relTokens : String -> RelList

data SandboxToken : Type lzero where
  allowDownloads allowForms allowModals allowOrientationLock allowPointerLock
    allowPopups allowPopupsToEscapeSandbox allowPresentation allowSameOrigin
    allowScripts allowStorageAccessByUserActivation allowTopNavigation
    allowTopNavigationByUserActivation allowTopNavigationToCustomProtocols
    : SandboxToken
  sandboxCustom : String -> SandboxToken

data Sandbox : Type lzero where
  sandboxAll : Sandbox
  sandboxOne : SandboxToken -> Sandbox
  sandboxCons : SandboxToken -> Sandbox -> Sandbox
  sandboxTokens : String -> Sandbox

data ControlsListToken : Type lzero where
  noDownload noFullscreen noRemotePlayback : ControlsListToken
  controlsListCustom : String -> ControlsListToken

data ControlsList : Type lzero where
  controlsOne : ControlsListToken -> ControlsList
  controlsCons : ControlsListToken -> ControlsList -> ControlsList
  controlsTokens : String -> ControlsList

data InputType : Type lzero where
  hiddenInput textInput searchInput telInput urlInput emailInput passwordInput
    dateInput monthInput weekInput timeInput datetimeLocalInput numberInput
    rangeInput colorInput checkboxInput radioInput fileInput submitInput
    imageInput resetInput buttonInput : InputType

data ButtonType : Type lzero where
  submitButton resetButton plainButton : ButtonType

data FormMethod : Type lzero where
  get post dialogMethod : FormMethod

data FormEncoding : Type lzero where
  urlEncoded multipartFormData textPlain : FormEncoding

data Autocomplete : Type lzero where
  autocompleteOn autocompleteOff : Autocomplete
  autocompleteTokens : String -> Autocomplete

data Wrap : Type lzero where
  hard soft off : Wrap

data Capture : Type lzero where
  userCapture environmentCapture : Capture
  captureToken : String -> Capture

data ColorSpace : Type lzero where
  limitedSRGB displayP3 : ColorSpace

data Preload : Type lzero where
  preloadNone preloadMetadata preloadAuto : Preload

data TrackKind : Type lzero where
  subtitles captions descriptions chapters metadata : TrackKind

data TableScope : Type lzero where
  row col rowgroup colgroup : TableScope

data OrderedListType : Type lzero where
  decimal lowerAlpha upperAlpha lowerRoman upperRoman : OrderedListType

data ScriptKind : Type lzero where
  classicScript moduleScript importMap speculationRules : ScriptKind
  scriptMime : MimeType -> ScriptKind

data ShadowRootMode : Type lzero where
  shadowRootOpen shadowRootClosed : ShadowRootMode

data ShadowRootSlotAssignment : Type lzero where
  namedSlotAssignment manualSlotAssignment : ShadowRootSlotAssignment

renderBool : Bool -> String
renderBool true = "true"
renderBool false = "false"

renderCss : CssText -> String
renderCss (css raw) = raw

renderCssDeclaration : CSS.DeclarationT -> String
renderCssDeclaration declaration =
  CSSRender.renderDeclarationWithSemicolon CSS.renderer declaration

renderInlineStyle : InlineStyle -> String
renderInlineStyle (styleRaw raw) = raw
renderInlineStyle (styleOne declaration) = renderCssDeclaration declaration
renderInlineStyle (styleCons declaration rest) =
  renderCssDeclaration declaration ++ " " ++ renderInlineStyle rest

renderUrl : Url -> String
renderUrl (url raw) = raw

renderUrlList : UrlList -> String
renderUrlList (urls raw) = raw

renderMimeType : MimeType -> String
renderMimeType (mime raw) = raw

renderLanguageTag : LanguageTag -> String
renderLanguageTag (language raw) = raw

renderTokenList : TokenList -> String
renderTokenList (tokens raw) = raw

renderIdReference : IdReference -> String
renderIdReference (idRef raw) = raw

renderIdReferences : IdReferences -> String
renderIdReferences (idRefs raw) = raw

renderSourceSet : SourceSet -> String
renderSourceSet (srcset raw) = raw

renderMediaQuery : MediaQuery -> String
renderMediaQuery (mediaQuery raw) = raw

renderContentSecurityPolicy : ContentSecurityPolicy -> String
renderContentSecurityPolicy (csp raw) = raw

renderPrivateTokenOptions : PrivateTokenOptions -> String
renderPrivateTokenOptions (privateToken raw) = raw

renderSizes : Sizes -> String
renderSizes (sizes raw) = raw

renderCoordinates : Coordinates -> String
renderCoordinates (coords raw) = raw

renderIntegrityMetadata : IntegrityMetadata -> String
renderIntegrityMetadata (integrity raw) = raw

renderJavaScript : JavaScript -> String
renderJavaScript (js raw) = raw

renderDateTimeString : DateTimeString -> String
renderDateTimeString (dateTime raw) = raw

renderDirection : Direction -> String
renderDirection ltr = "ltr"
renderDirection rtl = "rtl"
renderDirection autoDir = "auto"

renderTranslate : Translate -> String
renderTranslate translateYes = "yes"
renderTranslate translateNo = "no"

renderContentEditable : ContentEditable -> String
renderContentEditable editableTrue = "true"
renderContentEditable editableFalse = "false"
renderContentEditable editablePlaintextOnly = "plaintext-only"

renderPresence : String -> Presence -> String
renderPresence name present = name

renderHiddenState : HiddenState -> String
renderHiddenState hiddenPresent = "hidden"
renderHiddenState hiddenUntilFound = "until-found"

renderPopover : Popover -> String
renderPopover popoverAuto = "auto"
renderPopover popoverHint = "hint"
renderPopover popoverManual = "manual"

renderPopoverTargetAction : PopoverTargetAction -> String
renderPopoverTargetAction hidePopover = "hide"
renderPopoverTargetAction showPopover = "show"
renderPopoverTargetAction togglePopover = "toggle"

renderButtonCommand : ButtonCommand -> String
renderButtonCommand showModalCommand = "show-modal"
renderButtonCommand closeCommand = "close"
renderButtonCommand requestCloseCommand = "request-close"
renderButtonCommand showPopoverCommand = "show-popover"
renderButtonCommand hidePopoverCommand = "hide-popover"
renderButtonCommand togglePopoverCommand = "toggle-popover"
renderButtonCommand (customCommand command) = "--" ++ customCommandSuffix command

renderDialogClosedBy : DialogClosedBy -> String
renderDialogClosedBy closedByAny = "any"
renderDialogClosedBy closedByCloseRequest = "closerequest"
renderDialogClosedBy closedByNone = "none"

renderAutoCapitalize : AutoCapitalize -> String
renderAutoCapitalize autoCapitalizeOff = "off"
renderAutoCapitalize autoCapitalizeNone = "none"
renderAutoCapitalize autoCapitalizeOn = "on"
renderAutoCapitalize autoCapitalizeSentences = "sentences"
renderAutoCapitalize autoCapitalizeWords = "words"
renderAutoCapitalize autoCapitalizeCharacters = "characters"

renderAutoCorrect : AutoCorrect -> String
renderAutoCorrect autoCorrectOn = "on"
renderAutoCorrect autoCorrectOff = "off"

renderEnterKeyHint : EnterKeyHint -> String
renderEnterKeyHint enter = "enter"
renderEnterKeyHint enterDone = "done"
renderEnterKeyHint enterGo = "go"
renderEnterKeyHint enterNext = "next"
renderEnterKeyHint enterPrevious = "previous"
renderEnterKeyHint enterSearch = "search"
renderEnterKeyHint enterSend = "send"

renderInputMode : InputMode -> String
renderInputMode inputNone = "none"
renderInputMode inputText = "text"
renderInputMode inputDecimal = "decimal"
renderInputMode inputNumeric = "numeric"
renderInputMode inputTel = "tel"
renderInputMode inputSearch = "search"
renderInputMode inputEmail = "email"
renderInputMode inputUrl = "url"

renderVirtualKeyboardPolicy : VirtualKeyboardPolicy -> String
renderVirtualKeyboardPolicy vkAuto = "auto"
renderVirtualKeyboardPolicy vkManual = "manual"

renderWritingSuggestions : WritingSuggestions -> String
renderWritingSuggestions writingSuggestionsTrue = "true"
renderWritingSuggestions writingSuggestionsFalse = "false"

renderCrossOrigin : CrossOrigin -> String
renderCrossOrigin anonymous = "anonymous"
renderCrossOrigin useCredentials = "use-credentials"

renderReferrerPolicy : ReferrerPolicy -> String
renderReferrerPolicy noReferrer = "no-referrer"
renderReferrerPolicy noReferrerWhenDowngrade = "no-referrer-when-downgrade"
renderReferrerPolicy originPolicy = "origin"
renderReferrerPolicy originWhenCrossOrigin = "origin-when-cross-origin"
renderReferrerPolicy sameOrigin = "same-origin"
renderReferrerPolicy strictOrigin = "strict-origin"
renderReferrerPolicy strictOriginWhenCrossOrigin = "strict-origin-when-cross-origin"
renderReferrerPolicy unsafeUrl = "unsafe-url"

renderLoading : Loading -> String
renderLoading eager = "eager"
renderLoading lazy = "lazy"

renderDecoding : Decoding -> String
renderDecoding sync = "sync"
renderDecoding async = "async"
renderDecoding autoDecoding = "auto"

renderFetchPriority : FetchPriority -> String
renderFetchPriority high = "high"
renderFetchPriority low = "low"
renderFetchPriority autoPriority = "auto"

renderTarget : Target -> String
renderTarget self = "_self"
renderTarget blank = "_blank"
renderTarget parent = "_parent"
renderTarget top = "_top"
renderTarget unfencedTop = "_unfencedTop"
renderTarget (targetName name) = name

renderLinkAs : LinkAs -> String
renderLinkAs asAudio = "audio"
renderLinkAs asAudioWorklet = "audioworklet"
renderLinkAs asDocument = "document"
renderLinkAs asEmbed = "embed"
renderLinkAs asFetch = "fetch"
renderLinkAs asFont = "font"
renderLinkAs asImage = "image"
renderLinkAs asJson = "json"
renderLinkAs asObject = "object"
renderLinkAs asPaintWorklet = "paintworklet"
renderLinkAs asScript = "script"
renderLinkAs asServiceWorker = "serviceworker"
renderLinkAs asSharedWorker = "sharedworker"
renderLinkAs asStyle = "style"
renderLinkAs asText = "text"
renderLinkAs asTrack = "track"
renderLinkAs asVideo = "video"
renderLinkAs asWorker = "worker"

renderBlocking : Blocking -> String
renderBlocking blockRender = "render"

renderAreaShape : AreaShape -> String
renderAreaShape rect = "rect"
renderAreaShape circle = "circle"
renderAreaShape poly = "poly"
renderAreaShape defaultShape = "default"

renderAttributionSrc : AttributionSrc -> String
renderAttributionSrc attributionPresent = "attributionsrc"
renderAttributionSrc (attributionUrls sourceUrls) = renderUrlList sourceUrls

renderRelToken : RelToken -> String
renderRelToken relAlternate = "alternate"
renderRelToken relAuthor = "author"
renderRelToken relBookmark = "bookmark"
renderRelToken relCanonical = "canonical"
renderRelToken relCompressionDictionary = "compression-dictionary"
renderRelToken relDnsPrefetch = "dns-prefetch"
renderRelToken relExternal = "external"
renderRelToken relExpect = "expect"
renderRelToken relHelp = "help"
renderRelToken relIcon = "icon"
renderRelToken relLicense = "license"
renderRelToken relManifest = "manifest"
renderRelToken relMe = "me"
renderRelToken relModulepreload = "modulepreload"
renderRelToken relNext = "next"
renderRelToken relNofollow = "nofollow"
renderRelToken relNoopener = "noopener"
renderRelToken relNoreferrer = "noreferrer"
renderRelToken relOpener = "opener"
renderRelToken relPingback = "pingback"
renderRelToken relPreconnect = "preconnect"
renderRelToken relPrefetch = "prefetch"
renderRelToken relPreload = "preload"
renderRelToken relPrerender = "prerender"
renderRelToken relPrev = "prev"
renderRelToken relPrivacyPolicy = "privacy-policy"
renderRelToken relSearch = "search"
renderRelToken relStylesheet = "stylesheet"
renderRelToken relTag = "tag"
renderRelToken relTermsOfService = "terms-of-service"
renderRelToken (relCustom value) = value

renderRelList : RelList -> String
renderRelList (relOne token) = renderRelToken token
renderRelList (relCons token rest) = renderRelToken token ++ " " ++ renderRelList rest
renderRelList (relTokens value) = value

renderSandboxToken : SandboxToken -> String
renderSandboxToken allowDownloads = "allow-downloads"
renderSandboxToken allowForms = "allow-forms"
renderSandboxToken allowModals = "allow-modals"
renderSandboxToken allowOrientationLock = "allow-orientation-lock"
renderSandboxToken allowPointerLock = "allow-pointer-lock"
renderSandboxToken allowPopups = "allow-popups"
renderSandboxToken allowPopupsToEscapeSandbox = "allow-popups-to-escape-sandbox"
renderSandboxToken allowPresentation = "allow-presentation"
renderSandboxToken allowSameOrigin = "allow-same-origin"
renderSandboxToken allowScripts = "allow-scripts"
renderSandboxToken allowStorageAccessByUserActivation = "allow-storage-access-by-user-activation"
renderSandboxToken allowTopNavigation = "allow-top-navigation"
renderSandboxToken allowTopNavigationByUserActivation = "allow-top-navigation-by-user-activation"
renderSandboxToken allowTopNavigationToCustomProtocols = "allow-top-navigation-to-custom-protocols"
renderSandboxToken (sandboxCustom value) = value

renderSandbox : Sandbox -> String
renderSandbox sandboxAll = ""
renderSandbox (sandboxOne token) = renderSandboxToken token
renderSandbox (sandboxCons token sandboxAll) = renderSandboxToken token
renderSandbox (sandboxCons token rest) = renderSandboxToken token ++ " " ++ renderSandbox rest
renderSandbox (sandboxTokens value) = value

renderControlsListToken : ControlsListToken -> String
renderControlsListToken noDownload = "nodownload"
renderControlsListToken noFullscreen = "nofullscreen"
renderControlsListToken noRemotePlayback = "noremoteplayback"
renderControlsListToken (controlsListCustom value) = value

renderControlsList : ControlsList -> String
renderControlsList (controlsOne token) = renderControlsListToken token
renderControlsList (controlsCons token rest) = renderControlsListToken token ++ " " ++ renderControlsList rest
renderControlsList (controlsTokens value) = value

renderInputType : InputType -> String
renderInputType hiddenInput = "hidden"
renderInputType textInput = "text"
renderInputType searchInput = "search"
renderInputType telInput = "tel"
renderInputType urlInput = "url"
renderInputType emailInput = "email"
renderInputType passwordInput = "password"
renderInputType dateInput = "date"
renderInputType monthInput = "month"
renderInputType weekInput = "week"
renderInputType timeInput = "time"
renderInputType datetimeLocalInput = "datetime-local"
renderInputType numberInput = "number"
renderInputType rangeInput = "range"
renderInputType colorInput = "color"
renderInputType checkboxInput = "checkbox"
renderInputType radioInput = "radio"
renderInputType fileInput = "file"
renderInputType submitInput = "submit"
renderInputType imageInput = "image"
renderInputType resetInput = "reset"
renderInputType buttonInput = "button"

renderButtonType : ButtonType -> String
renderButtonType submitButton = "submit"
renderButtonType resetButton = "reset"
renderButtonType plainButton = "button"

renderFormMethod : FormMethod -> String
renderFormMethod get = "get"
renderFormMethod post = "post"
renderFormMethod dialogMethod = "dialog"

renderFormEncoding : FormEncoding -> String
renderFormEncoding urlEncoded = "application/x-www-form-urlencoded"
renderFormEncoding multipartFormData = "multipart/form-data"
renderFormEncoding textPlain = "text/plain"

renderAutocomplete : Autocomplete -> String
renderAutocomplete autocompleteOn = "on"
renderAutocomplete autocompleteOff = "off"
renderAutocomplete (autocompleteTokens raw) = raw

renderWrap : Wrap -> String
renderWrap hard = "hard"
renderWrap soft = "soft"
renderWrap off = "off"

renderCapture : Capture -> String
renderCapture userCapture = "user"
renderCapture environmentCapture = "environment"
renderCapture (captureToken token) = token

renderColorSpace : ColorSpace -> String
renderColorSpace limitedSRGB = "limited-srgb"
renderColorSpace displayP3 = "display-p3"

renderPreload : Preload -> String
renderPreload preloadNone = "none"
renderPreload preloadMetadata = "metadata"
renderPreload preloadAuto = "auto"

renderTrackKind : TrackKind -> String
renderTrackKind subtitles = "subtitles"
renderTrackKind captions = "captions"
renderTrackKind descriptions = "descriptions"
renderTrackKind chapters = "chapters"
renderTrackKind metadata = "metadata"

renderTableScope : TableScope -> String
renderTableScope row = "row"
renderTableScope col = "col"
renderTableScope rowgroup = "rowgroup"
renderTableScope colgroup = "colgroup"

renderOrderedListType : OrderedListType -> String
renderOrderedListType decimal = "1"
renderOrderedListType lowerAlpha = "a"
renderOrderedListType upperAlpha = "A"
renderOrderedListType lowerRoman = "i"
renderOrderedListType upperRoman = "I"

renderScriptKind : ScriptKind -> String
renderScriptKind classicScript = "text/javascript"
renderScriptKind moduleScript = "module"
renderScriptKind importMap = "importmap"
renderScriptKind speculationRules = "speculationrules"
renderScriptKind (scriptMime mediaType) = renderMimeType mediaType

renderShadowRootMode : ShadowRootMode -> String
renderShadowRootMode shadowRootOpen = "open"
renderShadowRootMode shadowRootClosed = "closed"

renderShadowRootSlotAssignment : ShadowRootSlotAssignment -> String
renderShadowRootSlotAssignment namedSlotAssignment = "named"
renderShadowRootSlotAssignment manualSlotAssignment = "manual"