module Sol_Exercise_4 where
import Test.QuickCheck
import Data.List
import Data.Monoid
import Data.Tuple

{- G1 -}

hasFibonacciProperty :: [Integer] -> Bool
hasFibonacciProperty (x:y:z:zs) = x + y == z && hasFibonacciProperty (y:z:zs)
hasFibonacciProperty _ = True

{- G2 -}

cryptChar :: [(Char,Char)] -> Char -> Char
cryptChar [] c = '_'
cryptChar ((k,v) : ks) c = if k == c then v else cryptChar ks c

crypt :: [(Char,Char)] -> [Char] -> [Char]
crypt key [] = []
crypt key (x : xs) = cryptChar key x : crypt key xs

isKeyReversible :: [(Char,Char)] -> Bool
isKeyReversible [] = True
isKeyReversible ((k,v) : ks) = not (v `elem` values ks) && isKeyReversible ks
  where
    values [] = []
    values ((_,v) : ks) = v : values ks

prop_isKeyReversible_sound :: Char -> [(Char,Char)] -> Char -> [(Char,Char)] -> Char -> [(Char,Char)] -> Property
prop_isKeyReversible_sound v ks1 k1 ks2 k2 ks3 = k1 /= k2 ==>
    not (isKeyReversible (ks1 ++ [(k1,v)] ++ ks2 ++ [(k2,v)] ++ ks3))

prop_isKeyReversible_complete :: [(Char,Char)] -> Property
prop_isKeyReversible_complete ks = nub vs == vs ==> isKeyReversible ks
  where
    vs = values ks
    values [] = []
    values ((_,v) : ks) = v : values ks

{- G3 -}

{-
Note: [x] is just a syntactic abbreviation for (x : [])

Lemma reverse (snoc xs x) = x : reverse xs
Proof by structural induction on xs

Base case:
To show: reverse (snoc [] x) = x : reverse []
reverse (snoc [] x)
== reverse [x]                 (by snoc_Nil)
== reverse [] ++ [x]           (by reverse_Cons)
== [] ++ [x]                   (by reverse_Nil)
== [x]                         (by append_Nil)
x : reverse []
== [x]                         (by reverse_Nil)

Induction step:
IH: reverse (snoc ys x) = x : reverse ys
To show: reverse (snoc (y : ys) x) = x : reverse (y : ys)
reverse (snoc (y : ys) x)
== reverse (y : snoc ys x)     (by snoc_Cons)
== reverse (snoc ys x) ++ [y]  (by reverse_Cons)
== (x : reverse ys) ++ [y]     (by IH)
== x : (reverse ys ++ [y])     (by append_Cons)
x : reverse (y : ys)
== x : (reverse ys ++ [y])     (by reverse_Cons)
-}

{- G4 -}

match :: [Char] -> [Char] -> Bool
match [] ys = null ys
match ('?' : ps) (_ : ys) = match ps ys
match ('*' : ps) [] = match ps []
match ('*' : ps) (y : ys) = match ps (y : ys) || match ('*' : ps) ys
match (p : ps) [] = False
match (p : ps) (y : ys) = p == y && match ps ys


{- H1 -}

strictlyDescending :: [Integer] -> Bool
strictlyDescending (x:y:ys) = x > y && strictlyDescending (y:ys)
strictlyDescending _ = True

{- H2 -}

chunks :: Int -> [a] -> [[a]]
chunks _ [] = []
chunks k xs = take k xs : chunks k (drop k xs)

irregularChunks :: [Int] -> [a] -> [[a]]
irregularChunks _ [] = []
irregularChunks [] _ = []
irregularChunks (k : ks) xs = take k xs : irregularChunks ks (drop k xs)

{- H3 -}

{-WETT-}
upsAndDowns2 :: Ord a => [a] -> [a] -> [[a]]
upsAndDowns2 []	ys = [reverse ys]
upsAndDowns2 (x : xs) [] = upsAndDowns2 xs [x]
upsAndDowns2 (x : xs) (y : ys)
  | x >= y = upsAndDowns2 xs (x : y : ys)
  | otherwise = reverse (y : ys) : downsAndUps2 (x : xs) []

downsAndUps2 :: Ord a => [a] -> [a] -> [[a]]
downsAndUps2 []	ys = [reverse ys]
downsAndUps2 (x : xs) [] = downsAndUps2 xs [x]
downsAndUps2 (x : xs) (y : ys)
  | x <= y = downsAndUps2 xs (x : y : ys)
  | otherwise = reverse (y : ys) : upsAndDowns2 (x : xs) []

