module Exercise_9 where
{-WETT-}

{-T9.1.1-}
data NonEmptyList a = Single a | a `Cons` NonEmptyList a
  deriving (Eq, Show)

{-T9.1.2-}
fromList :: [a] -> Maybe (NonEmptyList a)
fromList [] = Nothing
fromList (a:as) = case fromList as of
                    Nothing -> Just $ Single a
                    Just as' -> Just $ a `Cons` as'

toList :: NonEmptyList a -> [a]
toList (Single a) = [a]
toList (a `Cons` as) = a:(toList as)

{-T9.1.3-}
nHead :: NonEmptyList a -> a
nHead (Single a) = a
nHead (a `Cons` _) = a

nTail :: NonEmptyList a -> Maybe (NonEmptyList a)
nTail (Single a) = Nothing
nTail (a `Cons` as) = Just as

nAppend :: NonEmptyList a -> NonEmptyList a -> NonEmptyList a
nAppend = undefined
-- nAppend (Single a) (Single b) = a `Cons` Single b
-- nAppend (a `Cons` as) (b `Cons` bs) = 

nTake :: Integer -> NonEmptyList a -> Maybe (NonEmptyList a)
nTake 1 (Single x) = Just $ Single x
nTake n (x `Cons` xs)
  | n == 1 = Just $ Single x
  | n > 1 = case nTake (n-1) xs of
              Nothing -> Nothing
              Just s -> Just $ x `Cons` s
  | n <= 0 = Nothing              -- redundant wegen nTake _ _
nTake _ _ = Nothing

{-T9.3.2-}
top :: Literal
top = Pos T

bottom :: Literal
bottom = Neg T

conjToForm :: ConjForm -> Form
conjToForm [] = L top
conjToForm [x] = clauseToForm x
conjToForm (c:cs) = (clauseToForm c) :&: conjToForm cs

clauseToForm :: Clause -> Form
clauseToForm [] = L bottom
clauseToForm [x] = L x
clauseToForm (l:ls) = L l :|: clauseToForm ls

{-T9.3.4-}
substConj :: Valuation -> ConjForm -> ConjForm
substConj = map . substClause

substClause :: Valuation -> Clause -> Clause
substClause = map . substLiteral

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

type Name = String  -- synonym 

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] -- Liste von Literalen
type ConjForm = [Clause]-- Liste von Klauseln

type Valuation = [(Name,Bool)]

{-H9.2.1-}
simpConj :: ConjForm -> ConjForm
simpConj cs = case elem [] cs' of
                True -> [[]]
                False -> [c | c <- cs', c /= [top]]
                where 
                  cs' = map simpClause cs

simpConjNoReduc :: ConjForm -> ConjForm
simpConjNoReduc cs = let cs' = map simpClauseNoReduc cs in [c | c <- cs', c /= []]

simpClause :: Clause -> Clause
simpClause ls = case elem top ls of
              True -> [top]
              False -> [l | l <- ls, l /= bottom]

simpClauseNoReduc :: Clause -> Clause
simpClauseNoReduc ls = [l | l <- ls, l /= top && l /= bottom]

{-H9.2.2-}
cnf :: Form -> ConjForm
cnf (L l) = [[l]]
cnf (a :&: b) = cnf a ++ cnf b
cnf (a :|: b) = cnf a `mult` cnf b

mult :: ConjForm -> ConjForm -> ConjForm
mult lcs rcs = [lc ++ rc | lc <- lcs, rc <- rcs]


{-H9.2.3-}
selectV :: ConjForm -> Maybe (Name, Bool)
selectV [] = Nothing
selectV [c] = findVariable c
selectV cs = case simpConjNoReduc cs of
              [] -> Nothing
              [c] -> findVariable c
              cs' -> findVariable $ findMinimalClause (tail cs') (head cs')

-- cmc stands for current minimal clause
-- where Cmin contains <= elements compared to all other clauses
findMinimalClause :: ConjForm -> Clause -> Clause
findMinimalClause [] cmc = cmc
findMinimalClause [c] cmc = if length c < length cmc && c /= [] then c else cmc
findMinimalClause _ cmc@[l] = cmc
findMinimalClause (c:cs) cmc = let lenc = length c
                               in case lenc < length cmc of
                                True -> if lenc == 1 then c else findMinimalClause cs c
                                False -> findMinimalClause cs cmc

findVariable :: Clause -> Maybe (Name, Bool)
findVariable [] = Nothing
findVariable [Pos (Var n)] = Just (n, True)
findVariable [Neg (Var n)] = Just (n, False)
-- findVariable [l] = Nothing   | redundant due to simpClauseNoReduc
findVariable (l:ls) = case findVariable [l] of
                        Nothing -> findVariable ls
                        Just (n,b) -> Just (n,b)

{-H9.2.5-}
satConj :: ConjForm -> Maybe Valuation
satConj [[]] = Nothing
satConj [] = Just []
satConj cs = satConj' cs []

satConj' :: ConjForm -> Valuation -> Maybe Valuation
satConj' [] vars = Just vars
satConj' cs vars = 
  let cs' = simpConj cs
  in if null cs' then Just vars else if [] `elem` cs' then Nothing else case selectV cs' of
    Nothing -> Nothing
    Just (n,b) -> case satConj' (simpConj $ substConj [(n,b)] cs') ((n,b):vars) of
                    Nothing -> satConj' (simpConj $ substConj [(n, not b)] cs') ((n,not b):vars)
                    Just v -> Just v

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

{-TTEW-}