module Exercise09 where

import Types
import Data.List (sort, sortOn)
import Data.Ord (Down(Down))
import Data.Set
import Data.Maybe


-- things from the tutorial
instance Show Polarity where
  show Pos = "Pos"
  show Neg = "Neg"

instance Show ELiteral where
  show (Literal p a) = "Literal " ++ show p ++ " \"" ++ a ++ "\""

lName :: Literal -> Name
lName (Literal _ n) = n

lPos :: Name -> Literal
lPos = Literal Pos

lNeg :: Name -> Literal
lNeg = Literal Neg

lIsPos :: Literal -> Bool
lIsPos (Literal p _) = p == Pos

lIsNeg :: Literal -> Bool
lIsNeg = not . lIsPos

lNegate :: Literal -> Literal
lNegate (Literal Pos n) = Literal Neg n
lNegate (Literal Neg n) = Literal Pos n

complements :: Literal -> Literal -> Bool
complements (Literal p n) (Literal p' n') = p /= p' && n == n'

evalLiteral :: Valuation -> Literal -> Bool
evalLiteral val l@(Literal _ n)
  | lIsPos l  = n `elem` val
  | otherwise = n `notElem` val

evalClause :: Valuation -> Clause -> Bool
evalClause = any . evalLiteral

eval :: Valuation -> ConjForm -> Bool
eval = all . evalClause

clauseIsTauto :: Clause -> Bool
clauseIsTauto [] = False
clauseIsTauto (l:ls) = lNegate l `elem` ls || clauseIsTauto ls

-- homework starts here

without :: Eq a => [a] -> a -> [a]
without xs l = [y | y <- xs, y /= l]

-- feel free to change behaviour and type
resolve :: Name -> Clause -> Clause -> Clause
resolve name cp cn = unify (cp `without` (Literal Pos name)) (cn `without` (Literal Neg name))

resolveSet :: Name -> Set Literal -> Set Literal -> Set Literal
resolveSet name cp cn =  (delete (Literal Pos name) cp) `union` (delete (Literal Neg name) cn)

unify:: Clause -> Clause -> Clause
unify lc rc = [a | a <- lc] ++ [a | a <- rc, a `notElem` lc]

-- feel free to change behaviour and type
resolvants ::  (Key, Set Literal) -> (Key, Set Literal) -> [(Resolve, Set Literal)]
resolvants (k1,c1) (k2,c2) = [if (Literal Pos name) `member` c1 then ((Resolve name k1 k2),resolveSet name c1 c2) else ((Resolve name k2 k1),resolveSet name (c2) c1) | name <- findAllResolveNames (k1,c1) (k2,c2)]

findAllResolveNames ::  (Key, (Set Literal)) ->  (Key, (Set Literal)) -> [Name]
findAllResolveNames (k1,c1) (k2,c2) = [name (elemAt i c1) | i <- [0..(size c1)-1], any ((`complements` (elemAt i c1))) c2]


findAllNames ::  (Set Literal) -> Set Name
findAllNames (c1) = Data.Set.map (\s -> name s) c1

name (Literal a b) = b

-- proof checking

-- don't change the type nor expected behaviour
proofCheck :: ConjForm -> Proof -> Bool
proofCheck cs (Model names) = eval names cs
proofCheck cs (Refutation xs) = proofCheckRef cs xs

proofCheckRef:: ConjForm -> [Resolve] -> Bool
proofCheckRef (cs) [] | [] `elem` cs = True
                      | otherwise = False
proofCheckRef (cs) ((Resolve name k1 k2):xs) | [] `elem` cs = True
                                             | otherwise = if Exercise09.empty (resolve name (cs !! k1) (cs !! k2)) then True
                                                           else proofCheckRef (cs ++ [(resolve name (cs !! k1) (cs !! k2))]) xs

empty [] = True
empty (x:xs) = False

emptyMaybe (Just []) = True
emptyMaybe Nothing = True
emptyMaybe (Just (x:xs)) = False

-- feel free to change behaviour and type
selClause :: SelClauseStrategy
selClause sset | Data.Set.null sset = Nothing
               | otherwise = Just (Data.Set.foldl (\(c1 , lacc) (c2, r) -> if (size (findAllNames r)) < (size (findAllNames lacc)) then (c2,r) else (c1,lacc)) (elemAt 0 sset) sset)

