module FF.HTML.Selector.Semantics where

open import Agda.Builtin.String using (String; primStringEquality)
open import Agda.Primitive using (Level; lzero; lsuc) renaming (Set to Type; _⊔_ to _lmax_)
open import Cubical.Data.Bool.Base
  using (Bool; true; false; not; _and_; _or_; if_then_else_)
open import Cubical.Data.List.Base
  using (List; []; _∷_; _++_)
open import Cubical.Data.Maybe.Base
  using (Maybe; nothing; just)

open import FF.HTML.Core
open import FF.HTML.Render using (Renderer)
open import FF.HTML.Selector.Core
  using
    ( MatchCase; documentCase
    ; AttributeOperator; exact; includes; dashMatch; prefix; suffix; substring
    ; RawAttributeTest; rawPresent; rawMatch
    ; AttributeTest; present; matchValue; matchString
    ; UntypedSimple; rawId; rawClass; rawAttribute; rawPseudoClass; rawFunctionalPseudoClass
    ; TypedSimple; id; class; attribute; pseudoClass; functionalPseudoClass
    ; CompoundSelector; universal; typed
    ; Combinator; descendant; child; nextSibling; subsequentSibling
    ; ComplexSelector; compound; combine
    ; SelectorList; one; cons
    )

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

record TextDeciders : Type lzero where
  field
    sameText : String -> String -> Bool
    matchText : AttributeOperator -> String -> MatchCase -> String -> Bool
    hasToken : String -> String -> Bool

open TextDeciders public

-- Useful for tests and examples. Operators beyond exact equality need a real
-- string/token implementation supplied by the caller.
exactOnlyTextDeciders : TextDeciders
exactOnlyTextDeciders =
  record
    { sameText = primStringEquality
    ; matchText = match
    ; hasToken = primStringEquality
    }
  where
    match : AttributeOperator -> String -> MatchCase -> String -> Bool
    match exact expected _ actual = primStringEquality expected actual
    match includes _ _ _ = false
    match dashMatch _ _ _ = false
    match prefix _ _ _ = false
    match suffix _ _ _ = false
    match substring _ _ _ = false

data ElementContext
  {tag key val atom : Level}
  (S : Spec tag key val atom)
  : Type (levelOf tag key val atom) where
  rootContext :
    (tagName : Tag S) ->
    List (Attribute S tagName) ->
    List (Html S) ->
    ElementContext S
  childContext :
    ElementContext S ->
    List (Html S) ->
    (tagName : Tag S) ->
    List (Attribute S tagName) ->
    List (Html S) ->
    List (Html S) ->
    ElementContext S

contextTag :
  {tag key val atom : Level}
  {S : Spec tag key val atom} ->
  ElementContext S ->
  Tag S
contextTag (rootContext tagName _ _) = tagName
contextTag (childContext _ _ tagName _ _ _) = tagName

contextAttrs :
  {tag key val atom : Level}
  {S : Spec tag key val atom} ->
  (context : ElementContext S) ->
  List (Attribute S (contextTag context))
contextAttrs (rootContext _ attrs _) = attrs
contextAttrs (childContext _ _ _ attrs _ _) = attrs

contextChildren :
  {tag key val atom : Level}
  {S : Spec tag key val atom} ->
  ElementContext S ->
  List (Html S)
contextChildren (rootContext _ _ children) = children
contextChildren (childContext _ _ _ _ children _) = children

contextHtml :
  {tag key val atom : Level}
  {S : Spec tag key val atom} ->
  ElementContext S ->
  Html S
contextHtml (rootContext tagName attrs children) = node tagName attrs children
contextHtml (childContext _ _ tagName attrs children _) = node tagName attrs children

containsElement :
  {tag key val atom : Level}
  {S : Spec tag key val atom} ->
  List (Html S) ->
  Bool
containsElement [] = false
containsElement (atomic _ ∷ rest) = containsElement rest
containsElement (node _ _ _ ∷ _) = true

