module FF.CSS.Spec.Safe.Value.Unit where

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

private
  infixr 5 _++_

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

-- MDN numeric data types:
-- https://developer.mozilla.org/en-US/docs/Web/CSS/Guides/Values_and_units/Numeric_data_types
record Number : Type lzero where
  constructor number
  field rawNumber : String

open Number public

renderNumber : Number -> String
renderNumber (number raw) = raw

record Integer : Type lzero where
  constructor integer
  field rawInteger : String

open Integer public

renderInteger : Integer -> String
renderInteger (integer raw) = raw

record Percentage : Type lzero where
  constructor percentage
  field rawPercentage : String

open Percentage public

renderPercentage : Percentage -> String
renderPercentage (percentage raw) = raw ++ "%"

record Ratio : Type lzero where
  constructor ratio
  field numerator denominator : Number

open Ratio public

renderRatio : Ratio -> String
renderRatio (ratio numerator denominator) =
  renderNumber numerator ++ " / " ++ renderNumber denominator

data LengthUnit : Type lzero where
  px em rem ex ch lh rlh vw vh vmin vmax vi vb svw svh lvw lvh dvw dvh cqw cqh cqi cqb cqmin cqmax cm mm q inch pt pc : LengthUnit

renderLengthUnit : LengthUnit -> String
renderLengthUnit px = "px"
renderLengthUnit em = "em"
renderLengthUnit rem = "rem"
renderLengthUnit ex = "ex"
renderLengthUnit ch = "ch"
renderLengthUnit lh = "lh"
renderLengthUnit rlh = "rlh"
renderLengthUnit vw = "vw"
renderLengthUnit vh = "vh"
renderLengthUnit vmin = "vmin"
renderLengthUnit vmax = "vmax"
renderLengthUnit vi = "vi"
renderLengthUnit vb = "vb"
renderLengthUnit svw = "svw"
renderLengthUnit svh = "svh"
renderLengthUnit lvw = "lvw"
renderLengthUnit lvh = "lvh"
renderLengthUnit dvw = "dvw"
renderLengthUnit dvh = "dvh"
renderLengthUnit cqw = "cqw"
renderLengthUnit cqh = "cqh"
renderLengthUnit cqi = "cqi"
renderLengthUnit cqb = "cqb"
renderLengthUnit cqmin = "cqmin"
renderLengthUnit cqmax = "cqmax"
renderLengthUnit cm = "cm"
renderLengthUnit mm = "mm"
renderLengthUnit q = "Q"
renderLengthUnit inch = "in"
renderLengthUnit pt = "pt"
renderLengthUnit pc = "pc"

data AngleUnit : Type lzero where
  deg grad rad turn : AngleUnit

renderAngleUnit : AngleUnit -> String
renderAngleUnit deg = "deg"
renderAngleUnit grad = "grad"
renderAngleUnit rad = "rad"
renderAngleUnit turn = "turn"

data TimeUnit : Type lzero where
  s ms : TimeUnit

renderTimeUnit : TimeUnit -> String
renderTimeUnit s = "s"
renderTimeUnit ms = "ms"

data FrequencyUnit : Type lzero where
  hz khz : FrequencyUnit

renderFrequencyUnit : FrequencyUnit -> String
renderFrequencyUnit hz = "Hz"
renderFrequencyUnit khz = "kHz"

data ResolutionUnit : Type lzero where
  dpi dpcm dppx x : ResolutionUnit

renderResolutionUnit : ResolutionUnit -> String
renderResolutionUnit dpi = "dpi"
renderResolutionUnit dpcm = "dpcm"
renderResolutionUnit dppx = "dppx"
renderResolutionUnit x = "x"

data FlexUnit : Type lzero where
  fr : FlexUnit

renderFlexUnit : FlexUnit -> String
renderFlexUnit fr = "fr"

record Dimension (Unit : Type lzero) : Type lzero where
  constructor dimension
  field
    magnitude : Number
    unit      : Unit

open Dimension public

renderDimension : {Unit : Type lzero} -> (Unit -> String) -> Dimension Unit -> String
renderDimension renderUnit (dimension magnitude unit) =
  renderNumber magnitude ++ renderUnit unit

data Length : Type lzero where
  zeroLength : Length
  length     : Dimension LengthUnit -> Length

renderLength : Length -> String
renderLength zeroLength = "0"
renderLength (length dim) = renderDimension renderLengthUnit dim

data LengthPercentage : Type lzero where
  lengthValue     : Length -> LengthPercentage
  percentageValue : Percentage -> LengthPercentage
  calcLengthPercentage : String -> LengthPercentage

renderLengthPercentage : LengthPercentage -> String
renderLengthPercentage (lengthValue value) = renderLength value
renderLengthPercentage (percentageValue value) = renderPercentage value
renderLengthPercentage (calcLengthPercentage value) = value

data LengthPercentageAuto : Type lzero where
  auto                  : LengthPercentageAuto
  lengthPercentageValue : LengthPercentage -> LengthPercentageAuto

renderLengthPercentageAuto : LengthPercentageAuto -> String
renderLengthPercentageAuto auto = "auto"
renderLengthPercentageAuto (lengthPercentageValue value) = renderLengthPercentage value

data Angle : Type lzero where
  angle : Dimension AngleUnit -> Angle

renderAngle : Angle -> String
renderAngle (angle dim) = renderDimension renderAngleUnit dim

data Time : Type lzero where
  time : Dimension TimeUnit -> Time

renderTime : Time -> String
renderTime (time dim) = renderDimension renderTimeUnit dim

data Frequency : Type lzero where
  frequency : Dimension FrequencyUnit -> Frequency

renderFrequency : Frequency -> String
renderFrequency (frequency dim) = renderDimension renderFrequencyUnit dim

data Resolution : Type lzero where
  resolution : Dimension ResolutionUnit -> Resolution

renderResolution : Resolution -> String
renderResolution (resolution dim) = renderDimension renderResolutionUnit dim

data Flex : Type lzero where
  flex : Dimension FlexUnit -> Flex

renderFlex : Flex -> String
renderFlex (flex dim) = renderDimension renderFlexUnit dim