module FF.CSS.Spec.Safe.Value.Inline 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
  ( Integer
  ; LengthPercentage
  ; Number
  ; renderInteger
  ; renderLengthPercentage
  ; renderNumber
  )

private
  infixr 5 _++_

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

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

data AlignmentBaseline : Type lzero where
  inlineAlignmentBaselineBaseline       : AlignmentBaseline
  inlineAlignmentBaselineAlphabetic     : AlignmentBaseline
  inlineAlignmentBaselineIdeographic    : AlignmentBaseline
  inlineAlignmentBaselineMiddle         : AlignmentBaseline
  inlineAlignmentBaselineCentral        : AlignmentBaseline
  inlineAlignmentBaselineMathematical   : AlignmentBaseline
  inlineAlignmentBaselineTextBeforeEdge : AlignmentBaseline
  inlineAlignmentBaselineTextAfterEdge  : AlignmentBaseline

renderAlignmentBaseline : AlignmentBaseline -> String
renderAlignmentBaseline inlineAlignmentBaselineBaseline = "baseline"
renderAlignmentBaseline inlineAlignmentBaselineAlphabetic = "alphabetic"
renderAlignmentBaseline inlineAlignmentBaselineIdeographic = "ideographic"
renderAlignmentBaseline inlineAlignmentBaselineMiddle = "middle"
renderAlignmentBaseline inlineAlignmentBaselineCentral = "central"
renderAlignmentBaseline inlineAlignmentBaselineMathematical = "mathematical"
renderAlignmentBaseline inlineAlignmentBaselineTextBeforeEdge = "text-before-edge"
renderAlignmentBaseline inlineAlignmentBaselineTextAfterEdge = "text-after-edge"

data BaselineShift : Type lzero where
  inlineBaselineShiftLengthPercentage : LengthPercentage -> BaselineShift
  inlineBaselineShiftSub              : BaselineShift
  inlineBaselineShiftSuper            : BaselineShift
  inlineBaselineShiftBaseline         : BaselineShift

renderBaselineShift : BaselineShift -> String
renderBaselineShift (inlineBaselineShiftLengthPercentage value) =
  renderLengthPercentage value
renderBaselineShift inlineBaselineShiftSub = "sub"
renderBaselineShift inlineBaselineShiftSuper = "super"
renderBaselineShift inlineBaselineShiftBaseline = "baseline"

data BaselineSource : Type lzero where
  inlineBaselineSourceAuto  : BaselineSource
  inlineBaselineSourceFirst : BaselineSource
  inlineBaselineSourceLast  : BaselineSource

renderBaselineSource : BaselineSource -> String
renderBaselineSource inlineBaselineSourceAuto = "auto"
renderBaselineSource inlineBaselineSourceFirst = "first"
renderBaselineSource inlineBaselineSourceLast = "last"

data DominantBaseline : Type lzero where
  inlineDominantBaselineAuto         : DominantBaseline
  inlineDominantBaselineTextBottom   : DominantBaseline
  inlineDominantBaselineAlphabetic   : DominantBaseline
  inlineDominantBaselineIdeographic  : DominantBaseline
  inlineDominantBaselineMiddle       : DominantBaseline
  inlineDominantBaselineCentral      : DominantBaseline
  inlineDominantBaselineMathematical : DominantBaseline
  inlineDominantBaselineHanging      : DominantBaseline
  inlineDominantBaselineTextTop      : DominantBaseline

renderDominantBaseline : DominantBaseline -> String
renderDominantBaseline inlineDominantBaselineAuto = "auto"
renderDominantBaseline inlineDominantBaselineTextBottom = "text-bottom"
renderDominantBaseline inlineDominantBaselineAlphabetic = "alphabetic"
renderDominantBaseline inlineDominantBaselineIdeographic = "ideographic"
renderDominantBaseline inlineDominantBaselineMiddle = "middle"
renderDominantBaseline inlineDominantBaselineCentral = "central"
renderDominantBaseline inlineDominantBaselineMathematical = "mathematical"
renderDominantBaseline inlineDominantBaselineHanging = "hanging"
renderDominantBaseline inlineDominantBaselineTextTop = "text-top"

data InitialLetter : Type lzero where
  inlineInitialLetterNormal   : InitialLetter
  inlineInitialLetterSize     : Number -> InitialLetter
  inlineInitialLetterSizeSink : Number -> Integer -> InitialLetter

renderInitialLetter : InitialLetter -> String
renderInitialLetter inlineInitialLetterNormal = "normal"
renderInitialLetter (inlineInitialLetterSize size) = renderNumber size
renderInitialLetter (inlineInitialLetterSizeSink size sink) =
  renderNumber size ++ " " ++ renderInteger sink

record TextEdge : Type lzero where
  constructor inlineTextEdge
  field rawTextEdge : RawValue

open TextEdge public