isRootContext :
  {tag key val atom : Level}
  {S : Spec tag key val atom} ->
  ElementContext S ->
  Bool
isRootContext (rootContext _ _ _) = true
isRootContext (childContext _ _ _ _ _ _) = false

isFirstChild :
  {tag key val atom : Level}
  {S : Spec tag key val atom} ->
  ElementContext S ->
  Bool
isFirstChild (rootContext _ _ _) = false
isFirstChild (childContext _ previous _ _ _ _) = not (containsElement previous)

isLastChild :
  {tag key val atom : Level}
  {S : Spec tag key val atom} ->
  ElementContext S ->
  Bool
isLastChild (rootContext _ _ _) = false
isLastChild (childContext _ _ _ _ _ next) = not (containsElement next)

isOnlyChild :
  {tag key val atom : Level}
  {S : Spec tag key val atom} ->
  ElementContext S ->
  Bool
isOnlyChild context = isFirstChild context and isLastChild context

hasNoChildren :
  {tag key val atom : Level}
  {S : Spec tag key val atom} ->
  ElementContext S ->
  Bool
hasNoChildren context with contextChildren context
... | [] = true
... | _ ∷ _ = false

-- Static pseudo-classes whose meaning only depends on this HTML tree.
-- :root is the root of the supplied Html value; :empty means no children.
structuralPseudoClassMatches :
  {tag key val atom : Level}
  {S : Spec tag key val atom} ->
  TextDeciders ->
  ElementContext S ->
  String ->
  Bool
structuralPseudoClassMatches text context name =
  if sameText text name "root" then isRootContext context else
  if sameText text name "first-child" then isFirstChild context else
  if sameText text name "last-child" then isLastChild context else
  if sameText text name "only-child" then isOnlyChild context else
  if sameText text name "empty" then hasNoChildren context else
  false

record SelectorMatcher
  {tag key val atom : Level}
  (S : Spec tag key val atom)
  : Type (lsuc (levelOf tag key val atom)) where
  field
    renderer : Renderer S
    textDeciders : TextDeciders

    tagMatches : Tag S -> Tag S -> Bool
    keyMatches :
      {selectorTag actualTag : Tag S} ->
      AttrKey S selectorTag ->
      AttrKey S actualTag ->
      Bool
    rawKeyMatches :
      {actualTag : Tag S} ->
      String ->
      AttrKey S actualTag ->
      Bool
    typedValueMatches :
      {selectorTag actualTag : Tag S} ->
      (selectorKey : AttrKey S selectorTag) ->
      (actualKey : AttrKey S actualTag) ->
      AttributeOperator ->
      AttrValue S selectorKey ->
      MatchCase ->
      AttrValue S actualKey ->
      Bool
    rawValueMatches :
      {actualTag : Tag S} ->
      (actualKey : AttrKey S actualTag) ->
      AttributeOperator ->
      String ->
      MatchCase ->
      AttrValue S actualKey ->
      Bool

    isIdKey : {actualTag : Tag S} -> AttrKey S actualTag -> Bool
    isClassKey : {actualTag : Tag S} -> AttrKey S actualTag -> Bool

    pseudoClassMatches : ElementContext S -> String -> Bool
    functionalPseudoClassMatches : ElementContext S -> String -> String -> Bool

open SelectorMatcher public

matcherFromRenderer :
  {tag key val atom : Level}
  {S : Spec tag key val atom} ->
  Renderer S ->
  TextDeciders ->
  ({tagName : Tag S} -> AttrKey S tagName -> Bool) ->
  ({tagName : Tag S} -> AttrKey S tagName -> Bool) ->
  (ElementContext S -> String -> Bool) ->
  (ElementContext S -> String -> String -> Bool) ->
  SelectorMatcher S
