module FF.CSS.Spec.Safe.Value.Misc 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 5 _++_

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

-- Small standalone MDN CSS property values not yet wired into the central
-- indexed property family.

data MiscNonEmptyCommaList (A : Type lzero) : Type lzero where
  miscCommaOne  : A -> MiscNonEmptyCommaList A
  miscCommaCons : A -> MiscNonEmptyCommaList A -> MiscNonEmptyCommaList A

renderMiscNonEmptyCommaList :
  {A : Type lzero} -> (A -> String) -> MiscNonEmptyCommaList A -> String
renderMiscNonEmptyCommaList renderA (miscCommaOne value) = renderA value
renderMiscNonEmptyCommaList renderA (miscCommaCons value rest) =
  renderA value ++ ", " ++ renderMiscNonEmptyCommaList renderA rest

data MiscNonEmptySpaceList (A : Type lzero) : Type lzero where
  miscSpaceOne  : A -> MiscNonEmptySpaceList A
  miscSpaceCons : A -> MiscNonEmptySpaceList A -> MiscNonEmptySpaceList A

renderMiscNonEmptySpaceList :
  {A : Type lzero} -> (A -> String) -> MiscNonEmptySpaceList A -> String
renderMiscNonEmptySpaceList renderA (miscSpaceOne value) = renderA value
renderMiscNonEmptySpaceList renderA (miscSpaceCons value rest) =
  renderA value ++ " " ++ renderMiscNonEmptySpaceList renderA rest

data All : Type lzero where
  miscAllInitial     : All
  miscAllInherit     : All
  miscAllUnset       : All
  miscAllRevert      : All
  miscAllRevertLayer : All

renderAll : All -> String
renderAll miscAllInitial = "initial"
renderAll miscAllInherit = "inherit"
renderAll miscAllUnset = "unset"
renderAll miscAllRevert = "revert"
renderAll miscAllRevertLayer = "revert-layer"

data WillChangeFeature : Type lzero where
  miscWillChangeScrollPosition : WillChangeFeature
  miscWillChangeContents       : WillChangeFeature
  miscWillChangeCustom         : CustomIdent -> WillChangeFeature

renderWillChangeFeature : WillChangeFeature -> String
renderWillChangeFeature miscWillChangeScrollPosition = "scroll-position"
renderWillChangeFeature miscWillChangeContents = "contents"
renderWillChangeFeature (miscWillChangeCustom value) = renderCustomIdent value

WillChangeFeatureList : Type lzero
WillChangeFeatureList = MiscNonEmptyCommaList WillChangeFeature

renderWillChangeFeatureList : WillChangeFeatureList -> String
renderWillChangeFeatureList value =
  renderMiscNonEmptyCommaList renderWillChangeFeature value

data WillChange : Type lzero where
  miscWillChangeAuto     : WillChange
  miscWillChangeFeatures : WillChangeFeatureList -> WillChange

renderWillChange : WillChange -> String
renderWillChange miscWillChangeAuto = "auto"
renderWillChange (miscWillChangeFeatures value) = renderWillChangeFeatureList value

data ViewportFit : Type lzero where
  miscViewportFitAuto    : ViewportFit
  miscViewportFitContain : ViewportFit
  miscViewportFitCover   : ViewportFit

renderViewportFit : ViewportFit -> String
renderViewportFit miscViewportFitAuto = "auto"
renderViewportFit miscViewportFitContain = "contain"
renderViewportFit miscViewportFitCover = "cover"

ViewTransitionClassList : Type lzero
ViewTransitionClassList = MiscNonEmptySpaceList CustomIdent

renderViewTransitionClassList : ViewTransitionClassList -> String
renderViewTransitionClassList value =
  renderMiscNonEmptySpaceList renderCustomIdent value

data ViewTransitionClass : Type lzero where
  miscViewTransitionClassNone    : ViewTransitionClass
  miscViewTransitionClassIdents  : ViewTransitionClassList -> ViewTransitionClass

renderViewTransitionClass : ViewTransitionClass -> String
renderViewTransitionClass miscViewTransitionClassNone = "none"
renderViewTransitionClass (miscViewTransitionClassIdents value) =
  renderViewTransitionClassList value

data ViewTransitionGroup : Type lzero where
  miscViewTransitionGroupNormal  : ViewTransitionGroup
  miscViewTransitionGroupContain : ViewTransitionGroup
  miscViewTransitionGroupNearest : ViewTransitionGroup
  miscViewTransitionGroupCustom  : CustomIdent -> ViewTransitionGroup

renderViewTransitionGroup : ViewTransitionGroup -> String
renderViewTransitionGroup miscViewTransitionGroupNormal = "normal"
renderViewTransitionGroup miscViewTransitionGroupContain = "contain"
renderViewTransitionGroup miscViewTransitionGroupNearest = "nearest"
renderViewTransitionGroup (miscViewTransitionGroupCustom value) =
  renderCustomIdent value

data ViewTransitionName : Type lzero where
  miscViewTransitionNameNone         : ViewTransitionName
  miscViewTransitionNameAuto         : ViewTransitionName
  miscViewTransitionNameMatchElement : ViewTransitionName
  miscViewTransitionNameCustom       : CustomIdent -> ViewTransitionName