renderTextEdge : TextEdge -> String
renderTextEdge (inlineTextEdge value) = renderRawValue value

data TextBoxEdge : Type lzero where
  inlineTextBoxEdgeAuto     : TextBoxEdge
  inlineTextBoxEdgeTextEdge : TextEdge -> TextBoxEdge

renderTextBoxEdge : TextBoxEdge -> String
renderTextBoxEdge inlineTextBoxEdgeAuto = "auto"
renderTextBoxEdge (inlineTextBoxEdgeTextEdge value) = renderTextEdge value

data TextBoxTrim : Type lzero where
  inlineTextBoxTrimNone      : TextBoxTrim
  inlineTextBoxTrimTrimStart : TextBoxTrim
  inlineTextBoxTrimTrimEnd   : TextBoxTrim
  inlineTextBoxTrimTrimBoth  : TextBoxTrim

renderTextBoxTrim : TextBoxTrim -> String
renderTextBoxTrim inlineTextBoxTrimNone = "none"
renderTextBoxTrim inlineTextBoxTrimTrimStart = "trim-start"
renderTextBoxTrim inlineTextBoxTrimTrimEnd = "trim-end"
renderTextBoxTrim inlineTextBoxTrimTrimBoth = "trim-both"

data TextBox : Type lzero where
  inlineTextBoxNormal   : TextBox
  inlineTextBoxTrim     : TextBoxTrim -> TextBox
  inlineTextBoxEdge     : TextBoxEdge -> TextBox
  inlineTextBoxTrimEdge : TextBoxTrim -> TextBoxEdge -> TextBox
  inlineTextBoxEdgeTrim : TextBoxEdge -> TextBoxTrim -> TextBox

renderTextBox : TextBox -> String
renderTextBox inlineTextBoxNormal = "normal"
renderTextBox (inlineTextBoxTrim trim) = renderTextBoxTrim trim
renderTextBox (inlineTextBoxEdge edge) = renderTextBoxEdge edge
renderTextBox (inlineTextBoxTrimEdge trim edge) =
  renderTextBoxTrim trim ++ " " ++ renderTextBoxEdge edge
renderTextBox (inlineTextBoxEdgeTrim edge trim) =
  renderTextBoxEdge edge ++ " " ++ renderTextBoxTrim trim

data VerticalAlign : Type lzero where
  inlineVerticalAlignBaseline         : VerticalAlign
  inlineVerticalAlignSub              : VerticalAlign
  inlineVerticalAlignSuper            : VerticalAlign
  inlineVerticalAlignTextTop          : VerticalAlign
  inlineVerticalAlignTextBottom       : VerticalAlign
  inlineVerticalAlignMiddle           : VerticalAlign
  inlineVerticalAlignTop              : VerticalAlign
  inlineVerticalAlignBottom           : VerticalAlign
  inlineVerticalAlignLengthPercentage : LengthPercentage -> VerticalAlign

renderVerticalAlign : VerticalAlign -> String
renderVerticalAlign inlineVerticalAlignBaseline = "baseline"
renderVerticalAlign inlineVerticalAlignSub = "sub"
renderVerticalAlign inlineVerticalAlignSuper = "super"
renderVerticalAlign inlineVerticalAlignTextTop = "text-top"
renderVerticalAlign inlineVerticalAlignTextBottom = "text-bottom"
renderVerticalAlign inlineVerticalAlignMiddle = "middle"
renderVerticalAlign inlineVerticalAlignTop = "top"
renderVerticalAlign inlineVerticalAlignBottom = "bottom"
renderVerticalAlign (inlineVerticalAlignLengthPercentage value) =
  renderLengthPercentage value

data InlinePropertyName : Type lzero where
  inlineAlignmentBaselineProp : InlinePropertyName
  inlineBaselineShiftProp     : InlinePropertyName
  inlineBaselineSourceProp    : InlinePropertyName
  inlineDominantBaselineProp  : InlinePropertyName
  inlineInitialLetterProp     : InlinePropertyName
  inlineTextBoxProp           : InlinePropertyName
  inlineTextBoxEdgeProp       : InlinePropertyName
  inlineTextBoxTrimProp       : InlinePropertyName
  inlineVerticalAlignProp     : InlinePropertyName

renderInlinePropertyName : InlinePropertyName -> String
renderInlinePropertyName inlineAlignmentBaselineProp = "alignment-baseline"
renderInlinePropertyName inlineBaselineShiftProp = "baseline-shift"
renderInlinePropertyName inlineBaselineSourceProp = "baseline-source"
renderInlinePropertyName inlineDominantBaselineProp = "dominant-baseline"
renderInlinePropertyName inlineInitialLetterProp = "initial-letter"
renderInlinePropertyName inlineTextBoxProp = "text-box"
renderInlinePropertyName inlineTextBoxEdgeProp = "text-box-edge"
renderInlinePropertyName inlineTextBoxTrimProp = "text-box-trim"
renderInlinePropertyName inlineVerticalAlignProp = "vertical-align"

