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 = if elem [] removeBottom then [[]] else removeBottom
 where
  removeClauseWithTop = [ x | x <- xs, not (elem top x)]
  removeBottom = [ filter (/= bottom) x | x <- removeClauseWithTop]

{-H9.2.2-}
cnf :: Form -> ConjForm
cnf (L l)     = [[l]]
cnf (l :&: r) = (cnf l) ++ (cnf r)
cnf (l :|: r) = [ left ++ right | left <- cfLeft, right <- cfRight]
 where cfLeft  = cnf l
       cfRight = cnf r

{-H9.2.3-}
selectV :: ConjForm -> Maybe (Name, Bool)
selectV cf
 | null plr'      = Nothing
 | isJust olr     = aux (head (fromJust olr))
 | not (null plr) = aux (head plr)
 | otherwise      = aux (head plr')
    where
     olr  = find (\e -> length e == 1 && head e /= top && head e /= bottom) cf
     plr' = [ x | x <- concat cf, isVar x ]
     plr  = [ x | x <- plr', not (isNegationIn x plr') ]

isNegationIn :: Literal -> [Literal] -> Bool
isNegationIn (Pos (Var name)) xs = elem (Neg (Var name)) xs
isNegationIn (Neg (Var name)) xs = elem (Pos (Var name)) xs

isVar :: Literal -> Bool
isVar (Pos T) = False
isVar (Neg T) = False
isVar _       = True

aux :: Literal -> Maybe (Name, Bool)
aux (Pos (Var name)) = Just (name, True)
aux (Neg (Var name)) = Just (name, False)
{-H9.2.5-}
satConj :: ConjForm -> Maybe Valuation
satConj f = satConj' f [] 

satConj' :: ConjForm -> Valuation -> Maybe Valuation
satConj' f val
 | null f'    = Just val
 | elem [] f' = Nothing
 | otherwise  = let positive = satConj' (substConj ((v,b):val) f) ((v,b):val) in if isJust positive then positive else satConj' (substConj ((v,not b):val) f) ((v,not b):val)
    where f'       = simpConj f
          (v, b)   = fromJust (selectV f)
          

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

{-TTEW-}