module Exercise_9 where
{-WETT-}

import Data.List
import Data.Function

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 = reduceToEmpty . (removeTop . (removeBottom . reduceToTop))
  where
    reduceToTop = map (\clause -> if elem top clause then [top] else clause)
    removeBottom = map (filter (/= bottom))
    removeTop = filter (/= [top])
    reduceToEmpty formula = if elem [] formula then [[]] else formula


{-H9.2.2-}
cnf :: Form -> ConjForm
cnf (L literal) = [[literal]]
cnf (formA :&: formB) = (cnf formA) ++ (cnf formB)
cnf (formA :|: formB) = [a ++ b | a <- (cnf formA), b <- (cnf formB)]

{-H9.2.3-}  -- This never returns Nothing, as top and bottoms are filtered out beforehand
selectV :: ConjForm -> Maybe (Name, Bool)
selectV f 
  | fFlat == [] = Nothing
  | otherwise = toVal (head fFlat)
  where
    toVal (Pos (Var n)) = Just (n, True)
    toVal (Neg (Var n)) = Just (n, False)
    toVal _ = Nothing
    isVar (Pos (Var n)) = True
    isVar (Neg (Var n)) = True
    isVar a = False
    fFlat = filter (isVar) (concat f)
  
  --selectV f = toVal (fst (head (sortBy (on compare snd) [(c, foldl (\s a -> if a == c then s+1 else s) 0 fFlat) | c <- nub fFlat])))


{-H9.2.5-}
satConj :: ConjForm -> Maybe Valuation
satConj = satConjAcc []
  where
    satConjAcc vs f
      | f' == [[]] = Nothing
      | f' == [] = Just vs
      | otherwise = case satConjAcc ((n, b):vs) (substConj [(n, b)] f') of
        Just xs -> Just xs
        Nothing -> satConjAcc ((n, not b):vs) (substConj [(n, not b)] f')
      where 
        f' = simpConj f
        (n, b) = toVal (head (concat f')) --No timeouts
          where
            toVal (Pos (Var n)) = (n, True)
            toVal (Neg (Var n)) = (n, False)

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

{-TTEW-}