content: {- Data/Metrology/Z.hs
  
     The units Package
     Copyright (c) 2013 Richard Eisenberg
     rae@cs.brynmawr.edu
  
     This file contains a definition of integers at the type-level, in terms
     of a promoted datatype 'Z'.
  -}
  
  {-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, UndecidableInstances,
               GADTs, PolyKinds, TemplateHaskell, ScopedTypeVariables,
               EmptyCase, CPP, TypeSynonymInstances, FlexibleInstances,
               InstanceSigs, FlexibleContexts #-}
  #if __GLASGOW_HASKELL__ >= 800
  {-# LANGUAGE TypeApplications #-}
  #endif
  #if __GLASGOW_HASKELL__ >= 810
  {-# LANGUAGE StandaloneKindSignatures #-}
  #endif
  {-# OPTIONS_GHC -fno-warn-missing-signatures #-}
  
  -----------------------------------------------------------------------------
  -- |
  -- Module      :  Data.Metrology.Z
  -- Copyright   :  (C) 2013 Richard Eisenberg
  -- License     :  BSD-style (see LICENSE)
  -- Maintainer  :  Richard Eisenberg (rae@cs.brynmawr.edu)
  -- Stability   :  experimental
  -- Portability :  non-portable
  --
  -- This module defines a datatype and operations to represent type-level
  -- integers. Though it's defined as part of the units package, it may be
  -- useful beyond dimensional analysis. If you have a compelling non-units
  -- use of this package, please let me (Richard, @rae@ at @cs.brynmawr.edu@)
  -- know.
  -----------------------------------------------------------------------------
  
  -- allow compilation even without Cabal
  #ifndef MIN_VERSION_singletons
  #define MIN_VERSION_singletons(a,b,c) 1
  #endif
  
  module Data.Metrology.Z (
    -- * The 'Z' datatype
    Z(..),
  #if MIN_VERSION_singletons(2,6,0)
    Sing, SZ(..),
  #else
    Sing(..), SZ,
  #endif
  
  #if MIN_VERSION_singletons(1,0,0)
    -- ** Defunctionalization symbols (these can be ignored)
    ZeroSym0, SSym0, SSym1, PSym0, PSym1,
  #endif
  
    -- * Conversions
    zToInt, szToInt,
  
    -- * Type-level operations
    -- ** Arithmetic
    Succ, Pred, Negate, type (#+), type (#-), type (#*), type (#/),
    sSucc, sPred, sNegate,
  
    -- ** Comparisons
    type (Data.Metrology.Z.<), NonNegative,
  
    -- * Synonyms for certain numbers
    One, Two, Three, Four, Five, MOne, MTwo, MThree, MFour, MFive,
    sZero, sOne, sTwo, sThree, sFour, sFive, sMOne, sMTwo, sMThree, sMFour, sMFive,
  
    -- * Deprecated synonyms
    pZero, pOne, pTwo, pThree, pFour, pFive, pMOne, pMTwo, pMThree, pMFour, pMFive,
    pSucc, pPred
    ) where
  
  import Data.Singletons.TH
  #if MIN_VERSION_singletons(3,0,0)
  import Data.Singletons.Base.TH hiding ( Negate, sNegate, NegateSym0, NegateSym1 )
  #endif
  import GHC.Exts ( Constraint )
  
  -- | The datatype for type-level integers.
  $(singletons [d| data Z = Zero | S Z | P Z deriving Eq |])
  
  -- | Convert a 'Z' to an 'Int'
  zToInt :: Z -> Int
  zToInt Zero = 0
  zToInt (S z) = zToInt z + 1
  zToInt (P z) = zToInt z - 1
  
  -- | Add one to an integer
  type family Succ (z :: Z) :: Z where
    Succ Zero = S Zero
    Succ (P z) = z
    Succ (S z) = S (S z)
  
  -- | Subtract one from an integer
  type family Pred (z :: Z) :: Z where
    Pred Zero = P Zero
    Pred (P z) = P (P z)
    Pred (S z) = z
  
  infixl 6 #+
  -- | Add two integers
  type family (a :: Z) #+ (b :: Z) :: Z where
    Zero   #+ z      = z
    (S z1) #+ (S z2) = S (S (z1 #+ z2))
    (S z1) #+ Zero   = S z1
    (S z1) #+ (P z2) = z1 #+ z2
    (P z1) #+ (S z2) = z1 #+ z2
    (P z1) #+ Zero   = P z1
    (P z1) #+ (P z2) = P (P (z1 #+ z2))
  
  infixl 6 #-
  -- | Subtract two integers
  type family (a :: Z) #- (b :: Z) :: Z where
    z      #- Zero = z
    (S z1) #- (S z2) = z1 #- z2
    Zero   #- (S z2) = P (Zero #- z2)
    (P z1) #- (S z2) = P (P (z1 #- z2))
    (S z1) #- (P z2) = S (S (z1 #- z2))
    Zero   #- (P z2) = S (Zero #- z2)
    (P z1) #- (P z2) = z1 #- z2
  
  infixl 7 #*
  -- | Multiply two integers
  type family (a :: Z) #* (b :: Z) :: Z where
    Zero #* z = Zero
    (S z1) #* z2 = (z1 #* z2) #+ z2
    (P z1) #* z2 = (z1 #* z2) #- z2
  
  -- | Negate an integer
  type family Negate (z :: Z) :: Z where
    Negate Zero = Zero
    Negate (S z) = P (Negate z)
    Negate (P z) = S (Negate z)
  
  -- | Divide two integers
  type family (a :: Z) #/ (b :: Z) :: Z where
    Zero #/ b      = Zero
    a    #/ (P b') = Negate (a #/ (Negate (P b')))
    a    #/ b      = ZDiv b b a
  
  -- | Helper function for division
  type family ZDiv (counter :: Z) (n :: Z) (z :: Z) :: Z where
    ZDiv One n (S z')        = S (z' #/ n)
    ZDiv One n (P z')        = P (z' #/ n)
    ZDiv (S count') n (S z') = ZDiv count' n z'
    ZDiv (S count') n (P z') = ZDiv count' n z'
  
  -- | Less-than comparison
  type family (a :: Z) < (b :: Z) :: Bool where
    -- fully qualify everywhere, because Data.Singletons.TH started exporting <
    -- at some point
    Zero  Data.Metrology.Z.< Zero   = False
    Zero  Data.Metrology.Z.< (S n)  = True
    Zero  Data.Metrology.Z.< (P n)  = False
    (S n) Data.Metrology.Z.< Zero   = False
    (S n) Data.Metrology.Z.< (S n') = n Data.Metrology.Z.< n'
    (S n) Data.Metrology.Z.< (P n') = False
    (P n) Data.Metrology.Z.< Zero   = True
    (P n) Data.Metrology.Z.< (S n') = True
    (P n) Data.Metrology.Z.< (P n') = n Data.Metrology.Z.< n'
  
  -- | Check if a type-level integer is in fact a natural number
  type family NonNegative z :: Constraint where
    NonNegative Zero  = ()
    NonNegative (S z) = ()
  
  type One   = S Zero
  type Two   = S One
  type Three = S Two
  type Four  = S Three
  type Five  = S Four
  
  type MOne   = P Zero
  type MTwo   = P MOne
  type MThree = P MTwo
  type MFour  = P MThree
  type MFive  = P MFour
  
  -- | This is the singleton value representing @Zero@ at the term level and
  -- at the type level, simultaneously. Used for raising units to powers.
  sZero  = SZero
  sOne   = SS sZero
  sTwo   = SS sOne
  sThree = SS sTwo
  sFour  = SS sThree
  sFive  = SS sFour
  
  sMOne   = SP sZero
  sMTwo   = SP sMOne
  sMThree = SP sMTwo
  sMFour  = SP sMThree
  sMFive  = SP sMFour
  
  -- | Add one to a singleton @Z@.
  sSucc :: Sing z -> Sing (Succ z)
  sSucc SZero   = sOne
  sSucc (SS z') = SS (SS z')
  sSucc (SP z') = z'
  
  -- | Subtract one from a singleton @Z@.
  sPred :: Sing z -> Sing (Pred z)
  sPred SZero   = sMOne
  sPred (SS z') = z'
  sPred (SP z') = SP (SP z')
  
  -- | Negate a singleton @Z@.
  sNegate :: Sing z -> Sing (Negate z)
  sNegate SZero = SZero
  sNegate (SS z') = SP (sNegate z')
  sNegate (SP z') = SS (sNegate z')
  
  -- | Convert a singleton @Z@ to an @Int@.
  szToInt :: Sing (z :: Z) -> Int
  szToInt = zToInt . fromSing
  
  {-# DEPRECATED pZero, pOne, pTwo, pThree, pFour, pFive, pMOne, pMTwo, pMThree, pMFour, pMFive, pSucc, pPred "The singleton prefix is changing from 'p' to 's'. The 'p' versions will be removed in a future release." #-}
  
  pZero  = sZero
  pOne   = sOne
  pTwo   = sTwo
  pThree = sThree
  pFour  = sFour
  pFive  = sFive
  
  pMOne   = sMOne
  pMTwo   = sMTwo
  pMThree = sMThree
  pMFour  = sMFour
  pMFive  = sMFive
  
  pSucc = sSucc
  pPred = sPred
  