{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}

-- | This module defines singleton types for integers and concrete
-- units.
module Data.UnitsOfMeasure.Singleton
    ( -- * Singletons for units
      SUnit(..)
    , forgetSUnit
    , KnownUnit(..)
    , unitVal
    , testEquivalentSUnit

      -- * Singletons for lists
    , SList(..)
    , KnownList(..)
    ) where

import GHC.TypeLits
import Data.List (foldl')
import qualified Data.Map as Map
import Data.Type.Equality
import Unsafe.Coerce

import Data.UnitsOfMeasure.Internal


-- | Singleton type for concrete units of measure represented as lists
-- of base units
data SUnit (u :: UnitSyntax Symbol) where
  SUnit :: SList xs -> SList ys -> SUnit (xs :/ ys)

-- | Singleton type for lists of base units
data SList (xs :: [Symbol]) where
  SNil :: SList '[]
  SCons :: KnownSymbol x => proxy x -> SList xs -> SList (x ': xs)

instance TestEquality SUnit where
  testEquality :: forall (a :: UnitSyntax Symbol) (b :: UnitSyntax Symbol).
SUnit a -> SUnit b -> Maybe (a :~: b)
testEquality (SUnit SList xs
xs SList ys
ys) (SUnit SList xs
xs' SList ys
ys') = case (SList xs -> SList xs -> Maybe (xs :~: xs)
forall (a :: [Symbol]) (b :: [Symbol]).
SList a -> SList b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality SList xs
xs SList xs
xs', SList ys -> SList ys -> Maybe (ys :~: ys)
forall (a :: [Symbol]) (b :: [Symbol]).
SList a -> SList b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality SList ys
ys SList ys
ys') of
                                                 (Just xs :~: xs
Refl, Just ys :~: ys
Refl) -> (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
                                                 (Maybe (xs :~: xs), Maybe (ys :~: ys))
_                      -> Maybe (a :~: b)
forall a. Maybe a
Nothing

instance TestEquality SList where
  testEquality :: forall (a :: [Symbol]) (b :: [Symbol]).
SList a -> SList b -> Maybe (a :~: b)
testEquality SList a
SNil SList b
SNil = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  testEquality (SCons proxy x
px SList xs
xs) (SCons proxy x
py SList xs
ys)
    | Just x :~: x
Refl <- proxy x -> proxy x -> Maybe (x :~: x)
forall (proxy :: Symbol -> *) (proxy' :: Symbol -> *) (x :: Symbol)
       (y :: Symbol).
(KnownSymbol x, KnownSymbol y) =>
proxy x -> proxy' y -> Maybe (x :~: y)
testEqualitySymbol proxy x
px proxy x
py
    , Just xs :~: xs
Refl <- SList xs -> SList xs -> Maybe (xs :~: xs)
forall (a :: [Symbol]) (b :: [Symbol]).
SList a -> SList b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality SList xs
xs SList xs
ys = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  testEquality SList a
_ SList b
_ = Maybe (a :~: b)
forall a. Maybe a
Nothing

-- | Annoyingly, base doesn't appear to export enough stuff to make it
-- possible to write a @TestEquality SSymbol@ instance, so we cheat.
testEqualitySymbol :: forall proxy proxy' x y . (KnownSymbol x, KnownSymbol y)
                   => proxy x -> proxy' y -> Maybe (x :~: y)
testEqualitySymbol :: forall (proxy :: Symbol -> *) (proxy' :: Symbol -> *) (x :: Symbol)
       (y :: Symbol).
(KnownSymbol x, KnownSymbol y) =>
proxy x -> proxy' y -> Maybe (x :~: y)
testEqualitySymbol proxy x
px proxy' y
py
  | proxy x -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal proxy x
px String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== proxy' y -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal proxy' y
py = (x :~: y) -> Maybe (x :~: y)
forall a. a -> Maybe a
Just ((Any :~: Any) -> x :~: y
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl)
  | Bool
otherwise                    = Maybe (x :~: y)
forall a. Maybe a
Nothing

-- | Test whether two 'SUnit's represent the same units, up to the
-- equivalence relation.  TODO: this currently uses 'unsafeCoerce',
-- but in principle it should be possible to avoid it.
testEquivalentSUnit :: SUnit u -> SUnit v -> Maybe (Pack u :~: Pack v)
testEquivalentSUnit :: forall (u :: UnitSyntax Symbol) (v :: UnitSyntax Symbol).
SUnit u -> SUnit v -> Maybe (Pack u :~: Pack v)
testEquivalentSUnit SUnit u
su SUnit v
sv
  | UnitSyntax String -> Map String Integer
normaliseUnitSyntax (SUnit u -> UnitSyntax String
forall (u :: UnitSyntax Symbol). SUnit u -> UnitSyntax String
forgetSUnit SUnit u
su) Map String Integer -> Map String Integer -> Bool
forall a. Eq a => a -> a -> Bool
== UnitSyntax String -> Map String Integer
normaliseUnitSyntax (SUnit v -> UnitSyntax String
forall (u :: UnitSyntax Symbol). SUnit u -> UnitSyntax String
forgetSUnit SUnit v
sv) = (Pack u :~: Pack v) -> Maybe (Pack u :~: Pack v)
forall a. a -> Maybe a
Just ((Any :~: Any) -> Pack u :~: Pack v
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl)
  | Bool
otherwise = Maybe (Pack u :~: Pack v)
forall a. Maybe a
Nothing

-- | Calculate a normal form of a syntactic unit: a map from base unit names to
-- non-zero integers.
--
-- >>> normaliseUnitSyntax ([] :/ [])
-- fromList []
--
-- >>> normaliseUnitSyntax (["m"] :/ [])
-- fromList [("m",1)]
--
-- >>> normaliseUnitSyntax (["m", "m"] :/ [])
-- fromList [("m",2)]
--
-- >>> normaliseUnitSyntax (["m", "m", "m"] :/ [])
-- fromList [("m",3)]
--
-- >>> normaliseUnitSyntax ([] :/ ["m"])
-- fromList [("m",-1)]
--
-- >>> normaliseUnitSyntax ([] :/ ["m", "m"])
-- fromList [("m",-2)]
--
-- >>> normaliseUnitSyntax ([] :/ ["m", "m", "m"])
-- fromList [("m",-3)]
--
-- >>> normaliseUnitSyntax (["m"] :/ ["m"])
-- fromList []
--
-- >>> normaliseUnitSyntax (["m", "m"] :/ ["m"])
-- fromList [("m",1)]
--
-- >>> normaliseUnitSyntax (["m"] :/ ["m", "m"])
-- fromList [("m",-1)]
--
-- >>> normaliseUnitSyntax (["m", "m"] :/ ["m", "m"])
-- fromList []
--
-- >>> normaliseUnitSyntax (["m", "m", "m"] :/ ["m", "m"])
-- fromList [("m",1)]
--
-- >>> normaliseUnitSyntax (["m", "m"] :/ ["m", "m", "m"])
-- fromList [("m",-1)]
--
-- >>> normaliseUnitSyntax (["m", "m", "m"] :/ ["m", "m", "m"])
-- fromList []
--
-- >>> normaliseUnitSyntax (replicate 3 "m" :/ [])
-- fromList [("m",3)]
--
-- >>> normaliseUnitSyntax ([] :/ replicate 3 "m")
-- fromList [("m",-3)]
--
-- >>> normaliseUnitSyntax (replicate 3 "m" :/ replicate 3 "m")
-- fromList []
--
-- >>> normaliseUnitSyntax (["m"] :/ ["s"])
-- fromList [("m",1),("s",-1)]
--
-- >>> normaliseUnitSyntax (["m"] :/ ["s", "s"])
-- fromList [("m",1),("s",-2)]
--
-- >>> normaliseUnitSyntax (["m", "m"] :/ []) == normaliseUnitSyntax (["m", "m"] :/ ["m", "m"])
-- False
--
-- >>> normaliseUnitSyntax (["m"] :/ []) == normaliseUnitSyntax (["m"] :/ ["m", "m"])
-- False
normaliseUnitSyntax :: UnitSyntax String -> Map.Map String Integer
normaliseUnitSyntax :: UnitSyntax String -> Map String Integer
normaliseUnitSyntax ([String]
xs :/ [String]
ys) =
    (Integer -> Bool) -> Map String Integer -> Map String Integer
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0)
        ((Map String Integer -> String -> Map String Integer)
-> Map String Integer -> [String] -> Map String Integer
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\ Map String Integer
m String
x -> (Integer -> Integer -> Integer)
-> String -> Integer -> Map String Integer -> Map String Integer
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+) String
x (Integer -> Integer
forall a. Num a => a -> a
negate Integer
1) Map String Integer
m)
            ((Map String Integer -> String -> Map String Integer)
-> Map String Integer -> [String] -> Map String Integer
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\ Map String Integer
m String
x -> (Integer -> Integer -> Integer)
-> String -> Integer -> Map String Integer -> Map String Integer
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+) String
x Integer
1 Map String Integer
m) Map String Integer
forall k a. Map k a
Map.empty [String]
xs) [String]
ys)


-- | Extract the runtime syntactic representation from a singleton unit
forgetSUnit :: SUnit u -> UnitSyntax String
forgetSUnit :: forall (u :: UnitSyntax Symbol). SUnit u -> UnitSyntax String
forgetSUnit (SUnit SList xs
xs SList ys
ys) = SList xs -> [String]
forall (xs :: [Symbol]). SList xs -> [String]
forgetSList SList xs
xs [String] -> [String] -> UnitSyntax String
forall s. [s] -> [s] -> UnitSyntax s
:/ SList ys -> [String]
forall (xs :: [Symbol]). SList xs -> [String]
forgetSList SList ys
ys

forgetSList :: SList xs -> [String]
forgetSList :: forall (xs :: [Symbol]). SList xs -> [String]
forgetSList SList xs
SNil = []
forgetSList (SCons proxy x
px SList xs
xs) = proxy x -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal proxy x
px String -> [String] -> [String]
forall a. a -> [a] -> [a]
: SList xs -> [String]
forall (xs :: [Symbol]). SList xs -> [String]
forgetSList SList xs
xs


-- | A constraint @'KnownUnit' u@ means that @u@ must be a concrete
-- unit that is statically known but passed at runtime
class KnownUnit (u :: UnitSyntax Symbol) where
  unitSing :: SUnit u

instance (KnownList xs, KnownList ys) => KnownUnit (xs :/ ys) where
  unitSing :: SUnit (xs ':/ ys)
unitSing = SList xs -> SList ys -> SUnit (xs ':/ ys)
forall (x :: [Symbol]) (proxy :: [Symbol]).
SList x -> SList proxy -> SUnit (x ':/ proxy)
SUnit SList xs
forall (xs :: [Symbol]). KnownList xs => SList xs
listSing SList ys
forall (xs :: [Symbol]). KnownList xs => SList xs
listSing


-- | A constraint @'KnownList' xs@ means that @xs@ must be a list of
-- base units that is statically known but passed at runtime
class KnownList (xs :: [Symbol]) where
  listSing :: SList xs

instance KnownList '[] where
  listSing :: SList '[]
listSing = SList '[]
SNil

instance (KnownSymbol x, KnownList xs) => KnownList (x ': xs) where
  listSing :: SList (x : xs)
listSing = Any x -> SList xs -> SList (x : xs)
forall (x :: Symbol) (proxy :: Symbol -> *) (xs :: [Symbol]).
KnownSymbol x =>
proxy x -> SList xs -> SList (x : xs)
SCons (proxy x
forall a. HasCallStack => a
forall {proxy :: Symbol -> *}. proxy x
undefined :: proxy x) SList xs
forall (xs :: [Symbol]). KnownList xs => SList xs
listSing


-- | Extract the runtime syntactic representation of a 'KnownUnit'
unitVal :: forall proxy u . KnownUnit u => proxy u -> UnitSyntax String
unitVal :: forall (proxy :: UnitSyntax Symbol -> *) (u :: UnitSyntax Symbol).
KnownUnit u =>
proxy u -> UnitSyntax String
unitVal proxy u
_ = SUnit u -> UnitSyntax String
forall (u :: UnitSyntax Symbol). SUnit u -> UnitSyntax String
forgetSUnit (SUnit u
forall (u :: UnitSyntax Symbol). KnownUnit u => SUnit u
unitSing :: SUnit u)