module Exercise_9 where
{-WETT-}

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 cf = let cf2 = (filter (/= [top]) (map (\c -> if elem top c then [top] else (filter (/= bottom) c)) cf)) in if elem [] cf2 then [[]] else cf2

{-H9.2.2-}
cnf :: Form -> ConjForm
cnf (L a) = [[a]]
cnf (f1 :&: f2) = (cnf f1) ++ (cnf f2)
cnf (f1 :|: f2) = [x++y | x <- (cnf f1), y <- (cnf f2)] 

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

{-H9.2.5-}
satConj :: ConjForm -> Maybe Valuation
satConj f = satConj2 (simpConj f) []

satConj2 :: ConjForm -> [(Name,Bool)] -> Maybe Valuation
satConj2 f acc 
  | null f = Just acc
  | elem [] f = Nothing
  | isNothing (selectV f) = Nothing
  | otherwise = let (a,b) = fromJust (selectV f) 
                    l = satConj2 (simpConj (substConj [(a,b)] f)) ((a,b):acc)
                    r = satConj2 (simpConj (substConj [(a,not b)] f)) ((a,not b):acc)
                    in if isNothing l then r  else l

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

{-TTEW-}