module FF.CSS.Spec.Safe.Value.List 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
; RawValue
; StringToken
; renderCustomIdent
; renderRawValue
; renderStringToken
)
open import FF.CSS.Spec.Safe.Value.Unit using (Integer; renderInteger)
private
infixr 5 _++_
_++_ : String -> String -> String
_++_ = primStringAppend
data ListStylePosition : Type lzero where
listStyleInside listStyleOutside : ListStylePosition
renderListStylePosition : ListStylePosition -> String
renderListStylePosition listStyleInside = "inside"
renderListStylePosition listStyleOutside = "outside"
data PredefinedCounterStyle : Type lzero where
counterDisc counterCircle counterSquare counterDecimal counterCjkDecimal counterDecimalLeadingZero : PredefinedCounterStyle
counterLowerRoman counterUpperRoman counterLowerGreek counterLowerAlpha counterLowerLatin : PredefinedCounterStyle
counterUpperAlpha counterUpperLatin counterArabicIndic counterArmenian counterBengali : PredefinedCounterStyle
counterCambodian counterCjkEarthlyBranch counterCjkHeavenlyStem counterCjkIdeographic : PredefinedCounterStyle
counterDevanagari counterEthiopicNumeric counterGeorgian counterGujarati counterGurmukhi : PredefinedCounterStyle
counterHebrew counterHiragana counterHiraganaIroha counterJapaneseFormal counterJapaneseInformal : PredefinedCounterStyle
counterKannada counterKatakana counterKatakanaIroha counterKhmer counterKoreanHangulFormal : PredefinedCounterStyle
counterKoreanHanjaFormal counterKoreanHanjaInformal counterLao counterLowerArmenian counterMalayalam : PredefinedCounterStyle
counterMongolian counterMyanmar counterOriya counterPersian counterSimpChineseFormal : PredefinedCounterStyle
counterSimpChineseInformal counterTamil counterTelugu counterThai counterTibetan : PredefinedCounterStyle
counterTradChineseFormal counterTradChineseInformal counterUpperArmenian : PredefinedCounterStyle
counterDisclosureOpen counterDisclosureClosed : PredefinedCounterStyle
renderPredefinedCounterStyle : PredefinedCounterStyle -> String
renderPredefinedCounterStyle counterDisc = "disc"
renderPredefinedCounterStyle counterCircle = "circle"
renderPredefinedCounterStyle counterSquare = "square"
renderPredefinedCounterStyle counterDecimal = "decimal"
renderPredefinedCounterStyle counterCjkDecimal = "cjk-decimal"
renderPredefinedCounterStyle counterDecimalLeadingZero = "decimal-leading-zero"
renderPredefinedCounterStyle counterLowerRoman = "lower-roman"
renderPredefinedCounterStyle counterUpperRoman = "upper-roman"
renderPredefinedCounterStyle counterLowerGreek = "lower-greek"
renderPredefinedCounterStyle counterLowerAlpha = "lower-alpha"
renderPredefinedCounterStyle counterLowerLatin = "lower-latin"
renderPredefinedCounterStyle counterUpperAlpha = "upper-alpha"
renderPredefinedCounterStyle counterUpperLatin = "upper-latin"
renderPredefinedCounterStyle counterArabicIndic = "arabic-indic"
renderPredefinedCounterStyle counterArmenian = "armenian"
renderPredefinedCounterStyle counterBengali = "bengali"
renderPredefinedCounterStyle counterCambodian = "cambodian"
renderPredefinedCounterStyle counterCjkEarthlyBranch = "cjk-earthly-branch"
renderPredefinedCounterStyle counterCjkHeavenlyStem = "cjk-heavenly-stem"
renderPredefinedCounterStyle counterCjkIdeographic = "cjk-ideographic"
renderPredefinedCounterStyle counterDevanagari = "devanagari"
renderPredefinedCounterStyle counterEthiopicNumeric = "ethiopic-numeric"
renderPredefinedCounterStyle counterGeorgian = "georgian"
renderPredefinedCounterStyle counterGujarati = "gujarati"
renderPredefinedCounterStyle counterGurmukhi = "gurmukhi"
renderPredefinedCounterStyle counterHebrew = "hebrew"
renderPredefinedCounterStyle counterHiragana = "hiragana"
renderPredefinedCounterStyle counterHiraganaIroha = "hiragana-iroha"
renderPredefinedCounterStyle counterJapaneseFormal = "japanese-formal"
renderPredefinedCounterStyle counterJapaneseInformal = "japanese-informal"
renderPredefinedCounterStyle counterKannada = "kannada"
renderPredefinedCounterStyle counterKatakana = "katakana"
renderPredefinedCounterStyle counterKatakanaIroha = "katakana-iroha"
renderPredefinedCounterStyle counterKhmer = "khmer"
renderPredefinedCounterStyle counterKoreanHangulFormal = "korean-hangul-formal"
renderPredefinedCounterStyle counterKoreanHanjaFormal = "korean-hanja-formal"
renderPredefinedCounterStyle counterKoreanHanjaInformal = "korean-hanja-informal"
renderPredefinedCounterStyle counterLao = "lao"
renderPredefinedCounterStyle counterLowerArmenian = "lower-armenian"
renderPredefinedCounterStyle counterMalayalam = "malayalam"
renderPredefinedCounterStyle counterMongolian = "mongolian"
renderPredefinedCounterStyle counterMyanmar = "myanmar"
renderPredefinedCounterStyle counterOriya = "oriya"
renderPredefinedCounterStyle counterPersian = "persian"
renderPredefinedCounterStyle counterSimpChineseFormal = "simp-chinese-formal"
renderPredefinedCounterStyle counterSimpChineseInformal = "simp-chinese-informal"
renderPredefinedCounterStyle counterTamil = "tamil"
renderPredefinedCounterStyle counterTelugu = "telugu"
renderPredefinedCounterStyle counterThai = "thai"
renderPredefinedCounterStyle counterTibetan = "tibetan"
renderPredefinedCounterStyle counterTradChineseFormal = "trad-chinese-formal"
renderPredefinedCounterStyle counterTradChineseInformal = "trad-chinese-informal"
renderPredefinedCounterStyle counterUpperArmenian = "upper-armenian"
renderPredefinedCounterStyle counterDisclosureOpen = "disclosure-open"
renderPredefinedCounterStyle counterDisclosureClosed = "disclosure-closed"
record CounterStyleName : Type lzero where
constructor counterStyleName
field rawCounterStyleName : CustomIdent
open CounterStyleName public
renderCounterStyleName : CounterStyleName -> String
renderCounterStyleName (counterStyleName value) = renderCustomIdent value
record SymbolsFunction : Type lzero where
constructor symbolsFunction
field rawSymbolsFunction : RawValue
open SymbolsFunction public
renderSymbolsFunction : SymbolsFunction -> String
renderSymbolsFunction (symbolsFunction value) = renderRawValue value
data CounterStyle : Type lzero where
predefinedCounterStyle : PredefinedCounterStyle -> CounterStyle
namedCounterStyle : CounterStyleName -> CounterStyle
symbolsCounterStyle : SymbolsFunction -> CounterStyle
renderCounterStyle : CounterStyle -> String
renderCounterStyle (predefinedCounterStyle value) = renderPredefinedCounterStyle value
renderCounterStyle (namedCounterStyle value) = renderCounterStyleName value
renderCounterStyle (symbolsCounterStyle value) = renderSymbolsFunction value
data ListStyleType : Type lzero where
listStyleTypeNone : ListStyleType
listStyleTypeCounter : CounterStyle -> ListStyleType
listStyleTypeString : StringToken -> ListStyleType
renderListStyleType : ListStyleType -> String
renderListStyleType listStyleTypeNone = "none"
renderListStyleType (listStyleTypeCounter value) = renderCounterStyle value
renderListStyleType (listStyleTypeString value) = renderStringToken value
record ListStyleImageSource : Type lzero where
constructor listStyleImageSource
field rawListStyleImageSource : RawValue
open ListStyleImageSource public
renderListStyleImageSource : ListStyleImageSource -> String
renderListStyleImageSource (listStyleImageSource value) = renderRawValue value
data ListStyleImage : Type lzero where
listStyleImageNone : ListStyleImage
listStyleImageValue : ListStyleImageSource -> ListStyleImage
renderListStyleImage : ListStyleImage -> String
renderListStyleImage listStyleImageNone = "none"
renderListStyleImage (listStyleImageValue value) = renderListStyleImageSource value
data ListStyle : Type lzero where
listStyleTypeOnly : ListStyleType -> ListStyle
listStylePositionOnly : ListStylePosition -> ListStyle
listStyleImageOnly : ListStyleImage -> ListStyle
listStyleTypePosition : ListStyleType -> ListStylePosition -> ListStyle
listStyleTypeImage : ListStyleType -> ListStyleImage -> ListStyle
listStylePositionImage : ListStylePosition -> ListStyleImage -> ListStyle
listStyleFull : ListStyleType -> ListStylePosition -> ListStyleImage -> ListStyle
renderListStyle : ListStyle -> String
renderListStyle (listStyleTypeOnly value) = renderListStyleType value
renderListStyle (listStylePositionOnly value) = renderListStylePosition value
renderListStyle (listStyleImageOnly value) = renderListStyleImage value
renderListStyle (listStyleTypePosition listType position) =
renderListStyleType listType ++ " " ++ renderListStylePosition position
renderListStyle (listStyleTypeImage listType image) =
renderListStyleType listType ++ " " ++ renderListStyleImage image
renderListStyle (listStylePositionImage position image) =
renderListStylePosition position ++ " " ++ renderListStyleImage image
renderListStyle (listStyleFull listType position image) =
renderListStyleType listType ++ " " ++ renderListStylePosition position ++ " " ++ renderListStyleImage image
record CounterName : Type lzero where
constructor counterName
field rawCounterName : CustomIdent
open CounterName public
renderCounterName : CounterName -> String
renderCounterName (counterName value) = renderCustomIdent value
renderReversedCounterName : CounterName -> String
renderReversedCounterName value = "reversed(" ++ renderCounterName value ++ ")"
data CounterChange : Type lzero where
counterChangeName : CounterName -> CounterChange
counterChangeValue : CounterName -> Integer -> CounterChange
renderCounterChange : CounterChange -> String
renderCounterChange (counterChangeName name) = renderCounterName name
renderCounterChange (counterChangeValue name value) =
renderCounterName name ++ " " ++ renderInteger value
data CounterResetItem : Type lzero where
resetCounter : CounterName -> CounterResetItem
resetCounterValue : CounterName -> Integer -> CounterResetItem
resetReversed : CounterName -> CounterResetItem
resetReversedValue : CounterName -> Integer -> CounterResetItem
renderCounterResetItem : CounterResetItem -> String
renderCounterResetItem (resetCounter name) = renderCounterName name
renderCounterResetItem (resetCounterValue name value) =
renderCounterName name ++ " " ++ renderInteger value
renderCounterResetItem (resetReversed name) = renderReversedCounterName name
renderCounterResetItem (resetReversedValue name value) =
renderReversedCounterName name ++ " " ++ renderInteger value
data NonEmptySpaceList (A : Type lzero) : Type lzero where
spaceOne : A -> NonEmptySpaceList A
spaceCons : A -> NonEmptySpaceList A -> NonEmptySpaceList A
renderNonEmptySpaceList : {A : Type lzero} -> (A -> String) -> NonEmptySpaceList A -> String
renderNonEmptySpaceList renderA (spaceOne value) = renderA value
renderNonEmptySpaceList renderA (spaceCons value rest) =
renderA value ++ " " ++ renderNonEmptySpaceList renderA rest
CounterChangeList : Type lzero
CounterChangeList = NonEmptySpaceList CounterChange
renderCounterChangeList : CounterChangeList -> String
renderCounterChangeList value = renderNonEmptySpaceList renderCounterChange value
CounterResetList : Type lzero
CounterResetList = NonEmptySpaceList CounterResetItem
renderCounterResetList : CounterResetList -> String
renderCounterResetList value = renderNonEmptySpaceList renderCounterResetItem value
data CounterIncrement : Type lzero where
counterIncrementNone : CounterIncrement
counterIncrementItems : CounterChangeList -> CounterIncrement
renderCounterIncrement : CounterIncrement -> String
renderCounterIncrement counterIncrementNone = "none"
renderCounterIncrement (counterIncrementItems value) = renderCounterChangeList value
data CounterSet : Type lzero where
counterSetNone : CounterSet
counterSetItems : CounterChangeList -> CounterSet
renderCounterSet : CounterSet -> String
renderCounterSet counterSetNone = "none"
renderCounterSet (counterSetItems value) = renderCounterChangeList value
data CounterReset : Type lzero where
counterResetNone : CounterReset
counterResetItems : CounterResetList -> CounterReset
renderCounterReset : CounterReset -> String
renderCounterReset counterResetNone = "none"
renderCounterReset (counterResetItems value) = renderCounterResetList value
data ListCounterPropertyName : Type lzero where
listCounterStylePositionProp listCounterStyleTypeProp listCounterStyleImageProp listCounterStyleProp : ListCounterPropertyName
listCounterResetProp listCounterIncrementProp listCounterSetProp : ListCounterPropertyName
renderListCounterPropertyName : ListCounterPropertyName -> String
renderListCounterPropertyName listCounterStylePositionProp = "list-style-position"
renderListCounterPropertyName listCounterStyleTypeProp = "list-style-type"
renderListCounterPropertyName listCounterStyleImageProp = "list-style-image"
renderListCounterPropertyName listCounterStyleProp = "list-style"
renderListCounterPropertyName listCounterResetProp = "counter-reset"
renderListCounterPropertyName listCounterIncrementProp = "counter-increment"
renderListCounterPropertyName listCounterSetProp = "counter-set"
data ListCounterPropertyValue : ListCounterPropertyName -> Type lzero where
listCounterStylePositionValue : ListStylePosition -> ListCounterPropertyValue listCounterStylePositionProp
listCounterStyleTypeValue : ListStyleType -> ListCounterPropertyValue listCounterStyleTypeProp
listCounterStyleImageValue : ListStyleImage -> ListCounterPropertyValue listCounterStyleImageProp
listCounterStyleValue : ListStyle -> ListCounterPropertyValue listCounterStyleProp
listCounterResetValue : CounterReset -> ListCounterPropertyValue listCounterResetProp
listCounterIncrementValue : CounterIncrement -> ListCounterPropertyValue listCounterIncrementProp
listCounterSetValue : CounterSet -> ListCounterPropertyValue listCounterSetProp
renderListCounterPropertyValue :
(propertyName : ListCounterPropertyName) -> ListCounterPropertyValue propertyName -> String
renderListCounterPropertyValue listCounterStylePositionProp (listCounterStylePositionValue value) =
renderListStylePosition value
renderListCounterPropertyValue listCounterStyleTypeProp (listCounterStyleTypeValue value) =
renderListStyleType value
renderListCounterPropertyValue listCounterStyleImageProp (listCounterStyleImageValue value) =
renderListStyleImage value
renderListCounterPropertyValue listCounterStyleProp (listCounterStyleValue value) =
renderListStyle value
renderListCounterPropertyValue listCounterResetProp (listCounterResetValue value) =
renderCounterReset value
renderListCounterPropertyValue listCounterIncrementProp (listCounterIncrementValue value) =
renderCounterIncrement value
renderListCounterPropertyValue listCounterSetProp (listCounterSetValue value) =
renderCounterSet value
record ListCounterDeclaration : Type lzero where
constructor listCounterDeclaration
field
propertyName : ListCounterPropertyName
propertyValue : ListCounterPropertyValue propertyName
open ListCounterDeclaration public
renderListCounterDeclaration : ListCounterDeclaration -> String
renderListCounterDeclaration (listCounterDeclaration propertyName propertyValue) =
renderListCounterPropertyName propertyName ++ ": " ++
renderListCounterPropertyValue propertyName propertyValue