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 ls = (containsFalse . removeTop) $ map (removeBottom . containsTop) ls

-- simplifies all Clauses containing top to top (otherwise not touching the clause)
containsTop :: Clause -> Clause
containsTop ls = ct ls []
 where
    ct :: Clause -> Clause -> Clause
    ct [] ls = reverse ls
    ct ((Pos T):ls) _ = [top]
    ct (l:ls) ls' = ct ls (l:ls')

-- removes every occurrence of bottom
removeBottom :: Clause -> Clause
removeBottom [] = []
removeBottom ((Neg T):ls) = removeBottom ls
removeBottom (l:ls) = l:removeBottom ls

-- reoves all true-clauses ([top])
removeTop :: ConjForm -> ConjForm
removeTop [] = []
removeTop ([(Pos T)]:ls) = removeTop ls
removeTop (l:ls) = l:removeTop ls

-- simplifies to empty Clause if contains empty clause
containsFalse :: ConjForm -> ConjForm
containsFalse ls = cf ls []
 where
    cf :: ConjForm -> ConjForm -> ConjForm
    cf [] ls' = reverse ls'
    cf ([]:ls) _ = [[]]
    cf (l:ls) ls' = cf ls (l:ls')

{-H9.2.2-}
cnf :: Form -> ConjForm
cnf (L l) = [[l]]
cnf (f1 :&: f2) = (cnf f1) ++ (cnf f2)
cnf ((L l1) :|: (L l2)) = [[l1, l2]]
cnf (f1 :|: f2) = multiply f1af f2af-- Und-Terme "ausmultiplizieren"
      where 
        f1af = cnf f1
        f2af = cnf f2
            

multiply :: ConjForm -> ConjForm -> ConjForm
multiply [x] ys = multi x ys
multiply (x:xs) ys = (multi x ys) ++ (multiply xs ys)

multi :: Clause -> ConjForm -> ConjForm
multi f [x] = [f ++ x]
multi f (x:xs) = [f ++ x] ++ (multi f xs)

{-H9.2.3-}
selectV :: ConjForm -> Maybe (Name, Bool)
selectV cs = if vs /= [] then Just (head vs, True) else Nothing
 where
    vs = getVarsCNF cs

getVarsCNF :: ConjForm -> [Name]
getVarsCNF xs = foldl (\ls x -> if getVarsC x /= [] then nub ((getVarsC x) ++ ls) else ls) [] xs

getVarsC :: Clause -> [Name]
getVarsC xs = foldl (\ls x -> if getVarsL x /= [] then nub ((getVarsL x)++ls) else ls) [] xs

getVarsL :: Literal -> [Name]
getVarsL (Pos (Var x)) = [x]
getVarsL (Neg (Var x)) = [x]
getVarsL _ = []

{-H9.2.5-}
satConj :: ConjForm -> Maybe Valuation
satConj cfs = sC (simpConj cfs) []
  where
    sC :: ConjForm -> Valuation -> Maybe Valuation
    sC [] vs = Just vs
    sC [[]] vs = Nothing
    sC cfs' vs 
        | selectV cfs' == Nothing = Nothing
        | otherwise = if caseTrue /= Nothing then caseTrue else caseFalse
          where
            caseTrue = sC (simpConj (substConj [trueSub] cfs')) (trueSub:vs)
              where 
                trueSub = fromJust (selectV cfs')
            caseFalse = sC (simpConj (substConj [falseSub] cfs')) (falseSub:vs)
              where
                falseSub = (fst (fromJust (selectV cfs')), not (snd (fromJust (selectV cfs'))))
{-H9.2.6-}
sat :: Form -> Maybe Valuation
sat = satConj . cnf
{-TTEW-}