module FF.HTML.Spec.Safe.Selector where

open import Agda.Builtin.String using (String)
open import Cubical.Data.Bool.Base using (Bool; true; false)
open import Cubical.Data.List.Base using (List; [])

import FF.HTML.Selector.Core as Selector
import FF.HTML.Selector.Semantics as Semantics
import FF.HTML.Spec.Safe as Safe

CompoundT : _
CompoundT = Selector.CompoundSelector Safe.spec

ComplexT : _
ComplexT = Selector.ComplexSelector Safe.spec

SelectorT : _
SelectorT = Selector.SelectorList Safe.spec

TypedSimpleT : Safe.TagName -> _
TypedSimpleT tagName = Selector.TypedSimple Safe.spec tagName

UntypedSimpleT : _
UntypedSimpleT = Selector.UntypedSimple Safe.spec

AttributeTestT : {tagName : Safe.TagName} -> Safe.AttributeKey tagName -> _
AttributeTestT keyName = Selector.AttributeTest Safe.spec keyName

any : CompoundT
any = Selector.universal []

tag : Safe.TagName -> CompoundT
tag tagName = Selector.typed tagName []

tagWith : (tagName : Safe.TagName) -> List (TypedSimpleT tagName) -> CompoundT
tagWith = Selector.typed

typedId : {tagName : Safe.TagName} -> String -> TypedSimpleT tagName
typedId = Selector.id

typedClass : {tagName : Safe.TagName} -> String -> TypedSimpleT tagName
typedClass = Selector.class

typedPseudo : {tagName : Safe.TagName} -> String -> TypedSimpleT tagName
typedPseudo = Selector.pseudoClass

typedFunctionalPseudo :
  {tagName : Safe.TagName} ->
  String ->
  String ->
  TypedSimpleT tagName
typedFunctionalPseudo = Selector.functionalPseudoClass

attrPresent :
  {tagName : Safe.TagName} ->
  (keyName : Safe.AttributeKey tagName) ->
  TypedSimpleT tagName
attrPresent keyName = Selector.attribute keyName Selector.present

attrMatches :
  {tagName : Safe.TagName} ->
  (keyName : Safe.AttributeKey tagName) ->
  AttributeTestT keyName ->
  TypedSimpleT tagName
attrMatches = Selector.attribute

attrValueEquals :
  {tagName : Safe.TagName} ->
  (keyName : Safe.AttributeKey tagName) ->
  Safe.AttributeValue keyName ->
  TypedSimpleT tagName
attrValueEquals keyName value =
  Selector.attribute keyName
    (Selector.matchValue Selector.exact value Selector.documentCase)

attrStringEquals :
  {tagName : Safe.TagName} ->
  (keyName : Safe.AttributeKey tagName) ->
  String ->
  TypedSimpleT tagName
attrStringEquals keyName value =
  Selector.attribute keyName
    (Selector.matchString Selector.exact value Selector.documentCase)

dataAttrEquals :
  {tagName : Safe.TagName} ->
  String ->
  String ->
  TypedSimpleT tagName
dataAttrEquals name value = attrStringEquals (Safe.dataAttr name) value

rawId : String -> UntypedSimpleT
rawId = Selector.rawId

rawClass : String -> UntypedSimpleT
rawClass = Selector.rawClass

rawAttrPresent : String -> UntypedSimpleT
rawAttrPresent name = Selector.rawAttribute name Selector.rawPresent

rawAttrEquals : String -> String -> UntypedSimpleT
rawAttrEquals name value =
  Selector.rawAttribute name
    (Selector.rawMatch Selector.exact value Selector.documentCase)

isIdKey : {tagName : Safe.TagName} -> Safe.AttributeKey tagName -> Bool
isIdKey Safe.idAttr = true
isIdKey _ = false

isClassKey : {tagName : Safe.TagName} -> Safe.AttributeKey tagName -> Bool
isClassKey Safe.classAttr = true
isClassKey _ = false

noPseudo : Semantics.ElementContext Safe.spec -> String -> Bool
noPseudo _ _ = false

noFunctionalPseudo :
  Semantics.ElementContext Safe.spec ->
  String ->
  String ->
  Bool
noFunctionalPseudo _ _ _ = false

matcherWith : Semantics.TextDeciders -> Semantics.SelectorMatcher Safe.spec
matcherWith text =
  Semantics.matcherFromRenderer
    Safe.renderer
    text
    isIdKey
    isClassKey
    noPseudo
    noFunctionalPseudo

matcher : Semantics.SelectorMatcher Safe.spec
matcher = matcherWith Semantics.exactOnlyTextDeciders

compound : CompoundT -> ComplexT
compound = Selector.compound

descendantOf : ComplexT -> CompoundT -> ComplexT
descendantOf left right = Selector.combine left Selector.descendant right

childOf : ComplexT -> CompoundT -> ComplexT
childOf left right = Selector.combine left Selector.child right

nextSiblingOf : ComplexT -> CompoundT -> ComplexT
nextSiblingOf left right = Selector.combine left Selector.nextSibling right

subsequentSiblingOf : ComplexT -> CompoundT -> ComplexT
subsequentSiblingOf left right =
  Selector.combine left Selector.subsequentSibling right

single : ComplexT -> SelectorT
single = Selector.one

render : SelectorT -> String
render = Selector.renderSelectorList Safe.renderer

matchesRootWith : Semantics.TextDeciders -> SelectorT -> Safe.HtmlT -> Bool
matchesRootWith text = Semantics.matchesRoot (matcherWith text)

matchesRoot : SelectorT -> Safe.HtmlT -> Bool
matchesRoot = Semantics.matchesRoot matcher

selectWith : Semantics.TextDeciders -> SelectorT -> Safe.HtmlT -> List Safe.HtmlT
selectWith text = Semantics.select (matcherWith text)

select : SelectorT -> Safe.HtmlT -> List Safe.HtmlT
select = Semantics.select matcher