FF.CSS.Spec.Safe.Value.Scroll

module FF.CSS.Spec.Safe.Value.Scroll 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)
open import FF.CSS.Spec.Safe.Value.Color using (Color; renderColor)
open import FF.CSS.Spec.Safe.Value.Unit using (Length; LengthPercentage; renderLength; renderLengthPercentage)

private
  infixr 5 _++_

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

data ScrollOneOrTwo (A : Type lzero) : Type lzero where
  scrollOneValue  : A -> ScrollOneOrTwo A
  scrollTwoValues : A -> A -> ScrollOneOrTwo A

renderScrollOneOrTwo : {A : Type lzero} -> (A -> String) -> ScrollOneOrTwo A -> String
renderScrollOneOrTwo renderA (scrollOneValue value) = renderA value
renderScrollOneOrTwo renderA (scrollTwoValues first second) =
  renderA first ++ " " ++ renderA second

data ScrollBoxSides (A : Type lzero) : Type lzero where
  scrollOneSide    : A -> ScrollBoxSides A
  scrollTwoSides   : A -> A -> ScrollBoxSides A
  scrollThreeSides : A -> A -> A -> ScrollBoxSides A
  scrollFourSides  : A -> A -> A -> A -> ScrollBoxSides A

renderScrollBoxSides : {A : Type lzero} -> (A -> String) -> ScrollBoxSides A -> String
renderScrollBoxSides renderA (scrollOneSide value) = renderA value
renderScrollBoxSides renderA (scrollTwoSides vertical horizontal) =
  renderA vertical ++ " " ++ renderA horizontal
renderScrollBoxSides renderA (scrollThreeSides top horizontal bottom) =
  renderA top ++ " " ++ renderA horizontal ++ " " ++ renderA bottom
renderScrollBoxSides renderA (scrollFourSides top right bottom left) =
  renderA top ++ " " ++ renderA right ++ " " ++ renderA bottom ++ " " ++ renderA left

data ScrollCommaList (A : Type lzero) : Type lzero where
  scrollCommaOne  : A -> ScrollCommaList A
  scrollCommaCons : A -> ScrollCommaList A -> ScrollCommaList A

renderScrollCommaList : {A : Type lzero} -> (A -> String) -> ScrollCommaList A -> String
renderScrollCommaList renderA (scrollCommaOne value) = renderA value
renderScrollCommaList renderA (scrollCommaCons value rest) =
  renderA value ++ ", " ++ renderScrollCommaList renderA rest

data OverscrollBehaviorKeyword : Type lzero where
  overscrollAuto overscrollContain overscrollNone : OverscrollBehaviorKeyword

renderOverscrollBehaviorKeyword : OverscrollBehaviorKeyword -> String
renderOverscrollBehaviorKeyword overscrollAuto = "auto"
renderOverscrollBehaviorKeyword overscrollContain = "contain"
renderOverscrollBehaviorKeyword overscrollNone = "none"

data OverscrollBehavior : Type lzero where
  overscrollBehaviorOne : OverscrollBehaviorKeyword -> OverscrollBehavior
  overscrollBehaviorTwo : OverscrollBehaviorKeyword -> OverscrollBehaviorKeyword -> OverscrollBehavior

renderOverscrollBehavior : OverscrollBehavior -> String
renderOverscrollBehavior (overscrollBehaviorOne value) = renderOverscrollBehaviorKeyword value
renderOverscrollBehavior (overscrollBehaviorTwo x y) =
  renderOverscrollBehaviorKeyword x ++ " " ++ renderOverscrollBehaviorKeyword y

OverscrollBehaviorX : Type lzero
OverscrollBehaviorX = OverscrollBehaviorKeyword

renderOverscrollBehaviorX : OverscrollBehaviorX -> String
renderOverscrollBehaviorX value = renderOverscrollBehaviorKeyword value

OverscrollBehaviorY : Type lzero
OverscrollBehaviorY = OverscrollBehaviorKeyword

renderOverscrollBehaviorY : OverscrollBehaviorY -> String
renderOverscrollBehaviorY value = renderOverscrollBehaviorKeyword value

