import Test.QuickCheck

---------------------------------------------------------------------------
-- 1. The Maximum Function

-- maxi x y returns the maximum of x and y
maxi :: Integer -> Integer -> Integer
maxi x y | x >= y = x
         | y >  x = y

-- alternatively:
{-
maxi :: Integer -> Integer -> Integer
maxi x y | x >= y    = x
         | otherwise = y
-}

prop_MaxiGreater x y =
  mx >= x && mx >= y
 where
  mx = maxi x y

prop_MaxiEither x y =
  mx == x || mx == y
 where
  mx = maxi x y

prop_MaxiX x y =
  x >= y ==>
    maxi x y == x

prop_MaxiY x y =
  y >= x ==>
    maxi x y == y

-- Q: Why is it better to say "x >= y" than "x > y" in the above?

---------------------------------------------------------------------------
-- 2. Sum of Squares

-- sumsq n returns 1*1 + 2*2 + ... + n*n
sumsq :: Integer -> Integer
sumsq 0         = 0
sumsq n | n > 0 = sumsq (n-1) + n*n

prop_SumSq n =
  n >= 0 ==>
    sumsq n == n * (n+1) * (2*n+1) `div` 6

-- Q: What happens when you take away the "n>=0 ==>" part? Try it!

---------------------------------------------------------------------------
-- 3. The Towers of Hanoi

{-
The recursive strategy is as follows: Recipe to move one pile of stones
from pillar "A" to pillar "B":

1. If there is no stone, there is nothing to move
2. Otherwise, call the third pillar "C"
3. Recursively move all but the biggest stone from "A" to "C"
4. Move the biggest stone to "B"
5. Recursively move all stones from "C" to "B"
6. Done!
-}

-- hanoi n computes the number of steps to move one pile with n stones
hanoi :: Integer -> Integer
hanoi 0         = 0
hanoi n | n > 0 = m + 1 + m
 where
  m = hanoi (n-1)

{-
Recipe to move one pile of stones from pillar "A" to pillar "B",
using 4 pillars in total:

1. If there is no stone, there is nothing to move
2. Otherwise, call the third and fourth pillar "C" and "D"
3. Recursively move k stones from "A" to "C", for some 0 < k < n
4. Using the 3-pile recipe and pile "D", move the rest of the stones from
   "A" to "B"
5. Recursively move the k stones from "C" to "B"
6. Done!
-}

-- first try:
{-
hanoi4 :: Integer -> Integer
hanoi4 0         = 0
hanoi4 n | n > 0 = m + hanoi (n-k) + m
 where
  m = hanoi4 k

-- what should k be?
-}

-- hanoi4 n computes the number of steps to move n stones using 4 pillars,
-- using strategy above where k=2
hanoi4 :: Integer -> Integer
hanoi4 0         = 0
hanoi4 1         = 1
hanoi4 n | n > 0 = m + 3 + m
 where
  m = hanoi4 (n-2)

-- överkurs:
{-
-- hanoi4 n computes the number of steps to move n stones using 4 pillars,
-- using the best possible k
hanoi4 :: Integer -> Integer
hanoi4 0         = 0
hanoi4 1         = 1
hanoi4 n | n > 0 = bestk 1 n

-- bestk k n computes the number of steps to move n stones using 4 pillars,
-- trying all choices for k, and choosing the best one
bestk :: Integer -> Integer -> Integer
bestk k n
  | k == n-1 = steps
  | k < n-1  = min steps (bestk (k+1) n)
 where
  m     = hanoi4 k
  steps = m + hanoi (n-k) + m
-}

prop_Hanoi n =
  n >= 0 ==>
    hanoi4 n <= hanoi n

prop_HanoiBetter n =
  n >= 3 ==>
    hanoi4 n < hanoi n

---------------------------------------------------------------------------
-- 4. Fibonacci Numbers

-- fib n computes the nth Fibonacci number
fib :: Integer -> Integer
fib 0 = 1
fib 1 = 1
fib n = fib (n - 1) + fib (n - 2)

-- fib2 n computes the nth Fibonacci number, but more efficiently
fib2 :: Integer -> Integer
fib2 n = fibAux n 1 1

-- fibAux i (fib n) (fib (n+1)) == fib (n+i)
fibAux :: Integer -> Integer -> Integer -> Integer
fibAux 0 a b         = a
fibAux i a b | i > 0 = fibAux (i-1) b (a+b)

prop_FibAux i n =
  i >= 0 && n >= 0 ==>
    fibAux i (fib2 n) (fib2 (n+1)) == fib2 (n+i)

prop_Fib2 n =
  n >= 0 ==>
    fib n == fib2 n

-- Q: Why don't we use fib in the definition of prop_FibAux?

{-
  fibAux 4 1 1
= fibAux (4-1) 1 (1+1)
= fibAux (3-1) 2 (1+2)
= fibAux (2-1) 3 (2+3)
= 5
-}

---------------------------------------------------------------------------
-- 5. Factors

-- smallestFactor lies between 1 and n
prop_SmallestFactor n =
  n > 0 ==>
    1 <= fact && fact <= n
 where
  fact = smallestFactor n

