module FF.HTML.Spec.Safe 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 (List; []) renaming (_∷_ to _::_)

open import FF.HTML.Core using (Spec; Attribute; Html; Map; attr; atomic; node; composeMap)
open import FF.HTML.Render using (Renderer; render; renderVia)
import FF.HTML.Spec.Common as Common
import FF.HTML.Spec.Loose as Loose
import FF.HTML.Spec.Safe.Feature
open import FF.HTML.Spec.Safe.Value public
open import FF.HTML.Spec.Safe.Tag public
open import FF.HTML.Spec.Safe.Attribute public

module Feature = FF.HTML.Spec.Safe.Feature

spec : Spec lzero lzero lzero lzero
spec =
  record
    { Tag = TagName
    ; AttrKey = AttributeKey
    ; AttrValue = AttributeValue
    ; Atom = String
    }

HtmlT : Type lzero
HtmlT = Html spec

renderer : Renderer spec
renderer =
  record
    { renderTag = tagString
    ; renderKey = keyString
    ; renderValue = valueString
    ; renderAtom = \ content -> content
    }

attribute : {tagName : TagName} -> (keyName : AttributeKey tagName) -> AttributeValue keyName -> Attribute spec tagName
attribute keyName value = attr keyName value

text : String -> HtmlT
text = atomic

element : (tagName : TagName) -> List (Attribute spec tagName) -> List HtmlT -> HtmlT
element = node

void : {tagName : TagName} -> Feature.VoidElement tagName -> List (Attribute spec tagName) -> HtmlT
void {tagName = tagName} _ attrs = node tagName attrs []

toCommon : Map spec Common.spec
toCommon =
  record
    { mapTag = \ tagName -> tagName
    ; mapKey = keyString
    ; mapValue = valueString
    ; mapAtom = \ content -> content
    }

toLoose : Map spec Loose.spec
toLoose = composeMap Common.toLoose toCommon

renderedByCommonRenderer : HtmlT -> String
renderedByCommonRenderer = renderVia toCommon Common.renderer

renderedByLooseRenderer : HtmlT -> String
renderedByLooseRenderer = renderVia toLoose Loose.renderer

paragraph : String -> HtmlT
paragraph content = node pTag [] (atomic content :: [])

link : Url -> String -> HtmlT
link destination label =
  node aTag
    (attr (hrefAttr hrefA) destination :: [])
    (atomic label :: [])

image : Url -> String -> HtmlT
image source alternative =
  node imgTag
    ( attr (srcAttr srcImg) source
    :: attr (altAttr altImg) alternative
    :: []
    )
    []

inputControl : String -> InputType -> HtmlT
inputControl name inputType =
  node inputTag
    ( attr (nameAttr nameInput) name
    :: attr inputTypeAttr inputType
    :: []
    )
    []

example : HtmlT
example =
  node sectionTag
    ( attr classAttr (tokens "document")
    :: attr styleAttr (styleRaw "max-width: 42rem")
    :: attr (ariaAttr "label") "Example document"
    :: []
    )
    ( node h1Tag [] (atomic "hello" :: [])
    :: paragraph "This is typed HTML."
    :: link (url "https://developer.mozilla.org/") "MDN"
    :: image (url "hero.png") "Decorative hero"
    :: inputControl "email" emailInput
    :: []
    )