module Sol_Exercise_6 where
import Data.Char
import Data.Ratio
import Test.QuickCheck

{- Library -- nicht verändern -}

type IList = [(Rational,Rational)]

ilist :: Rational -> [Rational] -> IList
ilist n (x:y:z:zs) = (s, s + y) : ilist (s + y + z) zs
    where s = n + x
ilist _ _ = []

rationalGen :: Gen Rational
rationalGen = do
    p <- choose (1,10)
    q <- elements [1,2,3,5,7]
    return $ p % q

ilistGen :: Gen IList
ilistGen = do
    xs <- sized (\size -> resize (3 * size) $ listOf $ rationalGen)
    return $ ilist 0 xs


{- G1 -}

{-
1. "(div 5) == (\x. div 5 x)", eine gecurryte Anwendung von "div". Also die
Funktion x |-> 5/x.

"(`div' 5) == (\x. x `div` 5) == (\x. div x 5)", eine Sektion. Also die Funktion
x |-> x/5.

2. "(+ 7) == (\x. x + 7)" (eine Sektion) vs. "((+) 7) == (\x. 7 + x)" (eine
gecurryte Anwendung). Beide sind gleich wenn "+" kommutativ ist.

3. "map (: []) :: [a] -> [[a]]" bildet die Liste "[x_1, ..., x_n]"
auf "[x_1 : [], ..., x_n : []]" ab, d.h. "[[x_1], ..., [x_n]]". Anders geschrieben:
"map (\x. [x])".

"map ([] :) :: [[[a]]] -> [[[a]]]" bildet die Liste "[x_1, ..., x_n]"
auf "[[] : x_1, ..., [] : x_n]" ab. Dafuer m\"ussen die "x"s Listen von Listen sein,
damit "[]" als Element vorne angehaengt werden kann.

4. "flip . flip :: (b -> a -> c) -> b -> a -> c" macht eigentlich nichts:
"flip (flip (>=)) == (>=)". D.h., sie ist die Identitaet, aber mit einem
beschraenkten Typ.

Anderseits hat "id :: a -> a" den allgemeinsten Typ fuer Identitaet. Man kann
beispielsweise "id 5" schreiben; "flip (flip 5)" geht nicht.

5. "[x, y, z]" ist eine dreielementige Liste, die "x :: a", "y :: a" und "z ::
a" enthält. "x : y : z" ist eine (2 oder mehr)-elementige Liste, mit "x :: a"
und "y :: a" vorne und der Teilliste "z :: [a]" hinten.
-}

{- G2 -}

