module Data.Number.Nat
(
Nat(..),
cmpNatLT, fromNat, toNat,
length, take, drop, replicate,
lengthNum, takeNum, dropNum, replicateNum,
divmodNat1
) where
import Prelude hiding ( length, take, drop, replicate )
import Data.Number.Nat1
import Data.Ratio ( (%) )
data Nat
= Zero
| Pos Nat1
deriving Eq
instance Show Nat where
show Zero = "0"
show (Pos n) = show n
instance Read Nat where
readsPrec n = map (\(x,str) -> (toEnum x,str)) . readsPrec n
instance Ord Nat where
compare Zero Zero = EQ
compare Zero _ = LT
compare _ Zero = GT
compare (Pos m) (Pos n) = compare m n
x < y = cmpNatLT y x == GT
x > y = cmpNatLT x y == GT
x <= y = cmpNatLT x y == LT
x >= y = cmpNatLT y x == LT
cmpNatLT :: Nat -> Nat -> Ordering
cmpNatLT Zero _ = LT
cmpNatLT _ Zero = GT
cmpNatLT (Pos m) (Pos n) = cmpNat1LT m n
instance Enum Nat where
succ = Pos . succ'
where
succ' Zero = IHi
succ' (Pos n) = succ n
pred Zero = error "predecessor of Zero"
pred (Pos IHi) = Zero
pred (Pos n) = Pos (pred n)
toEnum = toNat
fromEnum = fromNat
instance Num Nat where
Zero + n = n
n + Zero = n
Pos m + Pos n = Pos (m+n)
Zero Pos _ = error "negative result in (-)"
n Zero = n
Pos m Pos n = pred (Pos (minusNat1 m n))
Zero * _ = Zero
_ * Zero = Zero
Pos m * Pos n = Pos (m*n)
negate Zero = Zero
negate _ = error "negative result in negate"
signum Zero = Zero
signum (Pos _) = Pos IHi
abs = id
fromInteger = toNat
instance Integral Nat where
div m n = fst $ divmodNat m n
mod m n = snd $ divmodNat m n
quotRem = divmodNat
toInteger = fromNat
divmodNat :: Nat -> Nat -> (Nat,Nat)
divmodNat _ Zero = error "divide by zero"
divmodNat Zero _ = (Zero,Zero)
divmodNat (Pos x) (Pos y) = divmodNat1 x y
divmodNat1 :: Nat1 -> Nat1 -> (Nat,Nat)
divmodNat1 x IHi = (Pos x,Zero)
divmodNat1 (O x) (O y) = (q,o r)
where
(q,r) = divmodNat1 x y
divmodNat1 (I x) (O y) = (q,i r)
where
(q,r) = divmodNat1 x y
divmodNat1 x y
| x<y = (Zero,Pos x)
| otherwise = (succ q,r)
where
(q,r) = divmodNat (Pos xPos y) (Pos y)
o :: Nat -> Nat
o Zero = Zero
o (Pos n) = Pos (O n)
i :: Nat -> Nat
i Zero = Pos IHi
i (Pos n) = Pos (I n)
fromNat :: Num n => Nat -> n
fromNat Zero = 0
fromNat (Pos n) = fromNat1 n
toNat :: (Integral n,Num n) => n -> Nat
toNat n
| n<0 = error "fromInteger/toEnum of negative number"
| n==0 = Zero
| otherwise = Pos (toNat1 n)
instance Real Nat where
toRational n = toInteger n % 1
length :: [a] -> Nat
length [] = Zero
length (_:xs) = succ (length xs)
take :: Nat -> [a] -> [a]
take Zero _ = []
take _ [] = []
take n (x:xs) = x:take (pred n) xs
drop :: Nat -> [a] -> [a]
drop Zero xs = xs
drop _ [] = []
drop n (_:xs) = drop (pred n) xs
replicate :: Nat -> a -> [a]
replicate n = take n . repeat
lengthNum :: (Enum n,Num n) => [a] -> n
lengthNum [] = 0
lengthNum (_:xs) = succ (lengthNum xs)
takeNum :: (Enum n,Num n) => n -> [a] -> [a]
takeNum n l
| n==0 = []
| otherwise = takeNum' l
where
takeNum' [] = []
takeNum' (x:xs) = x:takeNum (pred n) xs
dropNum :: (Enum n,Num n) => n -> [a] -> [a]
dropNum n l
| n==0 = l
| otherwise = dropNum' l
where
dropNum' [] = []
dropNum' (_:xs) = dropNum (pred n) xs
replicateNum :: (Enum n,Num n) => n -> a -> [a]
replicateNum n = takeNum n . repeat