module Exercise_9 where
import Data.Maybe

{-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)
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 [] = []
simpConj (x:xs)
            | x == []     = [[]]
            | elem top x  = simpConj xs
            | elem bottom x = simpConj ((filter (\t -> t /= bottom) x):xs) 
            | otherwise = let t = simpConj xs in if (t == [[]]) then [[]] else x:t

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


{-H9.2.3-}

getName :: Literal -> Name
getName (Pos (Var x)) = x
getName (Neg (Var x)) = x
replace :: ConjForm -> Name -> Bool -> ConjForm
replace cf name b = map (\x -> map (\s -> if (getName s == name) then decide s b else s ) x) cf
decide :: Literal -> Bool -> Literal
decide (Pos a) True = top
decide (Pos a) False = bottom
decide (Neg a) True = bottom
decide (Neg a) False = top
isVar :: Literal -> Bool
isVar x = case x of
      top -> False
      bottom -> False
      _ -> True
selectV :: ConjForm -> Maybe (Name, Bool)
selectV [] = Nothing
selectV [[]] = Nothing
selectV f = let ls = [ x | xs <- f , x<-xs , isVar x] in if (ls == []) then Nothing else Just (getName(head ls),True)
selectV2 :: ConjForm -> Maybe (Name, Bool)
selectV2 f 
        | f'==[] || f'==[[]]  = Nothing
        | otherwise = if simpConj (replace f' (getName(head(head f'))) True) == [[]] then Just (getName(head(head f')) , False) else Just (getName(head(head f')) , True) 
     where f' = simpConj f     

{-H9.2.5-}
satConj :: ConjForm -> Maybe Valuation
satConj cf 
        | cf' == [[]] = Nothing 
        | cf' == [] = Just []
        | otherwise = satConj2 cf' 
          
          where cf' = simpConj cf
satConj2 :: ConjForm -> Maybe Valuation
satConj2 cf = if(val == Nothing ) then  combine name False (satConj cf'') else Just ((name, True) : (fromJust val)) 
        where name = getName (head (head (cf)))
              cf' = replace cf name True
              val = satConj cf' 
              cf'' = replace cf name False
combine :: Name -> Bool -> Maybe Valuation -> Maybe Valuation
combine _ _ Nothing = Nothing
combine name b val = Just ((name , b) : (fromJust val))
{-H9.2.6-}
sat :: Form -> Maybe Valuation
sat = satConj.cnf
{-TTEW-}