module FF.CSS.Spec.Safe.Value.Containment where

open import Agda.Builtin.String using (String; primStringAppend)
open import Agda.Primitive using (lzero) renaming (Set to Type)

open import FF.CSS.Spec.Safe.Value.Base using (CustomIdent; renderCustomIdent)

private
  infixr  _++_

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

-- MDN CSS Conditional Rules and CSS Containment property values:
-- https://developer.mozilla.org/en-US/docs/Web/CSS/CSS_conditional_rules
-- https://developer.mozilla.org/en-US/docs/Web/CSS/CSS_containment

data ContainmentNonEmptySpaceList (A : Type lzero) : Type lzero where
  containmentSpaceOne  : A -> ContainmentNonEmptySpaceList A
  containmentSpaceCons : A -> ContainmentNonEmptySpaceList A -> ContainmentNonEmptySpaceList A

renderContainmentNonEmptySpaceList :
  {A : Type lzero} -> (A -> String) -> ContainmentNonEmptySpaceList A -> String
renderContainmentNonEmptySpaceList renderA (containmentSpaceOne value) = renderA value
renderContainmentNonEmptySpaceList renderA (containmentSpaceCons value rest) =
  renderA value ++ " " ++ renderContainmentNonEmptySpaceList renderA rest

data ContainSizeClause : Type lzero where
  containmentSize              : ContainSizeClause
  containmentInlineSize        : ContainSizeClause
  containmentSizeAndInlineSize : ContainSizeClause

renderContainSizeClause : ContainSizeClause -> String
renderContainSizeClause containmentSize = "size"
renderContainSizeClause containmentInlineSize = "inline-size"
renderContainSizeClause containmentSizeAndInlineSize = "size inline-size"

data ContainLayoutFlag : Type lzero where
  containmentNoLayout   : ContainLayoutFlag
  containmentWithLayout : ContainLayoutFlag

renderContainLayoutSuffix : ContainLayoutFlag -> String
renderContainLayoutSuffix containmentNoLayout = ""
renderContainLayoutSuffix containmentWithLayout = " layout"

data ContainStyleFlag : Type lzero where
  containmentNoStyle   : ContainStyleFlag
  containmentWithStyle : ContainStyleFlag

renderContainStyleSuffix : ContainStyleFlag -> String
renderContainStyleSuffix containmentNoStyle = ""
renderContainStyleSuffix containmentWithStyle = " style"

data ContainPaintFlag : Type lzero where
  containmentNoPaint   : ContainPaintFlag
  containmentWithPaint : ContainPaintFlag

renderContainPaintSuffix : ContainPaintFlag -> String
renderContainPaintSuffix containmentNoPaint = ""
renderContainPaintSuffix containmentWithPaint = " paint"

data ContainFeatureSet : Type lzero where
  containmentContainWithSize :
    ContainSizeClause ->
    ContainLayoutFlag ->
    ContainStyleFlag ->
    ContainPaintFlag ->
    ContainFeatureSet
  containmentContainWithLayout : ContainStyleFlag -> ContainPaintFlag -> ContainFeatureSet
  containmentContainWithStyle  : ContainPaintFlag -> ContainFeatureSet
  containmentContainWithPaint  : ContainFeatureSet

renderContainFeatureSet : ContainFeatureSet -> String
renderContainFeatureSet (containmentContainWithSize size layout style paint) =
  renderContainSizeClause size ++
  renderContainLayoutSuffix layout ++
  renderContainStyleSuffix style ++
  renderContainPaintSuffix paint
renderContainFeatureSet (containmentContainWithLayout style paint) =
  "layout" ++ renderContainStyleSuffix style ++ renderContainPaintSuffix paint
renderContainFeatureSet (containmentContainWithStyle paint) =
  "style" ++ renderContainPaintSuffix paint
renderContainFeatureSet containmentContainWithPaint = "paint"

data Contain : Type lzero where
  containmentContainNone     : Contain
  containmentContainStrict   : Contain
  containmentContainContent  : Contain
  containmentContainFeatures : ContainFeatureSet -> Contain

renderContain : Contain -> String
renderContain containmentContainNone = "none"
renderContain containmentContainStrict = "strict"
renderContain containmentContainContent = "content"
renderContain (containmentContainFeatures value) = renderContainFeatureSet value

data ContentVisibility : Type lzero where
  containmentContentVisible : ContentVisibility
  containmentContentAuto    : ContentVisibility
  containmentContentHidden  : ContentVisibility

renderContentVisibility : ContentVisibility -> String
renderContentVisibility containmentContentVisible = "visible"
renderContentVisibility containmentContentAuto = "auto"
renderContentVisibility containmentContentHidden = "hidden"

ContainerNameList : Type lzero
ContainerNameList = ContainmentNonEmptySpaceList CustomIdent

renderContainerNameList : ContainerNameList -> String
renderContainerNameList value = renderContainmentNonEmptySpaceList renderCustomIdent value

data ContainerName : Type lzero where
  containmentContainerNameNone : ContainerName
  containmentContainerNames    : ContainerNameList -> ContainerName

renderContainerName : ContainerName -> String
renderContainerName containmentContainerNameNone = "none"
renderContainerName (containmentContainerNames value) = renderContainerNameList value