data InlinePropertyValue : InlinePropertyName -> Type lzero where
  inlineAlignmentBaselineValue :
    AlignmentBaseline -> InlinePropertyValue inlineAlignmentBaselineProp
  inlineBaselineShiftValue :
    BaselineShift -> InlinePropertyValue inlineBaselineShiftProp
  inlineBaselineSourceValue :
    BaselineSource -> InlinePropertyValue inlineBaselineSourceProp
  inlineDominantBaselineValue :
    DominantBaseline -> InlinePropertyValue inlineDominantBaselineProp
  inlineInitialLetterValue :
    InitialLetter -> InlinePropertyValue inlineInitialLetterProp
  inlineTextBoxValue :
    TextBox -> InlinePropertyValue inlineTextBoxProp
  inlineTextBoxEdgeValue :
    TextBoxEdge -> InlinePropertyValue inlineTextBoxEdgeProp
  inlineTextBoxTrimValue :
    TextBoxTrim -> InlinePropertyValue inlineTextBoxTrimProp
  inlineVerticalAlignValue :
    VerticalAlign -> InlinePropertyValue inlineVerticalAlignProp

renderInlinePropertyValue :
  (propertyName : InlinePropertyName) ->
  InlinePropertyValue propertyName ->
  String
renderInlinePropertyValue
  inlineAlignmentBaselineProp
  (inlineAlignmentBaselineValue value) =
  renderAlignmentBaseline value
renderInlinePropertyValue inlineBaselineShiftProp (inlineBaselineShiftValue value) =
  renderBaselineShift value
renderInlinePropertyValue inlineBaselineSourceProp (inlineBaselineSourceValue value) =
  renderBaselineSource value
renderInlinePropertyValue
  inlineDominantBaselineProp
  (inlineDominantBaselineValue value) =
  renderDominantBaseline value
renderInlinePropertyValue inlineInitialLetterProp (inlineInitialLetterValue value) =
  renderInitialLetter value
renderInlinePropertyValue inlineTextBoxProp (inlineTextBoxValue value) =
  renderTextBox value
renderInlinePropertyValue inlineTextBoxEdgeProp (inlineTextBoxEdgeValue value) =
  renderTextBoxEdge value
renderInlinePropertyValue inlineTextBoxTrimProp (inlineTextBoxTrimValue value) =
  renderTextBoxTrim value
renderInlinePropertyValue inlineVerticalAlignProp (inlineVerticalAlignValue value) =
  renderVerticalAlign value

record InlinePropertyPair : Type lzero where
  constructor inlinePair
  field
    inlinePairName  : InlinePropertyName
    inlinePairValue : InlinePropertyValue inlinePairName

open InlinePropertyPair public

inlineAlignmentBaselinePair : AlignmentBaseline -> InlinePropertyPair
inlineAlignmentBaselinePair value =
  inlinePair inlineAlignmentBaselineProp (inlineAlignmentBaselineValue value)

inlineBaselineShiftPair : BaselineShift -> InlinePropertyPair
inlineBaselineShiftPair value =
  inlinePair inlineBaselineShiftProp (inlineBaselineShiftValue value)

inlineBaselineSourcePair : BaselineSource -> InlinePropertyPair
inlineBaselineSourcePair value =
  inlinePair inlineBaselineSourceProp (inlineBaselineSourceValue value)

inlineDominantBaselinePair : DominantBaseline -> InlinePropertyPair
inlineDominantBaselinePair value =
  inlinePair inlineDominantBaselineProp (inlineDominantBaselineValue value)

inlineInitialLetterPair : InitialLetter -> InlinePropertyPair
inlineInitialLetterPair value =
  inlinePair inlineInitialLetterProp (inlineInitialLetterValue value)

inlineTextBoxPair : TextBox -> InlinePropertyPair
inlineTextBoxPair value =
  inlinePair inlineTextBoxProp (inlineTextBoxValue value)

inlineTextBoxEdgePair : TextBoxEdge -> InlinePropertyPair
inlineTextBoxEdgePair value =
  inlinePair inlineTextBoxEdgeProp (inlineTextBoxEdgeValue value)

inlineTextBoxTrimPair : TextBoxTrim -> InlinePropertyPair
inlineTextBoxTrimPair value =
  inlinePair inlineTextBoxTrimProp (inlineTextBoxTrimValue value)

inlineVerticalAlignPair : VerticalAlign -> InlinePropertyPair
inlineVerticalAlignPair value =
  inlinePair inlineVerticalAlignProp (inlineVerticalAlignValue value)

renderInlinePropertyPair : InlinePropertyPair -> String
renderInlinePropertyPair (inlinePair propertyName propertyValue) =
  renderInlinePropertyName propertyName ++ ": " ++
  renderInlinePropertyValue propertyName propertyValue