module Exercise_9 where

{-WETT-}
type Name = String
type Valuation = [(Name,Bool)]

data Atom = T | Var Name
  deriving (Eq, Show)
data Literal = Pos Atom | Neg Atom
  deriving (Eq, Show)
type Clause = [Literal]
type ConjForm = [Clause]

data Form = L Literal | Form :&: Form | Form :|: Form
  deriving (Eq, Show)

{-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 = if elem [] z then [[]] else deleteAll [top] z
  where z = map simpClause xs

simpClause :: Clause -> Clause
simpClause xs = if elem top xs then [top] else deleteAll bottom xs

deleteAll :: Eq a => a -> [a] -> [a]
deleteAll _ [] = []
deleteAll a (x : xs) = if a == x then deleteAll a xs else x : deleteAll a xs


{-H9.2.2-}
cnf :: Form -> ConjForm
cnf (L a)       = [[a]]
cnf (xs :&: ys) = cnf xs ++ cnf ys
cnf (xs :|: ys) = [a ++ b | a <- (cnf xs) , b <- (cnf ys)]


{-H9.2.3-}
selectV :: ConjForm -> Maybe (Name, Bool)
selectV []   = Nothing
selectV [[]] = Nothing
selectV (((Pos (Var a)) : as) : xs) = Just (a, True)
selectV (((Neg (Var a)) : as) : xs) = Just (a, False)
selectV ((a : as) : xs) = selectV (as : xs)
selectV ([] : xs) = selectV xs


{-H9.2.5-}

satConj :: ConjForm -> Maybe Valuation
satConj s = if a then Just b else Nothing
 where (a , b) = satX s []

satX :: ConjForm -> Valuation -> (Bool , Valuation)
satX f val
 | f' == []   = (True  , val)
 | f' == [[]] = (False , val)
 | otherwise  = if (fst x) then x else y

 where f'           = simpConj f
       Just (n , b) = selectV f'
       x            = satX (substConj [(n ,     b)] f') ((n ,     b) : val)
       y            = satX (substConj [(n , not b)] f') ((n , not b) : val)


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