```-- | The implementations of all functions except for rem, quot, div, mod are
--   supposed to be as non-strict as possible.
module Data.Number.Nat
(
-- * Datatype
Nat(..),
-- * Helper Functions
cmpNatLT, fromNat, toNat,

-- * Example Implementations using Nat
length, take, drop, replicate,
-- * Example Implementations using Num
lengthNum, takeNum, dropNum, replicateNum,

divmodNat1

) where

import Prelude hiding ( length, take, drop, replicate )
import Data.Number.Nat1
import Data.Ratio ( (%) )

-- | Natural numbers and zero
data Nat
-- | Constructor representing zero
= Zero
-- | A natural number
| Pos Nat1
deriving Eq

instance Show Nat where
show Zero = "0"
show (Pos n) = show n

instance Ord Nat where
compare Zero Zero = EQ
compare Zero _    = LT
compare _    Zero = GT
compare (Pos m) (Pos n) = compare m n

-- these instances are lazier than the standard implementation
-- for example Zero <= _|_ = 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 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

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 x-Pos 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)

-- | This is used for the implementation of toInteger and fromEnum.
fromNat :: Num n => Nat -> n
fromNat Zero    = 0
fromNat (Pos n) = fromNat1 n

-- | This is used for the implementation of fromInteger and toEnum.
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

-- example functions

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 :: (Eq n,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 :: (Eq n,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 :: (Eq n,Enum n,Num n) => n -> a -> [a]
replicateNum n = takeNum n . repeat

-- examples

-- lazy :: String
-- lazy =
--   if length [1::Int ..]>0 then "long"
--                          else "short"

```