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-}
simpConj :: ConjForm -> ConjForm
simpConj c = let result = map (filter (/= bottom)) $ filter (not . elem top) c in
  if elem [] result then [[]] else result

{-H9.2.2-}
cnf :: Form -> ConjForm
cnf (L l) = [[l]]
cnf (l :&: r) = (cnf l) ++ (cnf r)
cnf (l :|: r) = [el ++ er | el <- cnf l, er <- cnf r]

{-H9.2.3-}
-- select the first occurring variable with the truth value it has in its first occurrence.
-- This causes the first clause (with any variables) to be eliminated instantly.
-- I couldn't find a standard function which is like a filter and a map combined. I abuse concatMap for this.
selectV :: ConjForm -> Maybe (Name, Bool)
selectV = listToMaybe . concatMap (\(a, b) -> case a of T -> []; Var n -> [(n, b)]) . map (\l -> case l of Pos a -> (a, True); Neg a -> (a, False)) . concat

{-H9.2.5-}
satConj :: ConjForm -> Maybe Valuation
satConj fUnsimplified = let
    f = simpConj fUnsimplified
  in case selectV f of
    -- In simpConj, every Atom that is not Var is eliminated (because every top and bottom is eliminated, and these are the only Literals with T as the Atom).
    -- Because of this, there are exactly two possible cases where selectV returns a Nothing (given simpConj ...): [] and [[]].
    -- In simpConj, every trivially false formula is "reduced" to [[]]; and every trivially true formula to [].
    -- Because of these two statements:
    -- Iff selectV returns a Nothing, the formula is either trivially true or trivially false.
    Nothing ->
      -- Iff the simplified formula is equal to []  , the formula is trivially true; and
      -- iff the simplified formula is equal to [[]], the formula is trivially false.
      if f == [] then Just [] else Nothing
    Just (n, b) -> case (satConj $ substConj [(n, b)] f) of
      Just v -> Just $ (n, b):v
      Nothing -> case (satConj $ substConj [(n, not b)] f) of
        Just v -> Just $ (n, not b):v
        Nothing -> Nothing

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

{-TTEW-}