-- smallestFactor is a factor
prop_SmallestFactorIsFactor n =
  n > 0 ==>
    divides fact n
 where
  fact = smallestFactor n

-- smallestFactor is smallest
prop_SmallestFactorIsSmallest n fact' =
  n > 0 ==>
    2 <= fact' && fact' <= n ==>
      divides fact' n ==>
        fact <= fact'
 where
  fact = smallestFactor n

-- divides a b checks whether a divides b
divides :: Integer -> Integer -> Bool
divides a b = b `mod` a == 0

-- nextFactor k n lies between k and n
prop_NextFactor k n =
  0 < k && k <= n ==>
    k <= fact && fact <= n
 where
  fact = nextFactor k n

-- nextFactor k n is a factor
prop_NextFactorIsFactor k n =
  0 < k && k <= n ==>
    divides fact n
 where
  fact = nextFactor k n

-- smallestFactor n returns the smallest factor of n larger than one
smallestFactor :: Integer -> Integer
smallestFactor n = nextFactor 2 n

-- nextFactor k n returns the smallest factor of n larger than k
nextFactor :: Integer -> Integer -> Integer
nextFactor k n
  | k >= n      = n
  | divides k n = k
  | otherwise   = nextFactor (k+1) n

-- numFactors computes the number of factors of n in the range 1..n
numFactors :: Integer -> Integer
numFactors n = nextFactors 1 n

nextFactors :: Integer -> Integer -> Integer
nextFactors k n
  | k >= n    = 1
  | otherwise = 1 + nextFactors (nextFactor (k+1) n) n

prop_Prime n =
  n >= 2 && smallestFactor n == n ==>
    numFactors n == 2 -- namely 1 and n

-- Q: What happens when we take away the n >= 2?
-- Q: What happens when we change the n >= 2 to n >= 1 or n >= 0?

---------------------------------------------------------------------------
-- 6. Defining Types

-- a datatype for months
data Month
  = January
  | February
  | March
  | April
  | May
  | June
  | July
  | August
  | September
  | October
  | November
  | December
 deriving ( Eq, Show )

-- daysInMonth month year returns the days in the month in the year
daysInMonth :: Month -> Integer -> Integer
daysInMonth January   year = 31
daysInMonth February  year
  | leap year              = 29
  | otherwise              = 28
daysInMonth March     year = 31
daysInMonth April     year = 30
daysInMonth May       year = 31
daysInMonth June      year = 30
daysInMonth July      year = 31
daysInMonth August    year = 31
daysInMonth September year = 30
daysInMonth October   year = 31
daysInMonth November  year = 30
daysInMonth December  year = 31

-- leap year approximates whether year is a leap year
leap :: Integer -> Bool
leap year = year `mod` 4 == 0

-- a datatype for dates
data Date = Date{ year :: Integer, month :: Month, day :: Integer }

-- validDate date checks whether date is a valid date, regarding
-- numbers of days in the month
validDate :: Date -> Bool
validDate date = 1 <= day date
                   && day date <= daysInMonth (month date) (year date)

---------------------------------------------------------------------------
-- 7. Replication

repli :: Integer -> String -> String
repli 0 str = ""
repli n str = str ++ repli (n-1) str

---------------------------------------------------------------------------
-- 8. Muliplying list elements

-- multiply xs multiplies all elements in the list xs
multiply :: Num a => [a] -> a
multiply []     = 1
multiply (x:xs) = x * multiply xs

---------------------------------------------------------------------------
-- 9. Avoiding Duplicates

-- duplicates xs checks if there are duplicates in the list xs
duplicates :: Eq a => [a] -> Bool
duplicates []     = False
duplicates (x:xs) = exists x xs || duplicates xs

-- exists x xs checks whether x exists as an element in the list xs
exists :: Eq a => a -> [a] -> Bool
exists x []     = False
exists x (y:ys) = x == y || exists x ys

-- Note: "exists" is the standard Haskell function "elem"

-- removeDuplicates xs returns the list xs with all duplicate elements removed
removeDuplicates :: Eq a => [a] -> [a]
removeDuplicates []     = []
removeDuplicates (x:xs) = x : removeDuplicates (remove x xs)

-- remove x xs removes x from the list xs
remove :: Eq a => a -> [a] -> [a]
remove x []                 = []
remove x (y:ys) | x == y    = remove x ys
                | otherwise = y : remove x ys

{-
-- alternative solution:
-- (returns elements in different order!)

-- removeDuplicates xs returns the list xs with all duplicate elements removed
removeDuplicates :: Eq a => [a] -> [a]
removeDuplicates []                   = []
removeDuplicates (x:xs) | exists x xs = removeDuplicates xs
                        | otherwise   = x : removeDuplicates xs
-}

-- No, the property does not guarantee this. A function always returning the
-- empty list would also satisfy the property!

-- Missing is a property that checks that no elements disappear:

prop_RemoveDuplicatesKeepsElements xs =
  allExist xs (removeDuplicates xs)

-- allExist xs ys checks whether all x in xs exist as an element in ys
allExist :: Eq a => [a] -> [a] -> Bool
allExist []     ys = True
allExist (x:xs) ys = exists x ys && allExist xs ys

---------------------------------------------------------------------------