OverscrollBehaviorBlock : Type lzero
OverscrollBehaviorBlock = OverscrollBehaviorKeyword

renderOverscrollBehaviorBlock : OverscrollBehaviorBlock -> String
renderOverscrollBehaviorBlock value = renderOverscrollBehaviorKeyword value

OverscrollBehaviorInline : Type lzero
OverscrollBehaviorInline = OverscrollBehaviorKeyword

renderOverscrollBehaviorInline : OverscrollBehaviorInline -> String
renderOverscrollBehaviorInline value = renderOverscrollBehaviorKeyword value

data ScrollSnapAxis : Type lzero where
  snapAxisX snapAxisY snapAxisBlock snapAxisInline snapAxisBoth : ScrollSnapAxis

renderScrollSnapAxis : ScrollSnapAxis -> String
renderScrollSnapAxis snapAxisX = "x"
renderScrollSnapAxis snapAxisY = "y"
renderScrollSnapAxis snapAxisBlock = "block"
renderScrollSnapAxis snapAxisInline = "inline"
renderScrollSnapAxis snapAxisBoth = "both"

data ScrollSnapStrictness : Type lzero where
  snapMandatory snapProximity : ScrollSnapStrictness

renderScrollSnapStrictness : ScrollSnapStrictness -> String
renderScrollSnapStrictness snapMandatory = "mandatory"
renderScrollSnapStrictness snapProximity = "proximity"

data ScrollSnapType : Type lzero where
  scrollSnapNone : ScrollSnapType
  scrollSnapAxis : ScrollSnapAxis -> ScrollSnapType
  scrollSnapAxisStrictness : ScrollSnapAxis -> ScrollSnapStrictness -> ScrollSnapType

renderScrollSnapType : ScrollSnapType -> String
renderScrollSnapType scrollSnapNone = "none"
renderScrollSnapType (scrollSnapAxis axis) = renderScrollSnapAxis axis
renderScrollSnapType (scrollSnapAxisStrictness axis strictness) =
  renderScrollSnapAxis axis ++ " " ++ renderScrollSnapStrictness strictness

data ScrollSnapAlignKeyword : Type lzero where
  snapAlignNone snapAlignStart snapAlignEnd snapAlignCenter : ScrollSnapAlignKeyword

renderScrollSnapAlignKeyword : ScrollSnapAlignKeyword -> String
renderScrollSnapAlignKeyword snapAlignNone = "none"
renderScrollSnapAlignKeyword snapAlignStart = "start"
renderScrollSnapAlignKeyword snapAlignEnd = "end"
renderScrollSnapAlignKeyword snapAlignCenter = "center"

data ScrollSnapAlign : Type lzero where
  scrollSnapAlignOne : ScrollSnapAlignKeyword -> ScrollSnapAlign
  scrollSnapAlignTwo : ScrollSnapAlignKeyword -> ScrollSnapAlignKeyword -> ScrollSnapAlign

renderScrollSnapAlign : ScrollSnapAlign -> String
renderScrollSnapAlign (scrollSnapAlignOne value) = renderScrollSnapAlignKeyword value
renderScrollSnapAlign (scrollSnapAlignTwo block inline) =
  renderScrollSnapAlignKeyword block ++ " " ++ renderScrollSnapAlignKeyword inline

data ScrollSnapStop : Type lzero where
  snapStopNormal snapStopAlways : ScrollSnapStop

renderScrollSnapStop : ScrollSnapStop -> String
renderScrollSnapStop snapStopNormal = "normal"
renderScrollSnapStop snapStopAlways = "always"

data ScrollPaddingSide : Type lzero where
  scrollPaddingAuto : ScrollPaddingSide
  scrollPaddingLengthPercentage : LengthPercentage -> ScrollPaddingSide

renderScrollPaddingSide : ScrollPaddingSide -> String
renderScrollPaddingSide scrollPaddingAuto = "auto"
renderScrollPaddingSide (scrollPaddingLengthPercentage value) = renderLengthPercentage value

ScrollPaddingPair : Type lzero
ScrollPaddingPair = ScrollOneOrTwo ScrollPaddingSide

