module Sol_Exercise_6 where
import Data.Char
import Test.QuickCheck

{- Library -- nicht verändern -}

type PairList = [(Int,Int)]

{- G1 -}

instance Num b => Num (a -> b) where
    f + g = \x -> f x + g x
    f - g = \x -> f x - g x
    f * g = \x -> f x * g x
    negate f = \x -> negate (f x)
    abs f = \x -> abs (f x)
    signum f = \x -> signum (f x)
    fromInteger x = const (fromInteger x)

{- G2 -}

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

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

    a -> b -> c -> b

Und das dritte Argument ist eine Liste, wegen dem Mustervergleich:

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

Die zweite Gleichung gibt zwei arguemente 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 zweiten Argument an "foldl" rekursiv gegeben,
also "f" und "b" muessen gleich sein:

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

Kanonisch:

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

Lass uns gucken:

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

Fuer "foldr" findet man

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

auf aehnliche Weise.

"ffoldl = foldl . foldl" ist spannender. Der erste "foldl" hat den Typ

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

und der zweite den Typ

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

(Es ist immer eine gute Idee, die Typvariablen umzubenennen, damit keine
Clashes auftauchen.) 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 binare Funktion "a -> b -> a" und liftet sie auf
Listen von Listen von "b"s. Diese Funktion ist nuetzlich, 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 -}

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


{- G4 -}

{-
Lemma reverse = foldl (\xs x -> x : xs) []
Proof by extensionality
To show:
  *: reverse xs = foldl (\xs x -> x : xs) [] xs                       for all xs
Too specialized for an induction!

Generalization
To show:
  GEN: reverse xs ++ ys = foldl (\xs x -> x : xs) ys xs           for all xs, ys
Proof by structural induction on xs

Base case:
To show: reverse [] ++ ys = foldl (\xs x -> x : xs) ys []             for all ys
reverse [] ++ ys
== [] ++ ys                             (by reverse_Nil)
== ys                                   (by append_Nil)
foldl (\xs x -> x : xs) ys []
== ys                                   (by foldl_Nil)

Induction step:
IH: reverse zs ++ ys = foldl (\xs x -> x : xs) ys zs                  for all ys
To show: reverse (z : zs) ++ ys = foldl (\xs x -> x : xs) ys (z : zs) for all ys
reverse (z : zs) ++ ys
== (reverse zs ++ [z]) ++ ys            (by reverse_Cons)
== reverse zs ++ ([z] ++ ys)            (by append_assoc)
== reverse zs ++ z : ([] ++ ys)         (by append_Cons)
== reverse zs ++ z : ys                 (by append_Nil)
== foldl (\xs x -> x : xs) (z : ys) zs  (by IH with z : ys instead of ys)
foldl (\xs x -> x : xs) ys (z : zs)
== foldl (\xs x -> x : xs) ((\xs x -> x : xs) ys z) zs (by foldl_Cons)
== foldl (\xs x -> x : xs) ((\x -> x : ys) z) zs       (by eval of lambda)
== foldl (\xs x -> x : xs) (z : ys) zs                 (by eval of lambda)

QED for GEN

To prove * we instantiate GEN with [] for ys and apply append_Nil2.

QED

-}

{- G5 -}

f1 xs = map (\x -> x + 1) xs
f2 xs = map (\x -> 2 * x) (map (\x -> x + 1) xs)
f3 xs = filter (\x -> x > 1) (map (\x -> x + 1) xs)
f4 f g x = f (g x)
f5 f g x y = f (g x y)
f6 f g x y z = f (g x y z)
f7 f g h x = g (h (f x))

f1' = map (+1)

f2' = map (2*) . map (+1)
f2'' = map ((2*) . (+1))

f3' = filter (>1) . map (+1)

f4' f g = f . g
f4'' f = (.) f
f4''' = (.)

f5' f g x = f . g x
f5'' f g = ((.).(.)) f g
f5''' f = ((.).(.)) f
f5'''' = (.).(.)  -- vgl. "oo"

f6' f g x y = f . g x y
f6'' f g x = ((.).(.)) f . g
f6''' f g = ((.).(.).(.)) f g
f6'''' f = ((.).(.).(.)) f
f6''''' = (.).(.).(.)


f7' f g h = g . h . f
-- So weit, so gut. Vernünftigerweise hört man hier wohl auf. Das heißt aber
-- nicht, dass man das nicht noch weiter treiben kann ...
f7_2 f g h = (.) (g . h) f
f7_3 f g h = flip (.) f (g . h)
f7_4 f g h = flip (.) f ((.) g h)
f7_5 f = flip (.) f `oo` (.)
  where oo = (.).(.)
