module FF.CSS.Spec.Safe.Value.Ruby where

open import Agda.Builtin.String using (String; primStringAppend)
open import Agda.Primitive using (lzero) renaming (Set to Type)

private
  infixr 5 _++_

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

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

data RubyAlign : Type lzero where
  rubyAlignStart rubyAlignCenter rubyAlignSpaceBetween rubyAlignSpaceAround : RubyAlign

renderRubyAlign : RubyAlign -> String
renderRubyAlign rubyAlignStart = "start"
renderRubyAlign rubyAlignCenter = "center"
renderRubyAlign rubyAlignSpaceBetween = "space-between"
renderRubyAlign rubyAlignSpaceAround = "space-around"

data RubyOverhang : Type lzero where
  rubyOverhangAuto rubyOverhangNone : RubyOverhang

renderRubyOverhang : RubyOverhang -> String
renderRubyOverhang rubyOverhangAuto = "auto"
renderRubyOverhang rubyOverhangNone = "none"

data RubyPositionSide : Type lzero where
  rubyPositionOver rubyPositionUnder : RubyPositionSide

renderRubyPositionSide : RubyPositionSide -> String
renderRubyPositionSide rubyPositionOver = "over"
renderRubyPositionSide rubyPositionUnder = "under"

data RubyPosition : Type lzero where
  rubyPositionSide : RubyPositionSide -> RubyPosition
  rubyPositionAlternate : RubyPosition
  rubyPositionAlternateSide : RubyPositionSide -> RubyPosition
  rubyPositionInterCharacter : RubyPosition

renderRubyPosition : RubyPosition -> String
renderRubyPosition (rubyPositionSide value) = renderRubyPositionSide value
renderRubyPosition rubyPositionAlternate = "alternate"
renderRubyPosition (rubyPositionAlternateSide value) =
  "alternate " ++ renderRubyPositionSide value
renderRubyPosition rubyPositionInterCharacter = "inter-character"

data RubyMerge : Type lzero where
  rubyMergeSeparate rubyMergeCollapse rubyMergeAuto : RubyMerge

renderRubyMerge : RubyMerge -> String
renderRubyMerge rubyMergeSeparate = "separate"
renderRubyMerge rubyMergeCollapse = "collapse"
renderRubyMerge rubyMergeAuto = "auto"

data RubyPropertyName : Type lzero where
  rubyPropertyAlign rubyPropertyOverhang rubyPropertyPosition rubyPropertyMerge : RubyPropertyName

renderRubyPropertyName : RubyPropertyName -> String
renderRubyPropertyName rubyPropertyAlign = "ruby-align"
renderRubyPropertyName rubyPropertyOverhang = "ruby-overhang"
renderRubyPropertyName rubyPropertyPosition = "ruby-position"
renderRubyPropertyName rubyPropertyMerge = "ruby-merge"

data RubyPropertyValue : RubyPropertyName -> Type lzero where
  rubyValueAlign : RubyAlign -> RubyPropertyValue rubyPropertyAlign
  rubyValueOverhang : RubyOverhang -> RubyPropertyValue rubyPropertyOverhang
  rubyValuePosition : RubyPosition -> RubyPropertyValue rubyPropertyPosition
  rubyValueMerge : RubyMerge -> RubyPropertyValue rubyPropertyMerge

renderRubyPropertyValue : (propertyName : RubyPropertyName) -> RubyPropertyValue propertyName -> String
renderRubyPropertyValue rubyPropertyAlign (rubyValueAlign value) = renderRubyAlign value
renderRubyPropertyValue rubyPropertyOverhang (rubyValueOverhang value) = renderRubyOverhang value
renderRubyPropertyValue rubyPropertyPosition (rubyValuePosition value) = renderRubyPosition value
renderRubyPropertyValue rubyPropertyMerge (rubyValueMerge value) = renderRubyMerge value

record RubyPropertyPair : Type lzero where
  constructor rubyPair
  field
    rubyPairName : RubyPropertyName
    rubyPairValue : RubyPropertyValue rubyPairName

open RubyPropertyPair public

renderRubyPropertyPair : RubyPropertyPair -> String
renderRubyPropertyPair (rubyPair propertyName value) =
  renderRubyPropertyName propertyName ++ ": " ++ renderRubyPropertyValue propertyName value