module Exercise_9 where

import Data.Maybe

import Data.Set (toList, fromList)
import qualified Data.Set as Set
import qualified Data.Map.Strict as Map
import qualified Data.Sequence as Seq
import qualified Data.Graph as Graph

{-WETT-}
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 Prelude.lookup n v of
  Just b -> if b then top else bottom
  Nothing -> l
substLiteral v l@(Neg (Var n)) = case Prelude.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 xs = 
  let
    checker [] = []
    checker (x:xs)
      | x == [] = [[]]
      | head x == top && take 2 x == [head x] = checker xs
      | elem top x = checker xs
      | head x == bottom && tail x == [] = [[]]
      | elem bottom x = (filter (/=bottom) x):checker xs
      | otherwise = x:checker xs

    checkEmpty xs = if (elem [] xs) then [[]] else xs
  in 
  checkEmpty $ checker xs

testExamples = simpConj [[ top ] , [ top , Pos $ Var " v "]] == [] && 
               simpConj [[ bottom ] , [ Neg $ Var " v "]] == [[]] && 
               simpConj [[ Neg $ Var " v "] , [ bottom , Neg $ Var " v "]] == 
                  [[ Neg ( Var " v ")] ,[ Neg ( Var " v ")]] &&
               simpConj [[ Pos$ Var " v " , bottom ] , [ Pos $ Var " v " , top ]] ==
                  [[ Pos ( Var " v ")]] &&
               simpConj [[ Neg $ Var " v "] ,[ Neg $ Var " v "] ,[ Pos $ Var " w " , Neg $ Var " w "]] ==
                  [[ Neg ( Var " v ")] ,[ Neg ( Var " v ")] ,[ Pos ( Var " w ") , Neg ( Var " w ")]]

{-H9.2.2-}
cnf :: Form -> ConjForm
cnf f = 
  let
    toCNF (a :|: (b :&: c)) = toCNF (a :|: b) :&: toCNF (a :|: c)
    toCNF ((b :&: c) :|: a) = toCNF (b :|: a) :&: toCNF (c :|: a)
    toCNF (a :|: b) = (toCNF a :|: toCNF b)
    toCNF (a :&: b) = (toCNF a :&: toCNF b)
    toCNF x = x

    -- resolution = undefined
    
    convFormConj l@(L x) = [[x]]
    convFormConj (a :|: b) = [(concat $ convFormConj a)++(concat $ convFormConj b)]
    convFormConj (a :&: b) = (convFormConj a)++(convFormConj b)

    iter f
    	| it1 == it2 = it1
    	| otherwise = iter it2
	  	where
	  		it1 = toCNF f
	  		it2 = toCNF $ it1
  in
  convFormConj $ iter f

{-H9.2.3-}
selectV :: ConjForm -> Maybe (Name, Bool)
selectV xs =
  let
    getVar (Pos (Var x)) = Just (x, True)
    getVar (Neg (Var x)) = Just (x, False)
    getVar x = Nothing

    olr [] = Nothing
    olr ((x:[]):xs) = getVar x
    olr (x:xs) = olr xs

    getInit [] = Nothing
    getInit [[]] = Nothing
    getInit (x:xs) = if (vars /= []) then head vars else getInit xs
      where
        vars = filter (/=Nothing) [getVar y|y<-x]
    h = olr xs
  in
  if (h /= Nothing) then h else getInit xs


{-H9.2.5-}
satConj :: ConjForm -> Maybe Valuation
satConj xs = 
  let
    negate (Just (x, y)) = (x, not y)

    satc [[]] _ = Nothing -- Conflict
    satc [] ys = Just ys
    satc xs ys = if (s1 /= Nothing) then s1 else s2
      where
        s1 = satc (simpConj $ substConj (sel fromJust) xs) (sel fromJust)
        s2 = satc (simpConj $ substConj (sel negate) xs) (sel negate)
        sel op = ys++(if (selectV xs == Nothing) then [] else [op $ selectV xs])

  in
  satc (simpConj xs) []

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

