module FF.CSS.Spec.Safe.Value.GeneratedContent 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
  ; StringToken
  ; renderRawValue
  ; renderStringToken
  )

private
  infixr 5 _++_

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

-- MDN CSS Generated Content property values:
-- https://developer.mozilla.org/en-US/docs/Web/CSS/CSS_generated_content

record ContentReplacement : Type lzero where
  constructor generatedContentReplacement
  field rawContentReplacement : RawValue

open ContentReplacement public

renderContentReplacement : ContentReplacement -> String
renderContentReplacement (generatedContentReplacement value) = renderRawValue value

record ContentList : Type lzero where
  constructor generatedContentList
  field rawContentList : RawValue

open ContentList public

renderContentList : ContentList -> String
renderContentList (generatedContentList value) = renderRawValue value

record ContentCounter : Type lzero where
  constructor generatedContentCounter
  field rawContentCounter : RawValue

open ContentCounter public

renderContentCounter : ContentCounter -> String
renderContentCounter (generatedContentCounter value) = renderRawValue value

record ContentAttr : Type lzero where
  constructor generatedContentAttr
  field rawContentAttr : RawValue

open ContentAttr public

renderContentAttr : ContentAttr -> String
renderContentAttr (generatedContentAttr value) = renderRawValue value

data ContentPayload : Type lzero where
  generatedContentPayloadReplacement : ContentReplacement -> ContentPayload
  generatedContentPayloadList        : ContentList -> ContentPayload

renderContentPayload : ContentPayload -> String
renderContentPayload (generatedContentPayloadReplacement value) =
  renderContentReplacement value
renderContentPayload (generatedContentPayloadList value) = renderContentList value

data ContentAltTextPart : Type lzero where
  generatedContentAltTextString  : StringToken -> ContentAltTextPart
  generatedContentAltTextCounter : ContentCounter -> ContentAltTextPart
  generatedContentAltTextAttr    : ContentAttr -> ContentAltTextPart

renderContentAltTextPart : ContentAltTextPart -> String
renderContentAltTextPart (generatedContentAltTextString value) = renderStringToken value
renderContentAltTextPart (generatedContentAltTextCounter value) = renderContentCounter value
renderContentAltTextPart (generatedContentAltTextAttr value) = renderContentAttr value

data ContentAltText : Type lzero where
  generatedContentAltTextOne  : ContentAltTextPart -> ContentAltText
  generatedContentAltTextCons : ContentAltTextPart -> ContentAltText -> ContentAltText

renderContentAltText : ContentAltText -> String
renderContentAltText (generatedContentAltTextOne value) = renderContentAltTextPart value
renderContentAltText (generatedContentAltTextCons value rest) =
  renderContentAltTextPart value ++ " " ++ renderContentAltText rest

data Content : Type lzero where
  generatedContentNormal         : Content
  generatedContentNone           : Content
  generatedContentPayload        : ContentPayload -> Content
  generatedContentPayloadWithAlt : ContentPayload -> ContentAltText -> Content

renderContent : Content -> String
renderContent generatedContentNormal = "normal"
renderContent generatedContentNone = "none"
renderContent (generatedContentPayload value) = renderContentPayload value
renderContent (generatedContentPayloadWithAlt value altText) =
  renderContentPayload value ++ " / " ++ renderContentAltText altText

data QuotePair : Type lzero where
  generatedContentQuotePair : StringToken -> StringToken -> QuotePair

renderQuotePair : QuotePair -> String
renderQuotePair (generatedContentQuotePair openQuote closeQuote) =
  renderStringToken openQuote ++ " " ++ renderStringToken closeQuote

data QuotePairList : Type lzero where
  generatedContentQuotePairOne  : QuotePair -> QuotePairList
  generatedContentQuotePairCons : QuotePair -> QuotePairList -> QuotePairList

renderQuotePairList : QuotePairList -> String
renderQuotePairList (generatedContentQuotePairOne value) = renderQuotePair value
renderQuotePairList (generatedContentQuotePairCons value rest) =
  renderQuotePair value ++ " " ++ renderQuotePairList rest

data Quotes : Type lzero where
  generatedContentQuotesNone  : Quotes
  generatedContentQuotesAuto  : Quotes
  generatedContentQuotesPairs : QuotePairList -> Quotes

renderQuotes : Quotes -> String
renderQuotes generatedContentQuotesNone = "none"
renderQuotes generatedContentQuotesAuto = "auto"
renderQuotes (generatedContentQuotesPairs value) = renderQuotePairList value

data GeneratedContentPropertyName : Type lzero where
  generatedContentContentProp : GeneratedContentPropertyName
  generatedContentQuotesProp  : GeneratedContentPropertyName

renderGeneratedContentPropertyName : GeneratedContentPropertyName -> String
renderGeneratedContentPropertyName generatedContentContentProp = "content"
renderGeneratedContentPropertyName generatedContentQuotesProp = "quotes"

data GeneratedContentPropertyValue : GeneratedContentPropertyName -> Type lzero where
  generatedContentContentValue :
    Content -> GeneratedContentPropertyValue generatedContentContentProp
  generatedContentQuotesValue :
    Quotes -> GeneratedContentPropertyValue generatedContentQuotesProp

renderGeneratedContentPropertyValue :
  (propertyName : GeneratedContentPropertyName) ->
  GeneratedContentPropertyValue propertyName ->
  String
renderGeneratedContentPropertyValue
  generatedContentContentProp
  (generatedContentContentValue value) =
  renderContent value
renderGeneratedContentPropertyValue
  generatedContentQuotesProp
  (generatedContentQuotesValue value) =
  renderQuotes value

record GeneratedContentPropertyPair : Type lzero where
  constructor generatedContentPair
  field
    generatedContentPairName  : GeneratedContentPropertyName
    generatedContentPairValue : GeneratedContentPropertyValue generatedContentPairName

open GeneratedContentPropertyPair public

generatedContentContentPair : Content -> GeneratedContentPropertyPair
generatedContentContentPair value =
  generatedContentPair generatedContentContentProp (generatedContentContentValue value)

generatedContentQuotesPair : Quotes -> GeneratedContentPropertyPair
generatedContentQuotesPair value =
  generatedContentPair generatedContentQuotesProp (generatedContentQuotesValue value)

renderGeneratedContentPropertyPair : GeneratedContentPropertyPair -> String
renderGeneratedContentPropertyPair (generatedContentPair propertyName value) =
  renderGeneratedContentPropertyName propertyName ++ ": " ++
  renderGeneratedContentPropertyValue propertyName value