module Exercise09 where

import Types

import Data.List
import Data.Ord (Down(Down))
import qualified Data.Set as Set
import qualified Data.Map.Strict as Map

-- things from the tutorial

instance Show Polarity where
  show Pos = ""
  show Neg = "~"

instance Show ELiteral where
  show (Literal p a) = show p ++ a

lEName :: ELiteral -> EName
lEName (Literal _ n) = n

lName :: Literal -> Name
lName = abs

lPos :: Name -> Literal
lPos = id

lNeg :: Name -> Literal
lNeg = ((-1)*)

lIsPos :: Literal -> Bool
lIsPos = (>0)

lIsNeg :: Literal -> Bool
lIsNeg = not . lIsPos

lNegate :: Literal -> Literal
lNegate = ((-1)*)

complements :: Literal -> Literal -> Bool
complements l1 l2 = l1 /= l2 && abs l1 == abs l2

evalELiteral :: EValuation -> ELiteral -> Bool
evalELiteral val (Literal Pos n) = n `elem` val
evalELiteral val (Literal Neg n) = n `notElem` val

evalLiteral :: Valuation -> Literal -> Bool
evalLiteral val l
  | lIsPos l  = (lName l) `Set.member` val
  | otherwise = (lName l) `Set.notMember` val

evalEClause :: EValuation -> EClause -> Bool
evalEClause = any . evalELiteral

evalClause :: Valuation -> Clause -> Bool
evalClause = any . evalLiteral

eval :: Valuation -> ConjForm -> Bool
eval = all . evalClause

evalE :: EValuation -> EConjForm -> Bool
evalE = all . evalEClause

clauseIsTauto :: Clause -> Bool
clauseIsTauto cl = Set.size cl /= Set.size (Set.map (abs) cl)

-- homework starts here

-- feel free to change behaviour and type
resolveE :: EName -> EClause -> EClause -> EClause
resolveE n cp cn = filter (/= Literal Pos n) cp ++ filter (/= Literal Neg n) cn

resolve :: Name -> Clause -> Clause -> Clause
resolve n cp cn = Set.delete (lPos n) (Set.delete (lNeg n) (Set.union cp cn))

-- feel free to change behaviour and type
--resolvants :: KeyClause -> KeyClause -> [(Resolve, Clause)]
--resolvants (k1,cl) (k2,cr) = [(Resolve (lName n) k1 k2, resolve (lName n) cl cr) | n <- cl, lIsPos n, p <- cr, lIsNeg p, lName n == lName p] ++ [(Resolve (lName n) k2 k1, resolve (lName n) cr cl) | n <- cr, lIsPos n, p <- cl, lIsNeg p, lName n == lName p]

resolvantsH :: KeyClause -> KeyClause -> [(Resolve, Clause)]
resolvantsH (k1, cl) (k2, cr) = [(R (lName n) k1 k2, resolve (lName n) cl cr) | n <- ilrs]
  where
    pcl = Set.filter lIsPos cl
    ncr = Set.filter lIsNeg cr
    ilrs = (Set.toList . Set.intersection pcl . Set.map lNegate) ncr  

resolvants :: KeyClause -> KeyClause -> [(Resolve, Clause)]
resolvants k1 k2 = resolvantsH k1 k2 ++ resolvantsH k2 k1

-- proof checking
--
isIn :: ELiteral -> EClause -> Bool
isIn = elem

checkRes :: EConjForm -> [EResolve] -> Bool -> Bool
checkRes xs [] b = b
checkRes xs ((Resolve n k1 k2):ys) b = if or [k1 >= l, k2 >= l, k1 < 0, k2 < 0] then False else if pos then if null cs then checkRes (xs++[cs]) ys True else checkRes (xs++[cs]) ys b else False
  where
    l = length xs
    pos = isIn (Literal Pos n) c1 && isIn (Literal Neg n) c2
    c1 = (xs !! k1)
    c2 = (xs !! k2)
    cs = resolveE n c1 c2

proofECheck :: EConjForm -> EProof -> Bool
proofECheck con (Refutation []) = con == []
proofECheck con (Refutation xs) = checkRes con xs False  
proofECheck con (Model xs) = evalE xs con

-- don't change the type nor expected behaviour
proofCheck :: EConjForm -> Proof -> Bool
proofCheck con = proofECheck con . toEProof
   



-- feel free to change behaviour and type
selClause :: SelClauseStrategy 
selClause mp = if Map.null mp then Nothing else Just (minimumBy (\(_,s1) (_,s2) -> compare (Set.size s1) (Set.size s2)) (Map.toList mp))

insClause :: KeyConjForm -> KeyConjForm -> KeyClause -> (KeyConjForm,KeyConjForm,Bool)
insClause u p (k,c) 
  |clauseIsTauto c = (u,p,False)
  |any ((flip Set.isSubsetOf) c) u || any ((flip Set.isSubsetOf) c) p = (u,p,False)
  |otherwise = (Map.insert k c (Map.filter (not . Set.isSubsetOf c) u),(Map.filter (not . Set.isSubsetOf c) p),True)

insAll :: [(Resolve, Clause)] -> KeyConjForm -> KeyConjForm -> [Resolve] -> Int -> (KeyConjForm, KeyConjForm, [Resolve],Int)
insAll [] u p r k = (u,p,r,k)
insAll ((nr,kc):xs) u p r k = if ins then insAll xs nu np (nr:r) (k+1) else insAll xs nu np r k
  where
    (nu,np,ins) = insClause u p (k,kc)


insAllS :: [KeyClause] -> KeyConjForm -> KeyConjForm
insAllS [] u = u
insAllS (x:xs) u = insAllS xs nu
  where
    (nu,_,_) = insClause u Map.empty x


-- feel free to change behaviour and type
resolutionHelp :: SelClauseStrategy -> KeyConjForm -> KeyConjForm -> [Resolve] -> Int -> (Proof, KeyConjForm)
resolutionHelp s u p r k 
  |null u = (M (extractModel p),p)
  |null sc = (Ref (reverse r),Map.union p u)
  |otherwise = resolutionHelp s nu np nr nk
    where
      Just su@(dk,sc)= s u -- u /= empty
      nrc = concat [resolvants su pp | pp <- (Map.toList p)]
      nnu = Map.delete dk u
      nnp = Map.insert dk sc p
      (nu,np,nr,nk) = insAll nrc nnu nnp r k


resolutionParam :: SelClauseStrategy -> EConjForm -> (Proof, KeyConjForm)
resolutionParam s ec = resolutionHelp s nc (Map.empty) [] l
  where 
    c = toConjForm ec
    cl = Map.toList c
    nc = insAllS cl Map.empty  
    l = Map.size c
  
{-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

resolution :: EConjForm -> (Proof, KeyConjForm)
resolution = resolutionParam selClause

{-TTEW-}

-- extract a model as described on 

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 x =(toValuation . run [] . sort . Prelude.map (sortOn Down)) (toEConjForm x)
  where
    run val [] = val
    run val (c:cs)
      | evalEClause val c = run val cs
      | otherwise = run (lEName (head c):val) cs