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-}
{-
- simplifyRemove, for a given clause, checks whether the clause contains "top", if so returns [top], if not removes all "bottom"s.
- almostDone removes all [top] clauses after applying simplifyRemove to all clauses.
-}
simpConj :: ConjForm -> ConjForm;
 simpConj xs = if elem [] almostDone then [[]] else almostDone
  where
   almostDone = filter (/= [top]) (map simplifyRemove xs)
   simplifyRemove ys = if any (== top) ys then [top] else (filter (/= bottom) ys)


{-H9.2.2-}
{-
- mergeCNF converts 2 disjunctive CNF-formulas to 1 CNF-formula.
- The input is converted to [[Literal]], where :&: means concatenation and :|: means mergeCNF
-}
cnf :: Form -> ConjForm
cnf (a :&: b) = cnf a ++ cnf b
cnf (a :|: b) = mergeCNF (cnf a) (cnf b)
 where
  mergeCNF xs ys = [x ++ y | x <- xs, y <- ys]
cnf (L a) = [[a]]

{-H9.2.3-}
{-
selectV looks, in the head of the [[Literal]] input, for the first named-literal (called firstVar):
  - if firstVar is empty, we recursively start over by calling selectV on the tail of the input
  - else, it returns the label of firstVar and True.
-}
selectV :: ConjForm -> Maybe (Name, Bool)
selectV [] = Nothing
selectV (a:as) = let firstVar = dropWhile (\x -> x == top || x == bottom) a
  in case firstVar of
     [] -> selectV as
     _ -> Just ((name . head) firstVar, True)
              where
                 name (Pos (Var x)) = x
                 name (Neg (Var x)) = x

{-H9.2.5-}
{-
satConj replaces named-literals in the input with booleans until the input CNF-formula is satisfied.
In order to store which named-literals are replaced with which booleans, I use an aux function with an accumulator.
-}
satConj :: ConjForm -> Maybe Valuation
satConj [] = Just []
satConj xs = aux [] (simpConj xs)

{-
- "replace ys b" is a function that recursively calls aux, while substituting (using substConj) in ys a named-literal (given by selectV) by forReplacement
- forReplacement uses selectV to find a literal to replace by a boolean. b (given when calling "replace ys b") is the replacing boolean.
- We (arbitrarily) first try "replace xs True" and then "replace xs False"
-}
aux :: Valuation -> ConjForm -> Maybe Valuation
aux acc [] = Just acc
aux acc xs = if elem [] xs || isNothing (selectV xs) then Nothing else
               let replace ys b = aux (acc ++ forReplacement) (simpConj (substConj forReplacement ys))
                    where
                     forReplacement = [((fst . fromJust . selectV) ys, b)]
                   replaceTrue = replace xs True
               in case replaceTrue of
                 Nothing -> replace xs False
                 _ -> replaceTrue

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

{-TTEW-}