module Exercise_9 where
import Test.QuickCheck
import Control.Monad

{- Library DO NOT CHANGE -}
data Tree a = Empty | Node a (Tree a) (Tree a)
  deriving (Eq, Show)

data Tree23 a = Leaf a
              | Branch2 (Tree23 a) a (Tree23 a)
              | Branch3 (Tree23 a) a (Tree23 a) a (Tree23 a)
  deriving Show

mirror :: Tree a -> Tree a
mirror Empty = Empty
mirror (Node x l r) = Node x (mirror r) (mirror l)

flat :: Tree a -> [a]
flat Empty = []
flat (Node x l r) = flat l ++ [x] ++ flat r

-- allow QuickCheck to generate arbitrary values of type Tree
instance Arbitrary a => Arbitrary (Tree a) where
  arbitrary = sized tree
    where
    tree 0 = return Empty
    tree n | n > 0 = oneof [return Empty,
      liftM3 Node arbitrary (tree (n `div` 2)) (tree (n `div` 2))]
  shrink Empty = []
  shrink (Node x l r) = l : r : map (\l' -> Node x l' r) (shrink l)
        ++ map (\r' -> Node x l r') (shrink r)

-- examples for G9.2
balancedTrees =
    [ Empty
    , Node 0 Empty Empty
    , Node 0 (Node 1 Empty Empty) Empty
    , Node 4 (Node 2 Empty (Node 5 Empty Empty)) (Node 0 Empty Empty)
    , Node 1 (Node 0 Empty (Node 3 Empty Empty))
             (Node 0 Empty (Node 3 Empty Empty))
    ]

unbalancedTrees =
    [ Node 3 (Node 2 Empty (Node 1 Empty Empty)) Empty
    , Node 4 (Node 3 (Node 2 (Node 1 Empty Empty) Empty) Empty)
             (Node 3 Empty (Node 2 Empty (Node 1 Empty Empty)))
    , Node 9 (Node 8 (Node 7 Empty Empty ) Empty)
             (Node 1 (Node 0 Empty (Node 3 Empty Empty))
                     (Node 0 Empty (Node 3 Empty Empty)))
    ]
{- End Library -}


{---------------------------------------------------------------------}
{- Aufgabe G9.1 -}

{-
Lemma(t): mirror (mirror t) = t
Proof by structural induction on t

Base case: Lemma(Empty)
To show: mirror (mirror Empty) = Empty
mirror (mirror Empty)
= mirror Empty                          mirror_Empty
= Empty                                 mirror_Empty

Induction step: Lemma(l), Lemma(r) => Lemma((Node x l r))
IH1: mirror (mirror l) = l
IH2: mirror (mirror r) = r
To show: mirror (mirror (Node x l r)) = Node x l r
mirror (mirror (Node x l r))
= mirror (Node x (mirror r) (mirror l))                 mirror_Node
= Node x (mirror (mirror l)) (mirror (mirror r))        mirror_Node
= Node x l (mirror (mirror r))                          IH1
= Node x l r                                            IH2

QED!
-}



{---------------------------------------------------------------------}
{- Aufgabe G9.2 -}

balanced :: Tree a -> Bool
balanced t = dist max t - dist min t <= 1
        where
        dist f (Node _ l r) = 1 + f (dist f l) (dist f r)
        dist _ Empty = 0



{---------------------------------------------------------------------}
{- Aufgabe G9.3 -}

type Coords = (Int, Int)
data Shape =
        Line Coords Coords
        | Circle Coords Int


move :: Coords -> Shape -> Shape
move (x,y) (Line (a,b) (c,d)) = Line (a+x, b+y) (c+x, d+y)
move (x,y) (Circle (a,b) r)   = Circle (a+x, b+y) r


polygon :: [Shape] -> Bool
polygon ((Line from to) : ss) = polygon' from to ss
        where
        polygon' f t [] = f == t
        polygon' f t ((Line lf lt) : ss) = t == lf && polygon' f lt ss
        polygon' _ _ _ = False
polygon _ = False



{---------------------------------------------------------------------}
{- Aufgabe H9.1 -}

{- 
Proof me!
-}



{---------------------------------------------------------------------}
{- Aufgabe H9.2 -}

inorder :: Tree a -> [a]
inorder = undefined

preorder :: Tree a -> [a]
preorder = undefined

postorder :: Tree a -> [a]
postorder = undefined



{---------------------------------------------------------------------}
{- Aufgabe H9.3 -}

-- makeBalanced :: Int -> SkeleTree
-- makeBalanced = undefined
--
-- makeAllBalanced :: Int -> SkeleTree
-- makeAllBalanced = undefined



{---------------------------------------------------------------------}
{- Aufgabe H9.4 -}

find23 :: Ord a => a -> Tree23 a -> Bool
find23 = undefined