module FF.CSS.Spec.Safe.Value.Transform 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; renderRawValue)
open import FF.CSS.Spec.Safe.Value.Unit using
  ( Length
  ; LengthPercentage
  ; Number
  ; Percentage
  ; Angle
  ; renderLength
  ; renderLengthPercentage
  ; renderNumber
  ; renderPercentage
  ; renderAngle
  )

private
  infixr  _++_

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

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

data BackfaceVisibility : Type lzero where
  backfaceVisible backfaceHidden : BackfaceVisibility

renderBackfaceVisibility : BackfaceVisibility -> String
renderBackfaceVisibility backfaceVisible = "visible"
renderBackfaceVisibility backfaceHidden = "hidden"

data TransformStyle : Type lzero where
  styleFlat stylePreserve3d : TransformStyle

renderTransformStyle : TransformStyle -> String
renderTransformStyle styleFlat = "flat"
renderTransformStyle stylePreserve3d = "preserve-3d"

data TransformBox : Type lzero where
  transformContentBox transformBorderBox transformFillBox transformStrokeBox transformViewBox : TransformBox

renderTransformBox : TransformBox -> String
renderTransformBox transformContentBox = "content-box"
renderTransformBox transformBorderBox = "border-box"
renderTransformBox transformFillBox = "fill-box"
renderTransformBox transformStrokeBox = "stroke-box"
renderTransformBox transformViewBox = "view-box"

data Perspective : Type lzero where
  perspectiveNone   : Perspective
  perspectiveLength : Length -> Perspective

renderPerspective : Perspective -> String
renderPerspective perspectiveNone = "none"
renderPerspective (perspectiveLength value) = renderLength value

data Translate : Type lzero where
  translateNone  : Translate
  translateOne   : LengthPercentage -> Translate
  translateTwo   : LengthPercentage -> LengthPercentage -> Translate
  translateThree : LengthPercentage -> LengthPercentage -> Length -> Translate

renderTranslate : Translate -> String
renderTranslate translateNone = "none"
renderTranslate (translateOne x) = renderLengthPercentage x
renderTranslate (translateTwo x y) =
  renderLengthPercentage x ++ " " ++ renderLengthPercentage y
renderTranslate (translateThree x y z) =
  renderLengthPercentage x ++ " " ++ renderLengthPercentage y ++ " " ++ renderLength z

data RotateAxis : Type lzero where
  rotateX rotateY rotateZ : RotateAxis
  rotateVector : Number -> Number -> Number -> RotateAxis

renderRotateAxis : RotateAxis -> String
renderRotateAxis rotateX = "x"
renderRotateAxis rotateY = "y"
renderRotateAxis rotateZ = "z"
renderRotateAxis (rotateVector x y z) =
  renderNumber x ++ " " ++ renderNumber y ++ " " ++ renderNumber z

data Rotate : Type lzero where
  rotateNone      : Rotate
  rotateAngle     : Angle -> Rotate
  rotateAxisAngle : RotateAxis -> Angle -> Rotate

renderRotate : Rotate -> String
renderRotate rotateNone = "none"
renderRotate (rotateAngle value) = renderAngle value
renderRotate (rotateAxisAngle axis value) = renderRotateAxis axis ++ " " ++ renderAngle value

data ScaleValue : Type lzero where
  scaleNumber     : Number -> ScaleValue
  scalePercentage : Percentage -> ScaleValue

renderScaleValue : ScaleValue -> String
renderScaleValue (scaleNumber value) = renderNumber value
renderScaleValue (scalePercentage value) = renderPercentage value

data Scale : Type lzero where
  scaleNone  : Scale
  scaleOne   : ScaleValue -> Scale
  scaleTwo   : ScaleValue -> ScaleValue -> Scale
  scaleThree : ScaleValue -> ScaleValue -> ScaleValue -> Scale

renderScale : Scale -> String
renderScale scaleNone = "none"
renderScale (scaleOne x) = renderScaleValue x
renderScale (scaleTwo x y) = renderScaleValue x ++ " " ++ renderScaleValue y
renderScale (scaleThree x y z) =
  renderScaleValue x ++ " " ++ renderScaleValue y ++ " " ++ renderScaleValue z

record TransformList : Type lzero where
  constructor transformListRaw
  field rawTransformList : RawValue

open TransformList public

renderTransformList : TransformList -> String
renderTransformList (transformListRaw value) = renderRawValue value

data Transform : Type lzero where
  transformNone : Transform
  transformList : TransformList -> Transform

renderTransform : Transform -> String
renderTransform transformNone = "none"
renderTransform (transformList value) = renderTransformList value

record TransformOrigin : Type lzero where
  constructor transformOriginRaw
  field rawTransformOrigin : RawValue

open TransformOrigin public

renderTransformOrigin : TransformOrigin -> String
renderTransformOrigin (transformOriginRaw value) = renderRawValue value

record PerspectiveOrigin : Type lzero where
  constructor perspectiveOriginRaw
  field rawPerspectiveOrigin : RawValue

open PerspectiveOrigin public

renderPerspectiveOrigin : PerspectiveOrigin -> String
renderPerspectiveOrigin (perspectiveOriginRaw value) = renderRawValue value