--------------------
-- Natural numbers (long version)
-- Fritz Ruehr * WU CS 451 * Spring 2006
--------------------

-- data type and sample values

data Nat = Zero | Succ Nat

one   =  Succ  Zero
two   =  Succ (Succ Zero)
three =  Succ (Succ (Succ Zero))


-- comparison and printing

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

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


-- conversion of numbers

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

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


-- conversion of functions

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

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


-- arithmetic operations

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)