renderScrollPaddingPair : ScrollPaddingPair -> String
renderScrollPaddingPair value = renderScrollOneOrTwo renderScrollPaddingSide value

ScrollPadding : Type lzero
ScrollPadding = ScrollBoxSides ScrollPaddingSide

renderScrollPadding : ScrollPadding -> String
renderScrollPadding value = renderScrollBoxSides renderScrollPaddingSide value

ScrollPaddingBlock : Type lzero
ScrollPaddingBlock = ScrollPaddingPair

renderScrollPaddingBlock : ScrollPaddingBlock -> String
renderScrollPaddingBlock value = renderScrollPaddingPair value

ScrollPaddingInline : Type lzero
ScrollPaddingInline = ScrollPaddingPair

renderScrollPaddingInline : ScrollPaddingInline -> String
renderScrollPaddingInline value = renderScrollPaddingPair value

ScrollPaddingBlockStart : Type lzero
ScrollPaddingBlockStart = ScrollPaddingSide

renderScrollPaddingBlockStart : ScrollPaddingBlockStart -> String
renderScrollPaddingBlockStart value = renderScrollPaddingSide value

ScrollPaddingBlockEnd : Type lzero
ScrollPaddingBlockEnd = ScrollPaddingSide

renderScrollPaddingBlockEnd : ScrollPaddingBlockEnd -> String
renderScrollPaddingBlockEnd value = renderScrollPaddingSide value

ScrollPaddingInlineStart : Type lzero
ScrollPaddingInlineStart = ScrollPaddingSide

renderScrollPaddingInlineStart : ScrollPaddingInlineStart -> String
renderScrollPaddingInlineStart value = renderScrollPaddingSide value

ScrollPaddingInlineEnd : Type lzero
ScrollPaddingInlineEnd = ScrollPaddingSide

renderScrollPaddingInlineEnd : ScrollPaddingInlineEnd -> String
renderScrollPaddingInlineEnd value = renderScrollPaddingSide value

ScrollPaddingTop : Type lzero
ScrollPaddingTop = ScrollPaddingSide

renderScrollPaddingTop : ScrollPaddingTop -> String
renderScrollPaddingTop value = renderScrollPaddingSide value

ScrollPaddingRight : Type lzero
ScrollPaddingRight = ScrollPaddingSide

renderScrollPaddingRight : ScrollPaddingRight -> String
renderScrollPaddingRight value = renderScrollPaddingSide value

ScrollPaddingBottom : Type lzero
ScrollPaddingBottom = ScrollPaddingSide

renderScrollPaddingBottom : ScrollPaddingBottom -> String
renderScrollPaddingBottom value = renderScrollPaddingSide value

ScrollPaddingLeft : Type lzero
ScrollPaddingLeft = ScrollPaddingSide

renderScrollPaddingLeft : ScrollPaddingLeft -> String
renderScrollPaddingLeft value = renderScrollPaddingSide value

ScrollMarginSide : Type lzero
ScrollMarginSide = Length

renderScrollMarginSide : ScrollMarginSide -> String
renderScrollMarginSide value = renderLength value

ScrollMarginPair : Type lzero
ScrollMarginPair = ScrollOneOrTwo ScrollMarginSide

renderScrollMarginPair : ScrollMarginPair -> String
renderScrollMarginPair value = renderScrollOneOrTwo renderScrollMarginSide value

ScrollMargin : Type lzero
ScrollMargin = ScrollBoxSides ScrollMarginSide

renderScrollMargin : ScrollMargin -> String
renderScrollMargin value = renderScrollBoxSides renderScrollMarginSide value

ScrollMarginBlock : Type lzero
ScrollMarginBlock = ScrollMarginPair

renderScrollMarginBlock : ScrollMarginBlock -> String
renderScrollMarginBlock value = renderScrollMarginPair value

ScrollMarginInline : Type lzero
ScrollMarginInline = ScrollMarginPair

renderScrollMarginInline : ScrollMarginInline -> String
renderScrollMarginInline value = renderScrollMarginPair value

ScrollMarginBlockStart : Type lzero
ScrollMarginBlockStart = ScrollMarginSide

