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

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

private
  infixr 5 _++_

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

-- MDN CSS Compositing and Blending property values:
-- https://developer.mozilla.org/en-US/docs/Web/CSS/CSS_compositing_and_blending

data BlendMode : Type lzero where
  blendNormal blendMultiply blendScreen blendOverlay blendDarken blendLighten : BlendMode
  blendColorDodge blendColorBurn blendHardLight blendSoftLight : BlendMode
  blendDifference blendExclusion blendHue blendSaturation blendColor blendLuminosity : BlendMode

renderBlendMode : BlendMode -> String
renderBlendMode blendNormal = "normal"
renderBlendMode blendMultiply = "multiply"
renderBlendMode blendScreen = "screen"
renderBlendMode blendOverlay = "overlay"
renderBlendMode blendDarken = "darken"
renderBlendMode blendLighten = "lighten"
renderBlendMode blendColorDodge = "color-dodge"
renderBlendMode blendColorBurn = "color-burn"
renderBlendMode blendHardLight = "hard-light"
renderBlendMode blendSoftLight = "soft-light"
renderBlendMode blendDifference = "difference"
renderBlendMode blendExclusion = "exclusion"
renderBlendMode blendHue = "hue"
renderBlendMode blendSaturation = "saturation"
renderBlendMode blendColor = "color"
renderBlendMode blendLuminosity = "luminosity"

data BlendModeList : Type lzero where
  blendModeOne  : BlendMode -> BlendModeList
  blendModeCons : BlendMode -> BlendModeList -> BlendModeList

renderBlendModeList : BlendModeList -> String
renderBlendModeList (blendModeOne value) = renderBlendMode value
renderBlendModeList (blendModeCons value rest) =
  renderBlendMode value ++ ", " ++ renderBlendModeList rest

data MixBlendMode : Type lzero where
  mixBlendMode : BlendMode -> MixBlendMode
  mixPlusDarker mixPlusLighter : MixBlendMode

renderMixBlendMode : MixBlendMode -> String
renderMixBlendMode (mixBlendMode value) = renderBlendMode value
renderMixBlendMode mixPlusDarker = "plus-darker"
renderMixBlendMode mixPlusLighter = "plus-lighter"

data Isolation : Type lzero where
  isolationAuto isolationIsolate : Isolation

renderIsolation : Isolation -> String
renderIsolation isolationAuto = "auto"
renderIsolation isolationIsolate = "isolate"

data CompositingPropertyName : Type lzero where
  compositingBackgroundBlendModeProp compositingIsolationProp compositingMixBlendModeProp :
    CompositingPropertyName

renderCompositingPropertyName : CompositingPropertyName -> String
renderCompositingPropertyName compositingBackgroundBlendModeProp = "background-blend-mode"
renderCompositingPropertyName compositingIsolationProp = "isolation"
renderCompositingPropertyName compositingMixBlendModeProp = "mix-blend-mode"

data CompositingPropertyValue : CompositingPropertyName -> Type lzero where
  compositingBackgroundBlendModeValue :
    BlendModeList -> CompositingPropertyValue compositingBackgroundBlendModeProp
  compositingIsolationValue :
    Isolation -> CompositingPropertyValue compositingIsolationProp
  compositingMixBlendModeValue :
    MixBlendMode -> CompositingPropertyValue compositingMixBlendModeProp

renderCompositingPropertyValue :
  (propertyName : CompositingPropertyName) ->
  CompositingPropertyValue propertyName ->
  String
renderCompositingPropertyValue
  compositingBackgroundBlendModeProp
  (compositingBackgroundBlendModeValue value) =
  renderBlendModeList value
renderCompositingPropertyValue compositingIsolationProp (compositingIsolationValue value) =
  renderIsolation value
renderCompositingPropertyValue compositingMixBlendModeProp (compositingMixBlendModeValue value) =
  renderMixBlendMode value

record CompositingPropertyPair : Type lzero where
  constructor compositingPair
  field
    compositingPairName  : CompositingPropertyName
    compositingPairValue : CompositingPropertyValue compositingPairName

open CompositingPropertyPair public

renderCompositingPropertyPair : CompositingPropertyPair -> String
renderCompositingPropertyPair (compositingPair propertyName value) =
  renderCompositingPropertyName propertyName ++ ": " ++
  renderCompositingPropertyValue propertyName value