module Exercise_14_Sol where

import Data.List
import Data.Maybe
import Test.QuickCheck


{-G14.1-}

{-

1) endrekursiv: der letzte Aufruf ist 'prod', alle weiteren Berechnungen finden
   in den Argumenten statt
2) nicht endrekursiv: nach dem Aufruf von 'prod' muss noch eine Multiplikation
   durchgeführt werden
3) endrekursiv: der letzte Aufruf ist 'prod', ebenso wie bei 1). Das
   'if-then-else' ist hier nicht ausschlaggebend, weil die Bedingung vor dem
   rekursiven Aufruf berechnet wird. Nach dem Aufruf muss nichts weiter getan
   werden.

-}

{-G14.2-}

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

{- Warum 'reverse'? Ohne 'reverse' müsste man hinten anhängen (acc ++ xs), was
 - aber quadratische Laufzeit erzeugt, denn die Laufzeit von '++' ist von der
 - Länge des ersten Arguments abhängig. -}

{-G14.3-}

{-
 - map (*2) (1 : threes) !! 1
 - = ((*2) 1 : map (*2) threes) !! 1
 - = map (*2) threes !! (1-1)
 - = map (*2) (3 : threes) !! (1-1)
 - = ((*2) 3 : map (*2) threes) !! (1-1)
 - = ((*2) 3 : map (*2) 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
 -
 - head (filter (/=3) threes)
 - head (filter (/=3) (3 : threes))
 - head (filter (/=3) threes)
 -
 -  --> terminiert nicht
 -
 -
 -}


{-G14.4-}

{- Richtige Implementierungen -}

uniqueElems_good1 :: Eq a => [a] -> [a]
uniqueElems_good1 = nub

uniqueElems_good2 :: Eq a => [a] -> [a]
uniqueElems_good2 = reverse . nub

uniqueElems_good3 :: Eq a => [a] -> [a]
uniqueElems_good3 [] = []
uniqueElems_good3 (x : xs) =
  if x `elem` xs then uniqueElems_good3 (reverse xs)
  else x : uniqueElems_good3 xs

{- Falsche Implementierungen -}

uniqueElems_bad1 :: Eq a => [a] -> [a]
uniqueElems_bad1 xs = xs

uniqueElems_bad2 :: Eq a => [a] -> [a]
uniqueElems_bad2 xs = xs

uniqueElems_bad3 :: Eq a => [a] -> [a]
uniqueElems_bad3 [] = []
uniqueElems_bad3 (x : xs) = x : uniqueElems_bad3 (delete x xs)

uniqueElems_bad4 :: Eq a => [a] -> [a]
uniqueElems_bad4 [] = []
uniqueElems_bad4 (_ : xs) = nub xs

{- Implementierung unter Test -}

uniqueElems :: Eq a => [a] -> [a]
uniqueElems = uniqueElems_bad4

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

{- Erste vollstaendige Testsuite

   Diese basiert auf eine Musterloesung. Im Allgemeinen ist dies eher
   suboptimal, weil nichts guarantiert, dass die Musterloesung richtig ist.
   Hier ist es in Ordung, weil wenn wir uns nich auf "nub" verlassen können,
   koennen wir auch davon ausgehen, dass "ghc" ganz falsch ist.
-}

prop_uniqueElems_vsMuster :: [Int] -> Bool
prop_uniqueElems_vsMuster xs =
  sort (uniqueElems xs) == sort (uniqueElems_good1 xs)


{- Zweite vollstaendige Testsuite

   Diese ist theoretisch besser, weil sie nur über abstrakte Eigenschaften
   spricht, die ganz offensichtlich gelten müssen.

   "Sound" heißt: die Ergebnisse sind korrekt (d.h. die Elemente, die in der
   Ausgabenliste stehen, gehören darin).

   "Complete" heißt: die Ergebnisse sind vollständig (d.h. alle Elemente, die
   in der Ausgabenliste stehen sollten, sind da).

   Am Ende überprüfen wir, dass das Ergebnis duplikatfrei ist. -}

prop_uniqueElems_sound :: [Int] -> Bool
prop_uniqueElems_sound xs = all (`elem` xs) (uniqueElems xs)

prop_uniqueElems_complete :: [Int] -> Bool
prop_uniqueElems_complete xs = all (`elem` uniqueElems xs) xs

prop_uniqueElems_noDups :: [Int] -> Bool
prop_uniqueElems_noDups xs =
  length (nub xs') == length xs' where xs' = uniqueElems xs


{-H14.1-}

{- Wir wenden drei Techniken an:
 -
 - "Precompute large data structures"
 -   - h wird immer auf dem Wert m aufgerufen, der sich im Laufe der
 -     Funktionsauswertung nicht verändert. Es reicht also aus, h m
 -     einmal zu berechnen.
 -
 - Deduplication:
 -   - g wird im rekursiven Fall zweimal gebraucht, es reicht aber, es einmal
 -     zu berechnen
 -
 - Tupling of results:
 -   - Der rekursive Fall braucht die Ergebnisse von f für n-1 und n-2, was
 -     zu einer exponentiellen Laufzeit führt. Dies lässt sich vermeiden,
 -     indem wir immer die Ergebnisse für den aktuellen und den vorherigen
 -     Schritt zurückliefern.
 -}

f :: ([a] -> Integer) -> [a] -> (Integer -> Integer) -> Integer -> Integer
f h xs g n = fst (f' g n)
  where
    hxs = h xs
    f' _ 0 = (1, undefined)
    f' g 1 = (1 + hxs, fst (f' g 0))
    f' g n = (fn0, fn1)
      where
        (fn1, fn2) = f' g (n - 1)
        gn = g n
        fn0 = if gn > -gn then fn1 + 2 * (hxs - fn2) else fn1 - hxs + gn

{- Statt auf "Tupling of results" können wir auch auf den Trick mit der
 - unendlichen Liste aus G13.3 zurückgreifen: -}

f2 :: ([a] -> Integer) -> [a] -> (Integer -> Integer) -> Integer -> Integer
f2 h xs g n = fst (fs !! fromInteger n)
  where
    fs = (1,0) : (1 + hxs,1) : zipWith fstep fs (tail fs)
    hxs = h xs
    fstep (fn2,_) (fn1, n1) = (fn0, n1 + 1)
      where
        gn = g (n1 + 1)
        fn0 = if gn > - gn then fn1 + 2 * (hxs - fn2) else fn1 - hxs + gn


{-H14.2-}

data Color = Red | Black deriving (Eq, Show)
data Tree a = Empty | Node Color a (Tree a) (Tree a) deriving (Eq, Show)

isOrdered :: Ord a => Maybe a -> Maybe a -> Tree a -> Bool
isOrdered _ _ Empty = True
isOrdered min max (Node _ a l r) = checkMin min a && checkMax max a && isOrdered min (Just a) l && isOrdered (Just a) max r
  where checkMin Nothing _ = True
        checkMin (Just min) a = min < a
        checkMax Nothing _ = True
        checkMax (Just max) a = a < max

isBlack :: Tree a -> Bool
isBlack (Node Red _ _ _) = False
isBlack _ = True

checkBlack :: Tree a -> Maybe Integer -- berechnet die gesamte Schwarztiefe des Baums
checkBlack Empty = Just 1
checkBlack (Node c _ l r) =
  case compare (checkBlack l) (checkBlack r) of
    Just d | c == Black -> Just (d + 1)
    d -> d
  where compare (Just x) (Just y) = if x == y then Just x else Nothing
        compare _ _ = Nothing

checkRed :: Tree a -> Bool
checkRed Empty = True
checkRed (Node Black _ l r) = checkRed l && checkRed r
checkRed (Node Red _ l r) = isBlack l && isBlack r && checkRed l && checkRed r

sameElements :: Ord a => [a] -> Tree a -> Bool
sameElements xs tree = sort (elems tree) == nub (sort xs)
  where elems Empty = []
        elems (Node _ x l r) = x : elems l ++ elems r

prop_fromList :: (Ord a, Show a, Arbitrary a) => ([a] -> Tree a) -> Property
prop_fromList f = property (my_prop_fromList f)

my_prop_fromList :: (Show a, Ord a) => ([a] -> Tree a) -> [a] -> Property
my_prop_fromList f xs = 
  -- mit 'counterexample' kann man sich eine genauere Fehlerbeschreibung
  -- anzeigen lassen (ändert aber nichts am Ergebnis)
  counterexample ("### Result tree\n" ++ show tree) $
    isOrdered Nothing Nothing tree &&
    isBlack tree &&
    checkRed tree &&
    isJust (checkBlack tree) &&
    sameElements xs tree
  where tree = f xs