{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Kinds.Integer
(
Integer(..), ToInteger
, KnownInteger(..)
, AddInteger, SubInteger, CmpInteger, MulInteger
, type (-#)
, plusMinusInverseL, plusMinusInverseR
, mulCommutes
, CaseOrdering
) where
import Prelude hiding (Integer)
import qualified Prelude as P
import Data.Type.Equality ((:~:)(..))
import GHC.Exts (proxy#)
import GHC.TypeNats (KnownNat, Nat, natVal')
import Unsafe.Coerce (unsafeCoerce)
import Kinds.Num (type (+), type (-), type (*), Cmp, FromNat, ToInteger)
data Integer = Pos Nat | Neg Nat
class KnownInteger (n :: Integer) where
integerVal :: P.Integer
instance KnownNat n => KnownInteger ('Pos n) where
integerVal :: Integer
integerVal = Natural -> Integer
forall a. Integral a => a -> Integer
toInteger (Natural -> Integer) -> Natural -> Integer
forall a b. (a -> b) -> a -> b
$ Proxy# n -> Natural
forall (n :: Nat). KnownNat n => Proxy# n -> Natural
natVal' @n Proxy# n
forall k (a :: k). Proxy# a
proxy#
instance KnownNat n => KnownInteger ('Neg n) where
integerVal :: Integer
integerVal =
let x :: Natural
x = Proxy# n -> Natural
forall (n :: Nat). KnownNat n => Proxy# n -> Natural
natVal' @n Proxy# n
forall k (a :: k). Proxy# a
proxy#
in if Natural
x Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
0
then [Char] -> Integer
forall a. HasCallStack => [Char] -> a
error [Char]
"illegal KnownInteger (-0)"
else Integer -> Integer
forall a. Num a => a -> a
negate (Integer -> Integer) -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
x
type instance Cmp x y = CmpInteger x y
type instance FromNat n = 'Pos n
type instance ToInteger n = n
type instance x + y = AddInteger x y
type instance x - y = SubInteger x y
type instance x * y = MulInteger x y
type family CmpInteger m n where
CmpInteger ('Pos m) ('Pos n) = Cmp m n
CmpInteger ('Pos 0) ('Neg 0) = 'EQ
CmpInteger ('Pos m) ('Neg n) = 'GT
CmpInteger ('Neg 0) ('Pos 0) = 'EQ
CmpInteger ('Neg m) ('Pos n) = 'LT
CmpInteger ('Neg m) ('Neg n) = Cmp n m
type family CaseOrdering (o :: Ordering) (lt :: k) (eq :: k) (gt :: k) :: k where
CaseOrdering 'LT lt eq gt = lt
CaseOrdering 'EQ lt eq gt = eq
CaseOrdering 'GT lt eq gt = gt
type family (m :: Nat) -# (n :: Nat) where
n -# 0 = 'Pos n
0 -# n = 'Neg n
m -# n = CaseOrdering (Cmp m n)
('Neg (n - m))
('Pos 0)
('Pos (m - n))
type family AddInteger m n where
AddInteger ('Pos m) ('Pos n) = 'Pos (m + n)
AddInteger ('Pos m) ('Neg n) = m -# n
AddInteger ('Neg m) ('Pos n) = n -# m
AddInteger ('Neg m) ('Neg n) = 'Neg (m + n)
type family SubInteger m n where
SubInteger ('Pos m) ('Pos n) = m -# n
SubInteger ('Pos m) ('Neg n) = 'Pos (m + n)
SubInteger ('Neg m) ('Pos n) = 'Neg (m + n)
SubInteger ('Neg m) ('Neg n) = n -# m
type family MulInteger m n where
MulInteger ('Pos m) ('Pos n) = 'Pos (m * n)
MulInteger ('Pos m) ('Neg n) = 0 -# (m * n)
MulInteger ('Neg m) ('Pos n) = 0 -# (m * n)
MulInteger ('Neg m) ('Neg n) = 'Pos (m * n)
unsafeAxiom :: a :~: b
unsafeAxiom :: a :~: b
unsafeAxiom = (Any :~: Any) -> a :~: b
forall a b. a -> b
unsafeCoerce Any :~: Any
forall k (a :: k). a :~: a
Refl
plusMinusInverseR :: (m + n) -# n :~: 'Pos m
plusMinusInverseR :: ((m + n) -# n) :~: 'Pos m
plusMinusInverseR = ((m + n) -# n) :~: 'Pos m
forall k (a :: k) (b :: k). a :~: b
unsafeAxiom
plusMinusInverseL :: (m + n) -# m :~: 'Pos n
plusMinusInverseL :: ((m + n) -# m) :~: 'Pos n
plusMinusInverseL = ((m + n) -# m) :~: 'Pos n
forall k (a :: k) (b :: k). a :~: b
unsafeAxiom
mulCommutes :: MulInteger m n :~: MulInteger n m
mulCommutes :: MulInteger m n :~: MulInteger n m
mulCommutes = MulInteger m n :~: MulInteger n m
forall k (a :: k) (b :: k). a :~: b
unsafeAxiom