{-# 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 #-}

-- | Experimental support for conversions between units with the same
-- dimension, for example feet and metres.  This interface is not
-- necessarily stable!
--
-- Rather than defining dimensions explicitly, we pick a "canonical"
-- base unit for each dimension, and record the conversion ratio
-- between each base unit and the canonical base unit for its
-- dimension.  This means we can automatically calculate the
-- conversion ratio between a unit and its canonical representation,
-- and hence between any two units that share a dimension (i.e. have
-- the same canonical representation).
--
-- For example, to declare @m@ as a canonical base unit, write:
--
-- > instance HasCanonicalBaseUnit "m"
--
-- To declare @ft@ as a derived unit, write:
--
-- > instance HasCanonicalBaseUnit "ft" where
-- >   type CanonicalBaseUnit "ft" = "m"
-- >   conversionBase _ = [u| 3.28 ft/m |]
--
-- The above declarations can be written using the 'u' declaration
-- quasiquoter as @['u'| m, ft = 1 % 3.28 ft/m |]@, or generated
-- automatically using 'declareConvertibleUnit'.
--
-- Now it is possible to 'convert' between quantities whose units
-- involve feet or metres.  For example:
--
-- >>> convert [u| 10m |] :: Quantity Double [u| ft |]
-- [u| 32.8 ft |]
-- >>> convert [u| 3ft^2 |] :: Quantity Double [u| m^2 |]
-- [u| 0.27885187388459254 m^2 |]
--
-- You are likely to get unpleasant compiler error messages if you
-- attempt to convert without the units being fully determined by type
-- inference, or if the units do not have the same dimension.
--
-- If you wish to define a dimensionless unit that requires explicit
-- conversion to @1@, such as radians, write @['u'| rad = 1 1 |]@.
-- The syntax @['u'| dimensionless = 1 |]@ defines @dimensionless@ as
-- a unit synonym for @1@ that does not require conversion.
module Data.UnitsOfMeasure.Convert
    ( convert
    , ratio
    , HasCanonicalBaseUnit(..)
      -- * Constraints
    , Good
    , IsCanonical
    , HasCanonical
    , Convertible
    , ToCanonicalUnit
    ) where

import Data.UnitsOfMeasure.Internal
import Data.UnitsOfMeasure.Singleton

import Data.Kind (Type, Constraint)
import GHC.TypeLits (Symbol)


-- | Class to capture the dimensions to which base units belong.  For
-- a canonical base unit, the class instance can be left empty.
class IsCanonical (Unpack (CanonicalBaseUnit b))
    => HasCanonicalBaseUnit (b :: Symbol) where
  -- | The canonical base unit for this base unit.  If @b@ is
  -- canonical, then @'CanonicalBaseUnit' b = b@.  Otherwise,
  -- @'CanonicalBaseUnit' b@ must itself be canonical.
  type CanonicalBaseUnit b :: Unit
  type CanonicalBaseUnit b = Base b

  -- | The conversion ratio between this base unit and its canonical
  -- base unit.  If @b@ is canonical then this ratio is @1@.
  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

-- | Convert a unit into its canonical representation, where units are
-- represented syntactically.
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

-- | This constraint will be satisfied if all the base units in a
-- syntactically represented unit have associated canonical
-- representations.
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)

-- | This constraint will be satisfied if all the base units in a
-- syntactically represented unit are in their canonical form.
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


-- | A unit is "good" if all its base units have been defined, and
-- have associated canonical base units.
type Good            u = (u ~ Pack (Unpack u), KnownUnit (Unpack u), HasCanonical (Unpack u))

-- | Two units are convertible if they are both 'Good' and they have
-- the same canonical units (and hence the same dimension).
type Convertible   u v = (Good u, Good v, ToCanonicalUnit u ~ ToCanonicalUnit v)

-- | Converts a unit to the corresponding canonical representation.
type ToCanonicalUnit u = ToCBU (Unpack u)

-- | Automatically convert a quantity with units @u@ so that its units
-- are @v@, provided @u@ and @v@ have the same dimension.
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 #-}

-- | Calculate the conversion ratio between two units with the same
-- dimension.  The slightly unusual proxy arguments allow this to be
-- called using quasiquoters to specify the units, for example
-- @'ratio' [u| ft |] [u| m |]@.
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 #-}