module FF.CSS.Spec.Safe where

open import Agda.Builtin.String using (String)
open import Agda.Primitive using (lzero) renaming (Set to Type)

open import FF.CSS.Core using (Spec; Declaration; Map; declare; composeMap)
open import FF.CSS.Render using (Renderer; renderDeclaration; renderVia)
import FF.CSS.Spec.Common as Common
import FF.CSS.Spec.Loose as Loose
open import FF.CSS.Spec.Safe.Property public
open import FF.CSS.Spec.Safe.Value public

spec : Spec lzero lzero
spec =
  record
    { Property = PropertyName
    ; Value = CssValue
    }

DeclarationT : Type lzero
DeclarationT = Declaration spec

renderer : Renderer spec
renderer =
  record
    { renderProperty = propertyString
    ; renderValue = valueString
    }

declaration : (propertyName : PropertyName) -> CssValue propertyName -> DeclarationT
declaration = declare

toCommon : Map spec Common.spec
toCommon =
  record
    { mapProperty = \ propertyName -> propertyName
    ; mapValue = valueString
    }

toLoose : Map spec Loose.spec
toLoose = composeMap Common.toLoose toCommon

renderedByCommonRenderer : DeclarationT -> String
renderedByCommonRenderer = renderVia toCommon Common.renderer

renderedByLooseRenderer : DeclarationT -> String
renderedByLooseRenderer = renderVia toLoose Loose.renderer

example : DeclarationT
example =
  declare colorProp (specific (colorValue (named rebeccapurple)))

renderedExample : String
renderedExample = renderDeclaration renderer example