module Exercise_9 where
{-WETT-}
import Data.Maybe
import Data.List
import Data.Function
import Data.Ord
import qualified Data.HashMap.Lazy as HashMap

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-}


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

{-H9.2.3-}
selectLiteral :: Literal -> Maybe (Name, Bool)
selectLiteral (Pos (Var name)) = Just(name, True)
selectLiteral (Neg (Var name)) = Just(name, False)
selectLiteral _ = Nothing


selectV :: ConjForm -> Maybe (Name, Bool)
selectV [] = Nothing
selectV css = fromMaybe Nothing $ fromMaybe Nothing $ find isJust $ map (find isJust) $ [map selectLiteral cs | cs <- css]


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


compSubstLiteral :: (Name,Bool) -> Literal -> Literal
compSubstLiteral (name,bool) l@(Pos (Var n)) = if n == name then (if bool then top else bottom) else l
compSubstLiteral (name,bool) l@(Neg (Var n))= if n ==  name then (if bool then bottom else top) else l
compSubstLiteral v l = l

compSubstConj :: (Name,Bool) -> ConjForm -> ConjForm
compSubstConj = map . map . compSubstLiteral


compSubstListLiteral :: Valuation -> Literal -> Literal
compSubstListLiteral v l@(Pos (Var n)) = case lookup n v of
  Just b -> if b then top else bottom
  Nothing -> l
compSubstListLiteral v l@(Neg (Var n)) = case lookup n v of
  Just b -> if b then bottom else top
  Nothing -> l
compSubstListLiteral v l = l

compSubstListConj :: Valuation -> ConjForm -> ConjForm
compSubstListConj = map . map . compSubstListLiteral

literalToName::Literal -> Name
literalToName (Pos (Var name)) = name
literalToName (Neg (Var name)) = name
literalToName _ = []

conjFormToNames::ConjForm -> [Name]
conjFormToNames = (filter (not . null)) . (map literalToName) . concat

literalToVal::Literal -> Maybe (Name,Bool)
literalToVal (Pos (Var n)) = Just(n,True)
literalToVal (Neg (Var n)) = Just(n,False)
literalToVal _ = Nothing

literalToVal2::Literal -> Maybe (Name,Maybe Bool)
literalToVal2 (Pos (Var n)) = Just(n,Just True)
literalToVal2 (Neg (Var n)) = Just(n,Just False)
literalToVal2 _ = Nothing

compSelectV::ConjForm -> Name
compSelectV css = head $ conjFormToNames css

simplifyCtoTop :: ConjForm -> ConjForm
simplifyCtoTop css = [ if top `elem` cs then [top] else cs | cs <- css]

removeBottoms :: ConjForm -> ConjForm
removeBottoms css = [ filter (/= bottom) cs | cs <- css]

removeTops::ConjForm -> ConjForm
removeTops css = filter (/= [top]) css

simplifyEmpty :: ConjForm -> ConjForm
simplifyEmpty css = if [] `elem` css then [[]] else css

simpConj :: ConjForm -> ConjForm
simpConj = simplifyEmpty . removeTops . removeBottoms . simplifyCtoTop

getPure :: ConjForm -> Valuation
getPure css =
  let
    vals = catMaybes $ map literalToVal2 $ nub $concat css
    handleClash (Just a) (Just b) = if a == b then Just a else Nothing
    handleClash _ _ = Nothing
    hash = HashMap.fromListWith handleClash vals
    pures = [ (name,bool) | (name,Just bool) <- vals, isJust $ hash HashMap.! name]
  in
    pures


satConjHelper:: Valuation ->ConjForm->Maybe Valuation
satConjHelper val f  =
  let
    --sort to select variable from small clause
    f' = sortBy (comparing length) $ simpConj f
  in
    if null f' then Just val
    else if [] `elem` f' then Nothing
    else
      let
        -- unit propagation
        units =  nub $ catMaybes (map literalToVal $ concat $ takeWhile (null . tail) f')
        unitProp = compSubstListConj units f'
        -- pure literal elimination
        pures = getPure unitProp
        replacements = units ++ pures
        --preprocessed
        f'' = compSubstListConj replacements f'
        val' = replacements ++ val

      in
        if length ((nubBy ((==) `on` fst)) units) /= length units
        then Nothing
        else
        if null $ simpConj f'' then Just val' else
          let
            name = compSelectV f''
            v = (name,True)
            w = (name,False)
            first = satConjHelper (v:val') (compSubstConj v f'')
          in
            if isJust first then first else satConjHelper (w:val') (compSubstConj w f'')

satConj :: ConjForm -> Maybe Valuation
satConj css  = (satConjHelper [] css)
{-TTEW-}