FF.HTML.StyleSheet.Core

module FF.HTML.StyleSheet.Core where

open import Agda.Builtin.String using (String; primStringAppend)
open import Agda.Primitive using (Level; lsuc) renaming (Set to Type; _⊔_ to _lmax_)
open import Cubical.Data.Bool.Base using (if_then_else_)
open import Cubical.Data.List.Base using (List; []; _∷_)
open import Cubical.Data.Nat.Base using (ℕ; zero; suc; _+_)

import FF.CSS.Core as CSS
import FF.CSS.Render as CSSRender
import FF.HTML.Core as HTML
import FF.HTML.Render as HTMLRender
import FF.HTML.Selector.Core as Selector
import FF.HTML.Selector.Semantics as SelectorSemantics

private
  infixr 5 _++_
  infixr 5 _++L_

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

  _++L_ : {a : Level} {A : Type a} -> List A -> List A -> List A
  [] ++L ys = ys
  (x ∷ xs) ++L ys = x ∷ (xs ++L ys)

  levelOf :
    Level -> Level -> Level -> Level ->
    Level -> Level ->
    Level
  levelOf tag key val atom property value =
    tag lmax key lmax val lmax atom lmax property lmax value

data StyleRule
  {tag key val atom property value : Level}
  (H : HTML.Spec tag key val atom)
  (C : CSS.Spec property value)
  : Type (levelOf tag key val atom property value) where
  styleRule :
    Selector.SelectorList H ->
    List (CSS.Declaration C) ->
    StyleRule H C

data StyleSheet
  {tag key val atom property value : Level}
  (H : HTML.Spec tag key val atom)
  (C : CSS.Spec property value)
  : Type (levelOf tag key val atom property value) where
  emptySheet : StyleSheet H C
  ruleCons : StyleRule H C -> StyleSheet H C -> StyleSheet H C

infixr 5 ruleCons

fromRules :
  {tag key val atom property value : Level}
  {H : HTML.Spec tag key val atom}
  {C : CSS.Spec property value} ->
  List (StyleRule H C) ->
  StyleSheet H C
fromRules [] = emptySheet
fromRules (rule ∷ rest) = ruleCons rule (fromRules rest)

toRules :
  {tag key val atom property value : Level}
  {H : HTML.Spec tag key val atom}
  {C : CSS.Spec property value} ->
  StyleSheet H C ->
  List (StyleRule H C)
toRules emptySheet = []
toRules (ruleCons rule rest) = rule ∷ toRules rest

renderDeclarations :
  {property value : Level}
  {C : CSS.Spec property value} ->
  CSSRender.Renderer C ->
  List (CSS.Declaration C) ->
  String
renderDeclarations renderer [] = ""
renderDeclarations renderer (declaration ∷ []) =
  CSSRender.renderDeclarationWithSemicolon renderer declaration
renderDeclarations renderer (declaration ∷ rest@(_ ∷ _)) =
  CSSRender.renderDeclarationWithSemicolon renderer declaration ++
  " " ++
  renderDeclarations renderer rest

renderRule :
  {tag key val atom property value : Level}
  {H : HTML.Spec tag key val atom}
  {C : CSS.Spec property value} ->
  HTMLRender.Renderer H ->
  CSSRender.Renderer C ->
  StyleRule H C ->
  String
renderRule htmlRenderer cssRenderer (styleRule selectors declarations) =
  Selector.renderSelectorList htmlRenderer selectors ++
  " { " ++
  renderDeclarations cssRenderer declarations ++
  " }"

renderStyleSheet :
  {tag key val atom property value : Level}
  {H : HTML.Spec tag key val atom}
  {C : CSS.Spec property value} ->
  HTMLRender.Renderer H ->
  CSSRender.Renderer C ->
  StyleSheet H C ->
  String
renderStyleSheet htmlRenderer cssRenderer emptySheet = ""
renderStyleSheet htmlRenderer cssRenderer (ruleCons rule emptySheet) =
  renderRule htmlRenderer cssRenderer rule
renderStyleSheet htmlRenderer cssRenderer (ruleCons rule rest@(ruleCons _ _)) =
  renderRule htmlRenderer cssRenderer rule ++
  "\n" ++
  renderStyleSheet htmlRenderer cssRenderer rest

mapDeclarations :
  {property value property' value' : Level}
  {From : CSS.Spec property value}
  {To : CSS.Spec property' value'} ->
  CSS.Map From To ->
  List (CSS.Declaration From) ->
  List (CSS.Declaration To)
