module FF.HTML.Render where

open import Agda.Builtin.String using (String; primStringAppend)
open import Agda.Primitive using (Level; lzero; lsuc) renaming (Set to Type; _⊔_ to _lmax_)
open import Cubical.Foundations.Prelude using ()
open import Cubical.Data.List.Base using (List; []) renaming (_∷_ to _::_)

open import FF.HTML.Core

infixr  _++_

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

private
  levelOf : Level -> Level -> Level -> Level -> Level
  levelOf tag key val atom = tag lmax key lmax val lmax atom

record Renderer
  {tag key val atom : Level}
  (S : Spec tag key val atom)
  : Type (levelOf tag key val atom) where
  field
    renderTag   : Tag S -> String
    renderKey   : {tagName : Tag S} -> AttrKey S tagName -> String
    renderValue : {tagName : Tag S} -> (keyName : AttrKey S tagName) -> AttrValue S keyName -> String
    renderAtom  : Atom S -> String

open Renderer public

renderAttribute :
  {tag key val atom : Level}
  {S : Spec tag key val atom}
  (renderer : Renderer S) ->
  {tagName : Tag S} ->
  Attribute S tagName ->
  String
renderAttribute renderer (attr keyName value) =
  Renderer.renderKey renderer keyName ++ "=\"" ++
  Renderer.renderValue renderer keyName value ++ "\""

renderAttributes :
  {tag key val atom : Level}
  {S : Spec tag key val atom}
  (renderer : Renderer S) ->
  {tagName : Tag S} ->
  List (Attribute S tagName) ->
  String
renderAttributes renderer [] = ""
renderAttributes renderer (attribute :: rest) =
  " " ++ renderAttribute renderer attribute ++ renderAttributes renderer rest

mutual
  render :
    {tag key val atom : Level}
    {S : Spec tag key val atom} ->
    Renderer S ->
    Html S ->
    String
  render renderer (atomic content) =
    Renderer.renderAtom renderer content
  render renderer (node tagName attrs children) =
    "<" ++ Renderer.renderTag renderer tagName ++ renderAttributes renderer attrs ++ ">" ++
    renderChildren renderer children ++
    "</" ++ Renderer.renderTag renderer tagName ++ ">"

  renderChildren :
    {tag key val atom : Level}
    {S : Spec tag key val atom} ->
    Renderer S ->
    List (Html S) ->
    String
  renderChildren renderer [] = ""
  renderChildren renderer (child :: rest) =
    render renderer child ++ renderChildren renderer rest

pullRenderer :
  {tag key val atom tag' key' val' atom' : Level}
  {From : Spec tag key val atom}
  {To : Spec tag' key' val' atom'} ->
  Map From To ->
  Renderer To ->
  Renderer From
pullRenderer f renderer =
  record
    { renderTag = \ tagName ->
        Renderer.renderTag renderer (Map.mapTag f tagName)
    ; renderKey = \ keyName ->
        Renderer.renderKey renderer (Map.mapKey f keyName)
    ; renderValue = \ keyName value ->
        Renderer.renderValue renderer (Map.mapKey f keyName) (Map.mapValue f keyName value)
    ; renderAtom = \ content ->
        Renderer.renderAtom renderer (Map.mapAtom f content)
    }

renderVia :
  {tag key val atom tag' key' val' atom' : Level}
  {From : Spec tag key val atom}
  {To : Spec tag' key' val' atom'} ->
  Map From To ->
  Renderer To ->
  Html From ->
  String
renderVia f renderer html = render renderer (mapHtml f html)