module Exercise09 where

import Data.List (sort, sortOn, minimumBy)
import Data.Ord (Down (Down), comparing)
import Types
import qualified Data.Set as Set
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 = if null cp || null cn then [Literal Pos ""] else p cp ++ ne cn
  where
    p [] = []
    p (x : xs) = if x == lPos n then p xs else x : p xs
    ne [] = []
    ne (x : xs) = if x == lNeg n then ne xs else x : ne xs

-- resolve with sets
resolveDiff :: Name -> Set.Set ELiteral -> Set.Set ELiteral -> Set.Set ELiteral
resolveDiff n cp cn =  Set.delete (lPos n) cp `Set.union` Set.delete (lNeg n) cn

resolvants :: (Int, Set.Set ELiteral) -> (Int, Set.Set ELiteral) -> [(Resolve, Set.Set ELiteral)]
resolvants (k1, c) (k2, l) = dups cl1
  where
    cl1 = Set.toList c
    dups [] = []
    dups (x : xs) 
      | lIsPos x && Set.member (lNegate x) l = (Resolve (lName x) k1 k2, resolveDiff (lName x) c l) : dups xs
      | lIsNeg x && Set.member (lNegate x) l = (Resolve (lName x) k2 k1, resolveDiff (lName x) l c) : dups xs
      | otherwise = dups xs

-- proof checking

-- don't change the type nor expected behaviour
proofCheck :: ConjForm -> Proof -> Bool
proofCheck cnf p = check cnf p
  where
    zipped = zip [0 .. length cnf] cnf
    find c k = snd$head$filter (\x->fst x==k) c
    check c (Model m) = eval m c 
    check c (Refutation r) = loop zipped (Refutation r)
    loop c (Refutation []) = any (null . snd) c
    loop c (Refutation (Resolve name k1 k2:xs)) = loop ((length c, resolve name (find c k1) (find c k2)):c) (Refutation xs)

-- feel free to change behaviour and type
selClause :: [(Int, Set.Set ELiteral)] -> (Int, Set.Set ELiteral)
selClause = minimumBy (comparing (Set.size . snd))

-- feel free to change behaviour and type
resolutionParam :: EConjForm -> (Proof, KeyConjForm)
resolutionParam cnf = loop sub [] (Refutation [])
  where
    sub = sortOn (Set.size .snd) (zip [0 ..] (map Set.fromList cnf))
    loop [] p _ = (Model (extractModel (map (Set.toList . snd) p)), [])
    -- for debugging: loop [] p _ = (Model (extractModel (map (Set.toList . snd) p)), map (\(x, y)->(x, Set.toList y))p)
    loop u [] r = loop (tail u) [head u] r
    loop u p (Refutation r) 
     | Set.null (snd (head u)) = (Refutation r, [])
     -- for debugging: | Set.null (snd (head u)) = (Refutation r, map (\(x, y)->(x, Set.toList y))(p++u))
     | inside (head u) p = loop (tail u) (head u : p) (Refutation r)
     | otherwise = loop (sortOn (Set.size . snd)(newclauses p u ++ tail u)) (head u : p) (Refutation (r ++ map fst (resolvan (head u) p)))
    resolvan selected p = concatMap (resolvants selected) p
    newclauses p u = zip [length (u++p)..] (map snd (resolvan (head u) p))

-- check redundancy
inside:: (Int, Set.Set ELiteral) -> [(Int, Set.Set ELiteral)] -> Bool
inside (_, cl) = any (\ (_, y) -> y `Set.isSubsetOf` cl) 

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