module FF.CSS.Render where

open import Agda.Builtin.String using (String; primStringAppend)
open import Agda.Primitive using (Level) renaming (Set to Type; _⊔_ to _lmax_)
open import Cubical.Foundations.Prelude using ()

open import FF.CSS.Core

infixr  _++_

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

private
  levelOf : Level -> Level -> Level
  levelOf property value = property lmax value

record Renderer
  {property value : Level}
  (S : Spec property value)
  : Type (levelOf property value) where
  field
    renderProperty : Property S -> String
    renderValue    : (propertyName : Property S) -> Value S propertyName -> String

open Renderer public

renderDeclaration :
  {property value : Level}
  {S : Spec property value} ->
  Renderer S ->
  Declaration S ->
  String
renderDeclaration renderer (declare propertyName value) =
  Renderer.renderProperty renderer propertyName ++ ": " ++
  Renderer.renderValue renderer propertyName value

renderDeclarationWithSemicolon :
  {property value : Level}
  {S : Spec property value} ->
  Renderer S ->
  Declaration S ->
  String
renderDeclarationWithSemicolon renderer declaration =
  renderDeclaration renderer declaration ++ ";"

pullRenderer :
  {property value property' value' : Level}
  {From : Spec property value}
  {To : Spec property' value'} ->
  Map From To ->
  Renderer To ->
  Renderer From
pullRenderer f renderer =
  record
    { renderProperty = \ propertyName ->
        Renderer.renderProperty renderer (Map.mapProperty f propertyName)
    ; renderValue = \ propertyName value ->
        Renderer.renderValue renderer (Map.mapProperty f propertyName) (Map.mapValue f propertyName value)
    }

renderVia :
  {property value property' value' : Level}
  {From : Spec property value}
  {To : Spec property' value'} ->
  Map From To ->
  Renderer To ->
  Declaration From ->
  String
renderVia f renderer declaration = renderDeclaration renderer (mapDeclaration f declaration)