t1 = ((((L (Neg (Var "16")) :&: L (Pos (Var "25"))) :|: (L (Pos (Var "22")) :&: L (Pos (Var "27")))) :&: ((L (Neg T) :|: L (Pos (Var "29"))) :&: (L (Pos (Var "29")) :&: L (Pos (Var "27"))))) :&: (((L (Pos (Var "15")) :&: L (Neg (Var "23"))) :&: (L (Neg (Var "1")) :&: L (Neg (Var "10")))) :|: ((L (Pos (Var "29")) :|: L (Neg (Var "7"))) :&: (L (Neg (Var "27")) :&: L (Pos (Var "26"))))))
t2 = ((((L (Pos (Var "158")) :|: L (Neg (Var "128"))) :&: (L (Pos (Var "124")) :|: L (Pos (Var "143")))) :|: ((L (Pos (Var "154")) :|: L (Neg (Var "118"))) :|: (L (Neg (Var "101")) :|: L (Neg (Var "35"))))) :|: (((L (Pos (Var "127")) :|: L (Neg (Var "115"))) :&: (L (Pos (Var "165")) :|: L (Pos (Var "114")))) :&: ((L (Pos (Var "42")) :&: L (Neg (Var "67"))) :&: (L (Pos (Var "24")) :&: L (Neg (Var "82")))))) :|: ((((L (Neg T) :&: L (Pos (Var "128"))) :&: (L (Neg (Var "60")) :&: L (Neg (Var "176")))) :&: ((L (Pos (Var "161")) :|: L (Neg (Var "12"))) :&: (L (Neg (Var "142")) :|: L (Neg (Var "151"))))) :|: (((L (Neg (Var "71")) :|: L (Neg (Var "110"))) :&: (L (Pos (Var "59")) :|: L (Pos (Var "96")))) :&: ((L (Neg (Var "102")) :&: L (Pos (Var "50"))) :|: (L (Pos (Var "180")) :&: L (Pos (Var "175"))))))
t3 = ((((((L (Neg (Var "156")) :&: L (Neg (Var "52"))) :|: (L (Pos (Var "11")) :&: L (Pos (Var "15")))) :&: ((L (Pos (Var "49")) :|: L (Neg (Var "99"))) :&: (L (Pos (Var "76")) :&: L (Neg (Var "102"))))) :|: (((L (Pos (Var "34")) :&: L (Pos (Var "65"))) :|: (L (Neg (Var "54")) :&: L (Neg (Var "115")))) :|: ((L (Pos (Var "109")) :&: L (Neg (Var "101"))) :|: (L (Pos (Var "120")) :|: L (Pos (Var "53")))))) :&: ((((L (Neg (Var "127")) :|: L (Pos (Var "103"))) :|: (L (Pos (Var "33")) :&: L (Neg (Var "89")))) :&: ((L (Neg (Var "73")) :|: L (Pos (Var "3"))) :|: (L (Neg (Var "30")) :|: L (Pos (Var "83"))))) :|: (((L (Neg (Var "19")) :&: L (Neg (Var "25"))) :&: (L (Neg (Var "47")) :&: L (Pos (Var "55")))) :|: ((L (Neg (Var "29")) :&: L (Neg (Var "159"))) :|: (L (Pos (Var "68")) :&: L (Neg (Var "130"))))))) :|: (((((L (Pos (Var "47")) :|: L (Pos (Var "11"))) :&: (L (Neg (Var "142")) :&: L (Neg (Var "73")))) :|: ((L (Neg (Var "10")) :&: L (Pos (Var "69"))) :&: (L (Pos (Var "10")) :&: L (Pos (Var "81"))))) :&: (((L (Pos (Var "62")) :|: L (Neg T)) :|: (L (Neg (Var "3")) :|: L (Pos (Var "146")))) :|: ((L (Neg (Var "15")) :|: L (Neg (Var "159"))) :|: (L (Neg (Var "40")) :|: L (Pos (Var "60")))))) :&: ((((L (Pos (Var "115")) :&: L (Neg (Var "45"))) :&: (L (Neg (Var "6")) :&: L (Pos (Var "22")))) :&: ((L (Neg (Var "53")) :&: L (Neg (Var "109"))) :&: (L (Pos (Var "109")) :&: L (Neg (Var "66"))))) :|: (((L (Pos (Var "80")) :&: L (Neg (Var "7"))) :|: (L (Pos (Var "67")) :|: L (Neg (Var "115")))) :|: ((L (Pos (Var "92")) :&: L (Pos (Var "145"))) :&: (L (Neg (Var "79")) :&: L (Neg (Var "105"))))))))
t31 = t2 :&: (t3 :|: t1)
t311 = cnf t31
t4 = ((((L (Pos (Var "6")) :&: L (Neg (Var "27"))) :&: (L (Neg T) :&: L (Pos T))) :|: ((L (Neg (Var "5")) :|: L (Neg (Var "26"))) :&: (L (Neg (Var "46")) :&: L (Pos (Var "46"))))) :&: (((L (Pos (Var "2")) :|: L (Pos (Var "23"))) :&: (L (Pos (Var "9")) :|: L (Neg (Var "10")))) :|: ((L (Pos (Var "20")) :&: L (Pos (Var "6"))) :&: (L (Pos (Var "26")) :|: L (Pos (Var "31"))))))
t41 = cnf t4
{-TTEW-}