{-# 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 #-}
module Data.UnitsOfMeasure.Singleton
(
SUnit(..)
, forgetSUnit
, KnownUnit(..)
, unitVal
, testEquivalentSUnit
, 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
data SUnit (u :: UnitSyntax Symbol) where
SUnit :: SList xs -> SList ys -> SUnit (xs :/ ys)
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
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
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
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)
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
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
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
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)