module Exercise_9 where
{-WETT-}
import Data.Maybe    

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 xs = if elem [] aux then [[]] else aux
  where
    aux = aux_c (aux_b (aux_a xs))
    aux_a = map (\x -> if elem top x then [top] else x)
    aux_b = map (filter (/= bottom))
    aux_c = foldr (\x acc -> if x == [top] then acc else x:acc) [] 

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

{-H9.2.3-}
selectV :: ConjForm -> Maybe (Name, Bool)
selectV [] = Nothing
selectV [[]] = Nothing
selectV xs 
  | null $ vars xs = Nothing
  | otherwise = literalToMaybeNameBool $ head $ vars xs

vars :: ConjForm -> [Literal]
vars [] = []
vars [[]] = []
vars xs = foldr (\y acc -> filter (isVar) y ++ acc) [] xs

isVar :: Literal -> Bool
isVar (Pos T) = False
isVar (Neg T) = False
isVar (Pos (Var name)) = True
isVar (Neg (Var name)) = True

extractName :: Literal -> Name
extractName (Pos T) = []
extractName (Neg T) = []
extractName (Pos (Var name)) = name
extractName (Neg (Var name)) = name

e_selectV xs 
  | null xs = Nothing
  | xs == [[]] = Nothing
  | null $ simpConj xs = Nothing
  | simpConj xs == [[]] = Nothing
  | otherwise = literalToMaybeNameBool $ head $ head $ simpConj xs

-- if any (\x -> length x == 1) xs then literalToMaybeNameBool $ head $ head $ filter (\x -> length x == 1) xs else 

literalToMaybeNameBool :: Literal -> Maybe (Name, Bool)
literalToMaybeNameBool (Pos T) = Nothing
literalToMaybeNameBool (Neg T) = Nothing
literalToMaybeNameBool (Pos (Var name)) = Just (name, True)
literalToMaybeNameBool (Neg (Var name)) = Just (name, False) 

literalToNameBool :: Literal -> (Name, Bool)
literalToNameBool = fromJust . literalToMaybeNameBool

{-H9.2.5-}

satConj :: ConjForm -> Maybe Valuation
satConj [] = Just []
satConj [[]] = Nothing
satConj xs 
  | elem [] xs = Nothing
  | otherwise = aux (simpConj xs) []


aux :: ConjForm -> Valuation -> Maybe Valuation
aux [[]] _ = Nothing 
aux [] acc = Just acc 
aux xs acc = 
  if unitClauseExists -- OLR
     then aux (simpConj $ substConj [literalToNameBool $ head firstUnitClause] (filter (/=firstUnitClause) xs)) ((literalToNameBool $ head firstUnitClause) : acc)
     else
       if pureLiteralExists --PLR
          then aux (simpConj $ substConj [firstPLVar] xs) (firstPLVar : acc) 
          else
           if left == Nothing
              then if right == Nothing
                      then Nothing
                      else right
              else left 
    where 
      v = fromJust $ selectV xs   
      left = aux (simpConj $ substConj [v] xs) (v:acc)
      right = aux (simpConj $ substConj [(fst v, not $ snd v)] xs) ((fst v, not $ snd v):acc)
      allVars = listAllVars xs
      unitClauseExists = any (\x -> length x == 1) xs
      firstUnitClause = head $ filter (\x -> length x == 1) xs 
      pureLiteralExists = any (\x -> if elem (fst x, not $ snd x) allVars then False else True) allVars
      firstPLVar = head (foldr (\x acc -> if elem (fst x, not $ snd x) allVars then acc else x:acc) [] allVars)
--elem (fst $ literalToNameBool x, not $ snd $ literalToNameBool x) allVars 

listAllVars :: ConjForm -> [(Name, Bool)]
listAllVars [] = []
listAllVars [[]] = []
listAllVars xss = foldr (\xs acc_o -> foldr (\x acc -> if elem (literalToNameBool x) acc then acc else ((literalToNameBool x):acc)) acc_o xs) [] xss


-- satConj :: ConjForm -> Maybe Valuation
-- satConj [] = Just []
-- satConj [[]] = Nothing
-- satConj xs 
--   | elem [] xs = Nothing
--   | otherwise = aux (simpConj xs) []


-- aux :: ConjForm -> Valuation -> Maybe Valuation
-- aux [[]] _ = Nothing 
-- aux [] acc = Just acc 
-- aux xs acc = 
--   if any (\x -> length x == 1) xs 
--      then let v0 = head $ filter (\x -> length x == 1) xs 
--           in aux (simpConj $ substConj [fromJust $ literalToMaybeNameBool $ head v0] (filter (/=v0) xs)) ((fromJust $ literalToMaybeNameBool $ head v0) : acc)
--      else
--        if left == Nothing
--           then if right == Nothing
--                  then Nothing
--                  else right
--           else left 
--     where 
--       v = fromJust $ selectV xs   
--       left = aux (simpConj $ substConj [v] xs) (v:acc)
--       right = aux (simpConj $ substConj [(fst v, not $ snd v)] xs) ((fst v, not $ snd v):acc)


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

















{-TTEW-}