module FF.HTML.Selector.Core where

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

open import FF.HTML.Core
open import FF.HTML.Render using (Renderer)

private
  infixr 5 _++_

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

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

-- Selectors Level 4: type/universal selectors, attribute selectors,
-- class/ID selectors, compound selectors, selector lists, and combinators.
-- https://www.w3.org/TR/selectors-4/

data MatchCase : Type lzero where
  documentCase asciiInsensitive caseSensitive : MatchCase

renderMatchCase : MatchCase -> String
renderMatchCase documentCase = ""
renderMatchCase asciiInsensitive = " i"
renderMatchCase caseSensitive = " s"

data AttributeOperator : Type lzero where
  exact includes dashMatch prefix suffix substring : AttributeOperator

renderAttributeOperator : AttributeOperator -> String
renderAttributeOperator exact = "="
renderAttributeOperator includes = "~="
renderAttributeOperator dashMatch = "|="
renderAttributeOperator prefix = "^="
renderAttributeOperator suffix = "$="
renderAttributeOperator substring = "*="

-- Raw attribute tests are needed for selectors that are valid CSS but cannot
-- be justified by an indexed AttrKey, such as a universal [href] in Safe HTML.
data RawAttributeTest : Type lzero where
  rawPresent : RawAttributeTest
  rawMatch : AttributeOperator -> String -> MatchCase -> RawAttributeTest

data AttributeTest
  {tag key val atom : Level}
  (S : Spec tag key val atom)
  {tagName : Tag S}
  (keyName : AttrKey S tagName)
  : Type val where
  present : AttributeTest S keyName
  matchValue : AttributeOperator -> AttrValue S keyName -> MatchCase -> AttributeTest S keyName
  matchString : AttributeOperator -> String -> MatchCase -> AttributeTest S keyName

data UntypedSimple
  {tag key val atom : Level}
  (S : Spec tag key val atom)
  : Type lzero where
  rawId : String -> UntypedSimple S
  rawClass : String -> UntypedSimple S
  rawAttribute : String -> RawAttributeTest -> UntypedSimple S
  rawPseudoClass : String -> UntypedSimple S
  rawFunctionalPseudoClass : String -> String -> UntypedSimple S

data TypedSimple
  {tag key val atom : Level}
  (S : Spec tag key val atom)
  (tagName : Tag S)
  : Type (key lmax val) where
  id : String -> TypedSimple S tagName
  class : String -> TypedSimple S tagName
  attribute : (keyName : AttrKey S tagName) -> AttributeTest S keyName -> TypedSimple S tagName
  pseudoClass : String -> TypedSimple S tagName
  functionalPseudoClass : String -> String -> TypedSimple S tagName

-- A typed compound with attributes needs a concrete subject tag, because
-- AttrKey is indexed by tag. Untyped compounds cover tag-independent CSS.
data CompoundSelector
  {tag key val atom : Level}
  (S : Spec tag key val atom)
  : Type (levelOf tag key val atom) where
  universal : List (UntypedSimple S) -> CompoundSelector S
  typed : (tagName : Tag S) -> List (TypedSimple S tagName) -> CompoundSelector S

data Combinator : Type lzero where
  descendant child nextSibling subsequentSibling : Combinator

data ComplexSelector
  {tag key val atom : Level}
  (S : Spec tag key val atom)
  : Type (levelOf tag key val atom) where
  compound : CompoundSelector S -> ComplexSelector S
  combine : ComplexSelector S -> Combinator -> CompoundSelector S -> ComplexSelector S

data SelectorList
  {tag key val atom : Level}
  (S : Spec tag key val atom)
  : Type (levelOf tag key val atom) where
  one : ComplexSelector S -> SelectorList S
  cons : ComplexSelector S -> SelectorList S -> SelectorList S