upsAndDowns :: Ord a => [a] -> [[a]]
upsAndDowns [] = []
upsAndDowns xs = upsAndDowns2 xs []
{-TTEW-}

{-WETT-}
upsAndDowns2' :: Ord a => Bool -> [a] -> [a] -> [[a]]
upsAndDowns2' _ [] ys = [reverse ys]
upsAndDowns2' up (x : xs) [] = upsAndDowns2' up xs [x]
upsAndDowns2' up (x : xs) (y : ys)
  | if up then x >= y else x <= y = upsAndDowns2' up xs (x : y : ys)
  | otherwise = reverse (y : ys) : upsAndDowns2' (not up) (x : xs) []

upsAndDowns' :: Ord a => [a] -> [[a]]
upsAndDowns' [] = []
upsAndDowns' xs = upsAndDowns2' True xs []
{-TTEW-}

{-WETT-}
upsAndDowns2'' :: Ord a => (a -> a -> Bool) -> [a] -> [a] -> [[a]]
upsAndDowns2'' _ [] ys = [reverse ys]
upsAndDowns2'' comp (x : xs) [] = upsAndDowns2'' comp xs [x]
upsAndDowns2'' comp (x : xs) (y : ys)
  | comp x y = upsAndDowns2'' comp xs (x : y : ys)
  | otherwise = reverse (y : ys) : upsAndDowns2'' (flip comp) (x : xs) []

upsAndDowns'' :: Ord a => [a] -> [[a]]
upsAndDowns'' [] = []
upsAndDowns'' xs = upsAndDowns2'' (>=) xs []
{-TTEW-}

{-WETT-}
upsAndDowns2''' :: Ord a => (a -> a -> Bool) -> [a] -> [a] -> [[a]]
upsAndDowns2''' _ [] ys = [reverse ys]
upsAndDowns2''' comp xs [] = upsAndDowns2'' comp (tail xs) [head xs]
upsAndDowns2''' comp xs ys =
  if comp (head xs) (head ys) then upsAndDowns2''' comp (tail xs) (head xs : ys)
  else reverse ys : upsAndDowns2''' (flip comp) xs []

upsAndDowns''' :: Ord a => [a] -> [[a]]
upsAndDowns''' [] = []
upsAndDowns''' xs = upsAndDowns2''' (>=) xs []
{-TTEW-}

{-WETT-}
upsAndDowns_4 :: Ord a => [a] -> [[a]]
upsAndDowns_4 xs = upsAndDowns2_4 (uncurry (>=)) $ zip xs $ head xs : xs

upsAndDowns2_4 :: Ord a => ((a,a) -> Bool) -> [(a,a)] -> [[a]]
upsAndDowns2_4 _ [] = mempty
upsAndDowns2_4 comp xs =
    map fst (takeWhile comp xs) : upsAndDowns2_4 (comp . swap) (dropWhile comp xs)
{-TTEW-}

{-WETT-}
upsAndDowns_5 :: Ord a => [a] -> [[a]]
upsAndDowns_5 xs = uncurry (>=) `upsAndDowns2_5` zip xs (head xs : xs)

upsAndDowns2_5 :: Ord a => ((a,a) -> Bool) -> [(a,a)] -> [[a]]
upsAndDowns2_5 _ [] = mempty
upsAndDowns2_5 comp xs =
    map fst (takeWhile comp xs) : (comp . swap) `upsAndDowns2_5` dropWhile comp xs
{-TTEW-}

{- H4 -}

{-
Note: [x] is just a syntactic abbreviation for (x : [])

Lemma length (reverse xs) = length xs
Proof by structural induction on xs

Base case:
To show: length (reverse []) = length []
length (reverse [])
== length []                          (by reverse_Nil)

Induction step:
IH: length (reverse ys) = length ys
To show: length (reverse (y : ys)) = length (y : ys)
length (reverse (y : ys))
== length (reverse ys ++ [y])         (by reverse_Cons)
== length (reverse ys) + length [y]   (by length_append)
== length ys + length [y]             (by IH)
== length ys + (length [] + 1)        (by length_Cons)
== length ys + (0 + 1)                (by length_Nil)
== length ys + 1                      (by add_0)
length (y : ys)
== length ys + 1                      (by length_Cons)
-}