-- feel free to change behaviour and type
resolutionParam :: SelClauseStrategy -> ConjForm -> (Proof, KeyConjForm)
resolutionParam ss cf = algorithm (k cf) (fromList []) [] (fromList [fromList $ c | c <- cf]) (size $ (k2 cf))
  where
    k cf = fromList $ cleanStart $ [(i, (fromList $ (cf !! i))) | i <- [0..(length cf) - 1]]
    k2 cf = fromList $ [(i, (fromList $ (cf !! i))) | i <- [0..(length cf) - 1]]


algorithm :: Set (Key, Set Literal)  -> Set (Key, Set Literal) -> [EResolve]  -> Set (Set Literal) -> Int -> (Proof, KeyConjForm)
algorithm unprocessed processed rsteps allC totallength | Data.Set.null unprocessed = ((Model (extractModel (toConjForm2 (Prelude.map (convertToList) (toList $ processed))))), [])
                                                        | Data.Set.null (snd uc) = ((Refutation rsteps), [])
                                                        | otherwise = algorithm ((knu) `union` (delete uc unprocessed)) (insert uc processed) (rsteps ++ nr) (Data.Set.union (fromList $ nu) allC) (totallength + size knu)
                                                         where
                                                            uc = fromJust (selClause unprocessed)
                                                            (nr, nu) =  clean (unpack [resolvants uc (elemAt i processed) | i <- [0..(size $ processed)-1]]) allC
                                                            knu = (toKey nu totallength)

toKey:: [(Set Literal)] -> Int -> Set (Int, Set Literal)
toKey as l  = fromList [(i + l, (as !! i)) | i <- [0..length as - 1]]

convertToList:: (Key, Set Literal) -> (Key, [Literal])
convertToList (k,l) = (k, (toList $ l))


notInKey:: Clause -> KeyConjForm -> Bool
notInKey c cs = notIn c (toConjForm2 cs)

notIn c cs = all (\k -> (c /= k)) cs

cleanStart::  [(Key, Set Literal)] -> [(Key, Set Literal)]
cleanStart [] = []
cleanStart ((a,b):as) | (b `notMember` (fromList (Prelude.map snd as))) && (not $ (subSummed b (fromList (Prelude.map snd as)))) && (not $ clauseIsTauto (toList b)) = ((a,b):(cleanStart as))
                      | otherwise = (cleanStart as)


clean:: ([Resolve], [(Set Literal)]) -> Set (Set Literal) -> ([Resolve], [(Set Literal)])
clean ([], b) clauses = ([], [])
clean (a, []) clauses = ([], [])
clean ((a:as),(b:bs)) clauses | (b `notMember` ((fromList bs) `union` clauses)) &&  (not $ (subSummed b ((fromList bs) `union` clauses))) &&  (not $ clauseIsTauto (toList b)) = addTL (a,b) (clean (as,bs) clauses)
                              | otherwise = (clean ((as),bs) clauses)
                                where
                                  addTL (a,b) (as,bs) = ((a:as), (b:bs))

unpack:: [[(Resolve, Set Literal)]] -> ([Resolve], [(Set Literal)])
unpack cs  = Prelude.foldl (\(accr, accl) list -> ((Prelude.map fst list) ++ accr, (Prelude.map snd list) ++ accl)) ([],[]) cs

toConjForm2:: KeyConjForm -> ConjForm
toConjForm2 kf = Prelude.map snd kf

subSummed:: Set Literal -> Set (Set Literal) -> Bool
subSummed a bs = any (\b -> b `isSubsetOf` a) bs

{-WETT-}

-- don't change the type; instantiate your best resolution prover here
-- Please leave some comments for the MC Jr to understand your ideas and code :')
resolution :: ConjForm -> (Proof, KeyConjForm)
resolution = resolutionParam selClause

{-TTEW-}

-- extract a model as described on https://lara.epfl.ch/w/_media/sav08/gbtalk.pdf

instance Ord Polarity where
  Neg <= Pos = False
  _ <= _ = True

instance Ord ELiteral where
  (Literal p a) <= (Literal p' a') = a < a' || a == a' && p <= p'

extractModel :: ConjForm -> Valuation
extractModel = run [] . sort . Prelude.map (sortOn Down)
  where
    run val [] = val
    run val (c:cs)
      | evalClause val c = run val cs
      | otherwise = run (lName (head c):val) cs

main:: IO()
main = do
        print $ show (fst $ resolutionParam (selClause) [[Literal Neg "1",Literal Neg "7"],[Literal Pos "5",Literal Pos "1",Literal Pos "3"],[Literal Neg "3",Literal Pos "7",Literal Neg "5"]])