module Sol_Exercise_14 where
import qualified Data.List
import Test.QuickCheck

{- Library -- nicht veraendern -}


{- G14.1 -}

delete :: Eq a => a -> [a] -> [a]
delete = Data.List.delete {- falsche Implementierung -}

{-
   Anmerkung: Tests sollten von einem konkret festgelegten Typ sein (unten z.B. Int):
   Die Standard-Instantiierung von Eq a durch QuickCheck ist () -- wenig hilfreich
-}

{- 1. vollstaendige Testsuite -}
prop_single :: Int -> Int -> Bool
prop_single x y = delete x [y] == if x == y then [] else [y]

prop_append :: Int -> [Int] -> [Int] -> Bool
prop_append x xs ys = delete x (xs ++ ys) == delete x xs ++ delete x ys

{- 2. vollstaendige Testsuite -}
prop_nil :: Int -> Bool
prop_nil x = null (delete x [])

prop_cons :: Int -> Int -> [Int] -> Bool
prop_cons x y xs = delete x (y : xs) == if x == y then delete x xs else y : delete x xs

{-
Beide Testsuites sind zwar vollstaendig, aber dennoch keine guten Tests.
Die Wahrscheinlichkeit fuer x == y in prop_single und prop_cons ist sehr gering da
der Typ Int viel Auswahl bietet. Deswegen braucht man sehr viele Tests um Fehler zu entdecken.
Stattdessen waere der Typ Bool schon besser geeignet.
-}

{- G14.2 -}

concat :: [[a]] -> [a]
concat = go []
    where go acc [] = reverse acc
          go acc (xs:xss) = go (reverse xs ++ acc) xss

{-
 - Als endrekursive Funktion braucht concat nur konstanten Stackspace.
 - Das "reverse acc" erzwingt allerdings, dass die gesamte Liste ausgewertet
 - wird, um auch nur das erste Element der konkatenierten Liste anschauen
 - zu können.
 -
 - Bei concat' muss dafür immer nur ein kleines Stück der Liste ausgewertet
 - werden. Aufgrund der Auswertungsstrategie von Haskell funktioniert
 - die Auswertung von concat' mit konstantem Speicher: Der rekursive
 - Aufruf in "xs ++ concat' xss" wird erst dann ausgewertet, wenn "xs"
 - bereits konsumiert wurde.
 -
 - Weiterführende Literatur findet sich z.B. unter
 -
 -    http://www.haskell.org/haskellwiki/Stack_overflow
 -
 -
 - Mit einer strikten Auswertungsstrategie muss auch concat' immer
 - vollständig ausgewertet werden um einzelne Listenelemente zu erhalten.
 - In einer strikten Programmiersprache würde concat' daher Stackspeicher
 - linear in der Länge der Liste xss brauchen.
 -}


{- G14.2 -}

{-
 - map (*2) (1 : threes) !! 1
 - = ((*2) 1 : map threes) !! 1
 - = map (*2) threes !! (1-1)
 - = map (*2) (3 : threes) !! (1-1)
 - = ((*2) 3 : map threes) !! (1-1)
 - = ((*2) 3 : map threes) !! 0
 - = (*2) 3
 - = 3*2
 - = 6
 -
 -
 - (\f -> \x -> x + f 2) (\y -> y * 2) (3 + 1)
 - = (\x -> x + (\y -> y * 2) 2) (3 + 1)
 - = (3 + 1) + (\y -> y * 2) 2
 - = 4 + (\y -> y * 2) 2
 - = 4 + 2 * 2
 - = 4 + 4
 - = 8
 -
 - filter (/=3) threes
 - filter (/=3) (3 : threes)
 - filter (/=3) threes
 -
 -  --> terminiert nicht
 -
 -
 -}


{- H14.1 -}

{-
:t Ausdruck
selber in ghci eingeben!
-}

{- H14.2 -}

{-
Lemma tmap f (mirror t) = mirror (tmap f t)
Proof by structural induction on t

Base case:
To show: tmap f (mirror Empty) = mirror (tmap f Empty)
tmap f (mirror Empty)
== tmap f Empty           (by mirror_Empty)
== Empty                  (by tmap_Empty)
mirror (tmap f Empty)
== mirror Empty           (by tmap_Empty)
== Empty                  (by mirror_Empty)

Induction step:
IH1: tmap f (mirror l) = mirror (tmap f l)
IH2: tmap f (mirror r) = mirror (tmap f r)
To show: tmap f (mirror (Node x l r)) = mirror (tmap f (Node x l r))
tmap f (mirror (Node x l r))
== tmap f (Node x (mirror r) (mirror l))                  (by mirror_Node)
== Node (f x) (tmap f (mirror r)) (tmap f (mirror l))     (by tmap_Node)
== Node (f x) (mirror (tmap f r)) (tmap f (mirror l))     (by IH2)
== Node (f x) (mirror (tmap f r)) (mirror (tmap f l))     (by IH1)
mirror (tmap f (Node x l r))
== mirror (Node (f x) (tmap f l) (tmap f r))              (by tmap_Node)
== Node (f x) (mirror (tmap f r)) (mirror (tmap f l))     (by mirror_Node)

QED
-}

{- H14.3 -}

filterMap :: (a -> Maybe b) -> [a] -> [b]
filterMap _ [] = []
filterMap f (x : xs) = case f x of
            Nothing -> filterMap f xs
            Just y -> y : filterMap f xs