module Sol_Exercise_9 where
import qualified Data.HashSet as HS
import Data.List as List
import Data.Maybe as Maybe
import Data.Ord as Ord
import Data.Function as Fun
import Control.Monad
import Test.QuickCheck

{- Library -- nicht veraendern -}

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
-- just ignore this
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 balanced trees
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))
    ]

-- examples for unbalanced trees
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)))
    ]


{- G9.1 -}

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

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

Induction step:
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))              (by mirror_Node)
== Node x (mirror (mirror l)) (mirror (mirror r))     (by mirror_Node)
== Node x l (mirror (mirror r))                       (by IH1)
== Node x l r                                         (by IH2)

QED
-}

{- G9.2 -}

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


{- G9.3 -}

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

move :: Coords -> Shape -> Shape
move (x,y) (Line (z1,w1) (z2,w2)) = Line (z1+x,w1+y) (z2+x,w2+y)
move (x,y) (Circle (z,w) s) = Circle (x+z,y+w) s

polygon :: [Shape] -> Bool
polygon (Line c1 c2 : xs) = polygon' c1 c2 xs
  where
    polygon' c1 c2 [] = c1 == c2
    polygon' c1 c2 (Line c3 c4 : xs) = c2 == c3 && polygon' c1 c4 xs
    polygon' _ _ _ = False
polygon _ = False


{- H9.1 -}

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

Base case:
To show: flat (mirror Empty) = reverse (flat Empty)
flat (mirror Empty)
== flat Empty             (by mirror_Empty)
== []                     (by flat_Empty)
reverse (flat Empty)
== reverse []             (by flat_Empty)
== []                     (by reverse_Nil)

Induction step:
IH1: flat (mirror l) = reverse (flat l)
IH2: flat (mirror r) = reverse (flat r)
To show: flat (mirror (Node x l r)) = reverse (flat (Node x l r))
flat (mirror (Node x l r))
== flat (Node x (mirror r) (mirror l))                    (by mirror_Node)
== flat (mirror r) ++ [x] ++ flat (mirror l)              (by flat_Node)
== flat (mirror r) ++ [x] ++ reverse (flat l)             (by IH1)
== reverse (flat r) ++ [x] ++ reverse (flat l)            (by IH2)
reverse (flat (Node x l r))
== reverse (flat l ++ [x] ++ flat r)                      (by flat_Node)
== reverse ([x] ++ flat r) ++ reverse (flat l)            (by reverse_append)
== (reverse (flat r) ++ reverse [x]) ++ reverse (flat l)  (by reverse_append)
== reverse (flat r) ++ reverse [x] ++ reverse (flat l)    (by append_assoc)
== reverse (flat r) ++ ([] ++ [x]) ++ reverse (flat l)    (by reverse_Cons)
== reverse (flat r) ++ [x] ++ reverse (flat l)            (by append_Nil)

QED
-}

{- H9.2 -}

-- Ein fold ist eine Funktion für eine allgemeine strukturelle Rekursionsfunktion,
-- die immer nach dem gleichen Schema aufgebaut ist. Für einen Typ (in unserem Fall "Tree a")
-- mit n Konstruktoren hat die Funktion n+1 Parameter. Eines für jeden Konstruktor
-- und eines für die Eingabe.
--
-- Der Typ der Parameter ergibt sich, wenn man überall "Tree a" durch b ersetzt:
--
-- Empty :: Tree a                          -->  empty :: b
-- Node :: a -> Tree a -> Tree a -> Tree a  -->  node :: a -> b -> b -> b
--
-- Dann wird einfach jeder Konstruktor durch den dazugehörigen Parameter ersetzt,
-- also in unserer Lösung Node durch node und Empty durch empty. Wenn die Konstruktoren
-- Parameter vom Typ "Tree a" haben, wird dieser durch einen rekursiven Aufruf ersetzt:
foldTree :: (a -> b -> b -> b) -> b -> Tree a -> b
foldTree node empty Empty = empty
foldTree node empty (Node x l r) = node x (foldTree node empty l) (foldTree node empty r)

inord x l r = l ++ [x] ++ r
preord x l r = [x] ++ l ++ r
postord x l r = l ++ r ++ [x]

inorder :: Tree a -> [a]
inorder = foldTree inord []

preorder :: Tree a -> [a]
preorder = foldTree preord []

postorder :: Tree a -> [a]
postorder = foldTree postord []


{- H9.3 -}

data SkeleTree = SEmpty | SNode SkeleTree SkeleTree
  deriving (Show, Eq)
-- alternative: type SkeleTree = Tree ()

splitNum :: Int -> (Int,Int)
splitNum n = (n - n `div` 2, n `div` 2)

makeBalanced :: Int -> SkeleTree
makeBalanced n
    | n <= 0 = SEmpty
    | otherwise = SNode (makeBalanced l) (makeBalanced r)
  where (l,r) = splitNum (n - 1)

skelBalanced :: SkeleTree -> Bool
skelBalanced t = depth min t + 1 >= depth max t
  where
    depth _ SEmpty = 0
    depth f (SNode l r) = 1 + f (depth f l) (depth f r)

