module Data.Number.Nat
(
Nat(..),
cmpNatLT, invOrd, minusNat, fromNat, toNat
) where
import Prelude hiding ( Int )
import Data.Ratio ( (%) )
data Nat
= IHi
| O Nat
| I Nat
deriving (Show,Eq)
instance Read Nat where
readsPrec n = map (\(x,str) -> (toEnum x,str)) . readsPrec n
instance Ord Nat where
compare IHi IHi = EQ
compare IHi (O _) = LT
compare IHi (I _) = LT
compare (O _) IHi = GT
compare (I _) IHi = GT
compare (O x) (O y) = compare x y
compare (I x) (I y) = compare x y
compare (O x) (I y) = cmpNatLT x y
compare (I x) (O y) = invOrd (cmpNatLT y x)
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 IHi _ = LT
cmpNatLT (O _) IHi = GT
cmpNatLT (I _) IHi = GT
cmpNatLT (O x) (O y) = cmpNatLT x y
cmpNatLT (I x) (I y) = cmpNatLT x y
cmpNatLT (O x) (I y) = cmpNatLT x y
cmpNatLT (I x) (O y) = invOrd (cmpNatLT y x)
invOrd :: Ordering -> Ordering
invOrd EQ = EQ
invOrd LT = GT
invOrd GT = LT
instance Enum Nat where
succ (O bs) = I bs
succ (I bs) = O (succ bs)
succ IHi = O IHi
pred IHi = error "predecessor of 1"
pred (O IHi) = IHi
pred (O x@(O _)) = I (pred x)
pred (O (I x)) = I (O x)
pred (I x) = O x
fromEnum = fromNat
toEnum = toNat
instance Num Nat where
O x + O y = O (x + y)
O x + I y = I (x + y)
O x + IHi = I x
I x + O y = I (x + y)
I x + I y = O (succ x + y)
I x + IHi = O (succ x)
IHi + y = succ y
x y =
case minusNat x y of
IHi -> error "result zero in (-)"
n -> pred n
IHi * y = y
I x * y = O (x * y) + y
O x * y = O (x * y)
negate = error "no non-positive numbers in Nat"
abs = id
signum = const IHi
fromInteger = toNat
minusNat :: Nat -> Nat -> Nat
minusNat x IHi = x
minusNat IHi (O _) = error "negative result in (-)"
minusNat IHi (I _) = error "negative result in (-)"
minusNat (O x) (O y) = pred (O $! minusNat x y)
minusNat (O x) (I y) = O $! pred (minusNat x y)
minusNat (I x) (O y) = O $! minusNat x y
minusNat (I x) (I y) = pred (O $! minusNat x y)
instance Real Nat where
toRational n = fromNat n % 1
fromNat :: Num n => Nat -> n
fromNat IHi = 1
fromNat (O n) = 2 * fromNat n
fromNat (I n) = 2 * fromNat n + 1
toNat :: (Integral n,Num n) => n -> Nat
toNat n
| n<1 = error "toEnum of negative number"
| n==1 = IHi
| even n = O (toNat (n `div` 2))
| otherwise = I (toNat (n `div` 2))