module FF.HTML.Spec.Loose 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; attr; atomic; node)
open import FF.HTML.Render using (Renderer; render)

spec : Spec lzero lzero lzero lzero
spec =
  record
    { Tag = String
    ; AttrKey = \ _ -> String
    ; AttrValue = \ _ -> String
    ; Atom = String
    }

HtmlT : Type lzero
HtmlT = Html spec

renderer : Renderer spec
renderer =
  record
    { renderTag = \ tagName -> tagName
    ; renderKey = \ keyName -> keyName
    ; renderValue = \ _ value -> value
    ; renderAtom = \ content -> content
    }

text : String -> HtmlT
text = atomic

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

attribute : {tagName : String} -> String -> String -> Attribute spec tagName
attribute keyName value = attr keyName value

example : HtmlT
example =
  node "p"
    (attr "class" "intro" :: [])
    (atomic "hello" :: [])

renderedExample : String
renderedExample = render renderer example