module FF.CSS.Spec.Safe.Value.Break 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.Unit using (Integer; renderInteger)

private
  infixr 5 _++_

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

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

data BreakBetween : Type lzero where
  breakBetweenAuto breakBetweenAvoid breakBetweenAlways breakBetweenAll : BreakBetween
  breakBetweenAvoidPage breakBetweenPage breakBetweenLeft breakBetweenRight : BreakBetween
  breakBetweenRecto breakBetweenVerso : BreakBetween
  breakBetweenAvoidColumn breakBetweenColumn : BreakBetween
  breakBetweenAvoidRegion breakBetweenRegion : BreakBetween

renderBreakBetween : BreakBetween -> String
renderBreakBetween breakBetweenAuto = "auto"
renderBreakBetween breakBetweenAvoid = "avoid"
renderBreakBetween breakBetweenAlways = "always"
renderBreakBetween breakBetweenAll = "all"
renderBreakBetween breakBetweenAvoidPage = "avoid-page"
renderBreakBetween breakBetweenPage = "page"
renderBreakBetween breakBetweenLeft = "left"
renderBreakBetween breakBetweenRight = "right"
renderBreakBetween breakBetweenRecto = "recto"
renderBreakBetween breakBetweenVerso = "verso"
renderBreakBetween breakBetweenAvoidColumn = "avoid-column"
renderBreakBetween breakBetweenColumn = "column"
renderBreakBetween breakBetweenAvoidRegion = "avoid-region"
renderBreakBetween breakBetweenRegion = "region"

BreakAfter : Type lzero
BreakAfter = BreakBetween

renderBreakAfter : BreakAfter -> String
renderBreakAfter value = renderBreakBetween value

BreakBefore : Type lzero
BreakBefore = BreakBetween

renderBreakBefore : BreakBefore -> String
renderBreakBefore value = renderBreakBetween value

data BreakInside : Type lzero where
  breakInsideAuto breakInsideAvoid breakInsideAvoidPage : BreakInside
  breakInsideAvoidColumn breakInsideAvoidRegion : BreakInside

renderBreakInside : BreakInside -> String
renderBreakInside breakInsideAuto = "auto"
renderBreakInside breakInsideAvoid = "avoid"
renderBreakInside breakInsideAvoidPage = "avoid-page"
renderBreakInside breakInsideAvoidColumn = "avoid-column"
renderBreakInside breakInsideAvoidRegion = "avoid-region"

data BoxDecorationBreak : Type lzero where
  boxDecorationSlice boxDecorationClone : BoxDecorationBreak

renderBoxDecorationBreak : BoxDecorationBreak -> String
renderBoxDecorationBreak boxDecorationSlice = "slice"
renderBoxDecorationBreak boxDecorationClone = "clone"

Orphans : Type lzero
Orphans = Integer

renderOrphans : Orphans -> String
renderOrphans value = renderInteger value

Widows : Type lzero
Widows = Integer

renderWidows : Widows -> String
renderWidows value = renderInteger value

data BreakPropertyName : Type lzero where
  breakPropertyAfter breakPropertyBefore breakPropertyInside : BreakPropertyName
  breakPropertyBoxDecorationBreak breakPropertyOrphans breakPropertyWidows : BreakPropertyName

renderBreakPropertyName : BreakPropertyName -> String
renderBreakPropertyName breakPropertyAfter = "break-after"
renderBreakPropertyName breakPropertyBefore = "break-before"
renderBreakPropertyName breakPropertyInside = "break-inside"
renderBreakPropertyName breakPropertyBoxDecorationBreak = "box-decoration-break"
renderBreakPropertyName breakPropertyOrphans = "orphans"
renderBreakPropertyName breakPropertyWidows = "widows"

data BreakPropertyValue : BreakPropertyName -> Type lzero where
  breakValueAfter              : BreakAfter -> BreakPropertyValue breakPropertyAfter
  breakValueBefore             : BreakBefore -> BreakPropertyValue breakPropertyBefore
  breakValueInside             : BreakInside -> BreakPropertyValue breakPropertyInside
  breakValueBoxDecorationBreak : BoxDecorationBreak -> BreakPropertyValue breakPropertyBoxDecorationBreak
  breakValueOrphans            : Orphans -> BreakPropertyValue breakPropertyOrphans
  breakValueWidows             : Widows -> BreakPropertyValue breakPropertyWidows

renderBreakPropertyValue : (propertyName : BreakPropertyName) -> BreakPropertyValue propertyName -> String
renderBreakPropertyValue breakPropertyAfter (breakValueAfter value) =
  renderBreakAfter value
renderBreakPropertyValue breakPropertyBefore (breakValueBefore value) =
  renderBreakBefore value
renderBreakPropertyValue breakPropertyInside (breakValueInside value) =
  renderBreakInside value
renderBreakPropertyValue breakPropertyBoxDecorationBreak (breakValueBoxDecorationBreak value) =
  renderBoxDecorationBreak value
renderBreakPropertyValue breakPropertyOrphans (breakValueOrphans value) =
  renderOrphans value
renderBreakPropertyValue breakPropertyWidows (breakValueWidows value) =
  renderWidows value

record BreakDeclaration : Type lzero where
  constructor breakDeclaration
  field
    propertyName  : BreakPropertyName
    propertyValue : BreakPropertyValue propertyName

open BreakDeclaration public

renderBreakDeclaration : BreakDeclaration -> String
renderBreakDeclaration (breakDeclaration propertyName propertyValue) =
  renderBreakPropertyName propertyName ++ ": " ++
  renderBreakPropertyValue propertyName propertyValue