module Exercise_6 where
import Data.Char
import Test.QuickCheck

{- Library DO NOT CHANGE -}
type PairList = [(Int,Int)]
{- End Library -}


{---------------------------------------------------------------------}
{- Aufgabe G6.1 -}

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)



{---------------------------------------------------------------------}
{- Aufgabe G6.2 -}

foldl' :: (a -> b -> a) -> a -> [b] -> a
foldl' f z [] = z
foldl' f z ( x : xs ) = foldl' f ( f z x ) xs

foldr' :: (c -> b -> b) -> b -> [c] -> b
foldr' f z [] = z
foldr' f z ( x : xs ) = f x ( foldr' f z xs )


ffoldl = foldl' . foldl'
{-
foldl' :: (a -> b -> a) -> a -> [b] -> a

f :: (a -> b -> a)

inner :: a -> [b] -> a

z :: a

xs :: [[b]]

ffoldl' :: (a -> b -> a) -> a -> [[b]] -> a
-}
ffoldl' :: (a -> b -> a) -> a -> [[b]] -> a
ffoldl' f z xs = outer inner z xs
        where
        inner = (foldl' f)
        outer = foldl'


oo = (.).(.)
oo' w = (.) ((.) w)
oo'' w x = (.) ((.) w) x
oo''' w x = ((.) w) . x
oo'''' w x y = (.) w (x y)
oo''''' w x y = w . (x y)

oo'''''' :: (c -> d) -> (a -> b -> c) -> a -> b -> d
oo'''''' f g u v = f (g u v)




{---------------------------------------------------------------------}
{- Aufgabe G6.3 -}

-- First vs. second parameter
a1 = (div 5)
a2 = (`div` 5)

-- First vs. second parameter
b1 = (+7)
b2 = (7+)

c1 = map (:[]) -- [[x] | x <- xs]
c2 = map ([]:) -- Prepend [] to every list element

o f g x = f (g x)
flip' f x y = f y x
-- Both ids, d2 is more general
d1 = flip . flip
d2 = id

e1 x y z = [x, y, z] -- z element
e2 x y z = x : y : z -- z list



{---------------------------------------------------------------------}
{- Aufgabe G6.4 -}

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

-}



{---------------------------------------------------------------------}
{- Aufgabe G6.5 -}

f1 xs = map (+ 1) xs
f1' = map (+1)

f2 xs = map (2 *) (map (+ 1) xs)
f2' = map (\z -> 2*(z+1))
f2'' = map ((*2) . (+1))
f2''' = map (*2) . map(+1)

f3 xs = f (g xs)
        where
        g = map (+ 1)
        f = filter (> 1)

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

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

f5 f g x y = f ((g x) y)
f5' f g x = f . (g x)
--
f5'' = (.).(.)

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

f7 f g h x = g (h (f x))
f7' f g h x = g . (h (f x))
f7'' f g h = g . h . f
--
f7''' = flip ((.).(.)) . flip (.)


{---------------------------------------------------------------------}
{- Aufgabe H6.1 -}

wellformed :: PairList -> Bool
wellformed = undefined


empty :: PairList
empty = undefined


member :: Int -> PairList -> Bool
member = undefined


insert :: Int -> PairList -> PairList
insert = undefined


union :: PairList -> PairList -> PairList
union = undefined


delete :: Int -> PairList -> PairList
delete = undefined



{---------------------------------------------------------------------}
{- Aufgabe H6.2 -}

{-WETT-}
anonymize :: String -> String
anonymize = undefined
{-TTEW-}