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 x = funD (funC (funB (funA x)))


funA1 :: Clause -> Bool
funA1 [] = False
funA1 (x:xs) 
  |x == top = True
  |otherwise = funA1 xs

funA :: ConjForm -> ConjForm
funA [] = []
funA (x:xs) 
  |funA1 x = [[top]] ++ funA xs
  |otherwise = [x] ++ funA xs

funB1 :: Clause -> Clause
funB1 [] = []
funB1 (x:xs) 
  |x == bottom = funB1 xs
  |otherwise = [x] ++ funB1 xs

funB :: ConjForm -> ConjForm
funB [] = []
funB (x:xs) = [funB1 x]  ++ funB xs

funC :: ConjForm -> ConjForm
funC [] = []
funC (x:xs) 
  |funA1 x = funC xs
  |otherwise = [x] ++ funC xs

funD1 :: ConjForm -> Bool
funD1 [] = False
funD1 (x:xs) 
  |x == [] = True
  |otherwise = funD1 xs

funD :: ConjForm -> ConjForm
funD [] = []
funD x 
  |funD1 x = [[]]
  |otherwise = x 


testA =  [[Pos$Var "v", bottom], [Pos$Var "v", top]] -- = [[Pos (Var "v")]]
testB =  [[Neg$Var "v"],[Neg$Var "v"],[Pos$Var "w", Neg$Var "w"]] -- = [[Neg (Var "v")],[Neg (Var "v")],[Pos (Var "w"),Neg (Var "w")]]

--conjForm = [Clause] (x:xs) = [[Literal]] ((y:ys):xs) = [[Pos Atom | Neg Atom]] == [[(T | Var Name) | (T | Var Name))]]

{-H9.2.2-}

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

cnf :: Form -> ConjForm
cnf (L a)  = [[a]]
cnf (a :&: b) = cnf a ++ cnf b
cnf (a :|: b) = funF aRec bRec  where 
  aRec  = cnf a 
  bRec  = cnf b
  
testCNF2 = ((L (Neg (Var "10")) :|: L (Neg (Var "24"))) :|: (L (Neg (Var "7")) :|: L (Neg (Var "31")))) 

testCNF3 = ((L (Neg (Var "10")) :&: L (Neg (Var "24"))) :|: (L (Neg (Var "7")) :&: L (Neg (Var "31")))) 


(a,b,c,d) = (Pos (Var "a"), Pos (Var "b"),Pos (Var "c"), Pos (Var "d"))

funE :: Clause -> ConjForm -> ConjForm
funE x [] = []
funE x (y:ys) = [x ++ y] ++ funE x ys

funF :: ConjForm -> ConjForm -> ConjForm
funF [] ys = []
funF (x:xs) ys = funE x ys ++ funF xs ys



{-H9.2.3-}
selectV :: ConjForm -> Maybe (Name, Bool)
selectV x 
  |y == [] || y == [[]] = Nothing
  |b == T = selectV ([tail(head y)] ++ (tail y))
  |otherwise = Just ((a, True))
  where 
    y = funG x
    b = funH (head (head y))
    Var a = b


selectVNeg :: ConjForm -> Maybe (Name, Bool)
selectVNeg x 
    |y == [] || y == [[]] = Nothing
    |b == T = selectV ([tail(head y)] ++ (tail y))
    |otherwise = Just ((a, False))
    where 
      y = funG x
      b = funH (head (head y))
      Var a = b

funG :: ConjForm -> ConjForm
funG [] = []
funG (x:xs) 
    |x == [] = funG xs
    |otherwise = (x:xs)

funH :: Literal -> Atom
funH (Pos g) = g
funH (Neg g) = g

testH = Neg $ Var "v"

funI :: Atom -> Name
funI T =  ""
--FunI (Var a) = a

{-H9.2.5-}


--type Valuation = [(Name,Bool)]


