module Exercise_9 where
{-WETT-}
import Test.QuickCheck

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 = simpConj' xs []
  where
    simpConj' [] y = y
    simpConj' (x:xs) y
      | simpCause x == [] = [[]]
      | simpCause x == [top] = simpConj' xs y
      | otherwise = simpConj' xs (y++[simpCause x])
    simpCause x = simpCause' x []
    simpCause' [] y = y
    simpCause' (x:xs) y
      | x == top = [top]
      | x == bottom = simpCause' xs y
      | otherwise = simpCause' xs (y++[x])


{-H9.2.2-}
cnf :: Form -> ConjForm
cnf (L l)= [[l]]
cnf ((:&:) f1 f2)= cnf f1 ++ cnf f2
cnf ((:|:) f1 f2)= or' (cnf f1) (cnf f2)
  where
    or' :: ConjForm -> ConjForm -> ConjForm
    or' c1 c2 = [ l1++l2 | l1 <- c1 , l2<-c2 ]

{-H9.2.3-}
selectV :: ConjForm -> Maybe (Name, Bool)
selectV [] = Nothing
selectV (c:cs)=let s=s' c in if s==Nothing then selectV cs else s
s' (((Pos (Var n)):lx))=Just (n,True)
s' (((Neg (Var n)):lx))=Just (n,False)
s' (l:ls)= s' ls
s' []=Nothing
{-H9.2.5-}
schnittValuation:: Maybe (Name,Bool)->Maybe Valuation->Maybe Valuation
schnittValuation _ Nothing = Nothing
schnittValuation Nothing _ = Nothing
schnittValuation (Just a) (Just v)= Just (a:v)

satConj :: ConjForm -> Maybe Valuation
-- satConj = undefined
satConj f = satConj' (simpConj f)
  where
    satConj' :: ConjForm -> Maybe Valuation
    satConj' [] = Just []
    satConj' [[]] = Nothing
    satConj' f' =
      -- if v'==Nothing then Just []
      -- else
      if sCv /= Nothing
      then schnittValuation v' sCv
      else if sCvn /= Nothing
        then schnittValuation nv' sCvn
        else Nothing
      where
        v' = selectV f
        nv'= vn' v'
        vn' Nothing = Nothing
        vn' (Just (n,b))= Just (n,not b)
        mbV2Val:: Maybe (Name, Bool)-> Valuation
        mbV2Val (Just (n,b))= [(n,b)]
        sCv = satConj (substConj (mbV2Val v') f)
        sCvn = satConj (substConj (mbV2Val nv') f)

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

{-TTEW-}