-- | The implementations of all functions are -- supposed to be as non-strict as possible. This is non-trivial as for -- example a naive implementation of (*) yields O _|_ for the application -- I _|_ * O IHi while a least-strict version yields O (I _|_). Also the -- naive / standard implementations of (\-), compare, (\<), (\<=), (\>), -- (\>=) are more strict than necessary. module Data.Number.Nat ( -- * Datatype Nat(..), -- * Helper Functions cmpNatLT, invOrd, minusNat, fromNat, toNat ) where import Prelude hiding ( Int ) import Data.Ratio ( (%) ) -- | A binary representation of natural numbers which starts with the least -- significant bit. data Nat -- | This constructor represents the most significant bit. There are no -- leading zero bits. = IHi -- | A zero bit | O Nat -- | A one bit | I Nat deriving (Show,Eq) -- instance Show Nat where -- show = show . fromEnum 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) -- these instances are lazier than the standard implementation -- for example IHi <= _|_ = True -- while the standard implementation yields _|_ x < y = cmpNatLT y x == GT x > y = cmpNatLT x y == GT x <= y = cmpNatLT x y == LT x >= y = cmpNatLT y x == LT -- | This function is used to implement lazy instances of compare and (\<), -- (\<=), (\>), (\>=). It is used to transfer information to more significant -- bits. Instead of yielding EQ it yields LT if the numbers are equal. 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) -- | Maps LT to GT and GT to LT. It is used instead of defining a function -- cmpNatGT. 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 (y * x) + 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 x y yields x - y + 1. This is used to implement (-) for natural -- numbers. 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 Integral Nat where -- toInteger = fromNat instance Real Nat where toRational n = fromNat n % 1 -- | This is used for the implementation of toInteger and fromEnum. fromNat :: Num n => Nat -> n fromNat IHi = 1 fromNat (O n) = 2 * fromNat n fromNat (I n) = 2 * fromNat n + 1 -- | This is used for the implementation of fromInteger and toEnum. 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))