module Exercise_9 where
{-WETT-}

import Data.List
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 cf = let
    oped = filter (/= [top]) (map (filter (/= bottom)) (map (\xs -> if any(==top) xs then [top] else xs) cf))
  in if any (==[]) oped then [[]] else oped

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

{-H9.2.3-}
selectV :: ConjForm -> Maybe (Name, Bool)
selectV cf = let
    names = getNames cf
  in if isJust names then Just (fromJust names, (simpConj $ substConj [(fromJust names, True)] cf) /= [[]]) else Nothing
  where
    getNames cf = litToString $ concat (map (filter (\x -> x /= top && x /= bottom)) cf)
    litToString (x@(Pos (Var n)):xs) = Just n
    litToString (x@(Neg (Var n)):xs) = Just n
    litToString _ = Nothing

{-H9.2.5-}
satConj :: ConjForm -> Maybe Valuation
satConj cf = let
    sch = satConjHelp cf []
  in if simpConj cf == [] then Just []
    else if sch /= [] then Just sch
    else Nothing
  where
    satConjHelp :: ConjForm -> Valuation -> Valuation
    satConjHelp cf vals = let substed = simpConj $ substConj vals cf in
      {-Belegung vals erfüllbar-}
      if simpConj substed == [] then vals
      {-Wenn Klauseln mit Singularliteral vorhanden, eliminieren-}
      else if eliminateOnesies substed /= [] then satConjHelp cf (vals ++ (eliminateOnesies substed))
      {-Literale nur positiv oder nur negativ-}
      else if eliminateSingulars substed /= [] then satConjHelp cf (head (eliminateSingulars substed):vals)
      {-Einfach eine Belegung wählen-}
      else if isJust $ selectV substed then satConjHelp cf ((fromJust $ selectV substed):vals)
      else []

    eliminateOnesies :: ConjForm -> Valuation
    eliminateOnesies cf = filterDoubles [determineNameAndVal $ head klaus | klaus <- simpConj cf, length klaus == 1]
    filterDoubles [] = []
    filterDoubles ((a,b):xs) = (a,b):[(c,d) | (c,d) <- xs, a /= c]

    determineNameAndVal x@(Pos (Var n)) = (n, True)
    determineNameAndVal x@(Neg (Var n)) = (n, False)

    eliminateSingulars :: ConjForm -> Valuation
    eliminateSingulars cf = let nubbedCf = nub $ concat cf in map determineNameAndVal $ filter (\x -> searchComplement x nubbedCf) nubbedCf
    searchComplement :: Literal -> [Literal] -> Bool
    searchComplement x@(Pos (Var n)) xs = not $ any(==(Neg (Var n))) xs
    searchComplement x@(Neg (Var n)) xs = not $ any(==(Pos (Var n))) xs

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

{-TTEW-}