module Exercise09 where

import Types

import Data.List
import Data.Ord
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 _ [] [] = []
resolve n [] (l:cn) | l == Literal Neg n = resolve n [] cn
                    | otherwise = l : resolve n [] cn
resolve n (l:cp) cn | l == Literal Pos n = resolve n cp cn
                    | otherwise = l : resolve n cp cn

-- feel free to change behaviour and type
resolvants :: KeyClause -> KeyClause -> [(Resolve, Clause)]
resolvants (k1, cs1) = resolvants' cs1 (k1, cs1)

resolvants' :: [ELiteral] -> KeyClause -> KeyClause -> [(Resolve, Clause)]
resolvants' [] _ _ = []
resolvants' ((Literal Pos n):c) (k1, cs1) (k2, cs2) 
    | Literal Neg n `elem` cs2 = (Resolve n k1 k2, resolve n cs1 cs2) : r
    | otherwise = r
    where r = resolvants' c (k1, cs1) (k2, cs2) 
resolvants' ((Literal Neg n):c) (k1, cs1) (k2, cs2) 
    | Literal Pos n `elem` cs2 = (Resolve n k2 k1, resolve n cs2 cs1) : r
    | otherwise = r
    where r = resolvants' c (k1, cs1) (k2, cs2) 
          
-- proof checking

initKeys :: Int -> ConjForm -> KeyConjForm
initKeys o cnf = zip [o..o + length cnf - 1] cnf

-- don't change the type nor expected behaviour
proofCheck :: ConjForm -> Proof -> Bool
proofCheck cnf (Model v) = eval v cnf
proofCheck cnf (Refutation r) = resolveCheck (length cnf) (initKeys 0 cnf) r

resolveCheck :: Int -> KeyConjForm -> [EResolve] -> Bool
resolveCheck _ cs [] = [] `elem` Prelude.map snd cs
resolveCheck k cs (Resolve n kp kn:rs) = isJust mc1 && isJust mc2 && Literal Pos n `elem` c1 && Literal Neg n `elem` c2
    && resolveCheck (k + 1) ((k, resolve n c1 c2):cs) rs
    where mc1 = lookup kp cs
          mc2 = lookup kn cs
          c1 = fromJust mc1
          c2 = fromJust mc2


-- feel free to change behaviour and type
selClause :: SelClauseStrategy 
selClause [] = Nothing
selClause cs = Just (minimumBy (comparing (length . snd)) cs)

-- feel free to change behaviour and type
resolutionParam :: SelClauseStrategy -> ConjForm -> (Proof, KeyConjForm)
resolutionParam s cnf = resolutionAlg s cnf' [] [] (length cnf)
      where cnf' = map (\(k, c) -> (k, nub c)) (filter (not . (clauseIsTauto . snd)) (initKeys 0 cnf))

resolutionAlg :: SelClauseStrategy -> KeyConjForm -> KeyConjForm -> [EResolve] -> Int -> (Proof, KeyConjForm)
resolutionAlg _ [] p _ _ = (Model (extractModel (map snd p)), p)
resolutionAlg s u p r k
  | isNothing muc || null (snd uc) = (Refutation r, u ++ p)
  | otherwise                      = resolutionAlg s (initKeys k nu ++ filter (\c -> c /= uc && all (isNotSubset (snd c)) nu) u) (uc : p) (r ++ nr) (k + n)
      where muc = s u
            uc = fromJust muc
            (nr, nu) = allResolvants p
            n = length nr

            allResolvants [] = ([], [])
            allResolvants (p':ps) = (rs ++ rs', us ++ us')
                where (rs', us') = allResolvants ps
                      (rs, us) = unzip (filter (\c -> all ((`isNotSubset` snd c) . snd) p) (resolvants uc p'))

            isNotSubset xs ys = not (all (`elem` ys) 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 :: ConjForm -> (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 . Prelude.map (sortOn Down)
  where
    run val [] = val
    run val (c:cs)
      | evalClause val c = run val cs
      | otherwise = run (lName (head c):val) cs