module Exercise_9 where
{-WETT-}

import Data.List
import Data.Maybe


type Name = String
type Valuation = [(Name,Bool)]
data Atom = T | Var Name
  deriving (Eq, Show)
data Literal = Pos Atom | Neg Atom
  deriving (Eq, Show)
data Form = L Literal | Form :&: Form | Form :|: Form
  deriving (Eq, Show)
type Clause = [Literal]
type ConjForm = [Clause]

{-T9.3.2-}
top :: Literal
top = Pos T

bottom :: Literal
bottom = Neg T

{-T9.3.3-}
clauseToForm :: Clause -> Form
clauseToForm [] = L bottom
clauseToForm ls = foldr ((:|:) . L) (L $ last ls) (init ls)

conjToForm :: ConjForm -> Form
conjToForm [] = L top
conjToForm ds = foldr ((:&:) . clauseToForm) (clauseToForm $ last ds) (init ds)

{-T9.3.4-}
substLiteral :: Valuation -> Literal -> Literal
substLiteral v l@(Pos (Var n)) = case lookup n v of
  Just b -> if b then top else bottom
  Nothing -> l
substLiteral v l@(Neg (Var n)) = case lookup n v of
  Just b -> if b then bottom else top
  Nothing -> l
substLiteral v l = l

substClause :: Valuation -> Clause -> Clause
substClause = map . substLiteral

substConj :: Valuation -> ConjForm -> ConjForm
substConj = map . substClause

{-H9.2.1-}
simpConj :: ConjForm -> ConjForm
simpConj xs =simpReduceToEmpty (simpRemoveBottom (simpReduceToTop xs))

simpReduceToTop :: ConjForm -> ConjForm
simpReduceToTop []= []
simpReduceToTop  (x:xs)
 | containsTop  x = simpReduceToTop xs
 | otherwise = [x] ++ simpReduceToTop xs
 where
  containsTop [] = False
  containsTop  (l:ls) = (containsTop ls) || l==top

simpRemoveBottom :: ConjForm -> ConjForm
simpRemoveBottom []= []   --leer zurückgeben, dai erstes Beispiel stimmt
simpRemoveBottom  (x:xs) = [filter (/=bottom) x] ++ simpRemoveBottom xs

simpReduceToEmpty :: ConjForm -> ConjForm
simpReduceToEmpty []= []   --leer zurückgeben, dai erstes Beispiel stimmt
simpReduceToEmpty  (xs)
 | onlyempty==[]=xs
 | otherwise = [[]]
  where
   onlyempty=filter (==[]) (xs)


{-H9.2.2 -}

cnf :: Form -> ConjForm
cnf x =  simpConj (cnfHelper x)
 where
  cnfHelper :: Form -> ConjForm
  cnfHelper (L a)= [[a]]
  cnfHelper (x :|: y) = matchEveryClause (cnfHelper x) (cnfHelper y)
   where
   matchEveryClause [] q = []
   matchEveryClause q [] = []
   matchEveryClause (x:xs) (y:ys) = [x ++ y]  ++ [ j ++ y | j<-xs] ++ [ j ++ x | j<-ys] ++ matchEveryClause xs ys
  cnfHelper (x :&: y)= (cnfHelper x) ++ (cnfHelper y)


{-H9.2.3-}
selectV :: ConjForm -> Maybe (Name, Bool)
selectV [] = Nothing
selectV (x:xs)
 | isJust variable = variable
 | otherwise = selectV xs
  where
   variable = contiansVariable x
    where
     contiansVariable [] = Nothing
     contiansVariable ((Pos T):xs) = contiansVariable xs
     contiansVariable ((Neg T):xs) = contiansVariable xs
     contiansVariable ((Pos (Var x)):xs) = Just (x, True)
     contiansVariable ((Neg (Var x)):xs) = Just (x, False)


{-H9.2.5-}
satConj :: ConjForm -> Maybe Valuation
satConj []=Just []
satConj [[]]= Nothing
satConj xs = satConjHelper (simpConj xs)
 where
  satConjHelper []=Just []
  satConjHelper [[]]= Nothing
  satConjHelper xs = evaluate vari xs
   where
    vari=selectV xs
    evaluate Nothing xs = satConjHelper xs --eventuell endlosschleife durch rekursion
    evaluate (Just (n,b)) xs
     | newAllocation == Nothing && newAllocationNot == Nothing = Nothing
     | newAllocation /= Nothing = Just([(n,b)] ++ (fromJust newAllocation))
     | otherwise = Just([(n, (not b))] ++ (fromJust newAllocationNot))
      where
       newAllocation = satConj (insertAllocation (n,b) xs)
       newAllocationNot = satConj (insertAllocation (n,(not b)) xs)


insertAllocation :: (Name, Bool) -> ConjForm -> ConjForm
insertAllocation (n,b) []=[]
insertAllocation (n,b) (x:xs) = [replaceVariable (n,b) x] ++ insertAllocation (n,b) xs
 where
  replaceVariable (n,b) [] =[]
  replaceVariable (n,b) ((Pos x):xs)=(replaceHelperPos (n,b) x) ++ replaceVariable (n,b) xs
  replaceVariable (n,b) ((Neg x):xs)=(replaceHelperNeg (n,b) x) ++ replaceVariable (n,b) xs



replaceHelperPos :: (Name, Bool) -> Atom -> [Literal]
replaceHelperPos (n,b) (Var a) 
 | n==a && b = [top]
 | n==a && (not b) = [bottom]
 | otherwise = [Pos (Var a)]
replaceHelperPos (n,b) (T) = [Neg T] ++[Pos (Var "Warum")]

replaceHelperNeg :: (Name, Bool) -> Atom -> [Literal]
replaceHelperNeg (n,b) (Var a)
 | n==a && b = [bottom]
 | n==a && (not b) = [top]
 | otherwise = [Neg (Var a)]
replaceHelperNeg (n,b) (T) = [Neg T]






{-H9.2.6-}
sat :: Form -> Maybe Valuation
sat xs = satConj (simpConj (cnf xs))
{-TTEW-}