module FF.CSS.Spec.Safe.Value.Filter 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.Color using (Color; renderColor)
open import FF.CSS.Spec.Safe.Value.Unit using
( Number
; Percentage
; renderNumber
; renderPercentage
)
private
infixr 5 _++_
_++_ : String -> String -> String
_++_ = primStringAppend
record FilterValueList : Type lzero where
constructor filterValueListRaw
field rawFilterValueList : RawValue
open FilterValueList public
renderFilterValueList : FilterValueList -> String
renderFilterValueList (filterValueListRaw value) = renderRawValue value
data Filter : Type lzero where
filterNone : Filter
filterValueList : FilterValueList -> Filter
renderFilter : Filter -> String
renderFilter filterNone = "none"
renderFilter (filterValueList value) = renderFilterValueList value
data BackdropFilter : Type lzero where
backdropFilterNone : BackdropFilter
backdropFilterValueList : FilterValueList -> BackdropFilter
renderBackdropFilter : BackdropFilter -> String
renderBackdropFilter backdropFilterNone = "none"
renderBackdropFilter (backdropFilterValueList value) = renderFilterValueList value
data ColorInterpolationFilters : Type lzero where
colorInterpolationFiltersAuto : ColorInterpolationFilters
colorInterpolationFiltersSRGB : ColorInterpolationFilters
colorInterpolationFiltersLinearRGB : ColorInterpolationFilters
renderColorInterpolationFilters : ColorInterpolationFilters -> String
renderColorInterpolationFilters colorInterpolationFiltersAuto = "auto"
renderColorInterpolationFilters colorInterpolationFiltersSRGB = "sRGB"
renderColorInterpolationFilters colorInterpolationFiltersLinearRGB = "linearRGB"
data FloodOpacity : Type lzero where
floodOpacityNumber : Number -> FloodOpacity
floodOpacityPercentage : Percentage -> FloodOpacity
renderFloodOpacity : FloodOpacity -> String
renderFloodOpacity (floodOpacityNumber value) = renderNumber value
renderFloodOpacity (floodOpacityPercentage value) = renderPercentage value
FloodColor : Type lzero
FloodColor = Color
renderFloodColor : FloodColor -> String
renderFloodColor value = renderColor value
LightingColor : Type lzero
LightingColor = Color
renderLightingColor : LightingColor -> String
renderLightingColor value = renderColor value
data FilterEffectsPropertyName : Type lzero where
filterEffectsFilterProp : FilterEffectsPropertyName
filterEffectsBackdropFilterProp : FilterEffectsPropertyName
filterEffectsColorInterpolationFiltersProp : FilterEffectsPropertyName
filterEffectsFloodColorProp : FilterEffectsPropertyName
filterEffectsFloodOpacityProp : FilterEffectsPropertyName
filterEffectsLightingColorProp : FilterEffectsPropertyName
renderFilterEffectsPropertyName : FilterEffectsPropertyName -> String
renderFilterEffectsPropertyName filterEffectsFilterProp = "filter"
renderFilterEffectsPropertyName filterEffectsBackdropFilterProp = "backdrop-filter"
renderFilterEffectsPropertyName filterEffectsColorInterpolationFiltersProp = "color-interpolation-filters"
renderFilterEffectsPropertyName filterEffectsFloodColorProp = "flood-color"
renderFilterEffectsPropertyName filterEffectsFloodOpacityProp = "flood-opacity"
renderFilterEffectsPropertyName filterEffectsLightingColorProp = "lighting-color"
data FilterEffectsPropertyValue : FilterEffectsPropertyName -> Type lzero where
filterEffectsFilterValue :
Filter -> FilterEffectsPropertyValue filterEffectsFilterProp
filterEffectsBackdropFilterValue :
BackdropFilter -> FilterEffectsPropertyValue filterEffectsBackdropFilterProp
filterEffectsColorInterpolationFiltersValue :
ColorInterpolationFilters ->
FilterEffectsPropertyValue filterEffectsColorInterpolationFiltersProp
filterEffectsFloodColorValue :
FloodColor -> FilterEffectsPropertyValue filterEffectsFloodColorProp
filterEffectsFloodOpacityValue :
FloodOpacity -> FilterEffectsPropertyValue filterEffectsFloodOpacityProp
filterEffectsLightingColorValue :
LightingColor -> FilterEffectsPropertyValue filterEffectsLightingColorProp
renderFilterEffectsPropertyValue :
(propertyName : FilterEffectsPropertyName) ->
FilterEffectsPropertyValue propertyName ->
String
renderFilterEffectsPropertyValue filterEffectsFilterProp (filterEffectsFilterValue value) =
renderFilter value
renderFilterEffectsPropertyValue filterEffectsBackdropFilterProp (filterEffectsBackdropFilterValue value) =
renderBackdropFilter value
renderFilterEffectsPropertyValue
filterEffectsColorInterpolationFiltersProp
(filterEffectsColorInterpolationFiltersValue value) =
renderColorInterpolationFilters value
renderFilterEffectsPropertyValue filterEffectsFloodColorProp (filterEffectsFloodColorValue value) =
renderFloodColor value
renderFilterEffectsPropertyValue filterEffectsFloodOpacityProp (filterEffectsFloodOpacityValue value) =
renderFloodOpacity value
renderFilterEffectsPropertyValue filterEffectsLightingColorProp (filterEffectsLightingColorValue value) =
renderLightingColor value
record FilterEffectsPropertyPair : Type lzero where
constructor filterEffectsPair
field
filterEffectsPairName : FilterEffectsPropertyName
filterEffectsPairValue : FilterEffectsPropertyValue filterEffectsPairName
open FilterEffectsPropertyPair public
renderFilterEffectsPropertyPair : FilterEffectsPropertyPair -> String
renderFilterEffectsPropertyPair (filterEffectsPair propertyName propertyValue) =
renderFilterEffectsPropertyName propertyName ++ ": " ++
renderFilterEffectsPropertyValue propertyName propertyValue