module NatsCheck (Nat(..), add, mult, two) where

import Test.QuickCheck

-- Peano representation of natural numbers:
-- Z: zero
-- S: successor of a natural number
data Nat = Z | S Nat
 deriving (Eq,Show)

-- Number 2 in Peano representation:
two :: Nat
two = S (S Z)

-- Number 3 in Peano representation:
three :: Nat
three = S two

-- Add two numbers:
add :: Nat -> Nat -> Nat
add Z     m = m
add (S n) m = S (add n m)

-- Multiply two numbers:
mult :: Nat -> Nat -> Nat
mult Z     m = Z
mult (S n) m = add m (mult n m)

-- Convert an integer into a Nat:
toNat :: Int -> Nat
toNat x | x == 0 = Z
        | x > 0  = S (toNat (x - 1))

-- Commutativity of add:
prop_add_comm_int :: Int -> Int -> Property
prop_add_comm_int x y = x >= 0 && y >= 0  ==>
  let m = toNat x
      n = toNat y
  in  add m n == add n m

-- The direct way with toNat:
{-
instance Arbitrary Nat where
  arbitrary = do x <- arbitrary `suchThat` (>= 0)
                 return (toNat x)
-}

-- The direct way:
instance Arbitrary Nat where
  arbitrary = do x <- arbitrary
                 --oneof [return Z, return (S x)]
                 frequency [(1, return Z), (4, return (S x))]

-- Commutativity of add:
prop_add_comm :: Nat -> Nat -> Bool
prop_add_comm x y = add x y == add y x

-- Associativy of add:
prop_add_assoc :: Nat -> Nat -> Nat -> Bool
prop_add_assoc x y z = x `add` (y `add` z) == (x `add` y) `add` z

-- Commutativity of add:
prop_mult_comm :: Nat -> Nat -> Bool
prop_mult_comm x y = mult x y == mult y x

-- Distributivity of mult and add
prop_add_distr :: Nat -> Nat -> Nat -> Bool
prop_add_distr x y z = x `mult` (y `add` z) == (x `mult` y) `add` (x `mult` z)


-- Distributivity of mult and add on integers
prop_add_distr_int :: Int -> Int -> Int -> Bool
prop_add_distr_int x y z = x * (y + z) == (x * y) + (x * z)

-- Distributivity of mult and add on floats
prop_add_distr_float :: Float -> Float -> Float -> Bool
prop_add_distr_float x y z = x * (y + z) == (x * y) + (x * z)