f7_6 f = ((.).(.)) (flip (.) f) (.)
f7_7 f = flip ((.).(.)) (.) (flip (.) f)
f7_8 = flip ((.).(.)) (.) . flip (.)
-- Jetzt haben wir alle Parameter eliminiert. Ein solcher Ausdruck
-- heißt 'point-free' (da keine expliziten "Punkte" (== Werte) mehr
-- vorkommen). Solche extremen Anwendungen werden in der Haskell-Welt
-- auch gerne mal als 'pointless' bezeichnet ...
--
-- Wer noch nicht genug hat, darf jetzt überlegen, warum wir die
-- Definition noch zu Folgendem vereinfachen dürfen:
f7_9 = flip ((.).(.)) . flip (.)

-- f7_9 f g h x
-- = (flip oo . flip (.)) f g h x
-- = (flip oo (flip (.) f)) g h x
-- = flip oo (. f) g h x
-- = (\y -> oo y (. f)) g h x
-- = oo g (. f) h x
-- = (\a b c d -> a (b c d)) g (. f) h x
-- = g ((. f) h x)
-- = g ((h . f) x)
-- = g (h (f x))

-- f7_8 f g h x
-- = (flip oo (.) . flip (.)) f g h x
-- = flip oo (.) (flip (.) f) g h x
-- = flip oo (.) (. f) g h x
-- = (\y z -> oo z y) (.) (. f) g h x
-- = oo (. f) (.) g h x
-- = (\a b c d -> a (b c d)) (. f) (.) g h x
-- = (. f) ((.)g h) x
-- = (. f) (g . h) x
-- = (g . h . f) x
-- = g (h (f x))




{- H1 -}


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

empty :: PairList
empty = []

member :: Int -> PairList -> Bool
member n [] = False
member n ((k,l):ks) = (k <= n && n <= l) || member n ks

insert :: Int -> PairList -> PairList
insert n [] = [(n,n)]
insert n ((k1,l1) : (k2,l2) : ks)
    | l1 + 1 == n && n + 1 == k2 = (k1,l2) : ks
insert n ((k,l) : ks)
    | n + 1 == k = (n,l) : ks
    | n < k = (n,n) : (k,l) : ks
    | k <= n && n <= l = (k,l) : ks
    | l + 1 == n = (k,n) : ks
    | otherwise = (k,l) : insert n ks

union :: PairList -> PairList -> PairList
union [] ls = ls
union ks [] = ks
union ((k1,l1):ks) ((k2,l2):ls) =
    if k1 <= k2
    then if l1 + 1 < k2 then (k1,l1) : union ks ((k2, l2):ls)
         else if l1 <= l2 then union ks ((k1,l2):ls)
         else {- l1 > l2 -} union ((k1,l1):ks) ls
    else if k1 <= l2 + 1
    then if l1 <= l2 then union ks ((k2,l2):ls)
         else {- l1 > l2 -} union ((k2,l1):ks) ls
    else (k2,l2) : union ((k1,l1):ks) ls

delete :: Int -> PairList -> PairList
delete n [] = []
delete n ((k,l) : ks)
    | n < k = (k,l) : ks
    | n == k = if k < l then (k+1,l) : ks else ks
    | k < n && n < l = (k,n-1) : (n+1,l) : ks
    | n == l = if k < l then (k,l-1) : ks else ks
    | otherwise = (k,l) : delete n ks


{- H2 -}

{-WETT-}
anonymize :: String -> String
anonymize = modify isEmailChar email
 where
  isEmailChar c = isAlphaNum c || c == '_' || c == '.' || c == '@'

email :: String -> String
email s | number (=='@') s == 1 = anon s
        | otherwise             = s

anon :: String -> String
anon = modify isPartChar underscores
 where
  isPartChar c = isAlphaNum c || c == '_' 

underscores :: String -> String  
underscores s = take 1 s ++ replicate (length s - 1) '_'

number :: (a -> Bool) -> [a] -> Int
number p = length . filter p

modify :: (a -> Bool) -> ([a] -> [a]) -> [a] -> [a]
modify p f [] = []
modify p f xs
  | null part = head xs' : modify p f (tail xs')
  | otherwise = f part ++ modify p f xs'
 where
  (part, xs') = splitWhile p xs

splitWhile :: (a -> Bool) -> [a] -> ([a],[a])
splitWhile p xs = (takeWhile p xs, dropWhile p xs)
{-TTEW-}