module Exercise09 where

import Types

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

-- 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([(Literal p en) | (Literal p en)<-cp, en /= n || p == Neg] ++ [(Literal p en) | (Literal p en)<-cn, en /= n ||p == Pos])

-- feel free to change behaviour and type
resolvants :: KeyClause -> KeyClause -> [(Resolve, Clause)]
resolvants c1 c2 = [((Resolve n (fst(c1)) (fst(c2))), resolve n (snd(c1)) (snd(c2))) | n <- [en | (Literal Pos en) <- snd(c1)], x<-[en | (Literal Neg en) <- snd(c2)], x == n] ++ [((Resolve n (fst(c2)) (fst(c1))), resolve n (snd(c2)) (snd(c1))) | n <- [en | (Literal Neg en) <- snd(c1)], x<-[en | (Literal Pos en) <- snd(c2)], x == n]

-- proof checking
recursiveCheck :: EKeyConjForm -> [EResolve] -> Bool
recursiveCheck fs xs
  | not (null [x | (y,x)<-fs, null x]) = True
  | null xs = False
  | otherwise = recursiveCheck (fs ++ [(length fs, resolve nam (snd(fs!!c1)) (snd(fs!!c2)))]) (tail xs)
  where (Resolve nam c1 c2) = head(xs)

-- don't change the type nor expected behaviour
proofCheck :: EConjForm -> Proof -> Bool
proofCheck f (Refutation xs) = recursiveCheck [(i, f !! i) | i <- [0..(length f)-1]] xs
proofCheck f (Model xs) = eval xs f

-- feel free to change behaviour and type
selClause :: SelClauseStrategy 
selClause i xs
  | null xs = Nothing
  | otherwise = Just (last xs)

removeFrom :: EKeyConjForm -> KeyClause -> EKeyConjForm
removeFrom [] _ = []
removeFrom xs (key2, y) = [(key, x) | (key, x)<-xs, key /= key2]

recursiveResolve :: SelClauseStrategy -> Int -> EKeyConjForm -> EKeyConjForm -> [EResolve] -> (Proof, KeyConjForm)
recursiveResolve _ _ [] processed xs = (Model (extractModel [clause | (key,clause) <- processed]), processed)
recursiveResolve strat counter unprocessed processed steps
  | null [key | (key, clause)<-unprocessed, null clause] = recursiveResolve strat (counter + length newSteps) ((removeFrom unprocessed uc)++newClauses) (processed ++ [uc]) (steps ++ [res | (res, clause) <- newSteps])
  | otherwise = (Refutation steps, unprocessed++processed)
  where { uc = fromJust(strat counter unprocessed);
    newSteps = [(res, clause) | (res, clause) <- concat[resolvants c1 uc | c1 <- processed], not(clauseIsTauto clause), null [key | (key, oldclause) <- processed, length oldclause == length clause, sort oldclause == sort clause]];
    newClauses = [(i, snd(newSteps !! (i-counter))) | i <- [counter..(counter + (length newSteps) - 1)]] }

preRecResolve::SelClauseStrategy -> Int -> EKeyConjForm -> EKeyConjForm -> [EResolve] -> (Proof, KeyConjForm)
preRecResolve strat xs unprocessed ys zs = recursiveResolve strat xs [(key,nub(clause)) | (key,clause)<-unprocessed] ys zs


-- feel free to change behaviour and type -- resolutionParam selClause [[Literal Neg "a",Literal Pos "a"],[Literal Pos "a",Literal Pos "b"]]
resolutionParam :: SelClauseStrategy -> EConjForm -> (Proof, KeyConjForm)
resolutionParam strat cs = recursiveResolve strat (length cs) [(i, cs !! i) | i <- [0..(length cs)-1], not (clauseIsTauto (cs!!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 :: EConjForm -> (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 . map (sortOn Down)
  where
    run val [] = val
    run val (c:cs)
      | evalClause val c = run val cs
      | otherwise = run (lName (head c):val) cs