peano.hs

module Peano where

import Test.QuickCheck
import Data.Monoid

-- p = 1 + p
data Peano = Zero | Succ Peano deriving Show

--------------------
---- Operations ----
--------------------

-- Addition
addP :: Peano -> Peano -> Peano
addP Zero b = b
addP (Succ a) b = Succ (addP a b)

-- Subtraction (safe)
subP :: Peano -> Peano -> Maybe Peano
subP Zero Zero = Just Zero
subP Zero _ = Nothing
subP a Zero = Just a
subP (Succ a) (Succ b) = subP a b

-- Subtraction (unsafe)
unsafeSubP :: Peano -> Peano -> Peano
unsafeSubP Zero Zero = Zero
unsafeSubP Zero _ = undefined
unsafeSubP a Zero = a
unsafeSubP (Succ a) (Succ b) = unsafeSubP a b

-- Successor
succP :: Peano -> Peano
succP a = (Succ a)

-- Predecessor (safe)
predP :: Peano -> Maybe Peano
predP Zero = Nothing
predP (Succ a) = Just a

-- Predecessor (unsafe)
unsafePredP :: Peano -> Peano
unsafePredP Zero = undefined
unsafePredP (Succ a) = a

-- Multiplication
multP :: Peano -> Peano -> Peano
multP a b = go a b
    where go (Succ Zero) y = y
          go (Succ x) y = go x (addP b y)
          go Zero y = Zero

-- Integral Division
divP :: Peano -> Peano -> Peano
divP n d = go n d Zero
    where go n d a
            | n == Zero = a
            | n < d = a
            | otherwise = go (n - d) d (Succ a)

-- Quotient
quotP :: Peano -> Peano -> Peano
quotP = divP

-- Remainder
remP :: Peano -> Peano -> Peano
remP n d = go n d Zero
    where go n' d a
            | n' == Zero = Zero
            | n' < d = n - (d * a)
            | otherwise = go (n' - d) d (Succ a)

-- Exponentiation
expP :: Peano -> Peano -> Peano
expP _ Zero = Succ Zero
expP a (Succ b) = go a b
    where go x Zero = x
          go x (Succ y) = go (multP a x) y
    
-- Equality
eqP :: Peano -> Peano -> Bool
eqP a b = case subP a b of
    Just Zero -> True
    Just _ -> False
    Nothing -> False

-- Greater Than
gtP :: Peano -> Peano -> Bool
gtP a b = case subP a b of
    Just Zero -> False
    Just _ -> True
    Nothing -> False

-- Less Than
ltP :: Peano -> Peano -> Bool
ltP a b = case subP a b of
    Just Zero -> False
    Just _ -> False
    Nothing -> True

-- Greater Than or Equal
gteP :: Peano -> Peano -> Bool
gteP a b = case subP a b of
    Just _ -> True
    Nothing -> False

-- Less Than or Equal
lteP :: Peano -> Peano -> Bool
lteP a b = case subP a b of
    Just Zero -> True
    Just _ -> False
    Nothing -> False

-- To Integer
toIntP :: Peano -> Integer
toIntP Zero = 0
toIntP (Succ a) = 1 + toIntP a

-- From Integer
fromIntP :: Integer -> Peano
fromIntP 0 = Zero
fromIntP a = (Succ $ fromIntP $ a - 1)

-----------------------------
---- Typeclass Instances ----
-----------------------------

instance Eq Peano where
    (==) a b = eqP a b
    (/=) a b = not $ eqP a b

instance Ord Peano where
    (>) a b = gtP a b
    (<) a b = ltP a b
    (>=) a b = gteP a b
    (<=) a b = lteP a b
    
instance Num Peano where
    (+) a b = addP a b
    (-) a b = unsafeSubP a b
    (*) a b = multP a b
    fromInteger = fromIntP 
    abs a = a
    signum Zero = Zero
    signum a = a

--instance Enum Peano where
--    succ a = Succ a

--instance Integral Peano where
--    div a b = divP a b

--instance Show Peano where
--    show a = show $ toIntP a

instance Monoid Peano where 
    mempty = Zero
    mappend a b = addP a b
    
instance Arbitrary Peano where
    arbitrary = do
        a <- arbitrary :: Gen Integer
        return (fromIntP $ abs a)

---------------
---- Tests ----
---------------

genPeano :: Gen Peano
genPeano = arbitrary

---- Addition

-- Zero is the identity value
prop_AddId :: Property
prop_AddId =
    forAll genPeano
    (\x -> x + Zero === x)

-- x + y is always greater then x
prop_Add :: Property
prop_Add = 
    forAll genPeano
    (\x y -> x + y >= x)

-- Is Associative
prop_AddAssoc :: Property
prop_AddAssoc =
    forAll genPeano
    (\x y z -> (x + y) + z === x + (y + z))

-- Is Commutative
prop_AddCommu :: Property
prop_AddCommu =
    forAll genPeano
    (\x y -> x + y === y + x)

---- Subtraction

---- Multiplication

-- (Succ Zero) is the identity value
prop_MultId :: Property
prop_MultId =
    forAll genPeano
    (\x -> x * (Succ Zero) == x)

-- Is Associative
prop_MultAssoc :: Property
prop_MultAssoc =
    forAll genPeano
    (\x y z -> (x * y) * z === x * (y * z))

-- Is Commutative
prop_MultCommu :: Property
prop_MultCommu =
    forAll genPeano
    (\x y -> x * y === y * x)

-- Is Distributive
prop_MultDist :: Property
prop_MultDist =
    forAll genPeano
    (\x y z -> (x * y) +(x * z) === x * (y + z))

-- Division

-- Exponentiation

---- Order

-- Successor is greater than
props_orderSuccGt :: Property
props_orderSuccGt =
    forAll genPeano
    (\x -> succP x > x)

-- Successor/Predecessor

-- succP x is always 1 greater than x
prop_Succ :: Property
prop_Succ = 
    forAll genPeano
    (\n -> succP n === n + (Succ Zero))

---- Test Runner
runTests = do
    quickCheck prop_Add
    quickCheck prop_AddId
    quickCheck prop_AddAssoc
    quickCheck prop_AddCommu
    quickCheck prop_MultId
    quickCheck prop_MultAssoc
    quickCheck prop_MultCommu
    quickCheck prop_MultDist
    quickCheck props_orderSuccGt