module Exercise09 where

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

-- 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 = filter (\(Literal p b) -> b /= n || p /= Pos) cp `union` filter (\(Literal p b) -> b /= n || p /= Neg) cn

-- feel free to change behaviour and type
resolvants :: KeyClause -> KeyClause -> [(Resolve, Clause)]
resolvants (k1, c1) (k2, c2) = [if p == Pos then (Resolve n k1 k2, resolve n c1 c2) else (Resolve n k2 k1, resolve n c2 c1) | (Literal p n) <- c1, any (\(Literal p2 n2) -> n == n2 && p /= p2) c2]

-- proof checking

-- don't change the type nor expected behaviour
proofCheck :: EConjForm -> Proof -> Bool
proofCheck formel (Refutation []) = any null formel
proofCheck formel (Refutation ((Resolve n k1 k2) : xs)) = proofCheck (formel ++ [resolve n (formel !! k1) (formel !! k2)]) (Refutation xs)
proofCheck formel (Model names) = eval names formel

-- feel free to change behaviour and type
selClause :: SelClauseStrategy
selClause [] = Nothing
selClause xs = Just mini
  where
    mini = minimumBy (\x y -> compare (length (snd x)) (length (snd y))) xs

-- feel free to change behaviour and type
resolutionParam :: SelClauseStrategy -> EConjForm -> (Proof, KeyConjForm)
resolutionParam strategy formel = if null u then (Model (extractModel (map snd p) `union` map (\(Literal _ name) -> name) positives), p) else (Refutation r, u `union` p)
  where
    keyCon = subsCheck (removeDuplicates (zip [0 ..] (map nub formel)))
    (r, u, p, positives) = helper strategy keyCon [] [] (length formel) []

helper :: SelClauseStrategy -> KeyConjForm -> KeyConjForm -> [Resolve] -> Int -> [ELiteral] -> ([Resolve], KeyConjForm, KeyConjForm, [ELiteral])
helper _ [] p r _ positives = (r, [], p, positives)
helper strategy u p r count positives = if null clau then (r, u, p, positives) else helper strategy newU newP newR (count + length tmp) (positives `union` vals)
  where
    uc = fromJust (strategy u)
    clau = snd uc
    (newU, newP, vals) = simp (delete uc u `union` zip [count ..] (map snd tmp)) (p `union` [uc])
    newR = r ++ map fst tmp
    tmp = concat [resolvants uc t | t <- p]

simp :: KeyConjForm -> KeyConjForm -> (KeyConjForm, KeyConjForm, [ELiteral])
simp u p = (filter (\(_, c) -> null [pL | pL <- pureLiterals, pL `elem` c]) (subsCheck (removeDuplicates u)), subsCheck (removeDuplicates p), posPures)
  where
    pureLiterals = map head (filter (\x -> head x == last x) (groupBy (\(Literal _ n1) (Literal _ n2) -> n1 == n2) (sort (concatMap snd (u `union` p)))))
    posPures = filter (\(Literal polar _) -> polar == Pos) pureLiterals

removeDuplicates :: KeyConjForm -> KeyConjForm
removeDuplicates xs = nubBy (\(_, c1) (_, c2) -> null (c1 \\ c2) && null (c2 \\ c1)) xs

subsCheck :: KeyConjForm -> KeyConjForm
subsCheck xs = filter (\(k1, c) -> not (clauseIsTauto c || any (\(k2, c2) -> k1 /= k2 && all (`elem` c) c2) xs)) xs

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