{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- | This module defines the core types used in the @uom-plugin@
-- library.  Note that importing this module may allow you to violate
-- invariants, so you should generally work with the safe interface in
-- "Data.UnitsOfMeasure" instead.
module Data.UnitsOfMeasure.Internal
    ( -- * Type-level units of measure
      Unit
    , type One
    , type Base
    , type (*:)
    , type (/:)
    , type (^:)

      -- * Values indexed by their units
    , Quantity(..)
    , unQuantity
    , zero
    , mk

      -- * Unit-safe 'Num' operations
    , (+:)
    , (*:)
    , (-:)
    , negate'
    , abs'
    , signum'
    , fromInteger'

      -- * Unit-safe 'Fractional' operations
    , (/:)
    , recip'
    , fromRational'

      -- * Unit-safe 'Real' operations
    , toRational'

      -- * Unit-safe 'Floating' operations
    , sqrt'

      -- * Syntactic representation of units
    , UnitSyntax(..)
    , Unpack
    , Pack
    , Prod

      -- * Internal
    , type (~~)
    , MkUnit
    ) where

import Control.DeepSeq
import Foreign.Storable
import GHC.Exts (Constraint)
import GHC.TypeLits (Symbol, Nat, type (-))

-- | (Kind) Units of measure
data Unit

-- | Dimensionless unit (identity element)
type family One :: Unit where

-- | Base unit
type Base :: Symbol -> Unit
type family Base b where

-- | Multiplication for units of measure
type (*:) :: Unit -> Unit -> Unit
type family u *: v where

-- | Division for units of measure
type (/:) :: Unit -> Unit -> Unit
type family u /: v where

-- | Exponentiation (to a positive power) for units of measure;
-- negative exponents are not yet supported (they require an Integer kind)
type (^:) :: Unit -> Nat -> Unit
type family u ^: n where
  u ^: 0 = One
  u ^: 1 = u
  u ^: n = u *: (u ^: (n-1))

infixl 6 +:, -:
infixl 7 *:, /:
infixr 8 ^:

-- | A @Quantity a u@ is represented identically to a value of
-- underlying numeric type @a@, but with units @u@.
newtype Quantity a (u :: Unit) = MkQuantity a
  -- ^ Warning: the 'MkQuantity' constructor allows module invariants
  -- to be violated, so use it with caution!
type role Quantity representational nominal

-- These classes work uniformly on the underlying representation,
-- regardless of the units
deriving instance Bounded a => Bounded (Quantity a u)
deriving instance Eq      a => Eq      (Quantity a u)
deriving instance Ord     a => Ord     (Quantity a u)

-- These classes are not unit-polymorphic, so we have to restrict the
-- unit index to be dimensionless
deriving instance (Enum       a, u ~ One) => Enum       (Quantity a u)
deriving instance (Floating   a, u ~ One) => Floating   (Quantity a u)
deriving instance (Fractional a, u ~ One) => Fractional (Quantity a u)
deriving instance (Integral   a, u ~ One) => Integral   (Quantity a u)
deriving instance (Num        a, u ~ One) => Num        (Quantity a u)
deriving instance (Real       a, u ~ One) => Real       (Quantity a u)
deriving instance (RealFloat  a, u ~ One) => RealFloat  (Quantity a u)
deriving instance (RealFrac   a, u ~ One) => RealFrac   (Quantity a u)

-- To enable marshalling into FFI code.
deriving instance Storable a => Storable (Quantity a u)

-- To enable deriving NFData for data types containing Quantity fields.
deriving instance NFData a => NFData (Quantity a u)

-- | Extract the underlying value of a quantity
unQuantity :: Quantity a u -> a
unQuantity :: forall a (u :: Unit). Quantity a u -> a
unQuantity (MkQuantity a
x) = a
x

-- | Zero is polymorphic in its units: this is required because the
-- 'Num' instance constrains the quantity to be dimensionless, so
-- @0 :: Quantity a u@ is not well typed.
zero :: Num a => Quantity a u
zero :: forall a (u :: Unit). Num a => Quantity a u
zero = a -> Quantity a u
forall a (u :: Unit). a -> Quantity a u
MkQuantity a
0

-- | Construct a 'Quantity' from a dimensionless value.  Note that for
-- numeric literals, the 'Num' and 'Fractional' instances allow them
-- to be treated as quantities directly.
mk :: a -> Quantity a One
mk :: forall a. a -> Quantity a One
mk = a -> Quantity a One
forall a (u :: Unit). a -> Quantity a u
MkQuantity


-- | Addition ('+') of quantities requires the units to match.
(+:) :: Num a => Quantity a u -> Quantity a u -> Quantity a u
MkQuantity a
x +: :: forall a (u :: Unit).
Num a =>
Quantity a u -> Quantity a u -> Quantity a u
+: MkQuantity a
y = a -> Quantity a u
forall a (u :: Unit). a -> Quantity a u
MkQuantity (a
x a -> a -> a
forall a. Num a => a -> a -> a
+ a
y)
{-# INLINE (+:) #-}

-- | Multiplication ('*') of quantities multiplies the units.
(*:) :: (Num a, w ~~ u *: v) => Quantity a u -> Quantity a v -> Quantity a w
MkQuantity a
x *: :: forall a (w :: Unit) (u :: Unit) (v :: Unit).
(Num a, w ~~ (u *: v)) =>
Quantity a u -> Quantity a v -> Quantity a w
*: MkQuantity a
y = a -> Quantity a w
forall a (u :: Unit). a -> Quantity a u
MkQuantity (a
x a -> a -> a
forall a. Num a => a -> a -> a
* a
y)
{-# INLINE (*:) #-}

-- | Subtraction ('-') of quantities requires the units to match.
(-:) :: Num a => Quantity a u -> Quantity a u -> Quantity a u
MkQuantity a
x -: :: forall a (u :: Unit).
Num a =>
Quantity a u -> Quantity a u -> Quantity a u
-: MkQuantity a
y = a -> Quantity a u
forall a (u :: Unit). a -> Quantity a u
MkQuantity (a
x a -> a -> a
forall a. Num a => a -> a -> a
- a
y)
{-# INLINE (-:) #-}

-- | Negation ('negate') of quantities is polymorphic in the units.
negate' :: Num a => Quantity a u -> Quantity a u
negate' :: forall a (u :: Unit). Num a => Quantity a u -> Quantity a u
negate' (MkQuantity a
x) = a -> Quantity a u
forall a (u :: Unit). a -> Quantity a u
MkQuantity (a -> a
forall a. Num a => a -> a
negate a
x)
{-# INLINE negate' #-}

-- | Absolute value ('abs') of quantities is polymorphic in the units.
abs' :: Num a => Quantity a u -> Quantity a u
abs' :: forall a (u :: Unit). Num a => Quantity a u -> Quantity a u
abs' (MkQuantity a
x) = a -> Quantity a u
forall a (u :: Unit). a -> Quantity a u
MkQuantity (a -> a
forall a. Num a => a -> a
abs a
x)
{-# INLINE abs' #-}

-- | The sign ('signum') of a quantity gives a dimensionless result.
signum' :: Num a => Quantity a u -> Quantity a One
signum' :: forall a (u :: Unit). Num a => Quantity a u -> Quantity a One
signum' (MkQuantity a
x) = a -> Quantity a One
forall a (u :: Unit). a -> Quantity a u
MkQuantity (a -> a
forall a. Num a => a -> a
signum a
x)
{-# INLINE signum' #-}

-- | Convert an 'Integer' quantity into any 'Integral' type ('fromInteger').
fromInteger' :: Integral a => Quantity Integer u -> Quantity a u
fromInteger' :: forall a (u :: Unit).
Integral a =>
Quantity Integer u -> Quantity a u
fromInteger' (MkQuantity Integer
x) = a -> Quantity a u
forall a (u :: Unit). a -> Quantity a u
MkQuantity (Integer -> a
forall a. Num a => Integer -> a
fromInteger Integer
x)
{-# INLINE fromInteger' #-}


-- | Division ('/') of quantities divides the units.
(/:) :: (Fractional a, w ~~ u /: v) => Quantity a u -> Quantity a v -> Quantity a w
MkQuantity a
x /: :: forall a (w :: Unit) (u :: Unit) (v :: Unit).
(Fractional a, w ~~ (u /: v)) =>
Quantity a u -> Quantity a v -> Quantity a w
/: MkQuantity a
y = a -> Quantity a w
forall a (u :: Unit). a -> Quantity a u
MkQuantity (a
x a -> a -> a
forall a. Fractional a => a -> a -> a
/ a
y)
{-# INLINE (/:) #-}

-- | Reciprocal ('recip') of quantities reciprocates the units.
recip' :: (Fractional a, w ~~ One /: u) => Quantity a u -> Quantity a w
recip' :: forall a (w :: Unit) (u :: Unit).
(Fractional a, w ~~ (One /: u)) =>
Quantity a u -> Quantity a w
recip' (MkQuantity a
x) = a -> Quantity a w
forall a (u :: Unit). a -> Quantity a u
MkQuantity (a -> a
forall a. Fractional a => a -> a
recip a
x)
{-# INLINE recip' #-}

-- | Convert a 'Rational' quantity into any 'Fractional' type ('fromRational').
fromRational' :: Fractional a => Quantity Rational u -> Quantity a u
fromRational' :: forall a (u :: Unit).
Fractional a =>
Quantity Rational u -> Quantity a u
fromRational' (MkQuantity Rational
x) = a -> Quantity a u
forall a (u :: Unit). a -> Quantity a u
MkQuantity (Rational -> a
forall a. Fractional a => Rational -> a
fromRational Rational
x)
{-# INLINE fromRational' #-}

-- | Convert any 'Real' quantity into a 'Rational' type ('toRational').
toRational' :: Real a => Quantity a u -> Quantity Rational u
toRational' :: forall a (u :: Unit). Real a => Quantity a u -> Quantity Rational u
toRational' (MkQuantity a
x) = Rational -> Quantity Rational u
forall a (u :: Unit). a -> Quantity a u
MkQuantity (a -> Rational
forall a. Real a => a -> Rational
toRational a
x)
{-# INLINE toRational' #-}


-- | Taking the square root ('sqrt') of a quantity requires its units
-- to be a square.  Fractional units are not currently supported.
sqrt' :: (Floating a, w ~~ u ^: 2) => Quantity a w -> Quantity a u
sqrt' :: forall a (w :: Unit) (u :: Unit).
(Floating a, w ~~ (u ^: 2)) =>
Quantity a w -> Quantity a u
sqrt' (MkQuantity a
x) = a -> Quantity a u
forall a (u :: Unit). a -> Quantity a u
MkQuantity (a -> a
forall a. Floating a => a -> a
sqrt a
x)
{-# INLINE sqrt' #-}


-- | Syntactic representation of a unit as a pair of lists of base
-- units, for example 'One' is represented as @[] ':/' []@ and
-- @'Base' "m" '/:' 'Base' "s" ^: 2@ is represented as @["m"] ':/' ["s","s"]@.
data UnitSyntax s = [s] :/ [s]
  deriving (UnitSyntax s -> UnitSyntax s -> Bool
(UnitSyntax s -> UnitSyntax s -> Bool)
-> (UnitSyntax s -> UnitSyntax s -> Bool) -> Eq (UnitSyntax s)
forall s. Eq s => UnitSyntax s -> UnitSyntax s -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall s. Eq s => UnitSyntax s -> UnitSyntax s -> Bool
== :: UnitSyntax s -> UnitSyntax s -> Bool
$c/= :: forall s. Eq s => UnitSyntax s -> UnitSyntax s -> Bool
/= :: UnitSyntax s -> UnitSyntax s -> Bool
Eq, Int -> UnitSyntax s -> ShowS
[UnitSyntax s] -> ShowS
UnitSyntax s -> String
(Int -> UnitSyntax s -> ShowS)
-> (UnitSyntax s -> String)
-> ([UnitSyntax s] -> ShowS)
-> Show (UnitSyntax s)
forall s. Show s => Int -> UnitSyntax s -> ShowS
forall s. Show s => [UnitSyntax s] -> ShowS
forall s. Show s => UnitSyntax s -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall s. Show s => Int -> UnitSyntax s -> ShowS
showsPrec :: Int -> UnitSyntax s -> ShowS
$cshow :: forall s. Show s => UnitSyntax s -> String
show :: UnitSyntax s -> String
$cshowList :: forall s. Show s => [UnitSyntax s] -> ShowS
showList :: [UnitSyntax s] -> ShowS
Show)

-- | Pack up a syntactic representation of a unit as a unit.  For example:
--
-- @ 'Pack' ([] ':/' []) = 'One' @
--
-- @ 'Pack' (["m"] ':/' ["s","s"]) = 'Base' "m" '/:' 'Base' "s" ^: 2 @
--
-- This is a perfectly ordinary closed type family.  'Pack' is a left
-- inverse of 'Unpack' up to the equational theory of units, but it is
-- not a right inverse (because there are multiple list
-- representations of the same unit).
type Pack :: UnitSyntax Symbol -> Unit
type family Pack u where
  Pack (xs :/ ys) = Prod xs /: Prod ys

-- | Take the product of a list of base units.
type Prod :: [Symbol] -> Unit
type family Prod xs where
  Prod '[]       = One
  Prod (x ': xs) = Base x *: Prod xs

-- | Unpack a unit as a syntactic representation, where the order of
-- units is deterministic.  For example:
--
-- @ 'Unpack' 'One' = [] ':/' [] @
--
-- @ 'Unpack' ('Base' "s" '*:' 'Base' "m") = ["m","s"] ':/' [] @
--
-- This does not break type soundness because
-- 'Unpack' will reduce only when the unit is entirely constant, and
-- it does not allow the structure of the unit to be observed.  The
-- reduction behaviour is implemented by the plugin, because we cannot
-- define it otherwise.
type Unpack :: Unit -> UnitSyntax Symbol
type family Unpack u where


-- | This is a bit of a hack, honestly, but a good hack.  Constraints
-- @u ~~ v@ are just like equalities @u ~ v@, except solving them will
-- be delayed until the plugin.  This may lead to better inferred types.
type (~~) :: Unit -> Unit -> Constraint
type family u ~~ v where

infix 4 ~~


-- | This type family is used for translating unit names (as
-- type-level strings) into units.  It will be 'Base' for base units
-- or expand the definition for derived units.
--
-- The instances displayed by Haddock are available only if
-- "Data.UnitsOfMeasure.Defs" is imported.
type MkUnit :: Symbol -> Unit
type family MkUnit s