module Sol_Exercise_8 where
import Form_8
import Data.Ratio
import qualified Data.List as L
import Test.QuickCheck

{- Library -- nicht veraendern -}



{- G1 -}

data Fraction = Over Integer Integer deriving Show

norm :: Fraction -> Fraction
norm (Over a b) = (a `div` c) `Over` (b `div` c)
  where c = gcd a b * (if b < 0 then -1 else 1)

instance Num Fraction where
    (a1 `Over` b1) + (a2 `Over` b2) = norm $ (a1*b2 + a2*b1) `Over` (b1 * b2)
    (a1 `Over` b1) * (a2 `Over` b2) = norm $ (a1 * a2) `Over` (b1 * b2)
    abs (a `Over` b) = abs a `Over` abs b
    signum (a `Over` b) = (signum a * signum b) `Over` 1
    fromInteger n = n `Over` 1

instance Eq Fraction where
    (a1 `Over` b1) == (a2 `Over` b2) = a1*b2 == a2*b1

instance Fractional Fraction where
    recip (a `Over` b) = (b `Over` a)
    fromRational r = numerator r `Over` denominator r


{- G2 -}

-- siehe ExtForm.hs


{- G3 -}

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

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


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


{- H1 -}

equivalent :: Form -> Form -> Bool
equivalent f g = all (\v -> eval v f == eval v g) $ vals $ L.nub (vars f ++ vars g)

{- H2 -}

sNot :: Form -> Form
sNot T = F
sNot F = T
sNot p = Not p

sAnd :: Form -> Form -> Form
sAnd T q = q
sAnd F q = F
sAnd p T = p
sAnd p F = F
sAnd p q = p :&: q

sOr :: Form -> Form -> Form
sOr T q = T
sOr F q = q
sOr p T = T
sOr p F = p
sOr p q = p :|: q

sForm :: Form -> Form
sForm (Not p) = sNot (sForm p)
sForm (p :&: q) = sAnd (sForm p) (sForm q)
sForm (p :|: q) = sOr (sForm p) (sForm q)
sForm p = p


{- H3 -}

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

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

isCnf :: Form -> Bool
isCnf (f :&: g) = isCnf f && isClause g
isCnf f = isClause 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

pushOr :: Form -> Form
pushOr (f :|: (g :&: h)) = pushOr ((f :|: g) :&: (f :|: h))
pushOr ((f :&: g) :|: h) = pushOr ((f :|: h) :&: (g :|: h))
pushOr (f :&: g) = pushOr f :&: pushOr g
pushOr (f :|: g) = pushOr f :|: pushOr g
pushOr 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)

toCnf :: Form -> Form
toCnf = fixpoint (==) (balance . pushOr . pushNot)

prop_isCnf_incl f =
  not ([True, False] `L.isInfixOf`
       map (\is -> is f) [isAtom, isLiteral, isClause, isCnf])

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

prop_isCnf_Not_Not f = let g = Not (Not f) in not (isCnf g)

prop_isCnf_Or = let f = Not F :|: Not T in not (isLiteral f) && isClause f

prop_isCnf_And = let f = Not F :&: Not T in not (isClause f) && isCnf f

prop_isCnf_And_Or_Not =
  let f = Var "x" :&: (Var "y" :|: Not (Var "z")) in
    not (isClause f) && isCnf f

prop_isCnf_And_Or_Not_Or =
  let f = Var "x" :&: ((Var "y" :|: Not (Var "z")) :|: Var "w") in
    not (isClause f) && isCnf f

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

prop_toCnf_isCnf f = isCnf (toCnf f)

prop_toCnf_equiv f = equivalent (toCnf f) f