mapDeclarations f [] = []
mapDeclarations f (declaration ∷ rest) =
  CSS.mapDeclaration f declaration ∷ mapDeclarations f rest

mapRule :
  {tag key val atom tag' key' val' atom' property value property' value' : Level}
  {HtmlFrom : HTML.Spec tag key val atom}
  {HtmlTo : HTML.Spec tag' key' val' atom'}
  {CssFrom : CSS.Spec property value}
  {CssTo : CSS.Spec property' value'} ->
  HTML.Map HtmlFrom HtmlTo ->
  CSS.Map CssFrom CssTo ->
  StyleRule HtmlFrom CssFrom ->
  StyleRule HtmlTo CssTo
mapRule htmlMap cssMap (styleRule selectors declarations) =
  styleRule
    (Selector.mapSelectorList htmlMap selectors)
    (mapDeclarations cssMap declarations)

mapStyleSheet :
  {tag key val atom tag' key' val' atom' property value property' value' : Level}
  {HtmlFrom : HTML.Spec tag key val atom}
  {HtmlTo : HTML.Spec tag' key' val' atom'}
  {CssFrom : CSS.Spec property value}
  {CssTo : CSS.Spec property' value'} ->
  HTML.Map HtmlFrom HtmlTo ->
  CSS.Map CssFrom CssTo ->
  StyleSheet HtmlFrom CssFrom ->
  StyleSheet HtmlTo CssTo
mapStyleSheet htmlMap cssMap emptySheet = emptySheet
mapStyleSheet htmlMap cssMap (ruleCons rule rest) =
  ruleCons
    (mapRule htmlMap cssMap rule)
    (mapStyleSheet htmlMap cssMap rest)

record Specificity : Type where
  constructor specificity
  field
    idCount : ℕ
    classCount : ℕ
    typeCount : ℕ

open Specificity public

zeroSpecificity : Specificity
zeroSpecificity = specificity zero zero zero

idSpecificity : Specificity
idSpecificity = specificity (suc zero) zero zero

classSpecificity : Specificity
classSpecificity = specificity zero (suc zero) zero

typeSpecificity : Specificity
typeSpecificity = specificity zero zero (suc zero)