renderRawAttributeTest : RawAttributeTest -> String
renderRawAttributeTest rawPresent = ""
renderRawAttributeTest (rawMatch operator value matchCase) =
  renderAttributeOperator operator ++ "\"" ++ value ++ "\"" ++ renderMatchCase matchCase

renderAttributeTest :
  {tag key val atom : Level}
  {S : Spec tag key val atom}
  (renderer : Renderer S) ->
  {tagName : Tag S} ->
  (keyName : AttrKey S tagName) ->
  AttributeTest S keyName ->
  String
renderAttributeTest renderer keyName present = ""
renderAttributeTest renderer keyName (matchValue operator value matchCase) =
  renderAttributeOperator operator ++ "\"" ++
  Renderer.renderValue renderer keyName value ++ "\"" ++
  renderMatchCase matchCase
renderAttributeTest renderer keyName (matchString operator value matchCase) =
  renderAttributeOperator operator ++ "\"" ++ value ++ "\"" ++ renderMatchCase matchCase

renderUntypedSimple :
  {tag key val atom : Level}
  {S : Spec tag key val atom} ->
  UntypedSimple S ->
  String
renderUntypedSimple (rawId value) = "#" ++ value
renderUntypedSimple (rawClass value) = "." ++ value
renderUntypedSimple (rawAttribute keyName test) =
  "[" ++ keyName ++ renderRawAttributeTest test ++ "]"
renderUntypedSimple (rawPseudoClass name) = ":" ++ name
renderUntypedSimple (rawFunctionalPseudoClass name argument) =
  ":" ++ name ++ "(" ++ argument ++ ")"

renderUntypedSimples :
  {tag key val atom : Level}
  {S : Spec tag key val atom} ->
  List (UntypedSimple S) ->
  String
renderUntypedSimples [] = ""
renderUntypedSimples (simple ∷ rest) =
  renderUntypedSimple simple ++ renderUntypedSimples rest

renderTypedSimple :
  {tag key val atom : Level}
  {S : Spec tag key val atom}
  (renderer : Renderer S) ->
  {tagName : Tag S} ->
  TypedSimple S tagName ->
  String
renderTypedSimple renderer (id value) = "#" ++ value
renderTypedSimple renderer (class value) = "." ++ value
renderTypedSimple renderer (attribute keyName test) =
  "[" ++ Renderer.renderKey renderer keyName ++
  renderAttributeTest renderer keyName test ++ "]"
renderTypedSimple renderer (pseudoClass name) = ":" ++ name
renderTypedSimple renderer (functionalPseudoClass name argument) =
  ":" ++ name ++ "(" ++ argument ++ ")"

renderTypedSimples :
  {tag key val atom : Level}
  {S : Spec tag key val atom}
  (renderer : Renderer S) ->
  {tagName : Tag S} ->
  List (TypedSimple S tagName) ->
  String
renderTypedSimples renderer [] = ""
renderTypedSimples renderer (simple ∷ rest) =
  renderTypedSimple renderer simple ++ renderTypedSimples renderer rest

renderCompound :
  {tag key val atom : Level}
  {S : Spec tag key val atom} ->
  Renderer S ->
  CompoundSelector S ->
  String
renderCompound renderer (universal []) = "*"
renderCompound renderer (universal simples) = renderUntypedSimples simples
renderCompound renderer (typed tagName simples) =
  Renderer.renderTag renderer tagName ++ renderTypedSimples renderer simples

renderCombinator : Combinator -> String
renderCombinator descendant = " "
renderCombinator child = " > "
renderCombinator nextSibling = " + "
renderCombinator subsequentSibling = " ~ "

renderComplex :
  {tag key val atom : Level}
  {S : Spec tag key val atom} ->
  Renderer S ->
  ComplexSelector S ->
  String
renderComplex renderer (compound selector) = renderCompound renderer selector
renderComplex renderer (combine left combinator right) =
  renderComplex renderer left ++ renderCombinator combinator ++ renderCompound renderer right

