module Exercise_9 where
{-WETT-}

import           Data.Function
import           Data.List
import           Data.Maybe
import qualified Data.Map                      as Map


type Name = String
type Valuation = [(Name, Bool)]
type Valuation2 = Map.Map Name Bool -- Map Type
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 _ l = l


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

substConj :: Valuation -> ConjForm -> ConjForm
substConj = map . substClause

-- Versions using Map
substLiteral2 :: Valuation2 -> Literal -> Literal
substLiteral2 v l@(Pos (Var n)) = case Map.lookup n v of
  Just b  -> if b then top else bottom
  Nothing -> l
substLiteral2 v l@(Neg (Var n)) = case Map.lookup n v of
  Just b  -> if b then bottom else top
  Nothing -> l
substLiteral2 _ l = l

substClause2 :: Valuation2 -> Clause -> Clause
substClause2 = map . substLiteral2

substConj2 :: Valuation2 -> ConjForm -> ConjForm
substConj2 = map . substClause2

{-H9.2.1-}
simpConj :: ConjForm -> ConjForm
simpConj [] = []
simpConj (x : xs) | null simpx     = [[]]
                  | simpxs == [[]] = [[]]
                  | simpx == [top] = simpxs
                  | otherwise      = simpx : simpxs
 where
  simpx  = simpClause x
  simpxs = simpConj xs

simpClause :: Clause -> Clause
simpClause [] = []
simpClause (x : xs) | simp == [top] = [top]
                    | x == top      = [top]
                    | x == bottom   = simp
                    | otherwise     = x : simp
  where simp = simpClause xs
{-H9.2.2-}
cnf :: Form -> ConjForm
cnf (L l      ) = [[l]]
cnf (f1 :&: f2) = cf1 ++ cf2
 where
  cf1 = cnf f1
  cf2 = cnf f2
cnf (f1 :|: f2) = [ c1 ++ c2 | c1 <- cnf f1, c2 <- cnf f2 ]

{-H9.2.3-}

selectV :: ConjForm -> Maybe (Name, Bool)
selectV []                       = Nothing
selectV ((Pos (Var n) : _ ) : _) = Just (n, True)
selectV ((Neg (Var n) : _ ) : _) = Just (n, False)
selectV ((_           : cs) : l) = selectV (cs : l)
selectV ([]                 : l) = selectV l

-- !! unsafe version (Assumes the formula is simplified) !!
-- Take most accuring Variable in the shortest clause
selectV' :: ConjForm -> Maybe (Name, Bool)
selectV' []       = Nothing
selectV' (c : cs) = getAssignment $ maximumBy
  (compare `on` fromJust . flip Map.lookup occ . fromJust . getName)
  c
 where
  occ =
    Map.fromList
      $ map (\c' -> (fromJust $ getName $ head c', length c'))
      $ groupBy ((==) `on` getName)
      $ sortOn (fromJust . getName)
      $ concat (c : cs)

-- Assignment to make the Variable True
getAssignment :: Literal -> Maybe (Name, Bool)
getAssignment (Pos (Var n)) = Just (n, True)
getAssignment (Neg (Var n)) = Just (n, False)
getAssignment _             = Nothing
{-H9.2.5-}
satConj :: ConjForm -> Maybe Valuation
satConj f | null plr_f            = Just $ v1 ++ v2
          | [] `elem` plr_f       = Nothing
          | not $ null $ v1 ++ v2 = select $ satConj plr_f
          | isJust c1             = Just $ (v, b) : fromJust c1
          | isJust c2             = Just $ (v, not b) : fromJust c2
          | otherwise             = Nothing
 where
  f'          = simpConj f
  (olr_f, v1) = olr f'
  (plr_f, v2) = plr olr_f
  (v    , b ) = fromJust $ selectV' $ sortOn length plr_f
  select p = case p of
    Nothing  -> Nothing
    Just val -> Just $ v1 ++ v2 ++ val
  c1 = select $ satConj $ substConj [(v, b)] plr_f
  c2 = select $ satConj $ substConj [(v, not b)] plr_f

-- One Literal Rule
olr :: ConjForm -> (ConjForm, Valuation)
olr f = (simpConj $ substConj2 (Map.fromList substitutions) f, substitutions)
  where substitutions = valTru [ u | [u] <- f ]

-- Substitutions that make the literals True
valTru :: [Literal] -> Valuation
valTru []                 = []
valTru (Pos (Var n) : us) = (n, True) : valTru us
valTru (Neg (Var n) : us) = (n, False) : valTru us
valTru (_           : us) = valTru us

-- Gets a list of pure Literals
pures :: ConjForm -> [Literal] --Assumption: f is simplified
pures f =
  concat
    $ filter ((== 1) . length)
    $ map nub
    $ groupBy ((==) `on` getName)
    $ sortOn (fromJust . getName)
    $ concat f

-- Extract Name from Literal
getName :: Literal -> Maybe Name
getName (Pos (Var n)) = Just n
getName (Neg (Var n)) = Just n
getName _             = Nothing
-- Pure literal Rule
plr :: ConjForm -> (ConjForm, Valuation)
plr f = (simpConj $ substConj2 (Map.fromList substitutions) f, substitutions)
  where substitutions = valTru $ pures f
{-H9.2.6-}
sat :: Form -> Maybe Valuation
sat = satConj . cnf
{-TTEW-}