renderScrollMarginBlockStart : ScrollMarginBlockStart -> String
renderScrollMarginBlockStart value = renderScrollMarginSide value

ScrollMarginBlockEnd : Type lzero
ScrollMarginBlockEnd = ScrollMarginSide

renderScrollMarginBlockEnd : ScrollMarginBlockEnd -> String
renderScrollMarginBlockEnd value = renderScrollMarginSide value

ScrollMarginInlineStart : Type lzero
ScrollMarginInlineStart = ScrollMarginSide

renderScrollMarginInlineStart : ScrollMarginInlineStart -> String
renderScrollMarginInlineStart value = renderScrollMarginSide value

ScrollMarginInlineEnd : Type lzero
ScrollMarginInlineEnd = ScrollMarginSide

renderScrollMarginInlineEnd : ScrollMarginInlineEnd -> String
renderScrollMarginInlineEnd value = renderScrollMarginSide value

ScrollMarginTop : Type lzero
ScrollMarginTop = ScrollMarginSide

renderScrollMarginTop : ScrollMarginTop -> String
renderScrollMarginTop value = renderScrollMarginSide value

ScrollMarginRight : Type lzero
ScrollMarginRight = ScrollMarginSide

renderScrollMarginRight : ScrollMarginRight -> String
renderScrollMarginRight value = renderScrollMarginSide value

ScrollMarginBottom : Type lzero
ScrollMarginBottom = ScrollMarginSide

renderScrollMarginBottom : ScrollMarginBottom -> String
renderScrollMarginBottom value = renderScrollMarginSide value

ScrollMarginLeft : Type lzero
ScrollMarginLeft = ScrollMarginSide

renderScrollMarginLeft : ScrollMarginLeft -> String
renderScrollMarginLeft value = renderScrollMarginSide value

data ScrollTimelineAxisKeyword : Type lzero where
  timelineAxisBlock timelineAxisInline timelineAxisX timelineAxisY : ScrollTimelineAxisKeyword

renderScrollTimelineAxisKeyword : ScrollTimelineAxisKeyword -> String
renderScrollTimelineAxisKeyword timelineAxisBlock = "block"
renderScrollTimelineAxisKeyword timelineAxisInline = "inline"
renderScrollTimelineAxisKeyword timelineAxisX = "x"
renderScrollTimelineAxisKeyword timelineAxisY = "y"

ScrollTimelineAxis : Type lzero
ScrollTimelineAxis = ScrollCommaList ScrollTimelineAxisKeyword

renderScrollTimelineAxis : ScrollTimelineAxis -> String
renderScrollTimelineAxis value = renderScrollCommaList renderScrollTimelineAxisKeyword value

data ScrollTimelineNameItem : Type lzero where
  timelineNameNone : ScrollTimelineNameItem
  timelineNameCustom : CustomIdent -> ScrollTimelineNameItem

renderScrollTimelineNameItem : ScrollTimelineNameItem -> String
renderScrollTimelineNameItem timelineNameNone = "none"
renderScrollTimelineNameItem (timelineNameCustom value) = renderCustomIdent value

ScrollTimelineName : Type lzero
ScrollTimelineName = ScrollCommaList ScrollTimelineNameItem

renderScrollTimelineName : ScrollTimelineName -> String
renderScrollTimelineName value = renderScrollCommaList renderScrollTimelineNameItem value

data ScrollbarColor : Type lzero where
  scrollbarColorAuto : ScrollbarColor
  scrollbarColors : Color -> Color -> ScrollbarColor

renderScrollbarColor : ScrollbarColor -> String
renderScrollbarColor scrollbarColorAuto = "auto"
renderScrollbarColor (scrollbarColors thumb track) =
  renderColor thumb ++ " " ++ renderColor track

data ScrollbarWidth : Type lzero where
  scrollbarWidthAuto scrollbarWidthThin scrollbarWidthNone : ScrollbarWidth

renderScrollbarWidth : ScrollbarWidth -> String
renderScrollbarWidth scrollbarWidthAuto = "auto"
renderScrollbarWidth scrollbarWidthThin = "thin"
renderScrollbarWidth scrollbarWidthNone = "none"