module FF.CSS.Spec.Safe.Value.Animation 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 (Time; Number; renderTime; renderNumber)

private
  infixr 5 _++_

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

-- Animation and transition values:
-- https://developer.mozilla.org/en-US/docs/Web/CSS/CSS_animations
-- https://developer.mozilla.org/en-US/docs/Web/CSS/CSS_transitions

data TimingValueList (A : Type lzero) : Type lzero where
  timingOne  : A -> TimingValueList A
  timingCons : A -> TimingValueList A -> TimingValueList A

renderTimingValueList : {A : Type lzero} -> (A -> String) -> TimingValueList A -> String
renderTimingValueList renderA (timingOne value) = renderA value
renderTimingValueList renderA (timingCons value rest) =
  renderA value ++ ", " ++ renderTimingValueList renderA rest

record EasingFunction : Type lzero where
  constructor easingFunction
  field rawEasingFunction : RawValue

open EasingFunction public

renderEasingFunction : EasingFunction -> String
renderEasingFunction (easingFunction value) = renderRawValue value

record KeyframesName : Type lzero where
  constructor keyframesName
  field rawKeyframesName : RawValue

open KeyframesName public

renderKeyframesName : KeyframesName -> String
renderKeyframesName (keyframesName value) = renderRawValue value

record TimelineRange : Type lzero where
  constructor timelineRange
  field rawTimelineRange : RawValue

open TimelineRange public

renderTimelineRange : TimelineRange -> String
renderTimelineRange (timelineRange value) = renderRawValue value

data AnimationDirection : Type lzero where
  directionNormal directionReverse directionAlternate directionAlternateReverse : AnimationDirection

renderAnimationDirection : AnimationDirection -> String
renderAnimationDirection directionNormal = "normal"
renderAnimationDirection directionReverse = "reverse"
renderAnimationDirection directionAlternate = "alternate"
renderAnimationDirection directionAlternateReverse = "alternate-reverse"

data AnimationFillMode : Type lzero where
  fillNone fillForwards fillBackwards fillBoth : AnimationFillMode

renderAnimationFillMode : AnimationFillMode -> String
renderAnimationFillMode fillNone = "none"
renderAnimationFillMode fillForwards = "forwards"
renderAnimationFillMode fillBackwards = "backwards"
renderAnimationFillMode fillBoth = "both"

data AnimationPlayState : Type lzero where
  playRunning playPaused : AnimationPlayState

renderAnimationPlayState : AnimationPlayState -> String
renderAnimationPlayState playRunning = "running"
renderAnimationPlayState playPaused = "paused"

data AnimationComposition : Type lzero where
  compositionReplace compositionAdd compositionAccumulate : AnimationComposition

renderAnimationComposition : AnimationComposition -> String
renderAnimationComposition compositionReplace = "replace"
renderAnimationComposition compositionAdd = "add"
renderAnimationComposition compositionAccumulate = "accumulate"

data AnimationIterationCount : Type lzero where
  iterationInfinite : AnimationIterationCount
  iterationNumber   : Number -> AnimationIterationCount

renderAnimationIterationCount : AnimationIterationCount -> String
renderAnimationIterationCount iterationInfinite = "infinite"
renderAnimationIterationCount (iterationNumber value) = renderNumber value

data TransitionBehavior : Type lzero where
  behaviorNormal behaviorAllowDiscrete : TransitionBehavior

renderTransitionBehavior : TransitionBehavior -> String
renderTransitionBehavior behaviorNormal = "normal"
renderTransitionBehavior behaviorAllowDiscrete = "allow-discrete"

AnimationNameList : Type lzero
AnimationNameList = TimingValueList KeyframesName

renderAnimationNameList : AnimationNameList -> String
renderAnimationNameList = renderTimingValueList renderKeyframesName

TimeList : Type lzero
TimeList = TimingValueList Time

renderTimeList : TimeList -> String
renderTimeList = renderTimingValueList renderTime

EasingFunctionList : Type lzero
EasingFunctionList = TimingValueList EasingFunction

renderEasingFunctionList : EasingFunctionList -> String
renderEasingFunctionList = renderTimingValueList renderEasingFunction

AnimationDirectionList : Type lzero
AnimationDirectionList = TimingValueList AnimationDirection

renderAnimationDirectionList : AnimationDirectionList -> String
renderAnimationDirectionList = renderTimingValueList renderAnimationDirection

AnimationFillModeList : Type lzero
AnimationFillModeList = TimingValueList AnimationFillMode

renderAnimationFillModeList : AnimationFillModeList -> String
renderAnimationFillModeList = renderTimingValueList renderAnimationFillMode

AnimationPlayStateList : Type lzero
AnimationPlayStateList = TimingValueList AnimationPlayState

renderAnimationPlayStateList : AnimationPlayStateList -> String
renderAnimationPlayStateList = renderTimingValueList renderAnimationPlayState

AnimationCompositionList : Type lzero
AnimationCompositionList = TimingValueList AnimationComposition

renderAnimationCompositionList : AnimationCompositionList -> String
renderAnimationCompositionList = renderTimingValueList renderAnimationComposition

AnimationIterationCountList : Type lzero
AnimationIterationCountList = TimingValueList AnimationIterationCount

renderAnimationIterationCountList : AnimationIterationCountList -> String
renderAnimationIterationCountList = renderTimingValueList renderAnimationIterationCount

TransitionBehaviorList : Type lzero
TransitionBehaviorList = TimingValueList TransitionBehavior

renderTransitionBehaviorList : TransitionBehaviorList -> String
renderTransitionBehaviorList = renderTimingValueList renderTransitionBehavior

TimelineRangeList : Type lzero
TimelineRangeList = TimingValueList TimelineRange

renderTimelineRangeList : TimelineRangeList -> String
renderTimelineRangeList = renderTimingValueList renderTimelineRange