import Test.QuickCheck

-- some more examples of recursive functions over lists, including properties

-- slow definition of "reverse", uses a quadratic number of steps
rev :: [a] -> [a]
rev []     = []
rev (x:xs) = rev xs ++ [x]

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

-- faster definition of "reverse", uses a linear number of steps
rev2 :: [a] -> [a]
rev2 xs = revHelp xs []

revHelp :: [a] -> [a] -> [a]
revHelp []     korg = korg
revHelp (x:xs) korg = revHelp xs (x:korg)

-- Note: The technique used in rev2 can be useful in lab 2 (e.g shuffling a deck
-- of cards).

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

-- properties of "reverse" that can be tested using QuickCheck

-- the length of a reversed lists should be the same as the original list
prop_ReverseLength xs =
  length (rev2 xs) == length (xs :: [Int])

-- indexing in the original list should give the same result as indexing
-- "from the back" in the reversed list
prop_ReverseIndex xs i =
  0 <= i && i < length (xs :: [Int]) ==>
    xs !! i  ==  rev2 xs !! (length xs - 1 - i)

{-
  0   1   2   3   4  (5)
['a','b','c','d','e']

  0   1   2   3   4
['e','d','c','b','a']
-}

-- testing a property
--   A ==> B
-- will find 100 tests that make A true, and then test B

-- this is a worse version of the above property, because all tests we run
-- are counted towards the 100 tests, even the ones where A is false
prop_ReverseIndex' :: [Int] -> Int -> Bool
prop_ReverseIndex' xs i
  | 0 <= i && i < length xs = xs !! i  ==  rev2 xs !! (length xs - 1 - i)
  | otherwise               = True

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

-- definition of "take"
tak :: Int -> [a] -> [a]
tak n _      | n <= 0 = []
tak _ []              = []
tak n (x:xs)          = x : tak (n-1) xs

-- predicting the length of the result of take, for values that are
-- small: if we take n elements from a list with at least n elements, the
-- result has length n
prop_TakeLength :: Int -> [Int] -> Property
prop_TakeLength n xs =
  0 <= n && n <= length xs ==>
    length (tak n xs) == n

-- predicting the length of the result of take, for values that are
-- small: if we take n elements from a list smaller than n elements, the
-- result has all the elements
prop_TakeLengthTooBig :: Int -> [Int] -> Property
prop_TakeLengthTooBig n xs =
  n > length xs ==>
    tak n xs == xs

-- property stating the relationship between the functions "take" and "drop"
prop_TakeDrop :: Int -> [Int] -> Bool
prop_TakeDrop n xs =
  take n xs ++ drop n xs == xs

prop_Maximum_Greater :: [Int] -> Bool
prop_Maximum_Greater xs =
  and [ maximum xs >= x | x <- xs ]

prop_Maximum_Element :: [Int] -> Property
prop_Maximum_Element xs =
  length xs > 0 ==>
    maximum xs `elem` xs

-- be careful, QuickCheck says the following is true
-- (because the type of xs defaults to [()])
prop_Reverse_Wierd xs =
  reverse xs == xs

-- proper test
prop_Reverse xs =
    reverse (reverse xs) == xs
  where
    _ = xs :: [Int]