{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeFamilies #-}
module Units.Simple.Unit where

import Data.Proxy
import GHC.TypeLits hiding (type (<=))

import Fcf hiding (type (<=))

import Units.Simple.Internals (Show', Intersperse, Sort, type (<=))

data Unit = Meter
          | Kilogram
          | Second
          | Ampere
          | Kelvin
          | Mole
          | Candela
  deriving (Unit -> Unit -> Bool
(Unit -> Unit -> Bool) -> (Unit -> Unit -> Bool) -> Eq Unit
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Unit -> Unit -> Bool
$c/= :: Unit -> Unit -> Bool
== :: Unit -> Unit -> Bool
$c== :: Unit -> Unit -> Bool
Eq, Eq Unit
Eq Unit
-> (Unit -> Unit -> Ordering)
-> (Unit -> Unit -> Bool)
-> (Unit -> Unit -> Bool)
-> (Unit -> Unit -> Bool)
-> (Unit -> Unit -> Bool)
-> (Unit -> Unit -> Unit)
-> (Unit -> Unit -> Unit)
-> Ord Unit
Unit -> Unit -> Bool
Unit -> Unit -> Ordering
Unit -> Unit -> Unit
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Unit -> Unit -> Unit
$cmin :: Unit -> Unit -> Unit
max :: Unit -> Unit -> Unit
$cmax :: Unit -> Unit -> Unit
>= :: Unit -> Unit -> Bool
$c>= :: Unit -> Unit -> Bool
> :: Unit -> Unit -> Bool
$c> :: Unit -> Unit -> Bool
<= :: Unit -> Unit -> Bool
$c<= :: Unit -> Unit -> Bool
< :: Unit -> Unit -> Bool
$c< :: Unit -> Unit -> Bool
compare :: Unit -> Unit -> Ordering
$ccompare :: Unit -> Unit -> Ordering
$cp1Ord :: Eq Unit
Ord, Int -> Unit -> ShowS
[Unit] -> ShowS
Unit -> String
(Int -> Unit -> ShowS)
-> (Unit -> String) -> ([Unit] -> ShowS) -> Show Unit
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Unit] -> ShowS
$cshowList :: [Unit] -> ShowS
show :: Unit -> String
$cshow :: Unit -> String
showsPrec :: Int -> Unit -> ShowS
$cshowsPrec :: Int -> Unit -> ShowS
Show)

type Unit' = (Unit, Nat)
type Units = ([Unit'], [Unit'])

type family UnitSymbol (u :: Unit) :: Symbol
type instance UnitSymbol 'Meter = "m"
type instance UnitSymbol 'Second = "s"
type instance UnitSymbol 'Kilogram = "kg"
type instance UnitSymbol 'Ampere = "A"
type instance UnitSymbol 'Kelvin = "K"
type instance UnitSymbol 'Mole = "mol"
type instance UnitSymbol 'Candela = "cd"

data ShowUnit :: Unit' -> Exp Symbol
type instance Eval (ShowUnit '(u, n)) =
  If (Eval (TyEq n 1))
     (UnitSymbol u)
     (UnitSymbol u `AppendSymbol` "^" `AppendSymbol` Eval (Show' n))

type ShowUnitList (ul :: [Unit']) = Eval (Intersperse "*" =<< Map ShowUnit =<< Sort ul)

type UnitRepr' (num :: [Unit']) (denom :: [Unit']) =
  If (Eval (Eval (Null num) && Eval (Null denom)))
     "<adimensional>"
     (If (Eval (Null denom))
         (ShowUnitList num)
         (If (Eval (Null num))
              ("1/" `AppendSymbol` ShowUnitList denom)
              (ShowUnitList num `AppendSymbol` "/" `AppendSymbol` ShowUnitList denom)))

type UnitRepr (us :: Units) = UnitRepr' (Eval (Fst us)) (Eval (Snd us))

-- | A string representation of 'Units'. Useful for debugging.
showUnits :: forall us. KnownSymbol (UnitRepr us) => String
showUnits :: String
showUnits = Proxy
  (If
     (Eval (Eval (Null (Eval (Fst us))) && Eval (Null (Eval (Snd us)))))
     "<adimensional>"
     (If
        (Eval (Null (Eval (Snd us))))
        (Eval
           (Intersperse
              "*" (Eval (Map ShowUnit (Eval (Sort (Eval (Fst us))))))))
        (If
           (Eval (Null (Eval (Fst us))))
           (AppendSymbol
              "1/"
              (Eval
                 (Intersperse
                    "*" (Eval (Map ShowUnit (Eval (Sort (Eval (Snd us)))))))))
           (AppendSymbol
              (AppendSymbol
                 (Eval
                    (Intersperse
                       "*" (Eval (Map ShowUnit (Eval (Sort (Eval (Fst us))))))))
                 "/")
              (Eval
                 (Intersperse
                    "*" (Eval (Map ShowUnit (Eval (Sort (Eval (Snd us))))))))))))
-> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (Proxy (UnitRepr us)
forall k (t :: k). Proxy t
Proxy @(UnitRepr us))

type instance Eval ((a :: Unit) <= (b :: Unit)) = Eval (UnitSymbol a <= UnitSymbol b)