matcherFromRenderer renderer text idKey classKey extraPseudo extraFunctional =
  record
    { renderer = renderer
    ; textDeciders = text
    ; tagMatches = \ left right ->
        sameText text (Renderer.renderTag renderer left) (Renderer.renderTag renderer right)
    ; keyMatches = \ left right ->
        sameText text (Renderer.renderKey renderer left) (Renderer.renderKey renderer right)
    ; rawKeyMatches = \ raw actual ->
        sameText text raw (Renderer.renderKey renderer actual)
    ; typedValueMatches = \ selectorKey actualKey operator expected matchCase actual ->
        matchText text operator
          (Renderer.renderValue renderer selectorKey expected)
          matchCase
          (Renderer.renderValue renderer actualKey actual)
    ; rawValueMatches = \ actualKey operator expected matchCase actual ->
        matchText text operator expected matchCase
          (Renderer.renderValue renderer actualKey actual)
    ; isIdKey = idKey
    ; isClassKey = classKey
    ; pseudoClassMatches = \ context name ->
        structuralPseudoClassMatches text context name or extraPseudo context name
    ; functionalPseudoClassMatches = extraFunctional
    }

renderedValueMatches :
  {tag key val atom : Level}
  {S : Spec tag key val atom} ->
  SelectorMatcher S ->
  AttributeOperator ->
  String ->
  MatchCase ->
  String ->
  Bool
renderedValueMatches matcher operator expected matchCase actual =
  matchText (textDeciders matcher) operator expected matchCase actual

rawAttributeTestMatches :
  {tag key val atom : Level}
  {S : Spec tag key val atom}
  (matcher : SelectorMatcher S) ->
  {actualTag : Tag S} ->
  (actualKey : AttrKey S actualTag) ->
  AttrValue S actualKey ->
  RawAttributeTest ->
  Bool
rawAttributeTestMatches matcher actualKey actualValue rawPresent = true
rawAttributeTestMatches matcher actualKey actualValue (rawMatch operator expected matchCase) =
  rawValueMatches matcher actualKey operator expected matchCase actualValue

attributeTestMatches :
  {tag key val atom : Level}
  {S : Spec tag key val atom}
  (matcher : SelectorMatcher S) ->
  {selectorTag actualTag : Tag S} ->
  (selectorKey : AttrKey S selectorTag) ->
  (actualKey : AttrKey S actualTag) ->
  AttrValue S actualKey ->
  AttributeTest S selectorKey ->
  Bool
attributeTestMatches matcher selectorKey actualKey actualValue present = true
attributeTestMatches matcher selectorKey actualKey actualValue
  (matchValue operator expected matchCase) =
  typedValueMatches matcher selectorKey actualKey operator expected matchCase actualValue
attributeTestMatches matcher selectorKey actualKey actualValue
  (matchString operator expected matchCase) =
  rawValueMatches matcher actualKey operator expected matchCase actualValue

rawAttributeMatches :
  {tag key val atom : Level}
  {S : Spec tag key val atom}
  (matcher : SelectorMatcher S) ->
  {actualTag : Tag S} ->
  String ->
  RawAttributeTest ->
  List (Attribute S actualTag) ->
  Bool
rawAttributeMatches matcher rawName test [] = false
rawAttributeMatches matcher rawName test (attr actualKey actualValue ∷ rest) =
  (rawKeyMatches matcher rawName actualKey and
   rawAttributeTestMatches matcher actualKey actualValue test)
  or rawAttributeMatches matcher rawName test rest

typedAttributeMatches :
  {tag key val atom : Level}
  {S : Spec tag key val atom}
  (matcher : SelectorMatcher S) ->
  {selectorTag actualTag : Tag S} ->
  (selectorKey : AttrKey S selectorTag) ->
  AttributeTest S selectorKey ->
  List (Attribute S actualTag) ->
  Bool
