{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE AutoDeriveTypeable #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
#if __GLASGOW_HASKELL__ > 805
{-# LANGUAGE NoStarIsType #-}
#endif
module Numeric.NumType.DK.Integers
(
type TypeInt(..),
Pred, Succ, Negate, Abs, Signum,
type (+), type (-), type (*), type (/), type (^),
pred, succ, negate, abs, signum,
(+), (-), (*), (/), (^),
zero,
pos1, pos2, pos3, pos4, pos5, pos6, pos7, pos8, pos9,
neg1, neg2, neg3, neg4, neg5, neg6, neg7, neg8, neg9,
KnownTypeInt(..)
)
where
import Data.Proxy
import Prelude hiding ((+), (-), (*), (/), (^), pred, succ, negate, abs, signum)
import qualified Prelude
#if MIN_VERSION_base(4, 8, 0)
import qualified GHC.TypeLits as TN
type Z = 0
type N1 = 1
#else
import qualified Numeric.NumType.DK.Naturals as TN
type Z = 'TN.Z
type N1 = 'TN.S 'TN.Z
#endif
infixr 8 ^
infixl 7 *, /
infixl 6 +, -
type family NatPred (n::TN.Nat) :: TN.Nat where NatPred n = n TN.- N1
type family NatSucc (n::TN.Nat) :: TN.Nat where NatSucc n = n TN.+ N1
data TypeInt = Neg10Minus TN.Nat
| Neg9
| Neg8
| Neg7
| Neg6
| Neg5
| Neg4
| Neg3
| Neg2
| Neg1
| Zero
| Pos1
| Pos2
| Pos3
| Pos4
| Pos5
| Pos6
| Pos7
| Pos8
| Pos9
| Pos10Plus TN.Nat
type family Pred (i::TypeInt) :: TypeInt where
Pred ('Neg10Minus n) = 'Neg10Minus (NatSucc n)
Pred 'Neg9 = 'Neg10Minus Z
Pred 'Neg8 = 'Neg9
Pred 'Neg7 = 'Neg8
Pred 'Neg6 = 'Neg7
Pred 'Neg5 = 'Neg6
Pred 'Neg4 = 'Neg5
Pred 'Neg3 = 'Neg4
Pred 'Neg2 = 'Neg3
Pred 'Neg1 = 'Neg2
Pred 'Zero = 'Neg1
Pred 'Pos1 = 'Zero
Pred 'Pos2 = 'Pos1
Pred 'Pos3 = 'Pos2
Pred 'Pos4 = 'Pos3
Pred 'Pos5 = 'Pos4
Pred 'Pos6 = 'Pos5
Pred 'Pos7 = 'Pos6
Pred 'Pos8 = 'Pos7
Pred 'Pos9 = 'Pos8
Pred ('Pos10Plus Z) = 'Pos9
Pred ('Pos10Plus n) = 'Pos10Plus (NatPred n)
type family Succ (i::TypeInt) :: TypeInt where
Succ ('Neg10Minus Z) = 'Neg9
Succ ('Neg10Minus n) = 'Neg10Minus (NatPred n)
Succ 'Neg9 = 'Neg8
Succ 'Neg8 = 'Neg7
Succ 'Neg7 = 'Neg6
Succ 'Neg6 = 'Neg5
Succ 'Neg5 = 'Neg4
Succ 'Neg4 = 'Neg3
Succ 'Neg3 = 'Neg2
Succ 'Neg2 = 'Neg1
Succ 'Neg1 = 'Zero
Succ 'Zero = 'Pos1
Succ 'Pos1 = 'Pos2
Succ 'Pos2 = 'Pos3
Succ 'Pos3 = 'Pos4
Succ 'Pos4 = 'Pos5
Succ 'Pos5 = 'Pos6
Succ 'Pos6 = 'Pos7
Succ 'Pos7 = 'Pos8
Succ 'Pos8 = 'Pos9
Succ 'Pos9 = 'Pos10Plus Z
Succ ('Pos10Plus n) = 'Pos10Plus (NatSucc n)
type family Negate (i::TypeInt) :: TypeInt where
Negate ('Neg10Minus n) = 'Pos10Plus n
Negate 'Neg9 = 'Pos9
Negate 'Neg8 = 'Pos8
Negate 'Neg7 = 'Pos7
Negate 'Neg6 = 'Pos6
Negate 'Neg5 = 'Pos5
Negate 'Neg4 = 'Pos4
Negate 'Neg3 = 'Pos3
Negate 'Neg2 = 'Pos2
Negate 'Neg1 = 'Pos1
Negate 'Zero = 'Zero
Negate 'Pos1 = 'Neg1
Negate 'Pos2 = 'Neg2
Negate 'Pos3 = 'Neg3
Negate 'Pos4 = 'Neg4
Negate 'Pos5 = 'Neg5
Negate 'Pos6 = 'Neg6
Negate 'Pos7 = 'Neg7
Negate 'Pos8 = 'Neg8
Negate 'Pos9 = 'Neg9
Negate ('Pos10Plus n) = 'Neg10Minus n
type family Abs (i::TypeInt) :: TypeInt where
Abs ('Neg10Minus n) = 'Pos10Plus n
Abs 'Neg9 = 'Pos9
Abs 'Neg8 = 'Pos8
Abs 'Neg7 = 'Pos7
Abs 'Neg6 = 'Pos6
Abs 'Neg5 = 'Pos5
Abs 'Neg4 = 'Pos4
Abs 'Neg3 = 'Pos3
Abs 'Neg2 = 'Pos2
Abs 'Neg1 = 'Pos1
Abs i = i
type family Signum (i::TypeInt) :: TypeInt where
Signum ('Neg10Minus n) = 'Neg1
Signum 'Neg9 = 'Neg1
Signum 'Neg8 = 'Neg1
Signum 'Neg7 = 'Neg1
Signum 'Neg6 = 'Neg1
Signum 'Neg5 = 'Neg1
Signum 'Neg4 = 'Neg1
Signum 'Neg3 = 'Neg1
Signum 'Neg2 = 'Neg1
Signum 'Neg1 = 'Neg1
Signum 'Zero = 'Zero
Signum i = 'Pos1
type family (i::TypeInt) + (i'::TypeInt) :: TypeInt where
'Zero + i = i
i + 'Neg10Minus n = Pred i + Succ ('Neg10Minus n)
i + 'Neg9 = Pred i + 'Neg8
i + 'Neg8 = Pred i + 'Neg7
i + 'Neg7 = Pred i + 'Neg6
i + 'Neg6 = Pred i + 'Neg5
i + 'Neg5 = Pred i + 'Neg4
i + 'Neg4 = Pred i + 'Neg3
i + 'Neg3 = Pred i + 'Neg2
i + 'Neg2 = Pred i + 'Neg1
i + 'Neg1 = Pred i
i + 'Zero = i
i + i' = Succ i + Pred i'
type family (i::TypeInt) - (i'::TypeInt) :: TypeInt where
i - i' = i + Negate i'
type family (i::TypeInt) * (i'::TypeInt) :: TypeInt
where
'Zero * i = 'Zero
i * 'Zero = 'Zero
i * 'Pos1 = i
i * 'Pos2 = i + i
i * 'Pos3 = i + i + i
i * 'Pos4 = i + i + i + i
i * 'Pos5 = i + i + i + i + i
i * 'Pos6 = i + i + i + i + i + i
i * 'Pos7 = i + i + i + i + i + i + i
i * 'Pos8 = i + i + i + i + i + i + i + i
i * 'Pos9 = i + i + i + i + i + i + i + i + i
i * 'Pos10Plus n = i + i * Pred ('Pos10Plus n)
i * i' = Negate (i * Negate i')
type family (i::TypeInt) ^ (i'::TypeInt) :: TypeInt
where
i ^ 'Zero = 'Pos1
i ^ 'Pos1 = i
i ^ 'Pos2 = i * i
i ^ 'Pos3 = i * i * i
i ^ 'Pos4 = i * i * i * i
i ^ 'Pos5 = i * i * i * i * i
i ^ 'Pos6 = i * i * i * i * i * i
i ^ 'Pos7 = i * i * i * i * i * i * i
i ^ 'Pos8 = i * i * i * i * i * i * i * i
i ^ 'Pos9 = i * i * i * i * i * i * i * i * i
i ^ 'Pos10Plus n = i * i ^ Pred ('Pos10Plus n)
type family (i::TypeInt) / (i'::TypeInt) :: TypeInt
where
i / 'Pos1 = i
i / 'Neg1 = Negate i
'Zero / ('Neg10Minus n) = 'Zero
'Zero / 'Neg9 = 'Zero
'Zero / 'Neg8 = 'Zero
'Zero / 'Neg7 = 'Zero
'Zero / 'Neg6 = 'Zero
'Zero / 'Neg5 = 'Zero
'Zero / 'Neg4 = 'Zero
'Zero / 'Neg3 = 'Zero
'Zero / 'Neg2 = 'Zero
'Zero / 'Pos2 = 'Zero
'Zero / 'Pos3 = 'Zero
'Zero / 'Pos4 = 'Zero
'Zero / 'Pos5 = 'Zero
'Zero / 'Pos6 = 'Zero
'Zero / 'Pos7 = 'Zero
'Zero / 'Pos8 = 'Zero
'Zero / 'Pos9 = 'Zero
'Zero / ('Pos10Plus n) = 'Zero
'Neg2 / 'Neg2 = 'Pos1
'Neg3 / 'Neg3 = 'Pos1
'Neg4 / 'Neg4 = 'Pos1
'Neg5 / 'Neg5 = 'Pos1
'Neg6 / 'Neg6 = 'Pos1
'Neg7 / 'Neg7 = 'Pos1
'Neg8 / 'Neg8 = 'Pos1
'Neg9 / 'Neg9 = 'Pos1
'Neg10Minus n / 'Neg10Minus n = 'Pos1
'Neg2 / 'Pos2 = 'Neg1
'Neg3 / 'Pos3 = 'Neg1
'Neg4 / 'Pos4 = 'Neg1
'Neg5 / 'Pos5 = 'Neg1
'Neg6 / 'Pos6 = 'Neg1
'Neg7 / 'Pos7 = 'Neg1
'Neg8 / 'Pos8 = 'Neg1
'Neg9 / 'Pos9 = 'Neg1
'Neg10Minus n / 'Pos10Plus n = 'Neg1
'Pos2 / 'Neg2 = 'Neg1
'Pos3 / 'Neg3 = 'Neg1
'Pos4 / 'Neg4 = 'Neg1
'Pos5 / 'Neg5 = 'Neg1
'Pos6 / 'Neg6 = 'Neg1
'Pos7 / 'Neg7 = 'Neg1
'Pos8 / 'Neg8 = 'Neg1
'Pos9 / 'Neg9 = 'Neg1
'Pos10Plus n / 'Neg10Minus n = 'Neg1
'Pos2 / 'Pos2 = 'Pos1
'Pos3 / 'Pos3 = 'Pos1
'Pos4 / 'Pos4 = 'Pos1
'Pos5 / 'Pos5 = 'Pos1
'Pos6 / 'Pos6 = 'Pos1
'Pos7 / 'Pos7 = 'Pos1
'Pos8 / 'Pos8 = 'Pos1
'Pos9 / 'Pos9 = 'Pos1
'Pos10Plus n / 'Pos10Plus n = 'Pos1
'Neg4 / 'Neg2 = 'Pos2
'Neg6 / 'Neg2 = 'Pos3
'Neg8 / 'Neg2 = 'Pos4
'Neg6 / 'Neg3 = 'Pos2
'Neg9 / 'Neg3 = 'Pos3
'Neg8 / 'Neg4 = 'Pos2
'Neg10Minus n / i = ('Neg10Minus n + Abs i) / i - Signum i
'Neg4 / 'Pos2 = 'Neg2
'Neg6 / 'Pos2 = 'Neg3
'Neg8 / 'Pos2 = 'Neg4
'Neg6 / 'Pos3 = 'Neg2
'Neg9 / 'Pos3 = 'Neg3
'Neg8 / 'Pos4 = 'Neg2
'Pos4 / 'Neg2 = 'Neg2
'Pos6 / 'Neg2 = 'Neg3
'Pos8 / 'Neg2 = 'Neg4
'Pos6 / 'Neg3 = 'Neg2
'Pos9 / 'Neg3 = 'Neg3
'Pos8 / 'Neg4 = 'Neg2
'Pos4 / 'Pos2 = 'Pos2
'Pos6 / 'Pos2 = 'Pos3
'Pos8 / 'Pos2 = 'Pos4
'Pos6 / 'Pos3 = 'Pos2
'Pos9 / 'Pos3 = 'Pos3
'Pos8 / 'Pos4 = 'Pos2
'Pos10Plus n / i = ('Pos10Plus n - Abs i) / i + Signum i
pred :: Proxy i -> Proxy (Pred i); pred :: Proxy i -> Proxy (Pred i)
pred Proxy i
_ = Proxy (Pred i)
forall k (t :: k). Proxy t
Proxy
succ :: Proxy i -> Proxy (Succ i); succ :: Proxy i -> Proxy (Succ i)
succ Proxy i
_ = Proxy (Succ i)
forall k (t :: k). Proxy t
Proxy
negate :: Proxy i -> Proxy (Negate i); negate :: Proxy i -> Proxy (Negate i)
negate Proxy i
_ = Proxy (Negate i)
forall k (t :: k). Proxy t
Proxy
abs :: Proxy i -> Proxy (Abs i); abs :: Proxy i -> Proxy (Abs i)
abs Proxy i
_ = Proxy (Abs i)
forall k (t :: k). Proxy t
Proxy
signum :: Proxy i -> Proxy (Signum i); signum :: Proxy i -> Proxy (Signum i)
signum Proxy i
_ = Proxy (Signum i)
forall k (t :: k). Proxy t
Proxy
(+) :: Proxy i -> Proxy i' -> Proxy (i + i'); Proxy i
_ + :: Proxy i -> Proxy i' -> Proxy (i + i')
+ Proxy i'
_ = Proxy (i + i')
forall k (t :: k). Proxy t
Proxy
(-) :: Proxy i -> Proxy i' -> Proxy (i - i'); Proxy i
_ - :: Proxy i -> Proxy i' -> Proxy (i - i')
- Proxy i'
_ = Proxy (i - i')
forall k (t :: k). Proxy t
Proxy
(*) :: Proxy i -> Proxy i' -> Proxy (i * i'); Proxy i
_ * :: Proxy i -> Proxy i' -> Proxy (i * i')
* Proxy i'
_ = Proxy (i * i')
forall k (t :: k). Proxy t
Proxy
(/) :: Proxy i -> Proxy i' -> Proxy (i / i'); Proxy i
_ / :: Proxy i -> Proxy i' -> Proxy (i / i')
/ Proxy i'
_ = Proxy (i / i')
forall k (t :: k). Proxy t
Proxy
(^) :: Proxy i -> Proxy i' -> Proxy (i ^ i'); Proxy i
_ ^ :: Proxy i -> Proxy i' -> Proxy (i ^ i')
^ Proxy i'
_ = Proxy (i ^ i')
forall k (t :: k). Proxy t
Proxy
neg9 :: Proxy 'Neg9
neg9 :: Proxy 'Neg9
neg9 = Proxy 'Neg9
forall k (t :: k). Proxy t
Proxy :: Proxy 'Neg9
neg8 :: Proxy 'Neg8
neg8 :: Proxy 'Neg8
neg8 = Proxy 'Neg8
forall k (t :: k). Proxy t
Proxy :: Proxy 'Neg8
neg7 :: Proxy 'Neg7
neg7 :: Proxy 'Neg7
neg7 = Proxy 'Neg7
forall k (t :: k). Proxy t
Proxy :: Proxy 'Neg7
neg6 :: Proxy 'Neg6
neg6 :: Proxy 'Neg6
neg6 = Proxy 'Neg6
forall k (t :: k). Proxy t
Proxy :: Proxy 'Neg6
neg5 :: Proxy 'Neg5
neg5 :: Proxy 'Neg5
neg5 = Proxy 'Neg5
forall k (t :: k). Proxy t
Proxy :: Proxy 'Neg5
neg4 :: Proxy 'Neg4
neg4 :: Proxy 'Neg4
neg4 = Proxy 'Neg4
forall k (t :: k). Proxy t
Proxy :: Proxy 'Neg4
neg3 :: Proxy 'Neg3
neg3 :: Proxy 'Neg3
neg3 = Proxy 'Neg3
forall k (t :: k). Proxy t
Proxy :: Proxy 'Neg3
neg2 :: Proxy 'Neg2
neg2 :: Proxy 'Neg2
neg2 = Proxy 'Neg2
forall k (t :: k). Proxy t
Proxy :: Proxy 'Neg2
neg1 :: Proxy 'Neg1
neg1 :: Proxy 'Neg1
neg1 = Proxy 'Neg1
forall k (t :: k). Proxy t
Proxy :: Proxy 'Neg1
zero :: Proxy 'Zero
zero :: Proxy 'Zero
zero = Proxy 'Zero
forall k (t :: k). Proxy t
Proxy :: Proxy 'Zero
pos1 :: Proxy 'Pos1
pos1 :: Proxy 'Pos1
pos1 = Proxy 'Pos1
forall k (t :: k). Proxy t
Proxy :: Proxy 'Pos1
pos2 :: Proxy 'Pos2
pos2 :: Proxy 'Pos2
pos2 = Proxy 'Pos2
forall k (t :: k). Proxy t
Proxy :: Proxy 'Pos2
pos3 :: Proxy 'Pos3
pos3 :: Proxy 'Pos3
pos3 = Proxy 'Pos3
forall k (t :: k). Proxy t
Proxy :: Proxy 'Pos3
pos4 :: Proxy 'Pos4
pos4 :: Proxy 'Pos4
pos4 = Proxy 'Pos4
forall k (t :: k). Proxy t
Proxy :: Proxy 'Pos4
pos5 :: Proxy 'Pos5
pos5 :: Proxy 'Pos5
pos5 = Proxy 'Pos5
forall k (t :: k). Proxy t
Proxy :: Proxy 'Pos5
pos6 :: Proxy 'Pos6
pos6 :: Proxy 'Pos6
pos6 = Proxy 'Pos6
forall k (t :: k). Proxy t
Proxy :: Proxy 'Pos6
pos7 :: Proxy 'Pos7
pos7 :: Proxy 'Pos7
pos7 = Proxy 'Pos7
forall k (t :: k). Proxy t
Proxy :: Proxy 'Pos7
pos8 :: Proxy 'Pos8
pos8 :: Proxy 'Pos8
pos8 = Proxy 'Pos8
forall k (t :: k). Proxy t
Proxy :: Proxy 'Pos8
pos9 :: Proxy 'Pos9
pos9 :: Proxy 'Pos9
pos9 = Proxy 'Pos9
forall k (t :: k). Proxy t
Proxy :: Proxy 'Pos9
class KnownTypeInt (i::TypeInt) where toNum :: Num a => Proxy i -> a
instance KnownTypeInt (Succ ('Neg10Minus n)) => KnownTypeInt ('Neg10Minus n)
where toNum :: Proxy ('Neg10Minus n) -> a
toNum = (a -> a -> a
forall a. Num a => a -> a -> a
Prelude.- a
1) (a -> a)
-> (Proxy ('Neg10Minus n) -> a) -> Proxy ('Neg10Minus n) -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy (Succ ('Neg10Minus n)) -> a
forall (i :: TypeInt) a. (KnownTypeInt i, Num a) => Proxy i -> a
toNum (Proxy (Succ ('Neg10Minus n)) -> a)
-> (Proxy ('Neg10Minus n) -> Proxy (Succ ('Neg10Minus n)))
-> Proxy ('Neg10Minus n)
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy ('Neg10Minus n) -> Proxy (Succ ('Neg10Minus n))
forall (i :: TypeInt). Proxy i -> Proxy (Succ i)
succ
instance KnownTypeInt 'Neg9 where toNum :: Proxy 'Neg9 -> a
toNum Proxy 'Neg9
_ = -a
9
instance KnownTypeInt 'Neg8 where toNum :: Proxy 'Neg8 -> a
toNum Proxy 'Neg8
_ = -a
8
instance KnownTypeInt 'Neg7 where toNum :: Proxy 'Neg7 -> a
toNum Proxy 'Neg7
_ = -a
7
instance KnownTypeInt 'Neg6 where toNum :: Proxy 'Neg6 -> a
toNum Proxy 'Neg6
_ = -a
6
instance KnownTypeInt 'Neg5 where toNum :: Proxy 'Neg5 -> a
toNum Proxy 'Neg5
_ = -a
5
instance KnownTypeInt 'Neg4 where toNum :: Proxy 'Neg4 -> a
toNum Proxy 'Neg4
_ = -a
4
instance KnownTypeInt 'Neg3 where toNum :: Proxy 'Neg3 -> a
toNum Proxy 'Neg3
_ = -a
3
instance KnownTypeInt 'Neg2 where toNum :: Proxy 'Neg2 -> a
toNum Proxy 'Neg2
_ = -a
2
instance KnownTypeInt 'Neg1 where toNum :: Proxy 'Neg1 -> a
toNum Proxy 'Neg1
_ = -a
1
instance KnownTypeInt 'Zero where toNum :: Proxy 'Zero -> a
toNum Proxy 'Zero
_ = a
0
instance KnownTypeInt 'Pos1 where toNum :: Proxy 'Pos1 -> a
toNum Proxy 'Pos1
_ = a
1
instance KnownTypeInt 'Pos2 where toNum :: Proxy 'Pos2 -> a
toNum Proxy 'Pos2
_ = a
2
instance KnownTypeInt 'Pos3 where toNum :: Proxy 'Pos3 -> a
toNum Proxy 'Pos3
_ = a
3
instance KnownTypeInt 'Pos4 where toNum :: Proxy 'Pos4 -> a
toNum Proxy 'Pos4
_ = a
4
instance KnownTypeInt 'Pos5 where toNum :: Proxy 'Pos5 -> a
toNum Proxy 'Pos5
_ = a
5
instance KnownTypeInt 'Pos6 where toNum :: Proxy 'Pos6 -> a
toNum Proxy 'Pos6
_ = a
6
instance KnownTypeInt 'Pos7 where toNum :: Proxy 'Pos7 -> a
toNum Proxy 'Pos7
_ = a
7
instance KnownTypeInt 'Pos8 where toNum :: Proxy 'Pos8 -> a
toNum Proxy 'Pos8
_ = a
8
instance KnownTypeInt 'Pos9 where toNum :: Proxy 'Pos9 -> a
toNum Proxy 'Pos9
_ = a
9
instance KnownTypeInt (Pred ('Pos10Plus n)) => KnownTypeInt ('Pos10Plus n)
where toNum :: Proxy ('Pos10Plus n) -> a
toNum = (a -> a -> a
forall a. Num a => a -> a -> a
Prelude.+ a
1) (a -> a)
-> (Proxy ('Pos10Plus n) -> a) -> Proxy ('Pos10Plus n) -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy (Pred ('Pos10Plus n)) -> a
forall (i :: TypeInt) a. (KnownTypeInt i, Num a) => Proxy i -> a
toNum (Proxy (Pred ('Pos10Plus n)) -> a)
-> (Proxy ('Pos10Plus n) -> Proxy (Pred ('Pos10Plus n)))
-> Proxy ('Pos10Plus n)
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy ('Pos10Plus n) -> Proxy (Pred ('Pos10Plus n))
forall (i :: TypeInt). Proxy i -> Proxy (Pred i)
pred