{-# LANGUAGE MagicHash #-}
{-# LANGUAGE UndecidableInstances #-}
module KindInteger
(
Integer
, type P
, type N
, Normalize
, KnownInteger(integerSing), integerVal, integerVal'
, SomeInteger(..)
, someIntegerVal
, sameInteger
, SInteger
, pattern SInteger
, fromSInteger
, withSomeSInteger
, withKnownInteger
, type (+), type (*), type (^), type (-)
, Negate, Div, Mod, Quot, Rem, Log2
, CmpInteger
, cmpInteger
, type (==?), type (==), type (/=?), type (/=)
) where
import GHC.Base (WithDict(..))
import GHC.Types (TYPE, Constraint)
import GHC.Show (appPrec, appPrec1)
import GHC.Prim (Proxy#)
import GHC.TypeLits qualified as L
import Data.Proxy
import Data.Type.Coercion
import Data.Type.Equality (TestEquality(..), (:~:)(..))
import Data.Type.Bool (If)
import Data.Type.Ord
import Numeric.Natural (Natural)
import Prelude hiding (Integer, (==), (/=))
import Prelude qualified as P
import Unsafe.Coerce(unsafeCoerce)
data Integer
= Positive Natural
| Negative Natural
type P (x :: Natural) = 'Positive x :: Integer
type N (x :: Natural) = 'Negative x :: Integer
termIntegerToTypeInteger :: P.Integer -> Integer
termIntegerToTypeInteger :: Integer -> Integer
termIntegerToTypeInteger Integer
i = let n :: Natural
n = Integer -> Natural
forall a. Num a => Integer -> a
fromInteger Integer
i
in if Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 then Natural -> Integer
Positive Natural
n else Natural -> Integer
Negative Natural
n
showsPrecInteger :: Int -> Integer -> ShowS
showsPrecInteger :: Int -> Integer -> ShowS
showsPrecInteger Int
p Integer
i = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
appPrec) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ case Integer
i of
Positive Natural
x -> String -> ShowS
showString String
"P " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> ShowS
forall a. Show a => a -> ShowS
shows Natural
x
Negative Natural
x -> String -> ShowS
showString String
"N " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> ShowS
forall a. Show a => a -> ShowS
shows Natural
x
class KnownInteger (i :: Integer) where
integerSing :: SInteger i
instance L.KnownNat x => KnownInteger (P x) where
integerSing :: SInteger (P x)
integerSing = Integer -> SInteger (P x)
forall (i :: Integer). Integer -> SInteger i
UnsafeSInteger (Proxy x -> Integer
forall (n :: Natural) (proxy :: Natural -> Type).
KnownNat n =>
proxy n -> Integer
L.natVal (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @x))
instance L.KnownNat x => KnownInteger (N x) where
integerSing :: SInteger (N x)
integerSing = Integer -> SInteger (N x)
forall (i :: Integer). Integer -> SInteger i
UnsafeSInteger (Integer -> Integer
forall a. Num a => a -> a
negate (Proxy x -> Integer
forall (n :: Natural) (proxy :: Natural -> Type).
KnownNat n =>
proxy n -> Integer
L.natVal (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @x)))
integerVal :: forall i proxy. KnownInteger i => proxy i -> P.Integer
integerVal :: forall (i :: Integer) (proxy :: Integer -> Type).
KnownInteger i =>
proxy i -> Integer
integerVal proxy i
_ = case SInteger i
forall (i :: Integer). KnownInteger i => SInteger i
integerSing :: SInteger i of UnsafeSInteger Integer
x -> Integer
x
integerVal' :: forall i. KnownInteger i => Proxy# i -> P.Integer
integerVal' :: forall (i :: Integer). KnownInteger i => Proxy# i -> Integer
integerVal' Proxy# i
_ = case SInteger i
forall (i :: Integer). KnownInteger i => SInteger i
integerSing :: SInteger i of UnsafeSInteger Integer
x -> Integer
x
data SomeInteger = forall n. KnownInteger n => SomeInteger (Proxy n)
someIntegerVal :: P.Integer -> SomeInteger
someIntegerVal :: Integer -> SomeInteger
someIntegerVal Integer
i = Integer
-> (forall (n :: Integer). SInteger n -> SomeInteger)
-> SomeInteger
forall r. Integer -> (forall (n :: Integer). SInteger n -> r) -> r
withSomeSInteger Integer
i (\(SInteger n
si :: SInteger i) ->
SInteger n -> (KnownInteger n => SomeInteger) -> SomeInteger
forall (i :: Integer) r. SInteger i -> (KnownInteger i => r) -> r
withKnownInteger SInteger n
si (forall (n :: Integer). KnownInteger n => Proxy n -> SomeInteger
SomeInteger @i Proxy n
forall {k} (t :: k). Proxy t
Proxy))
instance Eq SomeInteger where
SomeInteger Proxy n
x == :: SomeInteger -> SomeInteger -> Bool
== SomeInteger Proxy n
y = Proxy n -> Integer
forall (i :: Integer) (proxy :: Integer -> Type).
KnownInteger i =>
proxy i -> Integer
integerVal Proxy n
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
P.== Proxy n -> Integer
forall (i :: Integer) (proxy :: Integer -> Type).
KnownInteger i =>
proxy i -> Integer
integerVal Proxy n
y
instance Ord SomeInteger where
compare :: SomeInteger -> SomeInteger -> Ordering
compare (SomeInteger Proxy n
x) (SomeInteger Proxy n
y) =
Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Proxy n -> Integer
forall (i :: Integer) (proxy :: Integer -> Type).
KnownInteger i =>
proxy i -> Integer
integerVal Proxy n
x) (Proxy n -> Integer
forall (i :: Integer) (proxy :: Integer -> Type).
KnownInteger i =>
proxy i -> Integer
integerVal Proxy n
y)
instance Show SomeInteger where
showsPrec :: Int -> SomeInteger -> ShowS
showsPrec Int
p (SomeInteger Proxy n
x) = Int -> Integer -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p (Proxy n -> Integer
forall (i :: Integer) (proxy :: Integer -> Type).
KnownInteger i =>
proxy i -> Integer
integerVal Proxy n
x)
instance Read SomeInteger where
readsPrec :: Int -> ReadS SomeInteger
readsPrec Int
p String
xs = do (Integer
a, String
ys) <- Int -> ReadS Integer
forall a. Read a => Int -> ReadS a
readsPrec Int
p String
xs
[(Integer -> SomeInteger
someIntegerVal Integer
a, String
ys)]
type family Normalize (i :: Integer) :: Integer where
Normalize (N 0) = P 0
Normalize i = i
type NN (a :: Natural) = Normalize (N a) :: Integer
infixl 6 +, -
infixl 7 *, `Div`, `Mod`, `Quot`, `Rem`
infixr 8 ^
type family Negate (x :: Integer) :: Integer where
Negate (P 0) = P 0
Negate (P x) = N x
Negate (N x) = P x
type (a :: Integer) + (b :: Integer) = Add_ (Normalize a) (Normalize b) :: Integer
type family Add_ (a :: Integer) (b :: Integer) :: Integer where
Add_ (P a) (P b) = P (a L.+ b)
Add_ (N a) (N b) = NN (a L.+ b)
Add_ (P a) (N b) = If (b <=? a) (P (a L.- b)) (NN (b L.- a))
Add_ (N a) (P b) = Add_ (P b) (N a)
type (a :: Integer) * (b :: Integer) = Mul_ (Normalize a) (Normalize b) :: Integer
type family Mul_ (a :: Integer) (b :: Integer) :: Integer where
Mul_ (P a) (P b) = P (a L.* b)
Mul_ (N a) (N b) = Mul_ (P a) (P b)
Mul_ (P a) (N b) = NN (a L.* b)
Mul_ (N a) (P b) = Mul_ (P a) (N b)
type (a :: Integer) ^ (b :: Integer) = Pow_ (Normalize a) (Normalize b) :: Integer
type family Pow_ (a :: Integer) (b :: Integer) :: Integer where
Pow_ (P a) (P b) = P (a L.^ b)
Pow_ (N a) (P b) = NN (a L.^ b)
Pow_ _ (N _) = L.TypeError ('L.Text "KindInteger.(^): Negative exponent")
type (a :: Integer) - (b :: Integer) = a + Negate b :: Integer
type Div (a :: Integer) (b :: Integer) = Div_ (Normalize a) (Normalize b) :: Integer
type family Div_ (a :: Integer) (b :: Integer) :: Integer where
Div_ _ (P 0) = L.TypeError ('L.Text "KindInteger.Div: Division by zero")
Div_ (P a) (P b) = P (L.Div a b)
Div_ (N a) (N b) = Div_ (P a) (P b)
Div_ (P a) (N b) = NN (If (b L.* (L.Div a b) ==? a) (L.Div a b) (L.Div a b L.+ 1))
Div_ (N a) (P b) = Div_ (P a) (N b)
type Mod (a :: Integer) (b :: Integer) = Div a b * Negate b + a :: Integer
type Quot (a :: Integer) (b :: Integer) = Quot_ (Normalize a) (Normalize b) :: Integer
type family Quot_ (a :: Integer) (b :: Integer) :: Integer where
Quot_ _ (P 0) = L.TypeError ('L.Text "KindInteger.Quot: Division by zero")
Quot_ (P a) (P b) = P (L.Div a b)
Quot_ (N a) (N b) = Quot_ (P a) (P b)
Quot_ (P a) (N b) = Negate (Quot_ (P a) (P b))
Quot_ (N a) (P b) = Quot_ (P a) (N b)
type Rem (a :: Integer) (b :: Integer) = Quot a b * Negate b + a :: Integer
type Log2 (a :: Integer) = Log2_ (Normalize a) :: Integer
type family Log2_ (a :: Integer) :: Integer where
Log2_ (P 0) = L.TypeError ('L.Text "KindInteger.Log2: Logarithm of zero")
Log2_ (P a) = P (L.Log2 a)
Log2_ (N a) = L.TypeError ('L.Text "KindInteger.Log2: Logarithm of negative number")
type CmpInteger (a :: Integer) (b :: Integer) = CmpInteger_ (Normalize a) (Normalize b) :: Ordering
type family CmpInteger_ (a :: Integer) (b :: Integer) :: Ordering where
CmpInteger_ a a = 'EQ
CmpInteger_ (P a) (P b) = Compare a b
CmpInteger_ (N a) (N b) = Compare b a
CmpInteger_ (N _) (P _) = 'LT
CmpInteger_ (P _) (N _) = 'GT
type instance Compare (a :: Integer) (b :: Integer) = CmpInteger a b :: Ordering
sameInteger
:: forall a b proxy1 proxy2
. (KnownInteger a, KnownInteger b)
=> proxy1 a
-> proxy2 b
-> Maybe (a :~: b)
sameInteger :: forall (a :: Integer) (b :: Integer) (proxy1 :: Integer -> Type)
(proxy2 :: Integer -> Type).
(KnownInteger a, KnownInteger b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameInteger proxy1 a
_ proxy2 b
_ = SInteger a -> SInteger b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Integer) (b :: Integer).
SInteger a -> SInteger b -> Maybe (a :~: b)
testEquality (forall (i :: Integer). KnownInteger i => SInteger i
integerSing @a) (forall (i :: Integer). KnownInteger i => SInteger i
integerSing @b)
cmpInteger
:: forall a b proxy1 proxy2
. (KnownInteger a, KnownInteger b)
=> proxy1 a
-> proxy2 b
-> OrderingI a b
cmpInteger :: forall (a :: Integer) (b :: Integer) (proxy1 :: Integer -> Type)
(proxy2 :: Integer -> Type).
(KnownInteger a, KnownInteger b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpInteger proxy1 a
x proxy2 b
y = case Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (proxy1 a -> Integer
forall (i :: Integer) (proxy :: Integer -> Type).
KnownInteger i =>
proxy i -> Integer
integerVal proxy1 a
x) (proxy2 b -> Integer
forall (i :: Integer) (proxy :: Integer -> Type).
KnownInteger i =>
proxy i -> Integer
integerVal proxy2 b
y) of
Ordering
EQ -> case (Any :~: Any, Any :~: Any)
-> (CmpInteger_ (Normalize a) (Normalize b) :~: 'EQ, a :~: b)
forall a b. a -> b
unsafeCoerce (Any :~: Any
forall {k} (a :: k). a :~: a
Refl, Any :~: Any
forall {k} (a :: k). a :~: a
Refl) :: (CmpInteger a b :~: 'EQ, a :~: b) of
(CmpInteger_ (Normalize a) (Normalize b) :~: 'EQ
Refl, a :~: b
Refl) -> OrderingI a a
OrderingI a b
forall {k} (a :: k). (Compare a a ~ 'EQ) => OrderingI a a
EQI
Ordering
LT -> case (Any :~: Any) -> CmpInteger_ (Normalize a) (Normalize b) :~: 'LT
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: (CmpInteger a b :~: 'LT) of
CmpInteger_ (Normalize a) (Normalize b) :~: 'LT
Refl -> OrderingI a b
forall {k} (a :: k) (b :: k). (Compare a b ~ 'LT) => OrderingI a b
LTI
Ordering
GT -> case (Any :~: Any) -> CmpInteger_ (Normalize a) (Normalize b) :~: 'GT
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: (CmpInteger a b :~: 'GT) of
CmpInteger_ (Normalize a) (Normalize b) :~: 'GT
Refl -> OrderingI a b
forall {k} (a :: k) (b :: k). (Compare a b ~ 'GT) => OrderingI a b
GTI
newtype SInteger (i :: Integer) = UnsafeSInteger P.Integer
pattern SInteger :: forall i. () => KnownInteger i => SInteger i
pattern $mSInteger :: forall {r} {i :: Integer}.
SInteger i -> (KnownInteger i => r) -> ((# #) -> r) -> r
$bSInteger :: forall (i :: Integer). KnownInteger i => SInteger i
SInteger <- (knownIntegerInstance -> KnownIntegeregerInstance)
where SInteger = SInteger i
forall (i :: Integer). KnownInteger i => SInteger i
integerSing
data KnownIntegeregerInstance (i :: Integer) where
KnownIntegeregerInstance :: KnownInteger i => KnownIntegeregerInstance i
knownIntegerInstance :: SInteger i -> KnownIntegeregerInstance i
knownIntegerInstance :: forall (i :: Integer). SInteger i -> KnownIntegeregerInstance i
knownIntegerInstance SInteger i
si = SInteger i
-> (KnownInteger i => KnownIntegeregerInstance i)
-> KnownIntegeregerInstance i
forall (i :: Integer) r. SInteger i -> (KnownInteger i => r) -> r
withKnownInteger SInteger i
si KnownIntegeregerInstance i
KnownInteger i => KnownIntegeregerInstance i
forall (i :: Integer). KnownInteger i => KnownIntegeregerInstance i
KnownIntegeregerInstance
instance Show (SInteger i) where
showsPrec :: Int -> SInteger i -> ShowS
showsPrec Int
p (UnsafeSInteger Integer
i) = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
appPrec) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
String -> ShowS
showString String
"SInteger @" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
Int -> Integer -> ShowS
showsPrecInteger Int
appPrec1 (Integer -> Integer
termIntegerToTypeInteger Integer
i)
instance TestEquality SInteger where
testEquality :: forall (a :: Integer) (b :: Integer).
SInteger a -> SInteger b -> Maybe (a :~: b)
testEquality (UnsafeSInteger Integer
x) (UnsafeSInteger Integer
y)
| Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
P.== Integer
y = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just ((Any :~: Any) -> a :~: b
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl)
| Bool
otherwise = Maybe (a :~: b)
forall a. Maybe a
Nothing
instance TestCoercion SInteger where
testCoercion :: forall (a :: Integer) (b :: Integer).
SInteger a -> SInteger b -> Maybe (Coercion a b)
testCoercion SInteger a
x SInteger b
y = ((a :~: b) -> Coercion a b)
-> Maybe (a :~: b) -> Maybe (Coercion a b)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (\a :~: b
Refl -> Coercion a b
forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion) (SInteger a -> SInteger b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Integer) (b :: Integer).
SInteger a -> SInteger b -> Maybe (a :~: b)
testEquality SInteger a
x SInteger b
y)
fromSInteger :: SInteger i -> P.Integer
fromSInteger :: forall (i :: Integer). SInteger i -> Integer
fromSInteger (UnsafeSInteger Integer
i) = Integer
i
withKnownInteger
:: forall i rep (r :: TYPE rep). SInteger i -> (KnownInteger i => r) -> r
withKnownInteger :: forall (i :: Integer) r. SInteger i -> (KnownInteger i => r) -> r
withKnownInteger = forall (cls :: Constraint) meth r.
WithDict cls meth =>
meth -> (cls => r) -> r
withDict @(KnownInteger i)
withSomeSInteger
:: forall rep (r :: TYPE rep). P.Integer -> (forall n. SInteger n -> r) -> r
withSomeSInteger :: forall r. Integer -> (forall (n :: Integer). SInteger n -> r) -> r
withSomeSInteger Integer
n forall (n :: Integer). SInteger n -> r
k = SInteger Any -> r
forall (n :: Integer). SInteger n -> r
k (Integer -> SInteger Any
forall (i :: Integer). Integer -> SInteger i
UnsafeSInteger Integer
n)
{-# NOINLINE withSomeSInteger #-}
infixr 4 /=, /=?, ==, ==?
type (a :: k) ==? (b :: k) = OrdCond (Compare a b) 'False 'True 'False :: Bool
type (a :: k) == (b :: k) = (a ==? b) ~ 'True :: Constraint
type (a :: k) /=? (b :: k) = OrdCond (Compare a b) 'True 'False 'True :: Bool
type (a :: k) /= (b :: k) = (a /=? b) ~ 'True :: Constraint