module Exercise_9 where
{-WETT-}

import Data.Maybe
import Data.List

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 c = if elem [] s then [[]] else s
             where s = [filter (/= bottom) x | x <- c, top `notElem` x]

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

{-H9.2.3-}
selectV :: ConjForm -> Maybe (Name, Bool)
selectV (x:xs) = if isNothing y then selectV xs else y
                 where y = selectFromC x
selectV _ = Nothing

selectFromC :: Clause -> Maybe (Name, Bool)
selectFromC (Pos (Var x):xs) = Just (x, True)
selectFromC (Neg (Var x):xs) = Just (x, False)
selectFromC (x:xs) = selectFromC xs
selectFromC _ = Nothing

{-H9.2.5-}
satConj :: ConjForm -> Maybe Valuation
satConj f = satConj' f (fromMaybe [] (getSimpleClauses f Nothing))

satConj' :: ConjForm -> Valuation -> Maybe Valuation
satConj' f v
  | null s = Just v
  | [] `elem` s = Nothing
  | isJust x && isJust p = p
  | isJust nx && isJust n = n
  | otherwise = Nothing
  where
    s = simpConj f
    x = selectV s
    nx = if isJust x then Just (negV (fromJust x)) else Nothing
    p = satConj' (substConj [fromJust x] s) (fromJust x : v)
    n = satConj' (substConj [fromJust nx] s) (fromJust nx : v)

negV :: (Name, Bool) -> (Name, Bool)
negV (x,y) = (x, not y)

--creates a valuation that is required so all unit clauses are true
getSimpleClauses :: ConjForm -> Maybe Valuation -> Maybe Valuation
getSimpleClauses (f:fs) xs
  | length f == 1 && isJust s = getSimpleClauses fs $ Just $ maybe [fromJust s] ((:) (fromJust s)) xs
  | otherwise = getSimpleClauses fs xs
    where s = selectVar $ head f
getSimpleClauses [] xs = xs

selectVar :: Literal -> Maybe(Name, Bool)
selectVar (Pos (Var x)) = Just (x, False)
selectVar (Neg (Var x)) = Just (x, True)
selectVar _ = Nothing


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



{-TTEW-}