module Exercise_9 where
{-WETT-}

import Data.Maybe
import Data.List
--import Debug.Trace

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 = simplifyEmpty . simplifyOnlyTop . simplifyBottom . simplifyTop where
  simplifyEmpty css | [] `elem` css = [[]]
                    | otherwise = css
  simplifyOnlyTop = filter (/= [top])
  simplifyBottom css = [filter (/= bottom) cs | cs <- css]
  simplifyTop css = [if top `elem` cs then [top] else cs | cs <- css]

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

{-H9.2.3-}
-- selectV selects the first variable
selectV :: ConjForm -> Maybe (Name, Bool)
selectV css = select (getVars css) where
  select [] = Nothing
  select (c:cs) = Just (c, True)
  getVars css = catMaybes (concat [map onlyVars cs | cs <- css])
  onlyVars (Pos (Var x)) = Just x
  onlyVars (Neg (Var x)) = Just x
  onlyVars _ = Nothing

{-H9.2.5-}
satConj :: ConjForm -> Maybe Valuation
satConj css = satConjVal (simpConj css) [] where
  satConjVal :: ConjForm -> Valuation -> Maybe Valuation
  --satConjVal css vals | trace ("css: " ++ show css ++ " vals: " ++ show vals) False = undefined
  satConjVal css vals | simpConj css == [] = Just vals
  satConjVal css vals | [] `elem` (simpConj css) = Nothing
  satConjVal css vals | otherwise = let f = simpConj css in case selectV f of
    Just (name, val) -> head' (catMaybes [satConjVal (substConj [(name, val)] f) ((name, val):vals), satConjVal (substConj [(name, not val)] f) ((name, (not val)):vals)]) where
      head' [] = Nothing
      head' (x:xs) = Just x
    Nothing -> Nothing

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