-- Peano natural numbers
data Peano = Zero | Succ Peano

-- convert Int to Peano
i2p :: Int -> Peano
i2p 0 = Zero
i2p x = Succ (i2p (x - 1))

-- convert Peano to Int
p2i :: Peano -> Int
p2i Zero = 0
p2i (Succ x) = 1 + (p2i x)

-- True if x > y
pgt :: Peano -> Peano -> Bool
pgt Zero _ = False
pgt _ Zero = True
pgt (Succ x) (Succ y) = pgt x y

-- x + y
padd :: Peano -> Peano -> Peano
padd x Zero = x
padd x (Succ y) = Succ (padd x y)

iadd :: Int -> Int -> Int
iadd x y = p2i (padd (i2p x) (i2p y))

-- x - y
psub :: Peano -> Peano -> Peano
psub x Zero = x
psub (Succ x) (Succ y) = psub x y

isub :: Int -> Int -> Int
isub x y = p2i (psub (i2p x) (i2p y))

-- x * y
pmul :: Peano -> Peano -> Peano
pmul Zero _ = Zero
pmul _ Zero = Zero
pmul x (Succ y) = padd x (pmul x y)

imul :: Int -> Int -> Int
imul x y = p2i (pmul (i2p x) (i2p y))

-- quotient and remainder of x / y
pdiv :: Peano -> Peano -> (Peano, Peano)
pdiv x y
    | y `pgt` x = (Zero, x)
    | otherwise = (Succ q, r) where (q, r) = pdiv (psub x y) y

idiv :: Int -> Int -> (Int, Int)
idiv x y = (p2i q, p2i r) where (q, r) = pdiv (i2p x) (i2p y)

-- quotient of x / y
pdivq :: Peano -> Peano -> Peano
pdivq x y
	| y `pgt` x = Zero
	| otherwise = Succ (pdivq (psub x y) y)

idivq :: Int -> Int -> Int
idivq x y = p2i (pdivq (i2p x) (i2p y))

-- remainder of x / y
pdivr :: Peano -> Peano -> Peano
pdivr x y = psub x (pmul (pdivq x y) y)

idivr :: Int -> Int -> Int
idivr x y = p2i (pdivr (i2p x) (i2p y))

-- tests
two   = iadd 1 1
three = isub 5 2
four  = imul 2 2
(five, _) = idiv 10 2
ten = idivr 10 0
inf = idivq 10 0

tests = do
	putStrLn (show two)
	putStrLn (show three)
	putStrLn (show four)
	putStrLn (show five)
	putStrLn (show ten)
--	putStrLn (show inf) -- don't try this :)

-- now run ghci
-- type ":load divide" to load this module
-- type "tests"
-- note that ten exists and can be printed
-- but if you type "let (q, r) = idiv 10 0", then you cannot print r.