_+specificity_ : Specificity -> Specificity -> Specificity
specificity ids classes types +specificity specificity ids' classes' types' =
  specificity (ids + ids') (classes + classes') (types + types')

untaggedSimpleSpecificity :
  {tag key val atom : Level}
  {H : HTML.Spec tag key val atom} ->
  Selector.UntypedSimple H ->
  Specificity
untaggedSimpleSpecificity (Selector.rawId _) = idSpecificity
untaggedSimpleSpecificity (Selector.rawClass _) = classSpecificity
untaggedSimpleSpecificity (Selector.rawAttribute _ _) = classSpecificity
untaggedSimpleSpecificity (Selector.rawPseudoClass _) = classSpecificity
untaggedSimpleSpecificity (Selector.rawFunctionalPseudoClass _ _) = classSpecificity

typedSimpleSpecificity :
  {tag key val atom : Level}
  {H : HTML.Spec tag key val atom}
  {tagName : HTML.Tag H} ->
  Selector.TypedSimple H tagName ->
  Specificity
typedSimpleSpecificity (Selector.id _) = idSpecificity
typedSimpleSpecificity (Selector.class _) = classSpecificity
typedSimpleSpecificity (Selector.attribute _ _) = classSpecificity
typedSimpleSpecificity (Selector.pseudoClass _) = classSpecificity
typedSimpleSpecificity (Selector.functionalPseudoClass _ _) = classSpecificity

untaggedSimplesSpecificity :
  {tag key val atom : Level}
  {H : HTML.Spec tag key val atom} ->
  List (Selector.UntypedSimple H) ->
  Specificity
untaggedSimplesSpecificity [] = zeroSpecificity
untaggedSimplesSpecificity (simple ∷ rest) =
  untaggedSimpleSpecificity simple +specificity
  untaggedSimplesSpecificity rest

typedSimplesSpecificity :
  {tag key val atom : Level}
  {H : HTML.Spec tag key val atom}
  {tagName : HTML.Tag H} ->
  List (Selector.TypedSimple H tagName) ->
  Specificity
typedSimplesSpecificity [] = zeroSpecificity
typedSimplesSpecificity (simple ∷ rest) =
  typedSimpleSpecificity simple +specificity
  typedSimplesSpecificity rest

compoundSpecificity :
  {tag key val atom : Level}
  {H : HTML.Spec tag key val atom} ->
  Selector.CompoundSelector H ->
  Specificity
compoundSpecificity (Selector.universal simples) =
  untaggedSimplesSpecificity simples
compoundSpecificity (Selector.typed _ simples) =
  typeSpecificity +specificity typedSimplesSpecificity simples

complexSpecificity :
  {tag key val atom : Level}
  {H : HTML.Spec tag key val atom} ->
  Selector.ComplexSelector H ->
  Specificity
complexSpecificity (Selector.compound selector) =
  compoundSpecificity selector
complexSpecificity (Selector.combine left _ right) =
  complexSpecificity left +specificity compoundSpecificity right

selectorListSpecificities :
  {tag key val atom : Level}
  {H : HTML.Spec tag key val atom} ->
  Selector.SelectorList H ->
  List Specificity
selectorListSpecificities (Selector.one selector) =
  complexSpecificity selector ∷ []
selectorListSpecificities (Selector.cons selector rest) =
  complexSpecificity selector ∷ selectorListSpecificities rest

matchingSelectorSpecificities :
  {tag key val atom : Level}
  {H : HTML.Spec tag key val atom} ->
  SelectorSemantics.SelectorMatcher H ->
  SelectorSemantics.ElementContext H ->
  Selector.SelectorList H ->
  List Specificity
matchingSelectorSpecificities matcher context (Selector.one selector) =
  if SelectorSemantics.matchesComplex matcher context selector
    then complexSpecificity selector ∷ []
    else []
matchingSelectorSpecificities matcher context (Selector.cons selector rest) =
  if SelectorSemantics.matchesComplex matcher context selector
    then complexSpecificity selector ∷
         matchingSelectorSpecificities matcher context rest
    else matchingSelectorSpecificities matcher context rest

data MatchedRule
  {tag key val atom property value : Level}
  (H : HTML.Spec tag key val atom)
  (C : CSS.Spec property value)
  : Type (levelOf tag key val atom property value) where
  matchedRule :
    ℕ ->
    SelectorSemantics.ElementContext H ->
    List Specificity ->
    List (CSS.Declaration C) ->
    MatchedRule H C

matchingRulesForContextFrom :
  {tag key val atom property value : Level}
  {H : HTML.Spec tag key val atom}
  {C : CSS.Spec property value} ->
  ℕ ->
  SelectorSemantics.SelectorMatcher H ->
  SelectorSemantics.ElementContext H ->
  StyleSheet H C ->
  List (MatchedRule H C)
matchingRulesForContextFrom order matcher context emptySheet = []
matchingRulesForContextFrom order matcher context (ruleCons (styleRule selectors declarations) rest)
  with matchingSelectorSpecificities matcher context selectors
... | [] = matchingRulesForContextFrom (suc order) matcher context rest
... | firstSpecificity ∷ restSpecificities =
  matchedRule order context (firstSpecificity ∷ restSpecificities) declarations ∷
  matchingRulesForContextFrom (suc order) matcher context rest

matchingRulesForContext :
  {tag key val atom property value : Level}
  {H : HTML.Spec tag key val atom}
  {C : CSS.Spec property value} ->
  SelectorSemantics.SelectorMatcher H ->
  SelectorSemantics.ElementContext H ->
  StyleSheet H C ->
  List (MatchedRule H C)
matchingRulesForContext = matchingRulesForContextFrom zero

declarationsForContext :
  {tag key val atom property value : Level}
  {H : HTML.Spec tag key val atom}
  {C : CSS.Spec property value} ->
  SelectorSemantics.SelectorMatcher H ->
  SelectorSemantics.ElementContext H ->
  StyleSheet H C ->
  List (CSS.Declaration C)
declarationsForContext matcher context emptySheet = []
declarationsForContext matcher context (ruleCons (styleRule selectors declarations) rest)
  with matchingSelectorSpecificities matcher context selectors
... | [] = declarationsForContext matcher context rest
... | _ ∷ _ = declarations ++L declarationsForContext matcher context rest

mutual
  matchingStyleSheetWithContext :
    {tag key val atom property value : Level}
    {H : HTML.Spec tag key val atom}
    {C : CSS.Spec property value} ->
    SelectorSemantics.SelectorMatcher H ->
    StyleSheet H C ->
    SelectorSemantics.ElementContext H ->
    HTML.Html H ->
    List (MatchedRule H C)
  matchingStyleSheetWithContext matcher sheet context (HTML.atomic _) = []
  matchingStyleSheetWithContext matcher sheet context (HTML.node _ _ children) =
    matchingRulesForContext matcher context sheet ++L
    matchingStyleSheetChildren matcher sheet context [] children

  matchingStyleSheetChildren :
    {tag key val atom property value : Level}
    {H : HTML.Spec tag key val atom}
    {C : CSS.Spec property value} ->
    SelectorSemantics.SelectorMatcher H ->
    StyleSheet H C ->
    SelectorSemantics.ElementContext H ->
    List (HTML.Html H) ->
    List (HTML.Html H) ->
    List (MatchedRule H C)
  matchingStyleSheetChildren matcher sheet parent previous [] = []
  matchingStyleSheetChildren matcher sheet parent previous (HTML.atomic content ∷ rest) =
    matchingStyleSheetChildren matcher sheet parent (HTML.atomic content ∷ previous) rest
  matchingStyleSheetChildren matcher sheet parent previous
    (HTML.node tagName attrs children ∷ rest) =
    matchingStyleSheetWithContext matcher sheet
      (SelectorSemantics.childContext parent previous tagName attrs children rest)
      (HTML.node tagName attrs children)
    ++L
    matchingStyleSheetChildren matcher sheet parent
      (HTML.node tagName attrs children ∷ previous)
      rest

matchingStyleSheet :
  {tag key val atom property value : Level}
  {H : HTML.Spec tag key val atom}
  {C : CSS.Spec property value} ->
  SelectorSemantics.SelectorMatcher H ->
  StyleSheet H C ->
  HTML.Html H ->
  List (MatchedRule H C)
matchingStyleSheet matcher sheet (HTML.atomic _) = []
matchingStyleSheet matcher sheet (HTML.node tagName attrs children) =
  matchingStyleSheetWithContext matcher sheet
    (SelectorSemantics.rootContext tagName attrs children)
    (HTML.node tagName attrs children)

data ElementStyle
  {tag key val atom property value : Level}
  (H : HTML.Spec tag key val atom)
  (C : CSS.Spec property value)
  : Type (levelOf tag key val atom property value) where
  elementStyle :
    SelectorSemantics.ElementContext H ->
    List (CSS.Declaration C) ->
    ElementStyle H C

mutual
  styledElementsWithContext :
    {tag key val atom property value : Level}
    {H : HTML.Spec tag key val atom}
    {C : CSS.Spec property value} ->
    SelectorSemantics.SelectorMatcher H ->
    StyleSheet H C ->
    SelectorSemantics.ElementContext H ->
    HTML.Html H ->
    List (ElementStyle H C)
  styledElementsWithContext matcher sheet context (HTML.atomic _) = []
  styledElementsWithContext matcher sheet context (HTML.node _ _ children)
    with declarationsForContext matcher context sheet
  ... | [] = styledElementChildren matcher sheet context [] children
  ... | declaration ∷ declarations =
    elementStyle context (declaration ∷ declarations) ∷
    styledElementChildren matcher sheet context [] children

  styledElementChildren :
    {tag key val atom property value : Level}
    {H : HTML.Spec tag key val atom}
    {C : CSS.Spec property value} ->
    SelectorSemantics.SelectorMatcher H ->
    StyleSheet H C ->
    SelectorSemantics.ElementContext H ->
    List (HTML.Html H) ->
    List (HTML.Html H) ->
    List (ElementStyle H C)
  styledElementChildren matcher sheet parent previous [] = []
  styledElementChildren matcher sheet parent previous (HTML.atomic content ∷ rest) =
    styledElementChildren matcher sheet parent (HTML.atomic content ∷ previous) rest
  styledElementChildren matcher sheet parent previous
    (HTML.node tagName attrs children ∷ rest) =
    styledElementsWithContext matcher sheet
      (SelectorSemantics.childContext parent previous tagName attrs children rest)
      (HTML.node tagName attrs children)
    ++L
    styledElementChildren matcher sheet parent
      (HTML.node tagName attrs children ∷ previous)
      rest

styledElements :
  {tag key val atom property value : Level}
  {H : HTML.Spec tag key val atom}
  {C : CSS.Spec property value} ->
  SelectorSemantics.SelectorMatcher H ->
  StyleSheet H C ->
  HTML.Html H ->
  List (ElementStyle H C)
styledElements matcher sheet (HTML.atomic _) = []
styledElements matcher sheet (HTML.node tagName attrs children) =
  styledElementsWithContext matcher sheet
    (SelectorSemantics.rootContext tagName attrs children)
    (HTML.node tagName attrs children)