skelSize :: SkeleTree -> Int
skelSize SEmpty = 0
skelSize (SNode l r) = 1 + skelSize l + skelSize r

prop_balanced (Positive n) = skelBalanced (makeBalanced n)
prop_size (Positive n) = skelSize (makeBalanced n) == n

-- very simple and inefficient variant: Generate all trees with n inner nodes,
-- delete the ones which are not balanced.
--
-- To make this a more efficient, think about the minimal and maximal sizes
-- of the left and right subgraphs.
makeAllBalanced :: Int -> [SkeleTree]
makeAllBalanced = filter skelBalanced . makeAll
  where
    makeAll 0 = [SEmpty]
    makeAll n = let prevTrees = map makeAll [0..n-1] in
      concat $ zipWith (\xs ys -> [SNode x y | x <- xs, y <- ys]) prevTrees (reverse prevTrees)

--makeAllBalanced' :: Int -> [SkeleTree]
--makeAllBalanced' = filter skelBalanced . makeAll
--  where
--    makeAll 0 = [SEmpty]
--    makeAll n = let prevTrees = map makeAll [0..maxSize n - 1] in
--      concat $ zipWith (\xs ys -> [SNode x y | x <- xs, y <- ys]) prevTrees (reverse prevTrees)
--    maxSize n = ceiling $ log $ fromIntegral $ n + 1



{- H9.4 -}

find23 :: Ord a => a -> Tree23 a -> Bool
find23 x (Leaf y) = x == y
find23 x (Branch2 t1 y t2)
  | x < y = find23 x t1
  | otherwise = find23 x t2
find23 x (Branch3 t1 y1 t2 y2 t3)
  | x < y1 = find23 x t1
  | x < y2 = find23 x t2
  | otherwise = find23 x t3


{- W9.1 -}

{-WETT-}
setOneInClause :: Int -> [Int] -> Maybe [Int]
setOneInClause l ls =
  if elem l ls then Nothing else Just (List.filter (/= - l) ls)

setOneInProblem :: Int -> [[Int]] -> [[Int]]
setOneInProblem = mapMaybe . setOneInClause

killPure :: [[Int]] -> ([Int], [[Int]])
killPure cs = (pures, List.foldl (flip setOneInProblem) cs pures)
  where
    insertIf p h l = if p l then HS.insert l h else h
    hashSetOf p = List.foldl (List.foldl (insertIf p)) HS.empty cs
    pos = hashSetOf (> 0)
    neg = HS.map negate (hashSetOf (< 0))
    pos' = HS.toList (pos `HS.difference` neg)
    neg' = List.map negate (HS.toList (neg `HS.difference` pos))
    pures = pos' ++ neg'

satisfySortedCnf :: [[Int]] -> Maybe [Int]
satisfySortedCnf [] = Just []
satisfySortedCnf ([] : _) = Nothing
satisfySortedCnf ((l : ls) : cs) =
  case satisfyUnsortedCnf (setOneInProblem l cs) of
    Just sol -> Just (l : sol)
    Nothing ->
      case satisfyUnsortedCnf (setOneInProblem (- l) (ls : cs)) of
        Just sol -> Just (- l : sol)
        Nothing -> Nothing

satisfyUnsortedCnf :: [[Int]] -> Maybe [Int]
satisfyUnsortedCnf = satisfySortedCnf . sortBy (Ord.comparing length)

fixpoint :: (a -> a -> Bool) -> (a -> a) -> a -> a
fixpoint eq f x = if eq x (f x) then x else fixpoint eq f (f x)

tryHorn :: [[Int]] -> Maybe [Int]
tryHorn cs =
  if length pns == length cs
  then collect $ fixpoint (==) horn (Just [], sort pns)
  else Nothing
  where
    pns = sort $ mapMaybe (\c -> let (ps, ns) = List.partition (>0) c
              in case ps of
                   [] -> Just (Nothing, List.sort $ List.map abs $ nub ns)
                   [x] -> Just (Just x, List.sort $ List.map abs $ nub ns)
                   _ -> Nothing) cs
    sort = sortBy (Ord.comparing (length . snd))
    horn (Nothing, pns) = (Nothing, pns)
    horn (Just sol, pns) = case List.find (any (`elem` sol) . snd) pns of
      Just (Nothing, _) -> (Nothing, pns)
      Just (c@(Just p, ns)) -> (Just (p : sol), deleteBy (\x y -> fst x == fst y) c pns)
      Nothing -> if [] `elem` map snd pns then (Nothing, pns) else (Just sol, pns)
    collect (Nothing, _) = Nothing
    collect (Just sol, pns) =
      Just (nub (sol ++ List.concatMap (List.map negate . snd) pns))

satisfyCnf :: [[Int]] -> Maybe [Int]
satisfyCnf cs =
  case tryHorn cs' of
    Just sol -> Just (pures ++ sol)
    Nothing ->
      case satisfyUnsortedCnf cs' of
        Just sol -> Just (pures ++ sol)
        Nothing -> Nothing
  where (pures, cs') = killPure cs
{-TTEW-}