module Exercise_9 where
{-WETT-}

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

instance Show Atom where
  show T = "True"
  show (Var a) = id a

instance Show Literal where
  show (Pos a) = show a
  show (Neg T) = "False"
  show (Neg a) = "!" ++ show a

instance Show Form where
  show (L a) = show a
  show (a :&: b) = "(" ++ show a ++ " ∧ " ++ show b ++ ")" 
  show (a :|: b) = "(" ++ show a ++ " ∨ " ++ show b ++ ")" 


{-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 _ l = l

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

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

{-H9.2.1-}
simpConj :: ConjForm -> ConjForm
simpConj cs = if [] `elem` cs' then [[]] else cs' 
              where cs' = (filter (/= [top]) . map (\c -> if top `elem` c then [top] else filter (/=bottom) c)) cs

{-H9.2.2-}
cnf :: Form -> ConjForm
cnf (L a) = [[a]]
cnf (cs :|: ds) = [c ++ d | c <- cnf cs, d <- cnf ds]
cnf (cs :&: ds) = cnf cs ++ cnf ds

a = L (Pos (Var "a")) 
b = L (Pos (Var "b")) 
c = L (Pos (Var "c")) 
d = L (Pos (Var "d")) 

aorb = a :|: b
aorborc = a :|: (b :|: c)
aandborcandd = (a :&: b) :|: (c :&: d)

cs = cnf aandborcandd

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

{-H9.2.5-}
satConj :: ConjForm -> Maybe Valuation
satConj [] = Just []
satConj [[]] = Nothing
satConj cs = case rs1 of
  Just v -> Just ((name, b):v)
  Nothing -> case rs2 of 
    Just v -> Just ((name, not b):v)
    Nothing -> Nothing
  where Just (name, b) = selectV cs
        cs1 = simpConj $ substConj [(name, b)] cs
        cs2 = simpConj $ substConj [(name, not b)] cs
        rs1 = satConj cs1
        rs2 = satConj cs2




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