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

{- Library -- nicht veraendern -}

data Fml a = Var a | Neg (Fml a) | Conj [Fml a] | Disj [Fml a]
    deriving (Eq, Show)

{- 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
 -
 -
 -}


{- H14.1 -}

{- Richtige Implementierungen -}

uniqueElems_good1 :: Eq a => [a] -> [a]
uniqueElems_good1 = Data.List.nub

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

uniqueElems_good3 :: Eq a => [a] -> [a]
uniqueElems_good3 [] = []
uniqueElems_good3 (x : xs) =
  if x `elem` xs then uniqueElems_good3 (Data.List.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 (Data.List.delete x xs)

uniqueElems_bad4 :: Eq a => [a] -> [a]
uniqueElems_bad4 [] = []
uniqueElems_bad4 (_ : xs) = Data.List.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 sie 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 =
  Data.List.sort (uniqueElems xs) == Data.List.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 = Data.List.all (`elem` xs) (uniqueElems xs)

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

prop_uniqueElems_noDups :: [Int] -> Bool
prop_uniqueElems_noDups xs =
  length (Data.List.nub xs') == length xs' where xs' = uniqueElems 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.
-}

{- H14.2 -}

rename :: (a -> a) -> Fml a -> Fml a
rename f (Var c) = Var $ f c
rename f (Neg fml) = Neg $ rename f fml
rename f (Conj fmls) = Conj $ map (rename f) fmls
rename f (Disj fmls) = Disj $ map (rename f) fmls