typedAttributeMatches matcher selectorKey test [] = false
typedAttributeMatches matcher selectorKey test (attr actualKey actualValue ∷ rest) =
  (keyMatches matcher selectorKey actualKey and
   attributeTestMatches matcher selectorKey actualKey actualValue test)
  or typedAttributeMatches matcher selectorKey test rest

idMatches :
  {tag key val atom : Level}
  {S : Spec tag key val atom}
  (matcher : SelectorMatcher S) ->
  {actualTag : Tag S} ->
  String ->
  List (Attribute S actualTag) ->
  Bool
idMatches matcher expected [] = false
idMatches matcher expected (attr actualKey actualValue ∷ rest) =
  (isIdKey matcher actualKey and
   renderedValueMatches matcher exact expected documentCase
     (Renderer.renderValue (renderer matcher) actualKey actualValue))
  or idMatches matcher expected rest

classMatches :
  {tag key val atom : Level}
  {S : Spec tag key val atom}
  (matcher : SelectorMatcher S) ->
  {actualTag : Tag S} ->
  String ->
  List (Attribute S actualTag) ->
  Bool
classMatches matcher expected [] = false
classMatches matcher expected (attr actualKey actualValue ∷ rest) =
  (isClassKey matcher actualKey and
   hasToken (textDeciders matcher) expected
     (Renderer.renderValue (renderer matcher) actualKey actualValue))
  or classMatches matcher expected rest

matchesUntypedSimple :
  {tag key val atom : Level}
  {S : Spec tag key val atom} ->
  SelectorMatcher S ->
  ElementContext S ->
  UntypedSimple S ->
  Bool
matchesUntypedSimple matcher context (rawId value) =
  idMatches matcher value (contextAttrs context)
matchesUntypedSimple matcher context (rawClass value) =
  classMatches matcher value (contextAttrs context)
matchesUntypedSimple matcher context (rawAttribute rawName test) =
  rawAttributeMatches matcher rawName test (contextAttrs context)
matchesUntypedSimple matcher context (rawPseudoClass name) =
  pseudoClassMatches matcher context name
matchesUntypedSimple matcher context (rawFunctionalPseudoClass name argument) =
  functionalPseudoClassMatches matcher context name argument

matchesUntypedSimples :
  {tag key val atom : Level}
  {S : Spec tag key val atom} ->
  SelectorMatcher S ->
  ElementContext S ->
  List (UntypedSimple S) ->
  Bool
matchesUntypedSimples matcher context [] = true
matchesUntypedSimples matcher context (simple ∷ rest) =
  matchesUntypedSimple matcher context simple and
  matchesUntypedSimples matcher context rest

matchesTypedSimple :
  {tag key val atom : Level}
  {S : Spec tag key val atom} ->
  SelectorMatcher S ->
  (context : ElementContext S) ->
  {selectorTag : Tag S} ->
  TypedSimple S selectorTag ->
  Bool
matchesTypedSimple matcher context (id value) =
  idMatches matcher value (contextAttrs context)
matchesTypedSimple matcher context (class value) =
  classMatches matcher value (contextAttrs context)
matchesTypedSimple matcher context (attribute selectorKey test) =
  typedAttributeMatches matcher selectorKey test (contextAttrs context)
matchesTypedSimple matcher context (pseudoClass name) =
  pseudoClassMatches matcher context name
matchesTypedSimple matcher context (functionalPseudoClass name argument) =
  functionalPseudoClassMatches matcher context name argument

matchesTypedSimples :
  {tag key val atom : Level}
  {S : Spec tag key val atom} ->
  SelectorMatcher S ->
  (context : ElementContext S) ->
  {selectorTag : Tag S} ->
  List (TypedSimple S selectorTag) ->
  Bool
matchesTypedSimples matcher context [] = true
matchesTypedSimples matcher context (simple ∷ rest) =
  matchesTypedSimple matcher context simple and
  matchesTypedSimples matcher context rest

matchesCompound :
  {tag key val atom : Level}
  {S : Spec tag key val atom} ->
  SelectorMatcher S ->
  ElementContext S ->
  CompoundSelector S ->
  Bool
