module FF.CSS.Spec.Safe.Value.Masking 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 (RawValue; Url; renderRawValue; renderUrl)
open import FF.CSS.Spec.Safe.Value.Unit using (LengthPercentageAuto; renderLengthPercentageAuto)

private
  infixr 5 _++_

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

-- MDN CSS Masking property values:
-- https://developer.mozilla.org/en-US/docs/Web/CSS/CSS_masking

data MaskingCommaList (A : Type lzero) : Type lzero where
  maskingCommaOne  : A -> MaskingCommaList A
  maskingCommaCons : A -> MaskingCommaList A -> MaskingCommaList A

renderMaskingCommaList : {A : Type lzero} -> (A -> String) -> MaskingCommaList A -> String
renderMaskingCommaList renderA (maskingCommaOne value) = renderA value
renderMaskingCommaList renderA (maskingCommaCons value rest) =
  renderA value ++ ", " ++ renderMaskingCommaList renderA rest

record BasicShape : Type lzero where
  constructor basicShape
  field rawBasicShape : RawValue

open BasicShape public

renderBasicShape : BasicShape -> String
renderBasicShape (basicShape value) = renderRawValue value

record CssImage : Type lzero where
  constructor cssImage
  field rawCssImage : RawValue

open CssImage public

renderCssImage : CssImage -> String
renderCssImage (cssImage value) = renderRawValue value

record ClipSource : Type lzero where
  constructor clipSource
  field rawClipSource : Url

open ClipSource public

renderClipSource : ClipSource -> String
renderClipSource (clipSource value) = renderUrl value

record MaskSource : Type lzero where
  constructor maskSource
  field rawMaskSource : Url

open MaskSource public

renderMaskSource : MaskSource -> String
renderMaskSource (maskSource value) = renderUrl value

record MaskPositionLayer : Type lzero where
  constructor maskPositionLayer
  field rawMaskPositionLayer : RawValue

open MaskPositionLayer public

renderMaskPositionLayer : MaskPositionLayer -> String
renderMaskPositionLayer (maskPositionLayer value) = renderRawValue value

data CoordBox : Type lzero where
  coordContentBox coordPaddingBox coordBorderBox coordFillBox coordStrokeBox coordViewBox : CoordBox

renderCoordBox : CoordBox -> String
renderCoordBox coordContentBox = "content-box"
renderCoordBox coordPaddingBox = "padding-box"
renderCoordBox coordBorderBox = "border-box"
renderCoordBox coordFillBox = "fill-box"
renderCoordBox coordStrokeBox = "stroke-box"
renderCoordBox coordViewBox = "view-box"

data GeometryBox : Type lzero where
  geometryContentBox geometryPaddingBox geometryBorderBox geometryMarginBox : GeometryBox
  geometryFillBox geometryStrokeBox geometryViewBox : GeometryBox

renderGeometryBox : GeometryBox -> String
renderGeometryBox geometryContentBox = "content-box"
renderGeometryBox geometryPaddingBox = "padding-box"
renderGeometryBox geometryBorderBox = "border-box"
renderGeometryBox geometryMarginBox = "margin-box"
renderGeometryBox geometryFillBox = "fill-box"
renderGeometryBox geometryStrokeBox = "stroke-box"
renderGeometryBox geometryViewBox = "view-box"

data ClipPath : Type lzero where
  clipPathNone                  : ClipPath
  clipPathSource                : ClipSource -> ClipPath
  clipPathBasicShape            : BasicShape -> ClipPath
  clipPathGeometryBox           : GeometryBox -> ClipPath
  clipPathBasicShapeGeometryBox : BasicShape -> GeometryBox -> ClipPath
  clipPathGeometryBoxBasicShape : GeometryBox -> BasicShape -> ClipPath

renderClipPath : ClipPath -> String
renderClipPath clipPathNone = "none"
renderClipPath (clipPathSource value) = renderClipSource value
renderClipPath (clipPathBasicShape value) = renderBasicShape value
renderClipPath (clipPathGeometryBox value) = renderGeometryBox value
renderClipPath (clipPathBasicShapeGeometryBox shape box) =
  renderBasicShape shape ++ " " ++ renderGeometryBox box
renderClipPath (clipPathGeometryBoxBasicShape box shape) =
  renderGeometryBox box ++ " " ++ renderBasicShape shape

data MaskClipLayer : Type lzero where
  maskClipCoordBox : CoordBox -> MaskClipLayer
  maskClipNoClip   : MaskClipLayer

renderMaskClipLayer : MaskClipLayer -> String
renderMaskClipLayer (maskClipCoordBox value) = renderCoordBox value
renderMaskClipLayer maskClipNoClip = "no-clip"

