module TypeLevel.Nat where
import TypeLevel.Singletons hiding (type (+),Nat)
import Data.List (unfoldr)
import Control.DeepSeq (NFData(rnf))
import GHC.Generics (Generic)
import Data.Data (Data,Typeable)
data Nat
= Z
| S Nat
deriving (Eq,Generic,Data,Typeable)
instance Ord Nat where
compare Z Z = EQ
compare (S n) (S m) = compare n m
compare Z (S _) = LT
compare (S _) Z = GT
min Z _ = Z
min (S n) (S m) = S (min n m)
min _ Z = Z
max Z m = m
max (S n) (S m) = S (max n m)
max n Z = n
Z <= _ = True
S n <= S m = n <= m
S _ <= Z = False
Z > _ = False
S n > S m = n > m
S _ > Z = True
_ >= Z = True
Z >= S _ = False
S n >= S m = n >= m
_ < Z = False
S n < S m = n < m
Z < S _ = True
data instance The Nat n where
Zy :: The Nat Z
Sy :: The Nat n -> The Nat (S n)
infixl 6 +
type family (+) (n :: Nat) (m :: Nat) :: Nat where
Z + m = m
S n + m = S (n + m)
instance Num Nat where
Z + m = m
S n + m = S (n + m)
Z * _ = Z
S n * m = m + n * m
abs = id
signum Z = 0
signum _ = 1
fromInteger = go . abs
where
go 0 = Z
go n = S (go (n1))
S n S m = n m
n _ = n
instance Bounded Nat where
minBound = Z
maxBound = S maxBound
instance Enum Nat where
succ = S
pred (S n) = n
pred Z = error "pred called on zero nat"
fromEnum = go 0
where
go !n Z = n
go !n (S m) = go (1 + n) m
toEnum = go . abs
where
go 0 = Z
go n = S (go (n1))
enumFrom = iterate S
enumFromTo n m = unfoldr f (n, S m n)
where
f (_,Z) = Nothing
f (e,S l) = Just (e, (S e, l))
enumFromThen n m = iterate t n
where
ts Z mm = (+) mm
ts (S nn) (S mm) = ts nn mm
ts nn Z = subtract nn
t = ts n m
enumFromThenTo n m t =
unfoldr
f
(n,either (const (S n t)) (const (S t n)) tt)
where
ts Z mm = Right mm
ts (S nn) (S mm) = ts nn mm
ts nn Z = Left nn
tt = ts n m
tf = either subtract (+) tt
td = either subtract subtract tt
f (_,Z) = Nothing
f (e,l@(S _)) = Just (e, (tf e,td l))
instance Real Nat where
toRational = fromInteger . toInteger
instance Integral Nat where
toInteger = go 0
where
go !p Z = p
go !p (S n) = go (p + 1) n
quotRem _ Z = error "divide by zero"
quotRem x (S y) = qr Z x (S y)
where
qr q n m = go n m
where
go nn Z = qr (S q) nn m
go (S nn) (S mm) = go nn mm
go Z (S _) = (q, n)
div _ Z = error "divide by zero"
div n m = go n where
go = subt m where
subt Z nn = S (go nn)
subt (S mm) (S nn) = subt mm nn
subt (S _) Z = Z
instance Show Nat where
showsPrec n = showsPrec n . toInteger
instance Read Nat where
readsPrec d r =
[ (fromInteger n, xs)
| (n,xs) <- readsPrec d r ]
instance NFData Nat where
rnf Z = ()
rnf (S n) = rnf n