matchesCompound matcher context (universal simples) =
  matchesUntypedSimples matcher context simples
matchesCompound matcher context (typed tagName simples) =
  tagMatches matcher tagName (contextTag context) and
  matchesTypedSimples matcher context simples

firstPreviousElementFrom :
  {tag key val atom : Level}
  {S : Spec tag key val atom} ->
  ElementContext S ->
  List (Html S) ->
  List (Html S) ->
  Maybe (ElementContext S)
firstPreviousElementFrom parent after [] = nothing
firstPreviousElementFrom parent after (atomic content ∷ rest) =
  firstPreviousElementFrom parent (atomic content ∷ after) rest
firstPreviousElementFrom parent after (node tagName attrs children ∷ rest) =
  just (childContext parent rest tagName attrs children after)

mutual
  matchesComplex :
    {tag key val atom : Level}
    {S : Spec tag key val atom} ->
    SelectorMatcher S ->
    ElementContext S ->
    ComplexSelector S ->
    Bool
  matchesComplex matcher context (compound selector) =
    matchesCompound matcher context selector
  matchesComplex matcher context (combine left combinator right) =
    matchesCompound matcher context right and
    matchesCombinator matcher context left combinator

  matchesCombinator :
    {tag key val atom : Level}
    {S : Spec tag key val atom} ->
    SelectorMatcher S ->
    ElementContext S ->
    ComplexSelector S ->
    Combinator ->
    Bool
  matchesCombinator matcher context left descendant =
    ancestorMatches matcher context left
  matchesCombinator matcher context left child =
    parentMatches matcher context left
  matchesCombinator matcher context left nextSibling =
    previousSiblingMatches matcher context left
  matchesCombinator matcher context left subsequentSibling =
    previousSiblingAnyMatches matcher context left

  parentMatches :
    {tag key val atom : Level}
    {S : Spec tag key val atom} ->
    SelectorMatcher S ->
    ElementContext S ->
    ComplexSelector S ->
    Bool
  parentMatches matcher (rootContext _ _ _) left = false
  parentMatches matcher (childContext parent _ _ _ _ _) left =
    matchesComplex matcher parent left

  ancestorMatches :
    {tag key val atom : Level}
    {S : Spec tag key val atom} ->
    SelectorMatcher S ->
    ElementContext S ->
    ComplexSelector S ->
    Bool
  ancestorMatches matcher (rootContext _ _ _) left = false
  ancestorMatches matcher (childContext parent _ _ _ _ _) left =
    matchesComplex matcher parent left or ancestorMatches matcher parent left

  previousSiblingMatches :
    {tag key val atom : Level}
    {S : Spec tag key val atom} ->
    SelectorMatcher S ->
    ElementContext S ->
    ComplexSelector S ->
    Bool
  previousSiblingMatches matcher (rootContext _ _ _) left = false
  previousSiblingMatches matcher context@(childContext parent previous tagName attrs children next) left
    with firstPreviousElementFrom parent (node tagName attrs children ∷ next) previous
  ... | nothing = false
  ... | just previousContext = matchesComplex matcher previousContext left

  previousSiblingAnyMatchesFrom :
    {tag key val atom : Level}
    {S : Spec tag key val atom} ->
    SelectorMatcher S ->
    ComplexSelector S ->
    ElementContext S ->
    List (Html S) ->
    List (Html S) ->
    Bool
  previousSiblingAnyMatchesFrom matcher left parent after [] = false
  previousSiblingAnyMatchesFrom matcher left parent after (atomic content ∷ rest) =
    previousSiblingAnyMatchesFrom matcher left parent (atomic content ∷ after) rest
  previousSiblingAnyMatchesFrom matcher left parent after (node tagName attrs children ∷ rest) =
    matchesComplex matcher (childContext parent rest tagName attrs children after) left
    or previousSiblingAnyMatchesFrom matcher left parent
      (node tagName attrs children ∷ after)
      rest

  previousSiblingAnyMatches :
    {tag key val atom : Level}
    {S : Spec tag key val atom} ->
    SelectorMatcher S ->
    ElementContext S ->
    ComplexSelector S ->
    Bool
  previousSiblingAnyMatches matcher (rootContext _ _ _) left = false
  previousSiblingAnyMatches matcher (childContext parent previous tagName attrs children next) left =
    previousSiblingAnyMatchesFrom matcher left parent
      (node tagName attrs children ∷ next)
      previous

