module Exercise_9 where
{-WETT-}

import Data.Function (on)
import Data.List (maximumBy, sortBy, groupBy, nub)
import Data.Maybe (catMaybes)

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 cs = if [] `elem` clauses then [[]] else clauses
    where
        clauses = filter (/= [top]) . map simpClause $ cs

simpClause :: Clause -> Clause
simpClause cs
    | top `elem` cs = [top]
    | otherwise = filter (/= bottom) cs

{-H9.2.2-}
cnf :: Form -> ConjForm
cnf (L l) = [[l]]
cnf (p :&: q) = cnf p ++ cnf q
cnf (ps :|: qs) = [ p ++ q | p <- cnf ps, q <- cnf qs ]

{-H9.2.3-}
selectV :: ConjForm -> Maybe (Name, Bool)
selectV cs = case groupBy ((==) `on` varName) 
    . sortBy (compare `on` varName)
    . filter (/= top)
    . filter (/= bottom)
    . concat 
    $ cs of
        [] -> Nothing
        xs -> Just $ valuation . head . maximumBy (compare `on` length) $ xs

valuation :: Literal -> (Name, Bool)
valuation l = (varName l, litToBool l)

litToBool :: Literal -> Bool
litToBool (Pos _) = True
litToBool (Neg _) = False

varName :: Literal -> Name
varName (Pos (Var name')) = name'
varName (Neg (Var name')) = name'

{-H9.2.5-}

type Name' = Int
type Literal' = (Name', Bool)
type Valuation' = [Literal']
type LitReplacement' = Literal'
type Clause' = [Literal']
type ConjForm' = [Clause']

transformCnf :: ConjForm -> ConjForm'
transformCnf = catMaybes . map (transformClause [])
    where
        transformClause xs [] = Just xs
        transformClause xs ((Pos (Var name)):cls) = transformClause ((read name :: Int, True):xs) cls 
        transformClause xs ((Neg (Var name)):cls) = transformClause ((read name :: Int, False):xs) cls
        transformClause xs ((Pos T):_) = Nothing
        transformClause xs ((Neg T):cls) = transformClause xs cls

satConj :: ConjForm -> Maybe Valuation
satConj conj = case satConj' . transformCnf $ conj of
    Nothing -> Nothing
    Just val -> Just $ map valuation' val

satConj' :: ConjForm' -> Maybe Valuation'
satConj' [] = Just []
satConj' cl = removeUnitClauses . simpConj' $ cl
    where
        removeUnitClauses = removeValuations findUnitClauses removePureVars
        removePureVars = removeValuations findPureVars removeSingleVar
        removeSingleVar conj' = case selectV' conj' of
            Nothing -> Nothing
            Just (name, bool) -> case (satConj' $ replaceLiteral (name, bool) conj', satConj' $ replaceLiteral (name, not bool) conj') of
                (Just val', _) -> Just $ (name, bool):val'
                (_, Just val') -> Just $ (name, not bool):val'
                _ -> Nothing

removeValuations :: (ConjForm' -> Valuation') -> (ConjForm' -> Maybe Valuation') -> ConjForm' -> Maybe Valuation'
removeValuations f nextStep conj = let val = f conj in
    case simpConj' $ foldr replaceLiteral conj val of
        [] -> Just val
        [[]] -> Nothing
        conj' -> case nextStep conj' of
            Nothing -> Nothing
            Just val' -> Just $ val ++ val'

findUnitClauses :: ConjForm' -> Valuation'
findUnitClauses [] = []
findUnitClauses ([unit]:conj) = unit : findUnitClauses conj
findUnitClauses (_:conj) = findUnitClauses conj

findPureVars :: ConjForm' -> Valuation'
findPureVars = map head
    . filter (\ls -> length ls == 1)
    . groupBy ((==) `on` fst)
    . sortBy (compare `on` fst)
    . nub
    . concat

replaceLiteral :: LitReplacement' -> ConjForm' -> ConjForm'
replaceLiteral r = catMaybes . map (replaceLiteralCl r [])

replaceLiteralCl :: LitReplacement' -> Clause' -> Clause' -> Maybe Clause'
replaceLiteralCl _ ret [] = Just $ ret
replaceLiteralCl r@(name, bool) ret (cl@(name', bool'):cs)
    | name /= name' = replaceLiteralCl r (cl:ret) cs
    | bool == bool' = Nothing
    | otherwise = replaceLiteralCl r ret cs

valuation' :: Literal' -> (Name, Bool)
valuation' (name, bool) = (show name, bool)

simpConj' :: ConjForm' -> ConjForm'
simpConj' cs = if [] `elem` cs then [[]] else cs

selectV' :: ConjForm' -> Maybe LitReplacement'
selectV' cs = case groupBy ((==) `on` fst) 
    . sortBy (compare `on` fst)
    . concat 
    $ cs of
        [] -> Nothing
        xs -> Just $ head . maximumBy (compare `on` length) $ xs


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



{-TTEW-}