module Data.Nat (
type Nat(..),
SNat,
IsNat(..),
natToInt,
type ToKnownNat,
type FromKnownNat,
fromKnownNat,
zero,
succ,
type (+),
plus,
type Pred,
pred,
type (),
monus,
type (*),
times,
type (^),
power,
type Min,
minimum,
type Max,
maximum,
type Cmp,
IsZero(..),
isZero,
LTE(..),
lte,
Compare(..),
cmp )where
import Prelude hiding (minimum,maximum,succ,pred)
import qualified GHC.TypeLits as GHC
import Data.Kind hiding (type (*))
import Unsafe.Coerce (unsafeCoerce)
import Data.Nat.Internal
type family FromKnownNat (a :: GHC.Nat) :: Nat where
FromKnownNat 0 = 'Z
FromKnownNat n = 'S (FromKnownNat (n GHC.- 1))
fromKnownNat :: forall proxy n. IsNat (FromKnownNat n) => proxy n -> SNat (FromKnownNat n)
fromKnownNat _ = witness
zero :: SNat 'Z
zero = SNat 0
succ :: SNat n -> SNat ('S n)
succ (SNat x) = SNat (1 + x)
type family (a :: Nat) + (b :: Nat) :: Nat where
'Z + n = n
('S n) + m = 'S (n + m)
plus :: SNat a -> SNat b -> SNat (a + b)
plus (SNat x) (SNat y) = SNat (x + y)
type family Pred (a :: Nat) :: Nat where
Pred 'Z = 'Z
Pred ('S n) = n
pred :: SNat n -> SNat (Pred n)
pred (SNat 0) = SNat 0
pred (SNat n) = SNat (n 1)
type family (a :: Nat) (b :: Nat) :: Nat where
n 'Z = n
'Z m = m
'S n 'S m = n m
monus :: SNat a -> SNat b -> SNat (a b)
monus (SNat x) (SNat y)
| x >= y = SNat (x y)
| otherwise = SNat 0
type family (a :: Nat) * (b :: Nat) :: Nat where
'Z * n = 'Z
('S n) * m = m + (n * m)
times :: SNat a -> SNat b -> SNat (a * b)
times (SNat x) (SNat y) = SNat (x * y)
type family (a :: Nat) ^ (b :: Nat) :: Nat where
base ^ 'Z = 'S 'Z
base ^ 'S n = base * (base ^ n)
power :: SNat a -> SNat b -> SNat (a ^ b)
power (SNat x) (SNat y) = SNat (x ^ y)
type family Min (a :: Nat) (b :: Nat) :: Nat where
Min 'Z m = 'Z
Min ('S 'Z) 'Z = 'Z
Min ('S n) ('S m) = 'S (Min n m)
minimum :: SNat a -> SNat b -> SNat (Min a b)
minimum (SNat a) (SNat b) = SNat (min a b)
type family Max (a :: Nat) (b :: Nat) :: Nat where
Max 'Z m = m
Max ('S 'Z) 'Z = 'S 'Z
Max ('S n) ('S m) = 'S (Max n m)
maximum :: SNat a -> SNat b -> SNat (Max a b)
maximum (SNat a) (SNat b) = SNat (max a b)
type family Cmp (a :: Nat) (b :: Nat) :: Ordering where
Cmp 'Z 'Z = 'EQ
Cmp ('S n) 'Z = 'GT
Cmp 'Z ('S m) = 'LT
Cmp ('S n) ('S m) = Cmp n m
data IsZero :: Nat -> Type where
SIsZ :: IsZero 'Z
isZero :: SNat n -> Maybe (IsZero n)
isZero (SNat x)
| x == 0 = Just (unsafeCoerce SIsZ)
| otherwise = Nothing
data LTE :: Nat -> Nat -> Type where
SLTE :: SNat y -> LTE (y + x) x
deriving instance Show (LTE n m)
lte :: SNat n -> SNat m -> Maybe (LTE n m)
lte (SNat x) (SNat y)
| x <= y = Just (unsafeCoerce (SLTE (SNat (y x))))
| otherwise = Nothing
data Compare :: Nat -> Nat -> Type where
SLT :: SNat y -> Compare x ('S y + x)
SEQ :: Compare x x
SGT :: SNat y -> Compare ('S y + x) x
deriving instance Show (Compare n m)
cmp :: SNat a -> SNat b -> Compare a b
cmp (SNat x) (SNat y) = case compare x y of
LT -> unsafeCoerce (SLT (SNat (y x 1)))
EQ -> unsafeCoerce SEQ
GT -> unsafeCoerce (SGT (SNat (x y 1)))