satConj :: ConjForm -> Maybe Valuation
satConj x 
    |y == [] = Just []
    |y == [[]] = Nothing
    |recT /= Nothing = Just ([a] ++ c )
    |recF /= Nothing = Just ([b] ++ d)
    |otherwise = Nothing
    where
        y =  simpConj x
        Just a = selectV y
        Just b = selectVNeg y
        t = substConj [a] y 
        f = substConj [b] y
        recT = satConj t
        recF = satConj f
        Just c = recT
        Just d = recF







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




testM = [[Neg (Var "32"),Pos (Var "42"),Pos (Var "49"),Pos T,Neg (Var "30"),Neg (Var "65"),Neg (Var "51")],[Neg (Var "2"),Neg (Var "35"),Neg T],[Pos T,Neg (Var "14")],[Pos (Var "64"),Pos (Var "46"),Pos T,Neg (Var "13"),Neg (Var "24")],[],[Pos (Var "44")],[Pos (Var "44"),Neg (Var "4"),Neg (Var "35"),Pos T],[Neg T],[],[Pos T,Pos T,Neg (Var "22"),Neg (Var "10"),Pos T,Neg T],[Neg (Var "59"),Pos (Var "24"),Neg T,Neg T,Neg T,Pos T,Neg (Var "3")],[Pos T,Neg (Var "8"),Neg T,Neg (Var "62")],[Neg T,Pos (Var "16"),Pos (Var "39")],[Pos T],[Neg T,Pos T,Neg T,Pos T],[Neg (Var "18"),Pos T,Pos T],[Neg T,Neg T,Pos (Var "16"),Neg T,Pos (Var "8"),Pos T,Pos T],[Pos (Var "56"),Pos T,Neg (Var "48"),Pos T],[Neg T,Neg T,Neg (Var "30"),Pos (Var "57"),Pos T,Pos T],[Neg T,Neg T],[Neg (Var "57")],[Pos T,Neg (Var "29")],[Pos (Var "61")],[Neg (Var "23"),Neg T,Pos T],[Neg T,Neg (Var "66"),Neg (Var "39"),Neg (Var "61"),Pos T],[Pos T,Neg (Var "54")],[Pos (Var "27"),Neg T,Neg T,Pos (Var "46"),Pos (Var "55")],[Neg T,Neg T],[Neg T,Pos T,Pos T,Neg T],[Neg (Var "5"),Pos T,Neg (Var "69"),Neg T,Neg T],[Neg (Var "38"),Neg (Var "48"),Neg T,Neg (Var "21"),Neg (Var "44"),Pos (Var "8"),Neg (Var "40")],[Pos (Var "22"),Neg (Var "9")],[],[Neg (Var "28"),Pos (Var "66"),Neg T,Neg (Var "42"),Pos T,Neg (Var "49"),Neg T],[Neg T,Pos T,Pos T],[Neg T,Neg T,Neg (Var "58"),Pos (Var "54")]]

testX = (((L (Neg (Var "50")) :|: L (Neg (Var "16"))) :|: (L (Pos (Var "3")) :|: L (Pos T))) :&: ((L (Pos T) :|: L (Neg (Var "21"))) :&: (L (Neg (Var "3")) :|: L (Pos (Var "29"))))) :|: (((L (Neg (Var "22")) :&: L (Pos (Var "42"))) :|: (L (Pos (Var "2")) :|: L (Neg (Var "6")))) :|: ((L (Pos (Var "21")) :&: L (Pos (Var "8"))) :&: (L (Pos (Var "6")) :|: L (Pos (Var "13")))))
testCNF = (((L (Pos (Var "2")) :&: L (Pos (Var "28"))) :&: (L (Pos (Var "12")) :|: L (Pos (Var "5")))) :|: ((L (Neg (Var "1")) :&: L (Neg (Var "18"))) :|: (L (Pos (Var "45")) :|: L (Pos (Var "20"))))) :&: (((L (Neg (Var "40")) :&: L (Pos (Var "9"))) :|: (L (Pos (Var "45")) :|: L (Neg (Var "12")))) :&: ((L (Pos (Var "28")) :&: L (Pos (Var "38"))) :&: (L (Neg (Var "16")) :&: L (Neg (Var "1")))))

{-TTEW-}