module Exercise_4 where
import Test.QuickCheck
import Data.List

{---------------------------------------------------------------------}
{- Aufgabe G4.1 -}

{- allEqual ist nicht Teil des Übungsblattes, nur ein Beispiel. -}
allEqual :: [Integer] -> Bool
--allEqual [] = True
--allEqual [x] = True
allEqual (x : y : ys) = x == y && allEqual (y : ys)
allEqual _ = True


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



{---------------------------------------------------------------------}
{- Aufgabe G4.2 -}

-- Beispielschlüssel vom Blatt
key = [('a','x'),('H','e'),('l','P'),('o','M')]

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


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

--Alternativ:
crypt' key [] = []
crypt' key (x : xs) = cryptChar key x : crypt' key xs 


isKeyReversible :: [(Char,Char)] -> Bool
isKeyReversible [] = True
isKeyReversible ((k,v) : ks) = null [1 | (k', v') <- ks, v' == v] && isKeyReversible ks

--Alternativ (wird in den QuickCheck Tests verwendet):
isKeyReversible' ks = nub vs == vs
        where vs = [v | (_, v) <- ks]


{- QuickCheck Tests -}
-- Wenn kein Value doppelt ist kommt True raus
prop_isKeyReversible_complete :: [(Char, Char)] -> Property
prop_isKeyReversible_complete ks = vs == nub vs ==> isKeyReversible ks
        where vs = [v | (_, v) <- ks]

-- Wenn ein Value doppelt ist kommt False raus
prop_isKeyReversible_sound :: Char -> Char-> Char -> [(Char, Char)] -> [(Char, Char)] -> [(Char, Char)] -> Bool
prop_isKeyReversible_sound v k1 k2 ks1 ks2 ks3 =
        not(isKeyReversible (ks1 ++ [(k1, v)] ++ ks2 ++ [(k2, v)] ++ ks3))



{---------------------------------------------------------------------}
{- Aufgabe G4.3 -}


-- Englisch, da schamlos aus der Musterlösung geklaut.
{-
 - 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)
-}



{---------------------------------------------------------------------}
{- Aufgabe G4.4 -}

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



{---------------------------------------------------------------------}
{- Aufgabe H4.1 -}

strictlyDescending :: [Integer] -> Bool
strictlyDescending = undefined



{---------------------------------------------------------------------}
{- Aufgabe H4.2 -}

chunks :: Int -> [a] -> [[a]]
chunks = undefined

irregularChunks :: [Int] -> [a] -> [[a]]
irregularChunks = undefined



{---------------------------------------------------------------------}
{- Aufgabe H4.3 -}

{-WETT-}
upsAndDowns :: Ord a => [a] -> [[a]]
upsAndDowns = undefined
{-TTEW-}



{---------------------------------------------------------------------}
{- Aufgabe H4.4 -}

{-
 - <Hier Induktionsbeweis einfügen>
 -}