{- 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 #-}
#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 :: Z -> Int
zToInt Z
Zero = Int
0
zToInt (S Z
z) = Z -> Int
zToInt Z
z Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
zToInt (P Z
z) = Z -> Int
zToInt Z
z Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
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 :: SZ 'Zero
sZero  = SZ 'Zero
SZero
sOne :: SZ ('S 'Zero)
sOne   = Sing 'Zero -> SZ ('S 'Zero)
forall (n :: Z). Sing n -> SZ ('S n)
SS Sing 'Zero
SZ 'Zero
sZero
sTwo :: SZ ('S ('S 'Zero))
sTwo   = Sing ('S 'Zero) -> SZ ('S ('S 'Zero))
forall (n :: Z). Sing n -> SZ ('S n)
SS Sing ('S 'Zero)
SZ ('S 'Zero)
sOne
sThree :: SZ ('S ('S ('S 'Zero)))
sThree = Sing ('S ('S 'Zero)) -> SZ ('S ('S ('S 'Zero)))
forall (n :: Z). Sing n -> SZ ('S n)
SS Sing ('S ('S 'Zero))
SZ ('S ('S 'Zero))
sTwo
sFour :: SZ ('S ('S ('S ('S 'Zero))))
sFour  = Sing ('S ('S ('S 'Zero))) -> SZ ('S ('S ('S ('S 'Zero))))
forall (n :: Z). Sing n -> SZ ('S n)
SS Sing ('S ('S ('S 'Zero)))
SZ ('S ('S ('S 'Zero)))
sThree
sFive :: SZ ('S ('S ('S ('S ('S 'Zero)))))
sFive  = Sing ('S ('S ('S ('S 'Zero)))) -> SZ ('S ('S ('S ('S ('S 'Zero)))))
forall (n :: Z). Sing n -> SZ ('S n)
SS Sing ('S ('S ('S ('S 'Zero))))
SZ ('S ('S ('S ('S 'Zero))))
sFour

sMOne :: SZ ('P 'Zero)
sMOne   = Sing 'Zero -> SZ ('P 'Zero)
forall (n :: Z). Sing n -> SZ ('P n)
SP Sing 'Zero
SZ 'Zero
sZero
sMTwo :: SZ ('P ('P 'Zero))
sMTwo   = Sing ('P 'Zero) -> SZ ('P ('P 'Zero))
forall (n :: Z). Sing n -> SZ ('P n)
SP Sing ('P 'Zero)
SZ ('P 'Zero)
sMOne
sMThree :: SZ ('P ('P ('P 'Zero)))
sMThree = Sing ('P ('P 'Zero)) -> SZ ('P ('P ('P 'Zero)))
forall (n :: Z). Sing n -> SZ ('P n)
SP Sing ('P ('P 'Zero))
SZ ('P ('P 'Zero))
sMTwo
sMFour :: SZ ('P ('P ('P ('P 'Zero))))
sMFour  = Sing ('P ('P ('P 'Zero))) -> SZ ('P ('P ('P ('P 'Zero))))
forall (n :: Z). Sing n -> SZ ('P n)
SP Sing ('P ('P ('P 'Zero)))
SZ ('P ('P ('P 'Zero)))
sMThree
sMFive :: SZ ('P ('P ('P ('P ('P 'Zero)))))
sMFive  = Sing ('P ('P ('P ('P 'Zero)))) -> SZ ('P ('P ('P ('P ('P 'Zero)))))
forall (n :: Z). Sing n -> SZ ('P n)
SP Sing ('P ('P ('P ('P 'Zero))))
SZ ('P ('P ('P ('P 'Zero))))
sMFour

-- | Add one to a singleton @Z@.
sSucc :: Sing z -> Sing (Succ z)
sSucc :: Sing z -> Sing (Succ z)
sSucc Sing z
SZero   = Sing (Succ z)
SZ ('S 'Zero)
sOne
sSucc (SS z') = Sing ('S n) -> SZ ('S ('S n))
forall (n :: Z). Sing n -> SZ ('S n)
SS (Sing n -> SZ ('S n)
forall (n :: Z). Sing n -> SZ ('S n)
SS Sing n
z')
sSucc (SP z') = Sing n
Sing (Succ z)
z'

-- | Subtract one from a singleton @Z@.
sPred :: Sing z -> Sing (Pred z)
sPred :: Sing z -> Sing (Pred z)
sPred Sing z
SZero   = Sing (Pred z)
SZ ('P 'Zero)
sMOne
sPred (SS z') = Sing n
Sing (Pred z)
z'
sPred (SP z') = Sing ('P n) -> SZ ('P ('P n))
forall (n :: Z). Sing n -> SZ ('P n)
SP (Sing n -> SZ ('P n)
forall (n :: Z). Sing n -> SZ ('P n)
SP Sing n
z')

-- | Negate a singleton @Z@.
sNegate :: Sing z -> Sing (Negate z)
sNegate :: Sing z -> Sing (Negate z)
sNegate Sing z
SZero = Sing (Negate z)
SZ 'Zero
SZero
sNegate (SS z') = Sing (Negate n) -> SZ ('P (Negate n))
forall (n :: Z). Sing n -> SZ ('P n)
SP (Sing n -> Sing (Negate n)
forall (z :: Z). Sing z -> Sing (Negate z)
sNegate Sing n
z')
sNegate (SP z') = Sing (Negate n) -> SZ ('S (Negate n))
forall (n :: Z). Sing n -> SZ ('S n)
SS (Sing n -> Sing (Negate n)
forall (z :: Z). Sing z -> Sing (Negate z)
sNegate Sing n
z')

-- | Convert a singleton @Z@ to an @Int@.
szToInt :: Sing (z :: Z) -> Int
szToInt :: Sing z -> Int
szToInt = Z -> Int
zToInt (Z -> Int) -> (SZ z -> Z) -> SZ z -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SZ z -> Z
forall k (a :: k). SingKind k => Sing a -> Demote k
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 :: SZ 'Zero
pZero  = SZ 'Zero
sZero
pOne :: SZ ('S 'Zero)
pOne   = SZ ('S 'Zero)
sOne
pTwo :: SZ ('S ('S 'Zero))
pTwo   = SZ ('S ('S 'Zero))
sTwo
pThree :: SZ ('S ('S ('S 'Zero)))
pThree = SZ ('S ('S ('S 'Zero)))
sThree
pFour :: SZ ('S ('S ('S ('S 'Zero))))
pFour  = SZ ('S ('S ('S ('S 'Zero))))
sFour
pFive :: SZ ('S ('S ('S ('S ('S 'Zero)))))
pFive  = SZ ('S ('S ('S ('S ('S 'Zero)))))
sFive

pMOne :: SZ ('P 'Zero)
pMOne   = SZ ('P 'Zero)
sMOne
pMTwo :: SZ ('P ('P 'Zero))
pMTwo   = SZ ('P ('P 'Zero))
sMTwo
pMThree :: SZ ('P ('P ('P 'Zero)))
pMThree = SZ ('P ('P ('P 'Zero)))
sMThree
pMFour :: SZ ('P ('P ('P ('P 'Zero))))
pMFour  = SZ ('P ('P ('P ('P 'Zero))))
sMFour
pMFive :: SZ ('P ('P ('P ('P ('P 'Zero)))))
pMFive  = SZ ('P ('P ('P ('P ('P 'Zero)))))
sMFive

pSucc :: Sing z -> Sing (Succ z)
pSucc = Sing z -> Sing (Succ z)
forall (z :: Z). Sing z -> Sing (Succ z)
sSucc
pPred :: Sing z -> Sing (Pred z)
pPred = Sing z -> Sing (Pred z)
forall (z :: Z). Sing z -> Sing (Pred z)
sPred