MaskClip : Type lzero
MaskClip = MaskingCommaList MaskClipLayer

renderMaskClip : MaskClip -> String
renderMaskClip value = renderMaskingCommaList renderMaskClipLayer value

data CompositingOperator : Type lzero where
  compositeAdd compositeSubtract compositeIntersect compositeExclude : CompositingOperator

renderCompositingOperator : CompositingOperator -> String
renderCompositingOperator compositeAdd = "add"
renderCompositingOperator compositeSubtract = "subtract"
renderCompositingOperator compositeIntersect = "intersect"
renderCompositingOperator compositeExclude = "exclude"

MaskComposite : Type lzero
MaskComposite = MaskingCommaList CompositingOperator

renderMaskComposite : MaskComposite -> String
renderMaskComposite value = renderMaskingCommaList renderCompositingOperator value

data MaskReference : Type lzero where
  maskReferenceNone   : MaskReference
  maskReferenceImage  : CssImage -> MaskReference
  maskReferenceSource : MaskSource -> MaskReference

renderMaskReference : MaskReference -> String
renderMaskReference maskReferenceNone = "none"
renderMaskReference (maskReferenceImage value) = renderCssImage value
renderMaskReference (maskReferenceSource value) = renderMaskSource value

MaskImage : Type lzero
MaskImage = MaskingCommaList MaskReference

renderMaskImage : MaskImage -> String
renderMaskImage value = renderMaskingCommaList renderMaskReference value

data MaskingMode : Type lzero where
  maskingAlpha maskingLuminance maskingMatchSource : MaskingMode

renderMaskingMode : MaskingMode -> String
renderMaskingMode maskingAlpha = "alpha"
renderMaskingMode maskingLuminance = "luminance"
renderMaskingMode maskingMatchSource = "match-source"

MaskMode : Type lzero
MaskMode = MaskingCommaList MaskingMode

renderMaskMode : MaskMode -> String
renderMaskMode value = renderMaskingCommaList renderMaskingMode value

MaskOrigin : Type lzero
MaskOrigin = MaskingCommaList CoordBox

renderMaskOrigin : MaskOrigin -> String
renderMaskOrigin value = renderMaskingCommaList renderCoordBox value

MaskPosition : Type lzero
MaskPosition = MaskingCommaList MaskPositionLayer

renderMaskPosition : MaskPosition -> String
renderMaskPosition value = renderMaskingCommaList renderMaskPositionLayer value

data MaskRepeatKeyword : Type lzero where
  maskRepeatRepeat maskRepeatSpace maskRepeatRound maskRepeatNoRepeat : MaskRepeatKeyword

renderMaskRepeatKeyword : MaskRepeatKeyword -> String
renderMaskRepeatKeyword maskRepeatRepeat = "repeat"
renderMaskRepeatKeyword maskRepeatSpace = "space"
renderMaskRepeatKeyword maskRepeatRound = "round"
renderMaskRepeatKeyword maskRepeatNoRepeat = "no-repeat"

data MaskRepeatLayer : Type lzero where
  maskRepeatX   : MaskRepeatLayer
  maskRepeatY   : MaskRepeatLayer
  maskRepeatOne : MaskRepeatKeyword -> MaskRepeatLayer
  maskRepeatTwo : MaskRepeatKeyword -> MaskRepeatKeyword -> MaskRepeatLayer

renderMaskRepeatLayer : MaskRepeatLayer -> String
renderMaskRepeatLayer maskRepeatX = "repeat-x"
renderMaskRepeatLayer maskRepeatY = "repeat-y"
renderMaskRepeatLayer (maskRepeatOne value) = renderMaskRepeatKeyword value
renderMaskRepeatLayer (maskRepeatTwo horizontal vertical) =
  renderMaskRepeatKeyword horizontal ++ " " ++ renderMaskRepeatKeyword vertical

MaskRepeat : Type lzero
MaskRepeat = MaskingCommaList MaskRepeatLayer

renderMaskRepeat : MaskRepeat -> String
renderMaskRepeat value = renderMaskingCommaList renderMaskRepeatLayer value

data MaskSizeLayer : Type lzero where
  maskSizeAuto maskSizeCover maskSizeContain : MaskSizeLayer
  maskSizeOne : LengthPercentageAuto -> MaskSizeLayer
  maskSizeTwo : LengthPercentageAuto -> LengthPercentageAuto -> MaskSizeLayer

