module FF.CSS.Spec.Safe.Value.Image 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 (Angle; renderAngle)
private
infixr 5 _++_
_++_ : String -> String -> String
_++_ = primStringAppend
data ImageOrientation : Type lzero where
imageOrientationFromImage : ImageOrientation
imageOrientationAngle : Angle -> ImageOrientation
imageOrientationFlip : ImageOrientation
imageOrientationAngleFlip : Angle -> ImageOrientation
renderImageOrientation : ImageOrientation -> String
renderImageOrientation imageOrientationFromImage = "from-image"
renderImageOrientation (imageOrientationAngle value) = renderAngle value
renderImageOrientation imageOrientationFlip = "flip"
renderImageOrientation (imageOrientationAngleFlip value) =
renderAngle value ++ " flip"
data ImageRendering : Type lzero where
imageRenderingAuto : ImageRendering
imageRenderingCrispEdges : ImageRendering
imageRenderingPixelated : ImageRendering
imageRenderingSmooth : ImageRendering
renderImageRendering : ImageRendering -> String
renderImageRendering imageRenderingAuto = "auto"
renderImageRendering imageRenderingCrispEdges = "crisp-edges"
renderImageRendering imageRenderingPixelated = "pixelated"
renderImageRendering imageRenderingSmooth = "smooth"
data ObjectFit : Type lzero where
objectFitFill : ObjectFit
objectFitContain : ObjectFit
objectFitCover : ObjectFit
objectFitNone : ObjectFit
objectFitScaleDown : ObjectFit
renderObjectFit : ObjectFit -> String
renderObjectFit objectFitFill = "fill"
renderObjectFit objectFitContain = "contain"
renderObjectFit objectFitCover = "cover"
renderObjectFit objectFitNone = "none"
renderObjectFit objectFitScaleDown = "scale-down"
record ObjectPosition : Type lzero where
constructor objectPosition
field rawObjectPosition : RawValue
open ObjectPosition public
renderObjectPosition : ObjectPosition -> String
renderObjectPosition (objectPosition value) = renderRawValue value
data CssImagesPropertyName : Type lzero where
cssImagesImageOrientationProp : CssImagesPropertyName
cssImagesImageRenderingProp : CssImagesPropertyName
cssImagesObjectFitProp : CssImagesPropertyName
cssImagesObjectPositionProp : CssImagesPropertyName
renderCssImagesPropertyName : CssImagesPropertyName -> String
renderCssImagesPropertyName cssImagesImageOrientationProp = "image-orientation"
renderCssImagesPropertyName cssImagesImageRenderingProp = "image-rendering"
renderCssImagesPropertyName cssImagesObjectFitProp = "object-fit"
renderCssImagesPropertyName cssImagesObjectPositionProp = "object-position"
data CssImagesPropertyValue : CssImagesPropertyName -> Type lzero where
cssImagesImageOrientationValue :
ImageOrientation -> CssImagesPropertyValue cssImagesImageOrientationProp
cssImagesImageRenderingValue :
ImageRendering -> CssImagesPropertyValue cssImagesImageRenderingProp
cssImagesObjectFitValue :
ObjectFit -> CssImagesPropertyValue cssImagesObjectFitProp
cssImagesObjectPositionValue :
ObjectPosition -> CssImagesPropertyValue cssImagesObjectPositionProp
renderCssImagesPropertyValue :
(propertyName : CssImagesPropertyName) ->
CssImagesPropertyValue propertyName ->
String
renderCssImagesPropertyValue
cssImagesImageOrientationProp
(cssImagesImageOrientationValue value) =
renderImageOrientation value
renderCssImagesPropertyValue
cssImagesImageRenderingProp
(cssImagesImageRenderingValue value) =
renderImageRendering value
renderCssImagesPropertyValue
cssImagesObjectFitProp
(cssImagesObjectFitValue value) =
renderObjectFit value
renderCssImagesPropertyValue
cssImagesObjectPositionProp
(cssImagesObjectPositionValue value) =
renderObjectPosition value
record CssImagesPropertyPair : Type lzero where
constructor cssImagesPair
field
cssImagesPairName : CssImagesPropertyName
cssImagesPairValue : CssImagesPropertyValue cssImagesPairName
open CssImagesPropertyPair public
renderCssImagesPropertyPair : CssImagesPropertyPair -> String
renderCssImagesPropertyPair (cssImagesPair propertyName propertyValue) =
renderCssImagesPropertyName propertyName ++ ": " ++
renderCssImagesPropertyValue propertyName propertyValue