module Exercise09 where

import Types

import Data.List
import Data.Maybe
import Data.Ord (Down(Down))

--import Debug.Trace

-- 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 (delete (lPos n) (nub cp) ++ delete (lNeg n) (nub cn))

-- feel free to change behaviour and type
resolvants :: KeyClause -> KeyClause -> [(Resolve, Clause)]
resolvants (k1, c1) (k2, c2) = [if lIsPos l then (Resolve (lName l) k1 k2, resolve (lName l) c1 c2) else (Resolve (lName l) k2 k1, resolve (lName l) c2 c1) | l <- c1, lNegate l `elem` c2]

-- proof checking

-- don't change the type nor expected behaviour
proofCheck :: ConjForm -> Proof -> Bool
proofCheck conj (Model val) = eval val conj
proofCheck conj (Refutation []) = [] `elem` conj
proofCheck conj (Refutation ((Resolve n k1 k2):rs)) 
  | lPos n `elem` (conj !! k1) = proofCheck (conj ++ [resolve n (conj !! k1) (conj !! k2)]) (Refutation rs)
  | otherwise = proofCheck (conj ++ [resolve n (conj !! k2) (conj !! k1)]) (Refutation rs)

-- feel free to change behaviour and type
selClause :: SelClauseStrategy 
selClause [] = (Nothing, [])
selClause (x:xs) = (Just x, xs)

-- feel free to change behaviour and type
resolutionParam :: SelClauseStrategy -> KeyConjForm -> KeyConjForm -> [EResolve] -> Int -> (Proof, KeyConjForm)
resolutionParam _ [] p _ _ = (Model (extractModel (map snd p)), p)
resolutionParam fSel u p r k = let (ucJ, u') = fSel (sortOn (length . snd) u) in
                               let uc = fromJust ucJ in if null (snd uc) then (Refutation r, uc:p) 
  else let nRes = newResolvants uc p (map snd u') in resolutionParam fSel (nub (u' ++ conjToKeyConj k (nub (map snd nRes)))) (uc:p) (r ++ map fst nRes) (k + length nRes)

newResolvants :: KeyClause -> KeyConjForm -> ConjForm -> [(Resolve, Clause)]
newResolvants uc p u = let pConj = map snd p in nub (concat [filter (\(_, c) -> not (clauseIsTauto c || c `elem` pConj || c `elem` u)) (resolvants uc pc) | pc <- p])
--newResolvants uc p u = trace (show uc) (let pConj = map snd p in nub (concat [filter (\(_, c) -> not (clauseIsTauto c || c `elem` pConj || c `elem` u)) (resolvants uc pc) | pc <- p]))

conjToKeyConj :: Int -> ConjForm -> KeyConjForm
conjToKeyConj i = zip [i..]

{-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 conj = let kcf = conjToKeyConj 0 conj in resolutionParam selClause (filter (\(k, c) -> not (clauseIsTauto c)) kcf) [] [] (length kcf)

-- 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

makeInputAux :: [Char] -> ConjForm
makeInputAux [] = []
makeInputAux ('[':xs) = makeInputAux xs
makeInputAux (']':xs) = makeInputAux xs
makeInputAux (',':xs) = makeInputAux xs
makeInputAux xs = let   clause_string = takeWhile (/= ']') xs
                        a = clauseFromString clause_string in
                          a:makeInputAux(xs\\clause_string)

clauseFromString :: [Char] -> Clause
clauseFromString [] = []
clauseFromString (',':xs) = clauseFromString xs
clauseFromString ('~':xs) = let   name = takeWhile (/= ',') xs in
                              Literal Neg name:clauseFromString (xs\\name)
clauseFromString xs = let   name = takeWhile (/= ',') xs
                                in
                              Literal Pos name:clauseFromString (xs\\name)
input :: String 
input = "[[1,~4,7,3,3],[~7,~8],[~1,~4,~4,~7],[~6,~4,~7,4,2],[~5,~6,7,~3,~3],[8,4,8,7,~6],[4,~5,5],[~8,1],[~7,2,8,~5],[~1],[2,~4,1],[~8,~4],[~6,~6],[~2,7,~8,8],[4],[2],[1,1,3],[8,4],[~4,8,4,~7],[3,~5,2,6],[7,4,4,~4],[3,~5],[~6,~7,8],[~2,4,~4,2],[5,5,~2],[1,~7],[8,8,8,4,8],[8,3]]"

input2 :: String
input2 = "[[1,~4,7,3,3],[~7,~8],[~1,~4,~4,~7],[~6,~4,~7,4,2],[~5,~6,7,~3,~3],[8,4,8,7,~6]]"