module Exercise09 where

import Types

import Data.List (sort, sortOn, nub)
import Data.Ord (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 (\l -> l /= Literal Pos n) cp ++ filter (\l -> l /= Literal Neg n) cn

-- feel free to change behaviour and type
resolvants :: KeyClause -> KeyClause -> [(Resolve, Clause)]
resolvants kC1 kC2 = resolvantsInOrder kC1 kC2 ++ resolvantsInOrder kC2 kC1

resolvantsInOrder :: KeyClause -> KeyClause -> [(Resolve, Clause)]
resolvantsInOrder (kp, cp) (kn, cn) = [(Resolve (lName n) kp kn,resolve (lName n) cp cn) | n <- cp, lIsPos n, lNegate n `elem` cn]

-- proof checking

-- don't change the type nor expected behaviour
proofCheck :: ConjForm -> Proof -> Bool
proofCheck cf (Refutation resolveSteps) = checkSteps (addKeys cf) resolveSteps
proofCheck cf (Model names) = calc cf names

addKeys :: ConjForm -> [KeyClause]
addKeys (c:conj) = (0,c) : map (\(n,x) -> (n+1,x)) (addKeys conj)
addKeys [] = []

checkSteps :: [KeyClause] -> [Resolve] -> Bool 
checkSteps cs (Resolve n kp kn : resolves) = canResolve cp cn n && checkSteps ((length cs, resolve n cp cn):cs) resolves
  where cp = head [c | (k,c) <- cs, k==kp]
        cn = head [c | (k,c) <- cs, k==kn]
checkSteps _ [] = True

canResolve :: Clause -> Clause -> Name -> Bool
canResolve cp cn n = Literal Pos n `elem` cp && Literal Neg n `elem` cn

calc :: ConjForm -> [Name] -> Bool
calc (c:conjForm) ns = any (literalCalc ns) c && calc conjForm ns
calc [] _ = True

literalCalc :: [Name] -> Literal -> Bool 
literalCalc ns (Literal Pos n) = n `elem` ns
literalCalc ns (Literal Neg n) = n `notElem` ns

-- feel free to change behaviour and type
selClause :: SelClauseStrategy 
selClause [] = Nothing 
selClause kCs = Just $ head [(k,c) | (k,c) <- kCs, length c == minLength]
  where minLength = minimum [length c | (_,c) <- kCs]



-- feel free to change behaviour and type
resolutionParam :: SelClauseStrategy -> ConjForm -> (Proof, KeyConjForm)
resolutionParam scs cf = if [] `elem` [c | (_,c) <- kcf] then (Refutation resolveSteps, kcf) else
  (Model (extractModel [c | (_,c) <- kcf]),kcf)
  where (resolveSteps, kcf) = algorithm2 scs (addKeys cf) []

algorithm2 :: SelClauseStrategy -> KeyConjForm -> KeyConjForm -> ([Resolve],KeyConjForm)
algorithm2 _ [] kcf = ([], kcf)
algorithm2 scs uKCs pKCs = (stepsFiltered ++ recRes,kcf)
  where selected = fromJust $ scs uKCs
        stepsAndClauses = concat [resolvants selected pKC | pKC <- pKCs]
        (stepsFiltered, clauseFiltered) = unzip [(s,c) | (s,c) <- dropSubsumed stepsAndClauses, not $ isSubsumed c (uKCs++pKCs)]
        newKC = map (\(n,c) -> (n + length uKCs + length pKCs,c)) $ addKeys clauseFiltered
        newUKCs = [uKC | uKC <- uKCs, uKC /= selected] ++ newKC
        (recRes,kcf) = algorithm2 scs newUKCs (selected:pKCs)



dropSubsumed :: [(a,Clause)]  -> [(a,Clause)]
dropSubsumed = dropSubsumedRunner 0

dropSubsumedRunner :: Int -> [(a,Clause)] -> [(a,Clause)]
dropSubsumedRunner i kcf
  | i == length kcf = kcf
  | isSubsumed (snd (kcf !! i)) others = dropSubsumedRunner i others
  | otherwise = dropSubsumedRunner (i+1) kcf
    where others = take i kcf ++ drop (i+1) kcf

isSubsumed :: Clause -> [(a,Clause)] -> Bool
isSubsumed c (x:kcf) = all (`elem` c) (snd x) || isSubsumed c kcf
isSubsumed _ [] = False

algorithm :: SelClauseStrategy -> KeyConjForm -> KeyConjForm -> Int -> ([Resolve],KeyConjForm)
algorithm _ [] pKCs _ = ([], pKCs)
algorithm scs uKCs pKCs i = (resolveSteps ++ recRes,kcf)
  where selected = (\(Just a) -> a) $ scs uKCs
        stepsClauses = concat [resolvants selected pKC | pKC <- pKCs]
        stepsClausesFiltered = filter (\(_,c) -> not(clauseIsTauto c) && c `notElem` ([uC | (_,uC) <- uKCs] ++ [pC | (_,pC) <- pKCs])) (nubKey $ map (\(s,c) -> (s,(sort . nub) c)) stepsClauses)
        (resolveSteps,newClauses) = unzip stepsClausesFiltered
        newKeyClauses = map (\(n,c) -> (n + length uKCs + length pKCs,c)) $ addKeys newClauses
        newUKCs = [uKC | uKC <- uKCs, uKC /= selected] ++ newKeyClauses
        (recRes,kcf) = if null selected then ([], pKCs ++ [(-1,[Literal Pos "A"])] ++ uKCs) else algorithm scs newUKCs (selected:pKCs) (i+1)
{-WETT-}

notSubsumed :: Clause -> Clause -> Bool
notSubsumed longer shorter = undefined

nubKey :: [(a,Clause)] -> [(a,Clause)]
nubKey ((k,c):kcs)
  |c `elem` map snd kcs = nubKey kcs
  |otherwise = (k,c) : nubKey kcs
nubKey [] = []

-- 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
--resolution = undefined 



testText :: [[String]] -> (Proof, KeyConjForm)
testText s = resolution $ map (map strToLit) s

strToLit :: String -> Literal 
strToLit ('~':str) = Literal Neg str
strToLit str = Literal Pos str

testT2 :: [String] -> (Proof, KeyConjForm)
testT2 strs = testText $ map words strs
{-TTEW-}

getConj :: [String] -> ConjForm 
getConj = map (map strToLit . words)

proofT2 :: [String] -> Bool
proofT2 str = proofCheck (getConj str) (fst (resolution (getConj str)))

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