{-
1. "foldl": Die Funktion nimmt drei Argumente. Das heißt, der Typ muss der Form

    a -> b -> c -> d
    
sein. Die erste Gleichung liefert das zweite Argument zurück. Daraus folgt dass
"b = d", also

    a -> b -> c -> b

Und das dritte Argument ist eine Liste, wegen des Mustervergleichs:

    a -> b -> [c] -> b

Die zweite Gleichung gibt zwei Argumente an "f", also

    (d -> e -> f) -> b -> [c] -> b

Das erste Argument an "f" ist "z", vom Typ "b", also

    (b -> e -> f) -> b -> [c] -> b

Das zweite Argument an "f" ist "x", vom Typ "c", also

    (b -> c -> f) -> b -> [c] -> b

Und das Ergebnis von "f" wird als zweites Argument an "foldl" rekursiv
übergeben, also müssen "f" und "b" gleich sein:

    (b -> c -> b) -> b -> [c] -> b

Kanonisch:

    (a -> b -> a) -> a -> [b] -> a

Schauen wir mal:

    $ ghci
    Prelude> :t foldl
    foldl :: (a -> b -> a) -> a -> [b] -> a

Für "foldr" findet man

    (a -> b -> b) -> b -> [a] -> b

auf ähnliche Weise.

Nun zu "not . null". Zuerst schauen wir uns die Basistypen an.

    not :: Bool -> Bool
    null :: [d] -> Bool
    (.) :: (b -> c) -> (a -> b) -> a -> c

(Es ist immer eine gute Idee, die Typvariablen umzubenennen, damit keine
Clashes auftauchen.)

"(.)" nimmt also offenbar zwei Funktionen als Argumente. Jetzt müssen wir nur
noch einsetzen:

    b -> c  = Bool -> Bool
    a -> b  = [d]  -> Bool

Daraus folgt direkt:

    b = Bool
    c = Bool
    a = [d]

Der Rückgabetyp von "(.)" ist "a -> c". Einsetzen:

    [d] -> Bool

Kanonisch:

    [a] -> Bool


"ffoldl = foldl . foldl" ist spannender. Das erste Vorkommen von "foldl" hat
den Typ

    (a -> b -> a) -> a -> [b] -> a

und das zweite den Typ

    (c -> d -> c) -> c -> [d] -> c

Der Operator "." hat den Typ

    (f -> g) -> (e -> f) -> e -> g

Beide Argumente an "." sind "foldl":

    f -> g  =  (a -> b -> a) -> a -> [b] -> a
    e -> f  =  (c -> d -> c) -> c -> [d] -> c

und "ffoldl" hat den Typ "e -> g".

Aus den zwei Gleichungen oben folgt

    f  =  a -> b -> a
    g  =  a -> [b] -> a
    e  =  c -> d -> c
    f  =  c -> [d] -> c

Die beiden "f = ..." Gleichungen erzwingen "a = c" und "b = [d]":

    e  =  c -> d -> c
    f  =  c -> [d] -> c
    g  =  c -> [[d]] -> c

Der Typ "e -> g" von "foldl . foldl" ist also

    (c -> d -> c) -> c -> [[d]] -> c

Kanonisch:

    (a -> b -> a) -> a -> [[b]] -> a

Auf ähnliche Weise kann man den Typ "(c -> d) -> (a -> b -> c) -> a -> b -> d"
für "(.).(.)" herleiten.

2. "ffoldl" nimmt also eine binäre Funktion "a -> b -> a" und liftet sie auf
Listen von Listen von "b"s. Diese Funktion ist nützlich, wenn man eine Liste
von Listen hat und sie als flache Liste behandeln will; z.B.

    ffoldl (+) 0 [[1, 3], [10]] == 14

In diesem Fall koennte man auch

    foldl (+) 0 (concat [[1, 3], [10]])

schreiben, aber "ffoldl" baut keine neuen Listen und ist deshalb effizienter.

"oo" komponiert eine zweisteillige Funktion "g" mit einer einstelligen "f". Die
expandierte Form ist

    oo f g x y = f (g x y)

Beispiel:

    absSum = abs `oo` (+)
    absSum 5 (-100) == 95
-}


{- G3 -}

{-
Lemma: sum . filter (/= 0) = sum

Beweis durch Extensionalität

Lemma': (sum . filter (/= 0)) xs = sum xs

Beweis durch Induktion über xs

Basisfall:
  z.z. (sum . filter (/= 0)) [] = sum []

  (sum . filter (/= 0)) []
  = sum (filter (/= 0) [])
  = sum []

Induktionsfall:
  IH:  (sum . filter (/= 0)) xs = sum xs
  z.z. (sum . filter (/= 0)) (x:xs) = sum (x:xs)

  vereinfachte Induktionshypothese:
    sum (filter (/= 0) xs) = sum xs

  vollständige Fallunterscheidung über x == 0

  1) True

  (sum . filter (/= 0)) (x:xs)
  = sum (filter (/= 0) (x:xs))                                          (by compose_def)
  = sum (if x /= 0 then x : filter (/= 0) xs else filter (/= 0) xs)     (by filter_Cons)
  = sum (if False then x : filter (/= 0) xs else filter (/= 0) xs)      (Fallunterscheidung/Arithmetik)
  = sum (filter (/= 0) xs)
  = sum xs                                                              (IH)

  sum (x:xs)
  = x + sum xs                                                          (sum_Cons)
  = 0 + sum xs                                                          (Fallunterscheidung)
  = sum xs                                                              (Arithmetik)

  2) False

  (sum . filter (/= 0)) (x:xs)
  = sum (filter (/= 0) (x:xs))                                          (by compose_def)
  = sum (if x /= 0 then x : filter (/= 0) xs else filter (/= 0) xs)     (by filter_Cons)
  = sum (if True then x : filter (/= 0) xs else filter (/= 0) xs)       (Fallunterscheidung/Arithmetik)
  = sum (x : filter (/= 0) xs)
  = x + sum (filter (/= 0) xs)                                          (by sum_Cons)
  = x + sum xs                                                          (IH)

  sum (x:xs)
  = x + sum xs                                                          (by sum_Cons)

