import QuickCheck
import Prelude hiding (even, odd)

------------------------------------------------------------------------
-- Factorial

-- Calculates the factorial of the argument.
factorial :: Integer -> Integer
factorial n | n < 0 = error "factorial: Negative input not allowed."
factorial 0 = 1
factorial n = n * factorial (n-1)

prop_factorial :: Integer -> Property
prop_factorial n = n >= 0 ==> factorial (n+1) `div` factorial n == n+1

-- n `divides` m is True iff n divides m.
divides :: Integer -> Integer -> Bool
n `divides` m | n == 0    = error "divides: Zero divisor."
              | otherwise = m `mod` n == 0

prop_factorial' :: Integer -> Property
prop_factorial' n = n >= 0 ==> factorial n `divides` factorial (n+1)

------------------------------------------------------------------------
-- Even/odd

-- Checks if argument is even.
even'' :: Integer -> Bool
even'' 0 = True
even'' n | n > 0 = not (even'' (n-1))
even'' n | n < 0 = not (even'' (n+1))

-- Checks if argument is odd.
odd'' :: Integer -> Bool
odd'' n = not (even'' n)

prop_even'' :: Integer -> Bool
prop_even'' n = even'' (2*n)

prop_odd'' :: Integer -> Bool
prop_odd'' n = odd'' (2*n + 1)

-- Checks if argument is even.
even :: Integer -> Bool
even 0 = True
even 1 = False
even n | n >= 2 = even (n-2)
even n | n < 0 = even (-n)

-- Checks if argument is odd.
odd :: Integer -> Bool
odd n = not (even n)

prop_even :: Integer -> Bool
prop_even n = even (2*n) && not (even (2*n + 1))

prop_odd :: Integer -> Bool
prop_odd n = odd (2*n + 1) && not (odd (2*n))

-- Checks if argument is even.
even' :: Integer -> Bool
even' 0 = True
even' n | n > 0 = odd' (n-1)
even' n | n < 0 = odd' (n+1)

-- Checks if argument is odd.
odd' :: Integer -> Bool
odd' 0 = False
odd' n | n > 0 = even' (n-1)
odd' n | n < 0 = even' (n+1)

prop_even' :: Integer -> Bool
prop_even' n = even' (2*n) && not (even' (2*n + 1))

prop_odd' :: Integer -> Bool
prop_odd'  n = odd' (2*n + 1) && not (odd' (2*n))

------------------------------------------------------------------------
-- Divisors

-- divisors n, for positive n, yields the number of positive divisors
-- of n.
divisors :: Integer -> Integer
divisors n | n <= 0    = error "divisors: Negative input."
           | otherwise = divisors' n
  where
  divisors' :: Integer -> Integer
  divisors' 1 = 1
  divisors' m | m `divides` n = 1 + divisors' (m - 1)
              | otherwise     = divisors' (m - 1)

-- All numbers greater than 1, also primes, have at least two divisors.
prop_divisors :: Integer -> Property
prop_divisors n = n > 1 ==> 2 <= divs && divs <= n
  where divs = divisors n

prop_divisors' :: Integer -> Integer -> Property
prop_divisors' m n =
  m > 0 && n > 0 ==>
    divisors m <= divisors (m * n)

prop_divisors'' :: Integer -> Integer -> Property
prop_divisors'' m n =
  m > 0 && n > 0 && m `divides` n ==>
    divisors m <= divisors n

divisors1 :: Integer -> Integer
divisors1 n | n <= 0    = error "divisors1: Negative input."
            | otherwise = divisors1' n n

-- Helper function for divisors1.
divisors1' :: Integer -> Integer -> Integer
divisors1' 1 n = 1
divisors1' m n | m `divides` n = 1 + divisors1' (m - 1) n
               | otherwise     = divisors1' (m - 1) n

-- All numbers greater than 1, also primes, have at least two divisors1.
prop_divisors1 :: Integer -> Property
prop_divisors1 n = n > 1 ==> 2 <= divs && divs <= n
  where divs = divisors1 n

prop_divisors1' :: Integer -> Integer -> Property
prop_divisors1' m n =
  m > 0 && n > 0 ==>
    divisors1 m <= divisors1 (m * n)

prop_divisors1'' :: Integer -> Integer -> Property
prop_divisors1'' m n =
  m > 0 && n > 0 && m `divides` n ==>
    divisors1 m <= divisors1 n

divisors' :: Integer -> [Integer]
divisors' n | n <= 0    = error "divisors: Negative input."
            | otherwise = reverse $ divisors'' n
  where
  divisors'' :: Integer -> [Integer]
  divisors'' 1 = [1]
  divisors'' m | m `divides` n = m : divisors'' (m - 1)
               | otherwise     = divisors'' (m - 1)

prop_divisors'Divisors n =
  n > 0 ==> and [ m `divides` n | m <- divisors' n ]

prop_divisors'All m n =
  m > 0 && n > 0 ==> m `elem` divisors' (m*n)

------------------------------------------------------------------------
-- Gcd

-- x =^= y is True iff the absolute values of x and y are equal.
(=^=) :: Integer -> Integer -> Bool
x =^= y = abs x == abs y

prop_gcdDivisor :: Integer -> Integer -> Property
prop_gcdDivisor m n =
  m /= 0 || n /= 0 ==> gcd' m n `divides` m

prop_gcdCommutative :: Integer -> Integer -> Property
prop_gcdCommutative m n =
  m /= 0 || n /= 0 ==> gcd' m n =^= gcd' n m

prop_gcdGreatest :: Integer -> Integer -> Integer -> Property
prop_gcdGreatest m n p =
  (m /= 0 || n /= 0) && p /= 0 &&
  p `divides` m && p `divides` n ==>
    p `divides` gcd' m n

prop_gcdGreatest' :: Integer -> Integer -> Integer -> Property
prop_gcdGreatest' m n p =
  (m /= 0 || n /= 0) && p /= 0 &&
  p `divides` m && p `divides` n ==>
    collect p $
      p `divides` gcd' m n

prop_gcdInternal m n = m /= 0 || n /= 0 ==> gcd m n =^= gcd' m n

-- gcd' m n computes the greatest common divisor of m and n. At most
-- one of m and n may be zero.
gcd' :: Integer -> Integer -> Integer
gcd' 0 0 = error "The gcd of 0 and 0 is undefined."
gcd' m 0 = m
gcd' m n = gcd' n (m `mod` n)