renderViewTransitionName : ViewTransitionName -> String
renderViewTransitionName miscViewTransitionNameNone = "none"
renderViewTransitionName miscViewTransitionNameAuto = "auto"
renderViewTransitionName miscViewTransitionNameMatchElement = "match-element"
renderViewTransitionName (miscViewTransitionNameCustom value) =
  renderCustomIdent value

data OverflowAnchor : Type lzero where
  miscOverflowAnchorAuto : OverflowAnchor
  miscOverflowAnchorNone : OverflowAnchor

renderOverflowAnchor : OverflowAnchor -> String
renderOverflowAnchor miscOverflowAnchorAuto = "auto"
renderOverflowAnchor miscOverflowAnchorNone = "none"

data MiscPropertyName : Type lzero where
  miscAllProp                 : MiscPropertyName
  miscWillChangeProp          : MiscPropertyName
  miscViewportFitProp         : MiscPropertyName
  miscViewTransitionClassProp : MiscPropertyName
  miscViewTransitionGroupProp : MiscPropertyName
  miscViewTransitionNameProp  : MiscPropertyName
  miscOverflowAnchorProp      : MiscPropertyName

renderMiscPropertyName : MiscPropertyName -> String
renderMiscPropertyName miscAllProp = "all"
renderMiscPropertyName miscWillChangeProp = "will-change"
renderMiscPropertyName miscViewportFitProp = "viewport-fit"
renderMiscPropertyName miscViewTransitionClassProp = "view-transition-class"
renderMiscPropertyName miscViewTransitionGroupProp = "view-transition-group"
renderMiscPropertyName miscViewTransitionNameProp = "view-transition-name"
renderMiscPropertyName miscOverflowAnchorProp = "overflow-anchor"

data MiscPropertyValue : MiscPropertyName -> Type lzero where
  miscAllValue :
    All -> MiscPropertyValue miscAllProp
  miscWillChangeValue :
    WillChange -> MiscPropertyValue miscWillChangeProp
  miscViewportFitValue :
    ViewportFit -> MiscPropertyValue miscViewportFitProp
  miscViewTransitionClassValue :
    ViewTransitionClass -> MiscPropertyValue miscViewTransitionClassProp
  miscViewTransitionGroupValue :
    ViewTransitionGroup -> MiscPropertyValue miscViewTransitionGroupProp
  miscViewTransitionNameValue :
    ViewTransitionName -> MiscPropertyValue miscViewTransitionNameProp
  miscOverflowAnchorValue :
    OverflowAnchor -> MiscPropertyValue miscOverflowAnchorProp

renderMiscPropertyValue :
  (propertyName : MiscPropertyName) ->
  MiscPropertyValue propertyName ->
  String
renderMiscPropertyValue miscAllProp (miscAllValue value) =
  renderAll value
renderMiscPropertyValue miscWillChangeProp (miscWillChangeValue value) =
  renderWillChange value
renderMiscPropertyValue miscViewportFitProp (miscViewportFitValue value) =
  renderViewportFit value
renderMiscPropertyValue
  miscViewTransitionClassProp
  (miscViewTransitionClassValue value) =
  renderViewTransitionClass value
renderMiscPropertyValue
  miscViewTransitionGroupProp
  (miscViewTransitionGroupValue value) =
  renderViewTransitionGroup value
renderMiscPropertyValue
  miscViewTransitionNameProp
  (miscViewTransitionNameValue value) =
  renderViewTransitionName value
renderMiscPropertyValue miscOverflowAnchorProp (miscOverflowAnchorValue value) =
  renderOverflowAnchor value

record MiscPropertyPair : Type lzero where
  constructor miscPair
  field
    miscPairName  : MiscPropertyName
    miscPairValue : MiscPropertyValue miscPairName

open MiscPropertyPair public

miscAllPair : All -> MiscPropertyPair
miscAllPair value =
  miscPair miscAllProp (miscAllValue value)

miscWillChangePair : WillChange -> MiscPropertyPair
miscWillChangePair value =
  miscPair miscWillChangeProp (miscWillChangeValue value)

miscViewportFitPair : ViewportFit -> MiscPropertyPair
miscViewportFitPair value =
  miscPair miscViewportFitProp (miscViewportFitValue value)

miscViewTransitionClassPair : ViewTransitionClass -> MiscPropertyPair
miscViewTransitionClassPair value =
  miscPair miscViewTransitionClassProp (miscViewTransitionClassValue value)

miscViewTransitionGroupPair : ViewTransitionGroup -> MiscPropertyPair
miscViewTransitionGroupPair value =
  miscPair miscViewTransitionGroupProp (miscViewTransitionGroupValue value)

miscViewTransitionNamePair : ViewTransitionName -> MiscPropertyPair
miscViewTransitionNamePair value =
  miscPair miscViewTransitionNameProp (miscViewTransitionNameValue value)

miscOverflowAnchorPair : OverflowAnchor -> MiscPropertyPair
miscOverflowAnchorPair value =
  miscPair miscOverflowAnchorProp (miscOverflowAnchorValue value)

renderMiscPropertyPair : MiscPropertyPair -> String
renderMiscPropertyPair (miscPair propertyName propertyValue) =
  renderMiscPropertyName propertyName ++ ": " ++
  renderMiscPropertyValue propertyName propertyValue