module FF.HTML.Spec.Common where

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

open import FF.HTML.Core using (Spec; Html; Map)
open import FF.HTML.Render using (Renderer; renderVia)
import FF.HTML.Spec.Loose as Loose
open import FF.HTML.Spec.Safe.Tag public using (TagName; tagString)

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

HtmlT : Type lzero
HtmlT = Html spec

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

toLoose : Map spec Loose.spec
toLoose =
  record
    { mapTag = tagString
    ; mapKey = \ keyName -> keyName
    ; mapValue = \ _ value -> value
    ; mapAtom = \ content -> content
    }

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