matchesSelectorList :
  {tag key val atom : Level}
  {S : Spec tag key val atom} ->
  SelectorMatcher S ->
  ElementContext S ->
  SelectorList S ->
  Bool
matchesSelectorList matcher context (one selector) =
  matchesComplex matcher context selector
matchesSelectorList matcher context (cons selector rest) =
  matchesComplex matcher context selector or
  matchesSelectorList matcher context rest

mutual
  selectHtmlWithContext :
    {tag key val atom : Level}
    {S : Spec tag key val atom} ->
    SelectorMatcher S ->
    SelectorList S ->
    ElementContext S ->
    Html S ->
    List (ElementContext S)
  selectHtmlWithContext matcher selector context (atomic _) = []
  selectHtmlWithContext matcher selector context (node _ _ children) =
    if matchesSelectorList matcher context selector
      then context ∷ selectChildLoop matcher selector context [] children
      else selectChildLoop matcher selector context [] children

  selectFromContext :
    {tag key val atom : Level}
    {S : Spec tag key val atom} ->
    SelectorMatcher S ->
    SelectorList S ->
    ElementContext S ->
    List (ElementContext S)
  selectFromContext matcher selector context =
    selectHtmlWithContext matcher selector context (contextHtml context)

  selectChildLoop :
    {tag key val atom : Level}
    {S : Spec tag key val atom} ->
    SelectorMatcher S ->
    SelectorList S ->
    ElementContext S ->
    List (Html S) ->
    List (Html S) ->
    List (ElementContext S)
  selectChildLoop matcher selector parent previous [] = []
  selectChildLoop matcher selector parent previous (atomic content ∷ rest) =
    selectChildLoop matcher selector parent (atomic content ∷ previous) rest
  selectChildLoop matcher selector parent previous (node tagName attrs children ∷ rest) =
    selectHtmlWithContext matcher selector
      (childContext parent previous tagName attrs children rest)
      (node tagName attrs children)
    ++ selectChildLoop matcher selector parent
      (node tagName attrs children ∷ previous)
      rest

selectContexts :
  {tag key val atom : Level}
  {S : Spec tag key val atom} ->
  SelectorMatcher S ->
  SelectorList S ->
  Html S ->
  List (ElementContext S)
selectContexts matcher selector (atomic _) = []
selectContexts matcher selector (node tagName attrs children) =
  selectHtmlWithContext matcher selector
    (rootContext tagName attrs children)
    (node tagName attrs children)

contextHtmls :
  {tag key val atom : Level}
  {S : Spec tag key val atom} ->
  List (ElementContext S) ->
  List (Html S)
contextHtmls [] = []
contextHtmls (context ∷ rest) = contextHtml context ∷ contextHtmls rest

select :
  {tag key val atom : Level}
  {S : Spec tag key val atom} ->
  SelectorMatcher S ->
  SelectorList S ->
  Html S ->
  List (Html S)
select matcher selector html = contextHtmls (selectContexts matcher selector html)

matchesRoot :
  {tag key val atom : Level}
  {S : Spec tag key val atom} ->
  SelectorMatcher S ->
  SelectorList S ->
  Html S ->
  Bool
matchesRoot matcher selector (atomic _) = false
matchesRoot matcher selector (node tagName attrs children) =
  matchesSelectorList matcher (rootContext tagName attrs children) selector