renderSelectorList :
  {tag key val atom : Level}
  {S : Spec tag key val atom} ->
  Renderer S ->
  SelectorList S ->
  String
renderSelectorList renderer (one selector) = renderComplex renderer selector
renderSelectorList renderer (cons selector rest) =
  renderComplex renderer selector ++ ", " ++ renderSelectorList renderer rest

mapAttributeTest :
  {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} ->
  (keyName : AttrKey From tagName) ->
  AttributeTest From keyName ->
  AttributeTest To (Map.mapKey f keyName)
mapAttributeTest f keyName present = present
mapAttributeTest f keyName (matchValue operator value matchCase) =
  matchValue operator (Map.mapValue f keyName value) matchCase
mapAttributeTest f keyName (matchString operator value matchCase) =
  matchString operator value matchCase

mapUntypedSimple :
  {tag key val atom tag' key' val' atom' : Level}
  {From : Spec tag key val atom}
  {To : Spec tag' key' val' atom'} ->
  UntypedSimple From ->
  UntypedSimple To
mapUntypedSimple (rawId value) = rawId value
mapUntypedSimple (rawClass value) = rawClass value
mapUntypedSimple (rawAttribute keyName test) = rawAttribute keyName test
mapUntypedSimple (rawPseudoClass name) = rawPseudoClass name
mapUntypedSimple (rawFunctionalPseudoClass name argument) =
  rawFunctionalPseudoClass name argument

mapUntypedSimples :
  {tag key val atom tag' key' val' atom' : Level}
  {From : Spec tag key val atom}
  {To : Spec tag' key' val' atom'} ->
  List (UntypedSimple From) ->
  List (UntypedSimple To)
mapUntypedSimples [] = []
mapUntypedSimples (simple ∷ rest) =
  mapUntypedSimple simple ∷ mapUntypedSimples rest

mapTypedSimple :
  {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} ->
  TypedSimple From tagName ->
  TypedSimple To (Map.mapTag f tagName)
mapTypedSimple f (id value) = id value
mapTypedSimple f (class value) = class value
mapTypedSimple f (attribute keyName test) =
  attribute (Map.mapKey f keyName) (mapAttributeTest f keyName test)
mapTypedSimple f (pseudoClass name) = pseudoClass name
mapTypedSimple f (functionalPseudoClass name argument) =
  functionalPseudoClass name argument

mapTypedSimples :
  {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 (TypedSimple From tagName) ->
  List (TypedSimple To (Map.mapTag f tagName))
mapTypedSimples f [] = []
mapTypedSimples f (simple ∷ rest) =
  mapTypedSimple f simple ∷ mapTypedSimples f rest

mapCompound :
  {tag key val atom tag' key' val' atom' : Level}
  {From : Spec tag key val atom}
  {To : Spec tag' key' val' atom'} ->
  Map From To ->
  CompoundSelector From ->
  CompoundSelector To
mapCompound f (universal simples) = universal (mapUntypedSimples simples)
mapCompound f (typed tagName simples) =
  typed (Map.mapTag f tagName) (mapTypedSimples f simples)

mapComplex :
  {tag key val atom tag' key' val' atom' : Level}
  {From : Spec tag key val atom}
  {To : Spec tag' key' val' atom'} ->
  Map From To ->
  ComplexSelector From ->
  ComplexSelector To
mapComplex f (compound selector) = compound (mapCompound f selector)
mapComplex f (combine left combinator right) =
  combine (mapComplex f left) combinator (mapCompound f right)

mapSelectorList :
  {tag key val atom tag' key' val' atom' : Level}
  {From : Spec tag key val atom}
  {To : Spec tag' key' val' atom'} ->
  Map From To ->
  SelectorList From ->
  SelectorList To
mapSelectorList f (one selector) = one (mapComplex f selector)
mapSelectorList f (cons selector rest) =
  cons (mapComplex f selector) (mapSelectorList f rest)