module Exercise09 where

import Types

import Data.List (nubBy, nub, minimumBy, sort, sortOn)
import Data.Ord (comparing, Down(Down))
import Data.Maybe

-- things from the tutorial

instance Show Polarity where
  show Pos = ""
  show Neg = "~"

instance Show ELiteral where
  show (Literal p a) = 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

-- feel free to change behaviour and type
resolve :: Name -> Clause -> Clause -> Clause
resolve n cp cn = nub $ (filter (/= (Literal Pos n)) cp) ++ (filter (/= (Literal Neg n)) cn)
--                filter (/= Literal Pos "a") [(Literal Pos "a"), (Literal Neg "a")] ++ filter (/= Literal Neg "a") [(Literal Pos "a"), (Literal Neg "a")]
--                resolve "a" [(Literal Pos "a"), (Literal Neg "a")] [(Literal Pos "a"), (Literal Neg "a")]
-- [c | c <-cp, c /= Literal Pos n ] ++ [c | c <-cn, c /= Literal Neg n]
--                [c | c <-[Literal Pos "a"], c /= Literal Pos "a" ] ++ [c | c <-[Literal Pos "a", Literal Neg "a"], c /= Literal Neg "a"]

-- feel free to change behaviour and type
resolvants :: KeyClause -> KeyClause -> [(Resolve, Clause)]
resolvants kc1 kc2 = nubBy (\a b -> snd a == snd b) [(Resolve a (fst b) (fst c), resolve a (snd b) (snd c)) | (a, b, c) <- validLiterals]
            where validLiterals = [(lName n, kc1, kc2) | n <- kc1Literals, lIsPos n, lNegate n `elem` kc2Literals] ++
                                  [(lName n, kc2, kc1) | n <- kc2Literals, lIsPos n, lNegate n `elem` kc1Literals]
                  kc1Literals = snd kc1
                  kc2Literals = snd kc2
-- proof checking

-- don't change the type nor expected behaviour
proofCheck :: EConjForm -> Proof -> Bool
proofCheck c (Model names ) = eval names c
proofCheck c (Refutation []) = [] `elem` c
proofCheck c (Refutation ((Resolve name key1 key2):xs)) = proofCheck (c ++ [resolve name (c!!key1) (c!!key2)]) (Refutation xs)

-- feel free to change behaviour and type
-- KeyConjForm -> Maybe KeyClause
selClause :: SelClauseStrategy 
selClause [] = Nothing 
selClause kcf = Just $ minimumBy (comparing (length . snd)) kcf

-- feel free to change behaviour and type
resolutionParam :: SelClauseStrategy -> EKeyConjForm -> EKeyConjForm -> [Resolve] -> Int -> (Proof, KeyConjForm)
resolutionParam _ [] p steps _
          | [] `elem` map snd p = (Refutation steps, p)
          | otherwise = (Model (extractModel (map snd p)), p)
resolutionParam selclause u p steps maxIndex
          | null (snd uc)  = (Refutation steps, p)
          | otherwise = resolutionParam selclause newU (uc:p) newSteps (maxIndex+ length addedClauses)

    where uc = fromJust (selclause u)
          newU = remove (snd uc) u ++ addedClauses
          newSteps = steps ++ map fst resolvantss -- und hier
          addedClauses = zip [maxIndex+1..maxIndex + length resolvantss] (map snd resolvantss)
          resolvantss = filter (\(_, b) -> b `notElem` map snd u && b `notElem` map snd p && (not . clauseIsTauto) b) (concat [resolvants uc ud | ud <- p])
         
--TODO: improve this
remove :: Clause -> EKeyConjForm -> EKeyConjForm
remove c conj = [a| a <- conj, snd a /= c]

{-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 :: EConjForm -> (Proof, KeyConjForm)
-- only feed non-tautologies into the resolutionparam function, but indexes must stay the same
resolution form = let newForm = filter (not . clauseIsTauto . snd) (zip [0..length form -1] form ) in resolutionParam selClause newForm [] [] (length form -1)

{-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 . map (sortOn Down)
  where
    run val [] = val
    run val (c:cs)
      | evalClause val c = run val cs
      | otherwise = run (lName (head c):val) cs