renderMaskSizeLayer : MaskSizeLayer -> String
renderMaskSizeLayer maskSizeAuto = "auto"
renderMaskSizeLayer maskSizeCover = "cover"
renderMaskSizeLayer maskSizeContain = "contain"
renderMaskSizeLayer (maskSizeOne value) = renderLengthPercentageAuto value
renderMaskSizeLayer (maskSizeTwo width height) =
  renderLengthPercentageAuto width ++ " " ++ renderLengthPercentageAuto height

MaskSize : Type lzero
MaskSize = MaskingCommaList MaskSizeLayer

renderMaskSize : MaskSize -> String
renderMaskSize value = renderMaskingCommaList renderMaskSizeLayer value

data MaskType : Type lzero where
  maskTypeLuminance maskTypeAlpha : MaskType

renderMaskType : MaskType -> String
renderMaskType maskTypeLuminance = "luminance"
renderMaskType maskTypeAlpha = "alpha"

data MaskingPropertyName : Type lzero where
  clipPathProperty maskClipProperty maskCompositeProperty maskImageProperty maskModeProperty : MaskingPropertyName
  maskOriginProperty maskPositionProperty maskRepeatProperty maskSizeProperty maskTypeProperty : MaskingPropertyName

renderMaskingPropertyName : MaskingPropertyName -> String
renderMaskingPropertyName clipPathProperty = "clip-path"
renderMaskingPropertyName maskClipProperty = "mask-clip"
renderMaskingPropertyName maskCompositeProperty = "mask-composite"
renderMaskingPropertyName maskImageProperty = "mask-image"
renderMaskingPropertyName maskModeProperty = "mask-mode"
renderMaskingPropertyName maskOriginProperty = "mask-origin"
renderMaskingPropertyName maskPositionProperty = "mask-position"
renderMaskingPropertyName maskRepeatProperty = "mask-repeat"
renderMaskingPropertyName maskSizeProperty = "mask-size"
renderMaskingPropertyName maskTypeProperty = "mask-type"

data MaskingPropertyValue : MaskingPropertyName -> Type lzero where
  maskingClipPathValue      : ClipPath -> MaskingPropertyValue clipPathProperty
  maskingMaskClipValue      : MaskClip -> MaskingPropertyValue maskClipProperty
  maskingMaskCompositeValue : MaskComposite -> MaskingPropertyValue maskCompositeProperty
  maskingMaskImageValue     : MaskImage -> MaskingPropertyValue maskImageProperty
  maskingMaskModeValue      : MaskMode -> MaskingPropertyValue maskModeProperty
  maskingMaskOriginValue    : MaskOrigin -> MaskingPropertyValue maskOriginProperty
  maskingMaskPositionValue  : MaskPosition -> MaskingPropertyValue maskPositionProperty
  maskingMaskRepeatValue    : MaskRepeat -> MaskingPropertyValue maskRepeatProperty
  maskingMaskSizeValue      : MaskSize -> MaskingPropertyValue maskSizeProperty
  maskingMaskTypeValue      : MaskType -> MaskingPropertyValue maskTypeProperty

renderMaskingPropertyValue : (propertyName : MaskingPropertyName) -> MaskingPropertyValue propertyName -> String
renderMaskingPropertyValue clipPathProperty (maskingClipPathValue value) = renderClipPath value
renderMaskingPropertyValue maskClipProperty (maskingMaskClipValue value) = renderMaskClip value
renderMaskingPropertyValue maskCompositeProperty (maskingMaskCompositeValue value) = renderMaskComposite value
renderMaskingPropertyValue maskImageProperty (maskingMaskImageValue value) = renderMaskImage value
renderMaskingPropertyValue maskModeProperty (maskingMaskModeValue value) = renderMaskMode value
renderMaskingPropertyValue maskOriginProperty (maskingMaskOriginValue value) = renderMaskOrigin value
renderMaskingPropertyValue maskPositionProperty (maskingMaskPositionValue value) = renderMaskPosition value
renderMaskingPropertyValue maskRepeatProperty (maskingMaskRepeatValue value) = renderMaskRepeat value
renderMaskingPropertyValue maskSizeProperty (maskingMaskSizeValue value) = renderMaskSize value
renderMaskingPropertyValue maskTypeProperty (maskingMaskTypeValue value) = renderMaskType value

record MaskingPropertyPair : Type lzero where
  constructor maskingPair
  field
    maskingPairName  : MaskingPropertyName
    maskingPairValue : MaskingPropertyValue maskingPairName

open MaskingPropertyPair public

renderMaskingPropertyPair : MaskingPropertyPair -> String
renderMaskingPropertyPair (maskingPair propertyName value) =
  renderMaskingPropertyName propertyName ++ ": " ++ renderMaskingPropertyValue propertyName value