module FF.HTML.Core where

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 _::_)

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

record Spec (tag key val atom : Level) : Type (lsuc (levelOf tag key val atom)) where
  field
    Tag       : Type tag
    AttrKey   : Tag -> Type key
    AttrValue : {tag : Tag} -> AttrKey tag -> Type val
    Atom      : Type atom

open Spec public

record Attribute
  {tag key val atom : Level}
  (S : Spec tag key val atom)
  (tagName : Tag S)
  : Type (key lmax val) where
  constructor attr
  field
    keyName : AttrKey S tagName
    value   : AttrValue S keyName

open Attribute public

data Html
  {tag key val atom : Level}
  (S : Spec tag key val atom)
  : Type (levelOf tag key val atom) where
  atomic : Atom S -> Html S
  node   : (tagName : Tag S) -> List (Attribute S tagName) -> List (Html S) -> Html S

record Map
  {tag key val atom tag' key' val' atom' : Level}
  (From : Spec tag key val atom)
  (To : Spec tag' key' val' atom')
  : Type (levelOf tag key val atom lmax levelOf tag' key' val' atom') where
  field
    mapTag   : Tag From -> Tag To
    mapKey   : {tagName : Tag From} -> AttrKey From tagName -> AttrKey To (mapTag tagName)
    mapValue :
      {tagName : Tag From} ->
      (keyName : AttrKey From tagName) ->
      AttrValue From keyName ->
      AttrValue To (mapKey keyName)
    mapAtom  : Atom From -> Atom To

open Map public

mapAttribute :
  {tag key val atom tag' key' val' atom' : Level}
  {From : Spec tag key val atom}
  {To : Spec tag' key' val' atom'}
  (f : Map From To) ->
  {tagName : Tag From} ->
  Attribute From tagName ->
  Attribute To (Map.mapTag f tagName)
mapAttribute f (attr keyName value) =
  attr (Map.mapKey f keyName) (Map.mapValue f keyName value)

mapAttributes :
  {tag key val atom tag' key' val' atom' : Level}
  {From : Spec tag key val atom}
  {To : Spec tag' key' val' atom'}
  (f : Map From To) ->
  {tagName : Tag From} ->
  List (Attribute From tagName) ->
  List (Attribute To (Map.mapTag f tagName))
mapAttributes f [] = []
mapAttributes f (attribute :: rest) =
  mapAttribute f attribute :: mapAttributes f rest

mutual
  mapHtml :
    {tag key val atom tag' key' val' atom' : Level}
    {From : Spec tag key val atom}
    {To : Spec tag' key' val' atom'}
    (f : Map From To) ->
    Html From ->
    Html To
  mapHtml f (atomic content) = atomic (Map.mapAtom f content)
  mapHtml f (node tagName attrs children) =
    node
      (Map.mapTag f tagName)
      (mapAttributes f attrs)
      (mapChildren f children)

  mapChildren :
    {tag key val atom tag' key' val' atom' : Level}
    {From : Spec tag key val atom}
    {To : Spec tag' key' val' atom'}
    (f : Map From To) ->
    List (Html From) ->
    List (Html To)
  mapChildren f [] = []
  mapChildren f (child :: rest) =
    mapHtml f child :: mapChildren f rest

idMap :
  {tag key val atom : Level}
  {S : Spec tag key val atom} ->
  Map S S
idMap =
  record
    { mapTag = \ tagName -> tagName
    ; mapKey = \ keyName -> keyName
    ; mapValue = \ keyName value -> value
    ; mapAtom = \ content -> content
    }

composeMap :
  {tagA keyA valA atomA tagB keyB valB atomB tagC keyC valC atomC : Level}
  {A : Spec tagA keyA valA atomA}
  {B : Spec tagB keyB valB atomB}
  {C : Spec tagC keyC valC atomC} ->
  Map B C ->
  Map A B ->
  Map A C
composeMap g f =
  record
    { mapTag = \ tagName ->
        Map.mapTag g (Map.mapTag f tagName)
    ; mapKey = \ keyName ->
        Map.mapKey g (Map.mapKey f keyName)
    ; mapValue = \ keyName value ->
        Map.mapValue g (Map.mapKey f keyName) (Map.mapValue f keyName value)
    ; mapAtom = \ content ->
        Map.mapAtom g (Map.mapAtom f content)
    }