module Exercise_9 where
{-WETT-}

import Data.List
import Data.Maybe
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import qualified Data.Set as Set

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 l = let lst = (filter (/=[top]) . map (\x -> if top `elem` x then [top] else x) . map (filter (/=bottom))) l in 
           if (not $ null lst) && ([] `elem` lst) then ([[]]::ConjForm) else lst

{-H9.2.2-}
cnf :: Form -> ConjForm
cnf (L lit) = [[lit]]
cnf (left :|: right) = 
    let leftCNF = cnf left
        rightCNF = cnf right in
    [le ++ re | le <- leftCNF, re <- rightCNF]
cnf (left :&: right) = 
    let leftCNF = cnf left
        rightCNF = cnf right in
    leftCNF ++ rightCNF


{-H9.2.3-}
selectV :: ConjForm -> Maybe (Name, Bool)
selectV fform 
  | isJust $ getNextOLR form = getNextOLR form
  | isJust $ getNextPLR form varsList = getNextPLR form varsList
  | otherwise = if not$null $ varsList then (Just . head) varsList else Nothing
  where form = map (filter (\ x -> (x/=bottom) && (x/= top))) fform
        varsList = createVarsList form


getNextOLR :: ConjForm -> Maybe (Name, Bool)
getNextOLR form = let lst = filter ((1 ==).length) form in if not$null lst then case (head.head) lst of
                                                                                          (Pos(Var n)) -> Just (n, True)
                                                                                          (Neg(Var n)) -> Just (n, False)
                                                                              else Nothing

createVarsList :: ConjForm -> [(Name, Bool)]
createVarsList = Set.toList . Set.fromList . map (
          \x -> case x of 
            (Pos (Var n)) -> (n, True)
            (Neg (Var n)) -> (n, False)
          ) . concat

createPureList :: [(Name, Bool)] -> [(Name, Bool)]
createPureList vars = let posVars = (map fst . filter (\x -> True == snd x)) vars
                          negVars = (map fst . filter (\ x -> snd x ==False)) vars 
                          pureVars = (posVars \\ negVars) ++ (negVars \\ posVars) in
                      filter (\x -> fst x `elem` pureVars) vars

getNextPLR :: ConjForm -> [(Name, Bool)] -> Maybe (Name, Bool)
getNextPLR form varsList = let plist = createPureList varsList in if not$null plist then Just $ head plist else Nothing

{-H9.2.5-}
satConj :: ConjForm -> Maybe Valuation
satConj f = satStep (simpConj f) Map.empty

satStep :: ConjForm -> Map Name Bool -> Maybe Valuation
satStep form vMap 
  | null fSimp = Just $ Map.toList vMap
  | [] `elem` fSimp = Nothing
  | otherwise = let f1 = substConj [(aktVName, aktVBeleg)] fSimp
                    f2 = substConj [(aktVName, not aktVBeleg)] fSimp 
                    erg1 = satStep f1 (Map.insert aktVName aktVBeleg vMap) in
                if isJust erg1 then erg1 else satStep f2 (Map.insert aktVName (not aktVBeleg) vMap)

  where
    fSimp = simpConj form
    (aktVName, aktVBeleg) = fromJust $ selectV fSimp
{-H9.2.6-}
sat :: Form -> Maybe Valuation
sat = satConj . cnf

{-TTEW-}