-}

{- G4 -}

partition_fold :: (a -> Bool) -> [a] -> ([a], [a])
partition_fold p =
  foldr (\x (ts, fs) -> if p x then (x : ts, fs) else (ts, x : fs)) ([], [])


{- H1 -}

wellformed :: IList -> Bool
wellformed [] = True
wellformed [(m,n)] = m <= n
wellformed ((m1,n1):(m2,n2):ms) =
    m1 <= n1 && n1 < m2 && wellformed ((m2,n2):ms)

empty :: IList
empty = []

member :: Rational -> IList -> Bool
member n = any (\(k,l) -> k <= n && n <= l)

insert :: (Rational, Rational) -> IList -> IList
insert ivl [] = [ivl]
insert (l,h) ((l',h') : ivls)
    | h < l' = (l,h) : (l',h') : ivls
    | h' < l = (l',h') : insert (l,h) ivls
    | otherwise = insert (min l l', max h h') ivls

wellformedIvl :: (Rational, Rational) -> Bool
wellformedIvl (l,h) = l <= h

{-
 - Wenn man QuickCheck ohne weitere Vorbereitungen aufruft, wird es nur in
 - Ausnahmefällen eine wohlgeformte Intervallliste erzeugen. Um dennoch
 - erfolgreich zu testen, haben wir einen sogenannten "Generator" für
 - Intervalllisten geschrieben. Damit wird QuickCheck vorgegeben, wie Werte
 - generiert werden sollen.
 -
 - Sie können die Tests so schreiben wie immer. Wenn Sie die Tests ausprobieren
 - wollen, rufen Sie QuickCheck wie folgt auf:
 -
 - Angenommen, prop ist eine Property, die als erstes Argument eine
 - Intervallliste bekommt. Dann schreiben Sie:
 -
 -      quickCheck (forAll ilistGen prop)
 -}

prop_insert_wellformed ivl ivls =
    wellformedIvl ivl ==> wellformed ivls ==> wellformed (insert ivl ivls)
{- Testen mit: quickCheck (\ivl -> forAll ilistGen (prop ivl)) -}

prop_member_empty r = not $ member r empty

prop_member_insert (l,h) ivls =
    wellformedIvl (l,h) ==> wellformed ivls ==>
    l `member` ivls' && h `member` ivls' && ((l + h) / 2) `member` ivls'
    where ivls' = insert (l,h) ivls
{- Testen mit: quickCheck (\ivl -> forAll ilistGen (prop ivl)) -}


{- H2 -}

foldlMap :: (a -> c -> (b, c)) -> [a] -> c -> ([b], c)
foldlMap _ [] c = ([], c)
foldlMap f (a : as) c =
  (b : bs, c'')
  where (b, c') = f a c
        (bs, c'') = foldlMap f as c'

fresh :: String -> [String] -> (String, [String])
fresh s names | elem s names = fresh (s ++ "_") names
fresh s names = (s, s : names)

freshes = foldlMap fresh

{- Uebrigens kann man "map" und "foldl" mit "foldlMap" implementieren. -}
mymap :: (a -> b) -> [a] -> [b]
mymap f as = fst (foldlMap (\a _ -> (f a, ())) as ())

myfoldl :: (c -> a -> c) -> c -> [a] -> c
myfoldl f c as = snd (foldlMap (\c a -> ((), f a c)) as c)


{- H3 -}

{-WETT-}
foldlMap4 = foldlMap . foldlMap . foldlMap . foldlMap
foldlMap16 = foldlMap4 . foldlMap4 . foldlMap4 . foldlMap4
foldlMap48 = foldlMap16 . foldlMap16 . foldlMap16
foldlMap144 = foldlMap48 . foldlMap48 . foldlMap48

index1 xs j = (enumFromTo j $ pred j', j') where j' = j + length xs
index432 = foldlMap144 $ foldlMap144 $ foldlMap144 index1
{-TTEW-}