module Exercise_9 where
{-WETT-}

import Control.Monad
import Data.List
import Data.Maybe
import qualified Data.Map as Map

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 form = if [] `elem` shortForm then [[]] else shortForm
  where 
    shortClause cs = if any (==top) cs then [top] else filter (/=bottom) cs
    shortForm = filter (/=[top]) [shortClause cs | cs <- form]

{-H9.2.2-}
cnf :: Form -> ConjForm
cnf (L a) = [[a]]
cnf (lf :&: rf) = cnf lf ++ cnf rf
cnf (lf :|: rf) = [ cl ++ cr | cl <- cnfLf, cr <- cnfRf]
  where 
    cnfLf = cnf lf
    cnfRf = cnf rf


{-H9.2.5-}
{-MCCOMMENT
Hello MC! This is the basic, "unoptimized" solution.
It could very well be, that even this basic solution is faster then my "optimization".

auxSatConj :: ConjForm -> (Name, Bool) -> Maybe Valuation
auxSatConj cs (n, v) = 
  case eval of
      Nothing -> case negEval of 
        Nothing -> Nothing
        Just negEval -> Just ((n, not v):negEval)
      Just eval -> Just ((n, v):eval)
  where 
    eval = satConj (substConj [(n, v)] cs)
    negEval = satConj (substConj [(n, not v)] cs)

satConj :: ConjForm -> Maybe Valuation
satConj cs
  | null simp = Just []
  | simp == [[]] = Nothing
  | otherwise = case var of
    Nothing  -> Nothing
    Just val -> auxSatConj simp val 
  where
    simp = simpConj cs
    var = selectV simp
-}

type LiteralStructure = Map.Map Name [Literal]

getN :: Literal -> Maybe Name
getN (Pos T) = Nothing
getN (Neg T) = Nothing
getN (Pos (Var n)) = Just n
getN (Neg (Var n)) = Just n

updateLiteral :: [Literal] -> LiteralStructure
updateLiteral [] = Map.empty
updateLiteral (l:ls) = case getN l of
  Nothing -> child
  Just n -> case Map.lookup n child of
    Nothing -> Map.insert n [l] child
    Just ms -> Map.insert n (l:ms) child
  where
    child = updateLiteral ls

isSameSign :: [Literal] -> Bool
isSameSign [] = False
isSameSign ls = and $ zipWith sameSign ls $ drop 1 ls
    where
      sameSign :: Literal -> Literal -> Bool
      sameSign (Pos (Var _)) (Pos (Var _)) = True
      sameSign (Neg (Var _)) (Neg (Var _)) = True
      sameSign _ _ = False

oneLiteralRule :: ConjForm -> Maybe Literal
oneLiteralRule cs = (listToMaybe . concat . filter (\c -> length c == 1)) cs

pureLiteralRule :: ConjForm -> Maybe Literal
pureLiteralRule lss = if null struc then Nothing else Just v
  where
    struc = (Map.filter isSameSign . updateLiteral . concat) lss
    (k,(v:vs)) = Map.elemAt 0 struc

ruleSatConj :: ConjForm -> Literal -> Maybe Valuation
ruleSatConj cs rl = 
  case eval of
      Nothing -> Nothing
      Just eval -> Just $ (n,v):eval
  where
    (n,v) = assignLiteral rl
    eval = satConj (substConj [(n,v)] cs) 

decSatConj :: ConjForm -> (Name, Bool) -> Maybe Valuation
decSatConj cs (n, v) = 
  case eval of
      Nothing -> case negEval of 
        Nothing -> Nothing
        Just negEval -> Just $ (n, not v):negEval
      Just eval -> Just $ (n, v):eval
  where 
    eval = satConj (substConj [(n, v)] cs)
    negEval = satConj (substConj [(n, not v)] cs)

satConj :: ConjForm -> Maybe Valuation
satConj cs
  | null simp = Just []
  | simp == [[]] = Nothing
  | otherwise = case oneLiteral of
      Nothing -> case pureLiteral of
        Nothing -> case var of 
          Nothing -> Nothing
          Just var -> decSatConj simp var
        Just pl -> ruleSatConj simp pl
      Just ol -> ruleSatConj simp ol
  where
    simp = simpConj cs
    oneLiteral = oneLiteralRule simp
    pureLiteral = pureLiteralRule simp
    var = selectV simp

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


{-H9.2.3-}
assignLiteral :: Literal -> (Name, Bool)
assignLiteral (Pos (Var n)) = (n, True)
assignLiteral (Neg (Var n)) = (n, False)

auxSelectV :: Literal -> Maybe (Name, Bool)
auxSelectV (Pos T) = Nothing
auxSelectV (Neg T) = Nothing
auxSelectV l = Just (assignLiteral l)

selectV :: ConjForm -> Maybe (Name, Bool)
selectV cs = (msum . concat) [ [auxSelectV l | l <- ls] | ls <- cs]
{-TTEW-}