module Nat where

data Nat = Zero | Succ Nat  deriving ({-Eq, Ord, Show-} Read)

-- instance Show Nat where show = show . ntoi

instance Show Nat where
	  show  Zero       = "Zero"
	  show (Succ Zero) = "Succ Zero"
	  show (Succ n)    = "Succ (" ++ show n ++ ")"

instance Eq Nat where
  (==)  Zero     Zero    = True
  (==) (Succ n) (Succ m) = n == m
  (==)  _        _       = False

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

nats = iterate Succ Zero

[zero, one, two, three, four, five] = take 6 nats

ntoi  Zero    = 0 :: Int
ntoi (Succ n) = 1 + ntoi n

iton (0::Int) = Zero
iton (i+1)    = Succ (iton i)

-- ifn f n = iton (f (ntoi n))
-- nfi f i = ntoi (f (iton i))

ifn f = iton . f . ntoi
nfi f = ntoi . f . iton

comp f g h x y = f (g (h x) (h y))

ibn' b = comp iton b ntoi
nbi' b = comp ntoi b iton

ibn b n m = iton (b (ntoi n) (ntoi m))
nbi b i j = ntoi (b (iton i) (iton j))

add n  Zero    = n
add n (Succ m) = Succ  (add n m)

mul n  Zero    = Zero
mul n (Succ m) = add n (mul n m)

pow n  Zero    = Succ Zero
pow n (Succ m) = mul n (pow n m)

prn z s  Zero    = z
prn z s (Succ n) = s (prn z s n)

pri z s  0    = z
pri z s (i+1) = s (pri z s i)

prl z s [] = z
prl z s (():l) = s (prl z s l)

pru z s [] = z
pru z s (_:l) = s (pru z s l)

add' n m = prn n     Succ   m
mul' n m = prn Zero (add n) m
pow' n m = prn one  (mul n) m

add'' = flip prn  Succ  
mul'' = prn Zero . add
pow'' = prn one  . mul

ntoi' = prn 0    (1+)
iton' = pri Zero Succ

sub n Zero = n
sub (Succ n) (Succ m) = sub n m
sub n m = Zero

instance Num Nat where
    (+)           = add
    (-)           = sub
    negate        = id
    (*)           = mul
    abs           = id
    signum        = prn zero (const one)
    fromInt       = iton . abs
    fromInteger   = fromInt . fromInteger

class Natty n where
    zeroN :: n
    succN :: n -> n
    addN, mulN, expN :: n -> n -> n