data ContainerQueryAxis : Type lzero where
  containmentContainerSize       : ContainerQueryAxis
  containmentContainerInlineSize : ContainerQueryAxis

renderContainerQueryAxis : ContainerQueryAxis -> String
renderContainerQueryAxis containmentContainerSize = "size"
renderContainerQueryAxis containmentContainerInlineSize = "inline-size"

data ContainerTypeFeatureSet : Type lzero where
  containmentContainerTypeAxis            : ContainerQueryAxis -> ContainerTypeFeatureSet
  containmentContainerTypeScrollState     : ContainerTypeFeatureSet
  containmentContainerTypeAxisScrollState : ContainerQueryAxis -> ContainerTypeFeatureSet

renderContainerTypeFeatureSet : ContainerTypeFeatureSet -> String
renderContainerTypeFeatureSet (containmentContainerTypeAxis axis) =
  renderContainerQueryAxis axis
renderContainerTypeFeatureSet containmentContainerTypeScrollState = "scroll-state"
renderContainerTypeFeatureSet (containmentContainerTypeAxisScrollState axis) =
  renderContainerQueryAxis axis ++ " scroll-state"

data ContainerType : Type lzero where
  containmentContainerTypeNormal   : ContainerType
  containmentContainerTypeFeatures : ContainerTypeFeatureSet -> ContainerType

renderContainerType : ContainerType -> String
renderContainerType containmentContainerTypeNormal = "normal"
renderContainerType (containmentContainerTypeFeatures value) =
  renderContainerTypeFeatureSet value

data Container : Type lzero where
  containmentContainerNameOnly : ContainerName -> Container
  containmentContainerWithType : ContainerName -> ContainerType -> Container

renderContainer : Container -> String
renderContainer (containmentContainerNameOnly name) = renderContainerName name
renderContainer (containmentContainerWithType name containerType) =
  renderContainerName name ++ " / " ++ renderContainerType containerType

data ContainmentPropertyName : Type lzero where
  containmentContainProp           : ContainmentPropertyName
  containmentContentVisibilityProp : ContainmentPropertyName
  containmentContainerNameProp     : ContainmentPropertyName
  containmentContainerTypeProp     : ContainmentPropertyName
  containmentContainerProp         : ContainmentPropertyName

renderContainmentPropertyName : ContainmentPropertyName -> String
renderContainmentPropertyName containmentContainProp = "contain"
renderContainmentPropertyName containmentContentVisibilityProp = "content-visibility"
renderContainmentPropertyName containmentContainerNameProp = "container-name"
renderContainmentPropertyName containmentContainerTypeProp = "container-type"
renderContainmentPropertyName containmentContainerProp = "container"

data ContainmentPropertyValue : ContainmentPropertyName -> Type lzero where
  containmentContainValue :
    Contain -> ContainmentPropertyValue containmentContainProp
  containmentContentVisibilityValue :
    ContentVisibility -> ContainmentPropertyValue containmentContentVisibilityProp
  containmentContainerNameValue :
    ContainerName -> ContainmentPropertyValue containmentContainerNameProp
  containmentContainerTypeValue :
    ContainerType -> ContainmentPropertyValue containmentContainerTypeProp
  containmentContainerValue :
    Container -> ContainmentPropertyValue containmentContainerProp

renderContainmentPropertyValue :
  (propertyName : ContainmentPropertyName) ->
  ContainmentPropertyValue propertyName ->
  String
renderContainmentPropertyValue containmentContainProp (containmentContainValue value) =
  renderContain value
renderContainmentPropertyValue
  containmentContentVisibilityProp
  (containmentContentVisibilityValue value) =
  renderContentVisibility value
renderContainmentPropertyValue containmentContainerNameProp (containmentContainerNameValue value) =
  renderContainerName value
renderContainmentPropertyValue containmentContainerTypeProp (containmentContainerTypeValue value) =
  renderContainerType value
renderContainmentPropertyValue containmentContainerProp (containmentContainerValue value) =
  renderContainer value

record ContainmentPropertyPair : Type lzero where
  constructor containmentPair
  field
    containmentPairName  : ContainmentPropertyName
    containmentPairValue : ContainmentPropertyValue containmentPairName

open ContainmentPropertyPair public

containmentContainPair : Contain -> ContainmentPropertyPair
containmentContainPair value =
  containmentPair containmentContainProp (containmentContainValue value)

containmentContentVisibilityPair : ContentVisibility -> ContainmentPropertyPair
containmentContentVisibilityPair value =
  containmentPair containmentContentVisibilityProp (containmentContentVisibilityValue value)

containmentContainerNamePair : ContainerName -> ContainmentPropertyPair
containmentContainerNamePair value =
  containmentPair containmentContainerNameProp (containmentContainerNameValue value)

containmentContainerTypePair : ContainerType -> ContainmentPropertyPair
containmentContainerTypePair value =
  containmentPair containmentContainerTypeProp (containmentContainerTypeValue value)

containmentContainerPair : Container -> ContainmentPropertyPair
containmentContainerPair value =
  containmentPair containmentContainerProp (containmentContainerValue value)

renderContainmentPropertyPair : ContainmentPropertyPair -> String
renderContainmentPropertyPair (containmentPair propertyName propertyValue) =
  renderContainmentPropertyName propertyName ++ ": " ++
  renderContainmentPropertyValue propertyName propertyValue