{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# OPTIONS_GHC -fplugin Data.UnitsOfMeasure.Plugin #-}
module Data.UnitsOfMeasure.Convert
( convert
, ratio
, HasCanonicalBaseUnit(..)
, Good
, IsCanonical
, HasCanonical
, Convertible
, ToCanonicalUnit
) where
import Data.UnitsOfMeasure.Internal
import Data.UnitsOfMeasure.Singleton
import Data.Kind (Type, Constraint)
import GHC.TypeLits (Symbol)
class IsCanonical (Unpack (CanonicalBaseUnit b))
=> HasCanonicalBaseUnit (b :: Symbol) where
type CanonicalBaseUnit b :: Unit
type CanonicalBaseUnit b = Base b
conversionBase :: proxy b -> Quantity Rational (Base b /: CanonicalBaseUnit b)
default conversionBase :: (Base b ~ CanonicalBaseUnit b) => proxy b -> Quantity Rational (Base b /: CanonicalBaseUnit b)
conversionBase proxy b
_ = Quantity Rational (Base b /: CanonicalBaseUnit b)
Quantity Rational (CanonicalBaseUnit b /: CanonicalBaseUnit b)
1
type ToCBU :: UnitSyntax Symbol -> Unit
type family ToCBU u where
ToCBU (xs :/ ys) = ListToCBU xs /: ListToCBU ys
type ListToCBU :: [Symbol] -> Unit
type family ListToCBU xs where
ListToCBU '[] = One
ListToCBU (x ': xs) = CanonicalBaseUnit x *: ListToCBU xs
type HasCanonical :: UnitSyntax Symbol -> Constraint
type family HasCanonical u where
HasCanonical (xs :/ ys) = (AllHasCanonical xs, AllHasCanonical ys)
type AllHasCanonical :: [Symbol] -> Constraint
type family AllHasCanonical xs where
AllHasCanonical '[] = ()
AllHasCanonical (x ': xs) = (HasCanonicalBaseUnit x, AllHasCanonical xs)
type IsCanonical :: UnitSyntax Symbol -> Constraint
type family IsCanonical u where
IsCanonical (xs :/ ys) = (AllIsCanonical xs, AllIsCanonical ys)
type AllIsCanonical :: [Symbol] -> Constraint
type family AllIsCanonical xs where
AllIsCanonical '[] = ()
AllIsCanonical (x ': xs) = (CanonicalBaseUnit x ~ Base x, AllIsCanonical xs)
conversionRatio :: forall proxy u . Good u
=> proxy u -> Quantity Rational (u /: ToCBU (Unpack u))
conversionRatio :: forall (proxy :: Unit -> *) (u :: Unit).
Good u =>
proxy u -> Quantity Rational (u /: ToCBU (Unpack u))
conversionRatio proxy u
_ = SUnit (Unpack u)
-> Quantity Rational (Pack (Unpack u) /: ToCBU (Unpack u))
forall (u :: UnitSyntax Symbol).
HasCanonical u =>
SUnit u -> Quantity Rational (Pack u /: ToCBU u)
help (SUnit (Unpack u)
forall (u :: UnitSyntax Symbol). KnownUnit u => SUnit u
unitSing :: SUnit (Unpack u))
{-# INLINABLE conversionRatio #-}
help :: forall u . HasCanonical u => SUnit u -> Quantity Rational (Pack u /: ToCBU u)
help :: forall (u :: UnitSyntax Symbol).
HasCanonical u =>
SUnit u -> Quantity Rational (Pack u /: ToCBU u)
help (SUnit SList xs
xs SList ys
ys) = SList xs -> Quantity Rational (Prod xs /: ListToCBU xs)
forall (xs :: [Symbol]).
AllHasCanonical xs =>
SList xs -> Quantity Rational (Prod xs /: ListToCBU xs)
help' SList xs
xs Quantity Rational (Prod xs /: ListToCBU xs)
-> Quantity Rational (Prod ys /: ListToCBU ys)
-> Quantity
Rational ((Prod xs /: Prod ys) /: (ListToCBU xs /: ListToCBU ys))
forall a (w :: Unit) (u :: Unit) (v :: Unit).
(Fractional a, w ~~ (u /: v)) =>
Quantity a u -> Quantity a v -> Quantity a w
/: SList ys -> Quantity Rational (Prod ys /: ListToCBU ys)
forall (xs :: [Symbol]).
AllHasCanonical xs =>
SList xs -> Quantity Rational (Prod xs /: ListToCBU xs)
help' SList ys
ys
help' :: forall xs . AllHasCanonical xs => SList xs -> Quantity Rational (Prod xs /: ListToCBU xs)
help' :: forall (xs :: [Symbol]).
AllHasCanonical xs =>
SList xs -> Quantity Rational (Prod xs /: ListToCBU xs)
help' SList xs
SNil = Quantity Rational (Prod xs /: ListToCBU xs)
Quantity Rational (One /: One)
1
help' (SCons proxy x
p SList xs1
xs) = proxy x -> Quantity Rational (Base x /: CanonicalBaseUnit x)
forall (b :: Symbol) (proxy :: Symbol -> *).
HasCanonicalBaseUnit b =>
proxy b -> Quantity Rational (Base b /: CanonicalBaseUnit b)
forall (proxy :: Symbol -> *).
proxy x -> Quantity Rational (Base x /: CanonicalBaseUnit x)
conversionBase proxy x
p Quantity Rational (Base x /: CanonicalBaseUnit x)
-> Quantity Rational (Prod xs1 /: ListToCBU xs1)
-> Quantity
Rational
((Base x *: Prod xs1) /: (CanonicalBaseUnit x *: ListToCBU xs1))
forall a (w :: Unit) (u :: Unit) (v :: Unit).
(Num a, w ~~ (u *: v)) =>
Quantity a u -> Quantity a v -> Quantity a w
*: SList xs1 -> Quantity Rational (Prod xs1 /: ListToCBU xs1)
forall (xs :: [Symbol]).
AllHasCanonical xs =>
SList xs -> Quantity Rational (Prod xs /: ListToCBU xs)
help' SList xs1
xs
type Good u = (u ~ Pack (Unpack u), KnownUnit (Unpack u), HasCanonical (Unpack u))
type Convertible u v = (Good u, Good v, ToCanonicalUnit u ~ ToCanonicalUnit v)
type ToCanonicalUnit u = ToCBU (Unpack u)
convert :: forall a u v . (Fractional a, Convertible u v) => Quantity a u -> Quantity a v
convert :: forall a (u :: Unit) (v :: Unit).
(Fractional a, Convertible u v) =>
Quantity a u -> Quantity a v
convert = (Any (Any v) -> Any (Any u) -> Quantity a (v /: u)
forall a (u :: Unit) (v :: Unit) (proxy :: Unit -> *)
(proxy' :: * -> *).
(Fractional a, Convertible u v) =>
proxy' (proxy u) -> proxy' (proxy v) -> Quantity a (u /: v)
ratio (proxy' (proxy v)
forall {k} {proxy' :: k -> *} {proxy :: Unit -> k}.
proxy' (proxy v)
forall a. HasCallStack => a
undefined :: proxy' (proxy v)) (proxy' (proxy u)
forall {k} {proxy' :: k -> *} {proxy :: Unit -> k}.
proxy' (proxy u)
forall a. HasCallStack => a
undefined :: proxy' (proxy u)) Quantity a (v /: u) -> Quantity a u -> Quantity a v
forall a (w :: Unit) (u :: Unit) (v :: Unit).
(Num a, w ~~ (u *: v)) =>
Quantity a u -> Quantity a v -> Quantity a w
*:)
{-# INLINABLE convert #-}
ratio :: forall a u v (proxy :: Unit -> Type) proxy' .
(Fractional a, Convertible u v)
=> proxy' (proxy u) -> proxy' (proxy v) -> Quantity a (u /: v)
ratio :: forall a (u :: Unit) (v :: Unit) (proxy :: Unit -> *)
(proxy' :: * -> *).
(Fractional a, Convertible u v) =>
proxy' (proxy u) -> proxy' (proxy v) -> Quantity a (u /: v)
ratio proxy' (proxy u)
_ proxy' (proxy v)
_ = Quantity Rational (u /: v) -> Quantity a (u /: v)
forall a (u :: Unit).
Fractional a =>
Quantity Rational u -> Quantity a u
fromRational' (Quantity Rational (u /: v) -> Quantity a (u /: v))
-> Quantity Rational (u /: v) -> Quantity a (u /: v)
forall a b. (a -> b) -> a -> b
$ proxy u -> Quantity Rational (u /: ToCanonicalUnit u)
forall (proxy :: Unit -> *) (u :: Unit).
Good u =>
proxy u -> Quantity Rational (u /: ToCBU (Unpack u))
conversionRatio (proxy u
forall a. HasCallStack => a
undefined :: proxy u) Quantity Rational (u /: ToCBU (Unpack v))
-> Quantity Rational (v /: ToCBU (Unpack v))
-> Quantity Rational (u /: v)
forall a (w :: Unit) (u :: Unit) (v :: Unit).
(Fractional a, w ~~ (u /: v)) =>
Quantity a u -> Quantity a v -> Quantity a w
/: proxy v -> Quantity Rational (v /: ToCBU (Unpack v))
forall (proxy :: Unit -> *) (u :: Unit).
Good u =>
proxy u -> Quantity Rational (u /: ToCBU (Unpack u))
conversionRatio (proxy v
forall a. HasCallStack => a
undefined :: proxy v)
{-# INLINABLE ratio #-}