{-# LANGUAGE UndecidableInstances #-}
module KindInteger
(
Integer
, type P
, type N
, Normalize
, toPrelude
, fromPrelude
, showsPrecTypeLit
, KnownInteger(integerSing), integerVal
, SomeInteger(..)
, someIntegerVal
, sameInteger
, SInteger
, pattern SInteger
, fromSInteger
, fromSInteger'
, withSomeSInteger
, withKnownInteger
, type (+), type (*), type (^), type (-)
, Odd, Even, Abs, Sign, Negate, GCD, LCM, Log2
, Div
, Rem
, DivRem
, Round(..)
, div
, rem
, divRem
, CmpInteger
, cmpInteger
, eqIntegerRep
, type (==?), type (==), type (/=?), type (/=)
)
where
import Control.Exception qualified as Ex
import Data.Bits
import Data.Proxy
import Data.Singletons
import Data.Singletons.Decide
import Data.Type.Bool (If)
import Data.Type.Coercion
import Data.Type.Equality (TestEquality(..))
import Data.Type.Ord
import GHC.Base (WithDict(..))
import GHC.Exts (TYPE, Constraint)
import GHC.Real qualified as P
import GHC.Show (appPrec, appPrec1)
import GHC.TypeLits qualified as L
import Numeric.Natural (Natural)
import Prelude hiding (Integer, (==), (/=), div, rem)
import Prelude qualified as P
import Unsafe.Coerce(unsafeCoerce)
data Integer
= P_ Natural
| N_ Natural
instance Eq Integer where
Integer
a == :: Integer -> Integer -> Bool
== Integer
b = Integer -> Integer
toPrelude Integer
a Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
P.== Integer -> Integer
toPrelude Integer
b
instance Ord Integer where
compare :: Integer -> Integer -> Ordering
compare Integer
a Integer
b = Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Integer -> Integer
toPrelude Integer
a) (Integer -> Integer
toPrelude Integer
b)
Integer
a <= :: Integer -> Integer -> Bool
<= Integer
b = Integer -> Integer
toPrelude Integer
a Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer -> Integer
toPrelude Integer
b
instance Show Integer where
showsPrec :: Int -> Integer -> ShowS
showsPrec Int
p = Int -> Integer -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p (Integer -> ShowS) -> (Integer -> Integer) -> Integer -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer
toPrelude
instance Read Integer where
readsPrec :: Int -> ReadS Integer
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 -> Integer
fromPrelude Integer
a, String
ys)]
showsPrecTypeLit :: Int -> Integer -> ShowS
showsPrecTypeLit :: Int -> Integer -> ShowS
showsPrecTypeLit 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
P_ 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
N_ 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
type P (x :: Natural) = 'P_ x :: Integer
type N (x :: Natural) = 'N_ x :: Integer
toPrelude :: Integer -> P.Integer
toPrelude :: Integer -> Integer
toPrelude (P_ Natural
n) = Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
n
toPrelude (N_ Natural
n) = Integer -> Integer
forall a. Num a => a -> a
negate (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
n)
fromPrelude :: P.Integer -> Integer
fromPrelude :: Integer -> Integer
fromPrelude Integer
i = if Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 then Natural -> Integer
P_ (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger Integer
i)
else Natural -> Integer
N_ (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger (Integer -> Integer
forall a. Num a => a -> a
negate Integer
i))
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 (Natural -> Integer
P_ (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger (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 (Natural -> Integer
N_ (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger (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 -> Integer
toPrelude 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`, `Rem`
infixr 8 ^
type Odd (x :: Integer) = L.Mod (Abs x) 2 ==? 1 :: Bool
type Even (x :: Integer) = L.Mod (Abs x) 2 ==? 0 :: Bool
type family Negate (x :: Integer) :: Integer where
Negate (P 0) = P 0
Negate (P x) = N x
Negate (N x) = P x
type family Sign (x :: Integer) :: Integer where
Sign (P 0) = P 0
Sign (N 0) = P 0
Sign (P _) = P 1
Sign (N _) = N 1
type family Abs (x :: Integer) :: Natural where
Abs (P x) = x
Abs (N x) = 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 DivRem (r :: Round) (a :: Integer) (b :: Integer) =
'( Div r a b, Rem r a b ) :: (Integer, Integer)
type Rem (r :: Round) (a :: Integer) (b :: Integer) =
a - b * Div r a b :: Integer
type Div (r :: Round) (a :: Integer) (b :: Integer) =
Div_ r (Normalize a) (Normalize b) :: Integer
type family Div_ (r :: Round) (a :: Integer) (b :: Integer) :: Integer where
Div_ r (P a) (P b) = Div__ r (P a) b
Div_ r (N a) (N b) = Div__ r (P a) b
Div_ r (P a) (N b) = Div__ r (N a) b
Div_ r (N a) (P b) = Div__ r (N a) b
type family Div__ (r :: Round) (a :: Integer) (b :: Natural) :: Integer where
Div__ _ _ 0 = L.TypeError ('L.Text "KindInteger.Div: Division by zero")
Div__ _ (P 0) _ = P 0
Div__ _ (N 0) _ = P 0
Div__ 'RoundDown (P a) b = P (L.Div a b)
Div__ 'RoundDown (N a) b = NN (If (b L.* L.Div a b ==? a)
(L.Div a b)
(L.Div a b L.+ 1))
Div__ 'RoundUp a b = Negate (Div__ 'RoundDown (Negate a) b)
Div__ 'RoundZero (P a) b = Div__ 'RoundDown (P a) b
Div__ 'RoundZero (N a) b = Negate (Div__ 'RoundDown (P a) b)
Div__ 'RoundAway (P a) b = Div__ 'RoundUp (P a) b
Div__ 'RoundAway (N a) b = Div__ 'RoundDown (N a) b
Div__ 'RoundHalfDown a b = If (HalfLT (R a b) (Div__ 'RoundUp a b))
(Div__ 'RoundUp a b)
(Div__ 'RoundDown a b)
Div__ 'RoundHalfUp a b = If (HalfLT (R a b) (Div__ 'RoundDown a b))
(Div__ 'RoundDown a b)
(Div__ 'RoundUp a b)
Div__ 'RoundHalfEven a b = If (HalfLT (R a b) (Div__ 'RoundDown a b))
(Div__ 'RoundDown a b)
(If (HalfLT (R a b) (Div__ 'RoundUp a b))
(Div__ 'RoundUp a b)
(If (Even (Div__ 'RoundDown a b))
(Div__ 'RoundDown a b)
(Div__ 'RoundUp a b)))
Div__ 'RoundHalfOdd a b = If (HalfLT (R a b) (Div__ 'RoundDown a b))
(Div__ 'RoundDown a b)
(If (HalfLT (R a b) (Div__ 'RoundUp a b))
(Div__ 'RoundUp a b)
(If (Odd (Div__ 'RoundDown a b))
(Div__ 'RoundDown a b)
(Div__ 'RoundUp a b)))
Div__ 'RoundHalfZero a b = If (HalfLT (R a b) (Div__ 'RoundDown a b))
(Div__ 'RoundDown a b)
(If (HalfLT (R a b) (Div__ 'RoundUp a b))
(Div__ 'RoundUp a b)
(Div__ 'RoundZero a b))
Div__ 'RoundHalfAway (P a) b = Div__ 'RoundHalfUp (P a) b
Div__ 'RoundHalfAway (N a) b = Div__ 'RoundHalfDown (N a) b
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 GCD (a :: Integer) (b :: Integer) = NatGCD (Abs a) (Abs b) :: Natural
type family NatGCD (a :: Natural) (b :: Natural) :: Natural where
NatGCD a 0 = a
NatGCD a b = NatGCD b (L.Mod a b)
type LCM (a :: Integer) (b :: Integer) = NatLCM (Abs a) (Abs b) :: Natural
type NatLCM (a :: Natural) (b :: Natural) =
L.Div a (NatGCD a b) L.* b :: Natural
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) -> CmpInteger_ (Normalize a) (Normalize b) :~: 'EQ
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: CmpInteger a b :~: 'EQ of
CmpInteger_ (Normalize a) (Normalize b) :~: 'EQ
Refl -> case (Any :~: Any) -> a :~: b
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: a :~: b of
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 Integer
type role SInteger representational
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
showsPrecTypeLit Int
appPrec1 Integer
i
instance TestEquality SInteger where
testEquality :: forall (a :: Integer) (b :: Integer).
SInteger a -> SInteger b -> Maybe (a :~: b)
testEquality = Sing a -> Sing b -> Maybe (a :~: b)
SInteger a -> SInteger b -> Maybe (a :~: b)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
decideEquality
{-# INLINE testEquality #-}
instance TestCoercion SInteger where
testCoercion :: forall (a :: Integer) (b :: Integer).
SInteger a -> SInteger b -> Maybe (Coercion a b)
testCoercion = Sing a -> Sing b -> Maybe (Coercion a b)
SInteger a -> SInteger b -> Maybe (Coercion a b)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (Coercion a b)
decideCoercion
{-# INLINE testCoercion #-}
fromSInteger :: SInteger i -> P.Integer
fromSInteger :: forall (i :: Integer). SInteger i -> Integer
fromSInteger (UnsafeSInteger Integer
i) = Integer -> Integer
toPrelude Integer
i
{-# INLINE fromSInteger #-}
fromSInteger' :: SInteger i -> Integer
fromSInteger' :: forall (i :: Integer). SInteger i -> Integer
fromSInteger' (UnsafeSInteger Integer
i) = Integer
i
{-# INLINE fromSInteger' #-}
eqIntegerRep :: Integer -> Integer -> Bool
eqIntegerRep :: Integer -> Integer -> Bool
eqIntegerRep (N_ Natural
l) (N_ Natural
r) = Natural
l Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
P.== Natural
r
eqIntegerRep (P_ Natural
l) (P_ Natural
r) = Natural
l Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
P.== Natural
r
eqIntegerRep Integer
_ Integer
_ = Bool
False
{-# INLINE eqIntegerRep #-}
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 -> Integer
fromPrelude Integer
n))
{-# NOINLINE withSomeSInteger #-}
type instance Sing = SInteger
instance SDecide Integer where
UnsafeSInteger Integer
l %~ :: forall (a :: Integer) (b :: Integer).
Sing a -> Sing b -> Decision (a :~: b)
%~ UnsafeSInteger Integer
r =
case Integer -> Integer -> Bool
eqIntegerRep Integer
l Integer
r of
Bool
True -> (a :~: b) -> Decision (a :~: b)
forall a. a -> Decision a
Proved ((Any :~: Any) -> a :~: b
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl)
Bool
False -> Refuted (a :~: b) -> Decision (a :~: b)
forall a. Refuted a -> Decision a
Disproved (\a :~: b
Refl -> String -> Void
forall a. HasCallStack => String -> a
error String
"SDecide.Integer")
data Round
= RoundUp
| RoundDown
| RoundZero
| RoundAway
| RoundHalfUp
| RoundHalfDown
| RoundHalfZero
| RoundHalfAway
| RoundHalfEven
| RoundHalfOdd
deriving (Round -> Round -> Bool
(Round -> Round -> Bool) -> (Round -> Round -> Bool) -> Eq Round
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Round -> Round -> Bool
== :: Round -> Round -> Bool
$c/= :: Round -> Round -> Bool
/= :: Round -> Round -> Bool
Eq, Eq Round
Eq Round
-> (Round -> Round -> Ordering)
-> (Round -> Round -> Bool)
-> (Round -> Round -> Bool)
-> (Round -> Round -> Bool)
-> (Round -> Round -> Bool)
-> (Round -> Round -> Round)
-> (Round -> Round -> Round)
-> Ord Round
Round -> Round -> Bool
Round -> Round -> Ordering
Round -> Round -> Round
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Round -> Round -> Ordering
compare :: Round -> Round -> Ordering
$c< :: Round -> Round -> Bool
< :: Round -> Round -> Bool
$c<= :: Round -> Round -> Bool
<= :: Round -> Round -> Bool
$c> :: Round -> Round -> Bool
> :: Round -> Round -> Bool
$c>= :: Round -> Round -> Bool
>= :: Round -> Round -> Bool
$cmax :: Round -> Round -> Round
max :: Round -> Round -> Round
$cmin :: Round -> Round -> Round
min :: Round -> Round -> Round
Ord, Int -> Round -> ShowS
[Round] -> ShowS
Round -> String
(Int -> Round -> ShowS)
-> (Round -> String) -> ([Round] -> ShowS) -> Show Round
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Round -> ShowS
showsPrec :: Int -> Round -> ShowS
$cshow :: Round -> String
show :: Round -> String
$cshowList :: [Round] -> ShowS
showList :: [Round] -> ShowS
Show, ReadPrec [Round]
ReadPrec Round
Int -> ReadS Round
ReadS [Round]
(Int -> ReadS Round)
-> ReadS [Round]
-> ReadPrec Round
-> ReadPrec [Round]
-> Read Round
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS Round
readsPrec :: Int -> ReadS Round
$creadList :: ReadS [Round]
readList :: ReadS [Round]
$creadPrec :: ReadPrec Round
readPrec :: ReadPrec Round
$creadListPrec :: ReadPrec [Round]
readListPrec :: ReadPrec [Round]
Read, Int -> Round
Round -> Int
Round -> [Round]
Round -> Round
Round -> Round -> [Round]
Round -> Round -> Round -> [Round]
(Round -> Round)
-> (Round -> Round)
-> (Int -> Round)
-> (Round -> Int)
-> (Round -> [Round])
-> (Round -> Round -> [Round])
-> (Round -> Round -> [Round])
-> (Round -> Round -> Round -> [Round])
-> Enum Round
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: Round -> Round
succ :: Round -> Round
$cpred :: Round -> Round
pred :: Round -> Round
$ctoEnum :: Int -> Round
toEnum :: Int -> Round
$cfromEnum :: Round -> Int
fromEnum :: Round -> Int
$cenumFrom :: Round -> [Round]
enumFrom :: Round -> [Round]
$cenumFromThen :: Round -> Round -> [Round]
enumFromThen :: Round -> Round -> [Round]
$cenumFromTo :: Round -> Round -> [Round]
enumFromTo :: Round -> Round -> [Round]
$cenumFromThenTo :: Round -> Round -> Round -> [Round]
enumFromThenTo :: Round -> Round -> Round -> [Round]
Enum, Round
Round -> Round -> Bounded Round
forall a. a -> a -> Bounded a
$cminBound :: Round
minBound :: Round
$cmaxBound :: Round
maxBound :: Round
Bounded)
div :: Round
-> P.Integer
-> P.Integer
-> P.Integer
div :: Round -> Integer -> Integer -> Integer
div Round
r Integer
a Integer
b = (Integer, Integer) -> Integer
forall a b. (a, b) -> a
fst (Round -> Integer -> Integer -> (Integer, Integer)
divRem Round
r Integer
a Integer
b)
rem :: Round
-> P.Integer
-> P.Integer
-> P.Integer
rem :: Round -> Integer -> Integer -> Integer
rem Round
r Integer
a Integer
b = (Integer, Integer) -> Integer
forall a b. (a, b) -> b
snd (Round -> Integer -> Integer -> (Integer, Integer)
divRem Round
r Integer
a Integer
b)
divRem
:: Round
-> P.Integer
-> P.Integer
-> (P.Integer, P.Integer)
{-# NOINLINE divRem #-}
divRem :: Round -> Integer -> Integer -> (Integer, Integer)
divRem Round
RoundZero = \Integer
a (Integer -> Integer
errDiv0 -> Integer
b) -> Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
P.quotRem Integer
a Integer
b
divRem Round
RoundDown = \Integer
a (Integer -> Integer
errDiv0 -> Integer
b) -> Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
P.divMod Integer
a Integer
b
divRem Round
RoundUp = \Integer
a (Integer -> Integer
errDiv0 -> Integer
b) -> Integer -> Integer -> (Integer, Integer)
_divRemRoundUpNoCheck Integer
a Integer
b
divRem Round
RoundAway = \Integer
a (Integer -> Integer
errDiv0 -> Integer
b) ->
if Bool -> Bool -> Bool
forall a. Bits a => a -> a -> a
xor (Integer
a Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0) (Integer
b Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0)
then Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
P.divMod Integer
a Integer
b
else Integer -> Integer -> (Integer, Integer)
_divRemRoundUpNoCheck Integer
a Integer
b
divRem Round
RoundHalfUp = (Bool
-> (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer))
-> Integer -> Integer -> (Integer, Integer)
_divRemHalf ((Bool
-> (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer))
-> Integer -> Integer -> (Integer, Integer))
-> (Bool
-> (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer))
-> Integer
-> Integer
-> (Integer, Integer)
forall a b. (a -> b) -> a -> b
$ \Bool
_ (Integer, Integer)
_ (Integer, Integer)
up -> (Integer, Integer)
up
divRem Round
RoundHalfDown = (Bool
-> (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer))
-> Integer -> Integer -> (Integer, Integer)
_divRemHalf ((Bool
-> (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer))
-> Integer -> Integer -> (Integer, Integer))
-> (Bool
-> (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer))
-> Integer
-> Integer
-> (Integer, Integer)
forall a b. (a -> b) -> a -> b
$ \Bool
_ (Integer, Integer)
down (Integer, Integer)
_ -> (Integer, Integer)
down
divRem Round
RoundHalfZero = (Bool
-> (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer))
-> Integer -> Integer -> (Integer, Integer)
_divRemHalf ((Bool
-> (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer))
-> Integer -> Integer -> (Integer, Integer))
-> (Bool
-> (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer))
-> Integer
-> Integer
-> (Integer, Integer)
forall a b. (a -> b) -> a -> b
$ \Bool
neg (Integer, Integer)
down (Integer, Integer)
up ->
if Bool
neg then (Integer, Integer)
up else (Integer, Integer)
down
divRem Round
RoundHalfAway = (Bool
-> (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer))
-> Integer -> Integer -> (Integer, Integer)
_divRemHalf ((Bool
-> (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer))
-> Integer -> Integer -> (Integer, Integer))
-> (Bool
-> (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer))
-> Integer
-> Integer
-> (Integer, Integer)
forall a b. (a -> b) -> a -> b
$ \Bool
neg (Integer, Integer)
down (Integer, Integer)
up ->
if Bool
neg then (Integer, Integer)
down else (Integer, Integer)
up
divRem Round
RoundHalfEven = (Bool
-> (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer))
-> Integer -> Integer -> (Integer, Integer)
_divRemHalf ((Bool
-> (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer))
-> Integer -> Integer -> (Integer, Integer))
-> (Bool
-> (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer))
-> Integer
-> Integer
-> (Integer, Integer)
forall a b. (a -> b) -> a -> b
$ \Bool
_ (Integer, Integer)
down (Integer, Integer)
up ->
if Integer -> Bool
forall a. Integral a => a -> Bool
even ((Integer, Integer) -> Integer
forall a b. (a, b) -> a
fst (Integer, Integer)
down) then (Integer, Integer)
down else (Integer, Integer)
up
divRem Round
RoundHalfOdd = (Bool
-> (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer))
-> Integer -> Integer -> (Integer, Integer)
_divRemHalf ((Bool
-> (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer))
-> Integer -> Integer -> (Integer, Integer))
-> (Bool
-> (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer))
-> Integer
-> Integer
-> (Integer, Integer)
forall a b. (a -> b) -> a -> b
$ \Bool
_ (Integer, Integer)
down (Integer, Integer)
up ->
if Integer -> Bool
forall a. Integral a => a -> Bool
odd ((Integer, Integer) -> Integer
forall a b. (a, b) -> a
fst (Integer, Integer)
down) then (Integer, Integer)
down else (Integer, Integer)
up
_divRemRoundUpNoCheck :: P.Integer -> P.Integer -> (P.Integer, P.Integer)
_divRemRoundUpNoCheck :: Integer -> Integer -> (Integer, Integer)
_divRemRoundUpNoCheck Integer
a Integer
b =
let q :: Integer
q = Integer -> Integer
forall a. Num a => a -> a
negate (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
P.div (Integer -> Integer
forall a. Num a => a -> a
negate Integer
a) Integer
b)
in (Integer
q, Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
b Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
q)
{-# INLINE _divRemRoundUpNoCheck #-}
_divRemHalf
:: (Bool ->
(P.Integer, P.Integer) ->
(P.Integer, P.Integer) ->
(P.Integer, P.Integer))
-> P.Integer
-> P.Integer
-> (P.Integer, P.Integer)
_divRemHalf :: (Bool
-> (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer))
-> Integer -> Integer -> (Integer, Integer)
_divRemHalf Bool
-> (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer)
f = \Integer
a (Integer -> Integer
errDiv0 -> Integer
b) ->
let neg :: Bool
neg = Bool -> Bool -> Bool
forall a. Bits a => a -> a -> a
xor (Integer
a Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0) (Integer
b Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0)
down :: (Integer, Integer)
down = Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
P.divMod Integer
a Integer
b
up :: (Integer, Integer)
up = Integer -> Integer -> (Integer, Integer)
_divRemRoundUpNoCheck Integer
a Integer
b
in case Ratio Integer -> Ratio Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Integer
a Integer -> Integer -> Ratio Integer
forall a. Integral a => a -> a -> Ratio a
P.% Integer
b Ratio Integer -> Ratio Integer -> Ratio Integer
forall a. Num a => a -> a -> a
- Integer -> Ratio Integer
forall a. Real a => a -> Ratio Integer
toRational ((Integer, Integer) -> Integer
forall a b. (a, b) -> a
fst (Integer, Integer)
down)) (Integer
1 Integer -> Integer -> Ratio Integer
forall a. a -> a -> Ratio a
P.:% Integer
2) of
Ordering
LT -> (Integer, Integer)
down
Ordering
GT -> (Integer, Integer)
up
Ordering
EQ -> Bool
-> (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer)
f Bool
neg (Integer, Integer)
down (Integer, Integer)
up
{-# INLINE _divRemHalf #-}
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
data Rat = Rat Integer Natural
type family R (n :: Integer) (d :: Natural) :: Rat where
R (P n) d = RatNormalize ('Rat (P n) d)
R (N n) d = RatNormalize ('Rat (N n) d)
type family RatNormalize (r :: Rat) :: Rat where
RatNormalize ('Rat _ 0) =
L.TypeError ('L.Text "KindInteger: Denominator is 0")
RatNormalize ('Rat (P 0) _) = 'Rat (P 0) 1
RatNormalize ('Rat (N 0) _) = 'Rat (P 0) 1
RatNormalize ('Rat (P n) d) = 'Rat (P (L.Div n (NatGCD n d)))
(L.Div d (NatGCD n d))
RatNormalize ('Rat (N n) d) = 'Rat (N (L.Div n (NatGCD n d)))
(L.Div d (NatGCD n d))
type family RatAbs (a :: Rat) :: Rat where
RatAbs ('Rat n d) = RatNormalize ('Rat (P (Abs n)) d)
type RatAdd (a :: Rat) (b :: Rat) =
RatNormalize (RatAdd_ (RatNormalize a) (RatNormalize b)) :: Rat
type family RatAdd_ (a :: Rat) (b :: Rat) :: Rat where
RatAdd_ ('Rat an ad) ('Rat bn bd) = 'Rat (an * P bd + bn * P ad) (ad L.* bd)
type family RatNegate (a :: Rat) :: Rat where
RatNegate ('Rat n d) = RatNormalize ('Rat (Negate n) d)
type RatMinus (a :: Rat) (b :: Rat) = RatAdd a (RatNegate b)
type instance Compare (a :: Rat) (b :: Rat) = RatCmp a b
type RatCmp (a :: Rat) (b :: Rat) =
RatCmp_ (RatNormalize a) (RatNormalize b) :: Ordering
type family RatCmp_ (a :: Rat) (b :: Rat) :: Ordering where
RatCmp_ a a = 'EQ
RatCmp_ ('Rat an ad) ('Rat bn bd) = CmpInteger (an * P bd) (bn * P ad)
type HalfLT (a :: Rat) (b :: Integer) =
(RatAbs (RatMinus a ('Rat b 1))) <? ('Rat (P 1) 2) :: Bool
errDiv0 :: P.Integer -> P.Integer
errDiv0 :: Integer -> Integer
errDiv0 Integer
0 = ArithException -> Integer
forall a e. Exception e => e -> a
Ex.throw ArithException
Ex.DivideByZero
errDiv0 Integer
i = Integer
i