module Sol_Exercise_9 where
import Form_9
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)

-- 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))]
  -- XXX Add shrink instance next year!


{- G1 -}

-- siehe ExtForm.hs


{- G2 -}

data Arith = Add Arith Arith | Mul Arith Arith | Const Integer | IVar String

evalA :: [(String,Integer)] -> Arith -> Integer
evalA val (Add x y) = evalA val x + evalA val y
evalA val (Mul x y) = evalA val x * evalA val y
evalA _ (Const x) = x
evalA val (IVar s) = get (lookup s val)
    where get (Just x) = x
          get Nothing = 0


{- G4 -}

mkTable :: Form -> [[String]]
mkTable phi = firstRow : secondRow : map (zipWith align lengths . mkRow) (vals $ vars phi)
  where
    firstRow = vars phi ++ ["|", show phi]
    secondRow = map (map (const '-')) firstRow
    lengths = map length firstRow

    mkRow val = map (stringOfBool . snd) val ++ ["|", stringOfBool $ eval val phi]

    stringOfBool True = "T"
    stringOfBool False = "F"

    align n xs = lpad ++ xs ++ rpad
      where
      (lpad, rpad) = splitAt ((n - length xs) `div` 2) (replicate (n - length xs) ' ')

showTable :: Form -> String
showTable = unlines . map unwords . mkTable

printTable :: Form -> IO ()
printTable = putStrLn . showTable


{- H9.1 -}

{-

Lemma: inorder t = reverse (niorder t)

Proof by structural induction over t.

Case t = Empty (base case):

    To show: inorder Empty = reverse (niorder Empty).

    inorder Empty
    = []                                                  -- by def. inorder

    reverse (niorder Empty)
    = reverse []                                          -- by def. niorder
    = []                                                  -- by def. reverse

Case t = Node a l r (induction step):

    IH1: inorder l = reverse (niorder l)
    IH2: inorder r = reverse (niorder r)

    To show: inorder (Node a l r) = reverse (niorder (Node a l r))

    inorder (Node a l r)
    = inorder l ++ [a] ++ inorder r                       -- by def. inorder
    = reverse (niorder l) ++ [a] ++ inorder r             -- by IH1
    = reverse (niorder l) ++ [a] ++ reverse (niorder r)   -- by IH2

    reverse (niorder (Node a l r))
    = reverse (niorder r ++ [a] ++ niorder l)             -- by def. niorder
    = reverse ([a] ++ niorder l) ++ reverse (niorder r)   -- by reverse_append
    = (reverse (niorder l) ++ [a]) ++ reverse (niorder r) -- by reverse_append
    = reverse (niorder l) ++ [a] ++ reverse (niorder r)   -- by append_assoc

QED

Lemma: inorder = reverse . niorder

Proof by extensionality.

To show: inorder t = (reverse . niorder) t

    inorder xs
    = reverse (niorder t)                                 -- by previous lemma
    = (reverse . niorder) t

-}

{- H9.2 -}

isAtom :: Form -> Bool
isAtom F = True
isAtom T = True
isAtom (Var _) = True
isAtom _ = False

isLiteral :: Form -> Bool
isLiteral (Not f) = isAtom f
isLiteral f = isAtom f

isCoclause :: Form -> Bool
isCoclause (f :&: g) = isCoclause f && isLiteral g
isCoclause f = isLiteral f

isDnf :: Form -> Bool
isDnf (f :|: g) = isDnf f && isCoclause g
isDnf f = isCoclause f

pushNot :: Form -> Form
pushNot (Not (Not f)) = pushNot f
pushNot (Not (f :&: g)) = pushNot (Not f :|: Not g)
pushNot (Not (f :|: g)) = pushNot (Not f :&: Not g)
pushNot (f :&: g) = pushNot f :&: pushNot g
pushNot (f :|: g) = pushNot f :|: pushNot g
pushNot f = f

pushAnd :: Form -> Form
pushAnd (f :&: (g :|: h)) = pushAnd ((f :&: g) :|: (f :&: h))
pushAnd ((f :|: g) :&: h) = pushAnd ((f :&: h) :|: (g :&: h))
pushAnd (f :|: g) = pushAnd f :|: pushAnd g
pushAnd (f :&: g) = pushAnd f :&: pushAnd g
pushAnd f = f

balance :: Form -> Form
balance (f :&: (g :&: h)) = balance ((f :&: g) :&: h)
balance (f :|: (g :|: h)) = balance ((f :|: g) :|: h)
balance (f :&: g) = balance f :&: balance g
balance (f :|: g) = balance f :|: balance g
balance f = f

{- Vgl. "Sol_Exercise_5.hs" -}
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)

toDnf :: Form -> Form
toDnf = fixpoint (==) (balance . pushAnd . pushNot)

prop_isDnf_incl f =
  not ([True, False] `List.isInfixOf`
       map (\is -> is f) [isAtom, isLiteral, isCoclause, isDnf])

prop_isDnf_Not = let f = Not F in not (isAtom f) && isLiteral f

prop_isDnf_Not_Not f = let g = Not (Not f) in not (isDnf g)

prop_isDnf_And = let f = Not F :&: Not T in not (isLiteral f) && isCoclause f

prop_isDnf_Or = let f = Not F :|: Not T in not (isCoclause f) && isDnf f

prop_isDnf_Or_And_Not =
  let f = Var "x" :|: (Var "y" :&: Not (Var "z")) in
    not (isCoclause f) && isDnf f

prop_isDnf_Or_And_Not_And =
  let f = Var "x" :|: ((Var "y" :&: Not (Var "z")) :&: Var "w") in
    not (isCoclause f) && isDnf f

prop_isDnf_Or_And_And_Not =
  let f = Var "x" :|: (Var "y" :&: (Not (Var "z") :&: Var "w")) in
    not (isDnf f)

prop_toDnf_isDnf f = isDnf (toDnf f)

prop_toDnf_equiv f = equivalent (toDnf f) f
  where equivalent f g = all (\v -> eval v f == eval v g) $ vals $ List.nub (vars f ++ vars g)


{- H9.3 -}

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

evens :: Tree Int -> [Int]
evens = foldTree (\a l r -> (if even a then [a] else []) ++ l ++ r) []

treeSum :: Tree Int -> Int
treeSum = foldTree (\a l r -> a + l + r) 0

treeMin :: Ord a => a -> Tree a -> a
treeMin m = foldTree (\a l r -> minimum [a, l, r]) m


{- H9.4 -}

{-WETT-}
quasiMajorityElems :: Eq a => [a] -> [a]
quasiMajorityElems xs =
    checkAll (List.nub xs)
  where checkAll [] = []
        checkAll (y : ys) =
          (if 2 * length (filter (== y) xs) >= length xs then [y] else [])
          ++ checkAll ys
{-TTEW-}