module FF.CSS.Core where

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

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

record Spec (property value : Level)
  : Type (lsuc (levelOf property value)) where
  field
    Property : Type property
    Value    : Property -> Type value

open Spec public

data Declaration
  {property value : Level}
  (S : Spec property value)
  : Type (property lmax value) where
  declare : (propertyName : Property S) -> Value S propertyName -> Declaration S

record Map
  {property value property' value' : Level}
  (From : Spec property value)
  (To : Spec property' value')
  : Type (levelOf property value lmax levelOf property' value') where
  field
    mapProperty : Property From -> Property To
    mapValue    :
      (propertyName : Property From) ->
      Value From propertyName ->
      Value To (mapProperty propertyName)

open Map public

mapDeclaration :
  {property value property' value' : Level}
  {From : Spec property value}
  {To : Spec property' value'}
  (f : Map From To) ->
  Declaration From ->
  Declaration To
mapDeclaration f (declare propertyName value) =
  declare (Map.mapProperty f propertyName) (Map.mapValue f propertyName value)

idMap :
  {property value : Level}
  {S : Spec property value} ->
  Map S S
idMap =
  record
    { mapProperty = \ propertyName -> propertyName
    ; mapValue = \ propertyName value -> value
    }

composeMap :
  {propertyA valueA propertyB valueB propertyC valueC : Level}
  {A : Spec propertyA valueA}
  {B : Spec propertyB valueB}
  {C : Spec propertyC valueC} ->
  Map B C ->
  Map A B ->
  Map A C
composeMap g f =
  record
    { mapProperty = \ propertyName ->
        Map.mapProperty g (Map.mapProperty f propertyName)
    ; mapValue = \ propertyName value ->
        Map.mapValue g (Map.mapProperty f propertyName) (Map.mapValue f propertyName value)
    }