module Exercise09 where

import Types

import Data.List (sort, sortOn, delete, union, nub,intersect)
import Data.Ord (Down(Down))
import Data.Maybe


--debug stuff

-- import Debug.Trace

-- debug = flip trace

--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 $ aux n cp cn
    where
      aux name (x : xs) (y : ys)
        | lName x == name && lIsPos x &&
          lName y == name && lIsNeg y       = aux name xs ys
        | lName x == name && lIsPos x       = y : aux name xs ys
        | lName y == name && lIsNeg y       = x : aux name xs ys
        | otherwise                         = x : y : aux name xs ys
      aux name (x : xs) []
        | lName x == name && lIsPos x       = aux name xs []
        | otherwise                         = x : aux name xs []
      aux name [] (y : ys)
        | lName y == name && lIsNeg y       = aux name [] ys
        | otherwise                         = y : aux name [] ys
      aux _ _ _                             = []
          

-- feel free to change behaviour and type
resolvants :: KeyClause -> KeyClause -> [(Resolve, Clause)]
resolvants (k1, c1) (k2, c2) = [ getPosNeg (lName l1) c1 k1 l1 c2 k2 l2 | l1 <- c1, l2 <- c2, complements l1 l2 ]
    where 
        getPosNeg name ca ka la cb kb lb
            | lIsPos la         = (Resolve name ka kb, resolve name ca cb)
            | otherwise         = getPosNeg name cb kb lb ca ka la


-- proof checking

-- don't change the type nor expected behaviour
proofCheck :: ConjForm -> Proof -> Bool
proofCheck cs (Refutation rs)   = containsEmpty $ check (getKeys cs 0) rs
    where
        check kcs (Resolve n k1 k2 : rs)      = 
            if isNothing cA || isNothing cB then
                []
            else 
                check (kcs ++ [(fst (last kcs) + 1, resolve n (fromJust cA) (fromJust cB))]) rs
            where 
                cA = lookup k1 kcs
                cB = lookup k2 kcs
        check kcs _                             = kcs
proofCheck cs (Model val)       = eval val cs

getKeys :: ConjForm -> Int -> KeyConjForm
getKeys (c : cs) i   = (i, c) : getKeys cs (i+1)
getKeys _ i          = []

containsEmpty :: KeyConjForm -> Bool
containsEmpty  = any (\(k, c) -> null c)

-- feel free to change behaviour and type
selClause :: SelClauseStrategy 
selClause []        = Nothing
selClause kcs       = Just (key, fromJust $ lookup key kcs)
    where
        --key = fst (foldr (\(k1, l1) (k2, l2) -> if l1 > l2 then (k1,l1) else (k2,l2)) (-1,-1) (map (\(k, c) -> (k, length c)) kcs))
        key = getFirst kcs (fst $ head kcs)--getShortest kcs 1000000 0

getLongest :: KeyConjForm -> Int -> Int -> Int
getLongest [] _ maxKey = maxKey
getLongest ((key, clause) : kcs) max maxKey
    |  l == 0      = key
    |  l < max     = getLongest kcs max maxKey
    |  otherwise   = getLongest kcs l key
    where 
        l = length clause


getShortest :: KeyConjForm -> Int -> Int -> Int
getShortest [] _ minKey = minKey
getShortest ((key, clause) : kcs) min minKey
    |  l == 0      = key
    |  l >= min    = getLongest kcs min minKey
    |  otherwise   = getLongest kcs l key
    where 
        l = length clause

getFirst :: KeyConjForm -> Int -> Int
getFirst [] def = def
getFirst ((key, clause) : kcs) def
    | null clause      = key
    | otherwise        = getFirst kcs def

-- feel free to change behaviour and type
resolutionParam :: SelClauseStrategy -> ConjForm -> (Proof, KeyConjForm)
resolutionParam selStrat cs = aux selStrat (getKeys safeCs 0) [] [] (length safeCs)
    where 
        safeCs = map nub cs

aux :: SelClauseStrategy -> KeyConjForm -> KeyConjForm -> [Resolve] -> Int ->(Proof, KeyConjForm)
aux _ [] p _ _     = (Model (extractModel m), p) --`debug` "Model"
    where
      m = map snd p
aux s u  p r i       
    | null (snd uc)         = (Refutation r, u ++ [(1337,[Literal Pos "Cut"])] ++ p) --`debug` "Refutation"
    | otherwise             = 
        let 
            newU = delete uc u
            newP = setAdd p uc
            resolv = concatMap (resolvants uc) p                -- [(Resolve, Clause)]
            newResolv = unzip $ onlyNew resolv newU newP        -- ([Resolve], [Clause])
            newR = r ++ fst newResolv
            endU = newU `union` getKeys (snd newResolv) i
        in
            aux s endU newP newR (i + length (snd newResolv)) --`debug` ({- "uc: " ++ show uc ++  -}"U: " ++ show (map snd endU) ++ "\nP: " ++ show (map snd newP){-  ++ ", R: " ++  show newR -})
    where 
        uc = fromJust $ s u

onlyNew :: [(Resolve, Clause)] -> KeyConjForm -> KeyConjForm -> [(Resolve, Clause)]
onlyNew [] _ _ = []
onlyNew (n : ns) u p 
    | contains u (snd n) || contains p (snd n)  = onlyNew ns u p
    | otherwise                                 = n : onlyNew ns u p

contains :: KeyConjForm -> Clause -> Bool
contains [] c           = False
contains (k : kcs) c 
    | snd k `clauseEqauls` c        = True
    | otherwise                     = contains kcs c


setAdd :: KeyConjForm -> KeyClause -> KeyConjForm
setAdd [] c = pure c
setAdd (k : kcs) c
    | snd k `clauseEqauls` snd c            = k : kcs
    | otherwise                             = k : setAdd kcs c

-- setUnion :: KeyConjForm -> KeyConjForm -> KeyConjForm
-- setUnion = foldl setAdd

clauseEqauls :: Clause -> Clause -> Bool
clauseEqauls c1 c2 = length (c1 `intersect` c2) == length c1

-- setRem :: KeyConjForm -> KeyClause -> KeyConjForm
-- setRem [] _ = []
-- setRem (k : kcs) c 
--     | k == c        = kcs
--     | otherwise     = k : setRem kcs 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 :: 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 . map (sortOn Down)
  where
    run val [] = val
    run val (c:cs)
      | evalClause val c = run val cs
      | otherwise = run (lName (head c):val) cs