module Exercise09 where

import Types

import Data.List (sort, sortOn, groupBy, nub, minimumBy, maximumBy, (\\))
import Data.Ord (Down(Down))
-- import Debug.Trace (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 $ sort (filter (lPos n /=) cp ++ filter (lNeg n /=) cn)

-- feel free to change behaviour and type
resolvants :: KeyClause -> KeyClause -> [(Resolve, Clause)]
resolvants (k1, c1) (k2, c2) = [(res lit, cls lit) | lit <- c1, lNegate lit `elem` c2, not $ clauseIsTauto $ cls lit]
  where 
    res lit = if lIsPos lit then Resolve (lName lit) k1 k2 else Resolve (lName lit) k2 k1
    cls lit = if lIsPos lit then resolve (lName lit) c1 c2 else resolve (lName lit) c2 c1

-- proof checking

-- don't change the type nor expected behaviour
proofCheck :: ConjForm -> Proof -> Bool
proofCheck clauses (Model valuation) = eval valuation clauses
proofCheck clauses (Refutation []) = [] `elem` clauses
proofCheck clauses (Refutation ((Resolve l k1 k2):steps)) = proofCheck newClauses (Refutation steps)
  where
    newClauses = clauses ++ [resolve l (clauses!!k1) (clauses!!k2)]


-- feel free to change behaviour and type
selClause :: SelClauseStrategy 
selClause [] = Nothing
selClause clauses 
  | [] `elem` map snd clauses = Just (0, [])
  | otherwise = Just $ head $ sortOn snd clauses

-- feel free to change behaviour and type
resolutionParam :: SelClauseStrategy -> ConjForm -> (Proof, KeyConjForm)
resolutionParam sel c = solve relevant [] [] (length c)
  where
    -- give every clause a key
    keyed  = zip [0..] (map (nub . sort) c)
    -- remove the tautologies
    noTauto  = filter (not . clauseIsTauto . snd) keyed
    -- remove redundant clauses
    relevant   = filter (`notRedundant` noTauto) noTauto
    solve u p r idC = case sel u of
                    Just (_, [])  -> (Refutation r, p ++ u)
                    Just uc       -> solve nextU (nub (uc:p)) (r++nr) (idC + length nu)
                      where
                        nextU            = filter (\(_,x) -> x `notElem` processedClauses && (0, x) `notRedundant` knownClauses) (u++nu)
                        processedClauses = map snd (uc:p)
                        knownClauses     = u++nu++p 
                        revv             = concatMap (resolvants uc) p
                        nr               = map fst revv
                        nu               = zip [idC..] $ map (sort . snd) revv
                    Nothing       -> (Model $ extractModel $ map snd p, u)

-- check wheter a keyclause is redundant in a list of clauses
notRedundant :: KeyClause -> [KeyClause] -> Bool
notRedundant (_, x) = not . any (\(_, y) -> length y < length x && y `subSet` x)

subSet :: Ord a => [a] -> [a] -> Bool
subSet [] [] = True
subSet _ [] = False
subSet [] _  = True
subSet (x:xs) (y:ys)
    | x < y     = False    
    | x == y    = subSet xs ys   
    | otherwise = subSet (x:xs) ys

makeInputAux :: [Char] -> ConjForm
makeInputAux [] = []
makeInputAux ('[':xs) = makeInputAux xs
makeInputAux (']':xs) = makeInputAux xs
makeInputAux (',':xs) = makeInputAux xs
makeInputAux xs = let   clause_string = takeWhile (/= ']') xs
                        a = clauseFromString clause_string in
                          a:makeInputAux(xs\\clause_string)

clauseFromString :: [Char] -> Clause
clauseFromString [] = []
clauseFromString (',':xs) = clauseFromString xs
clauseFromString ('~':xs) = let   name = takeWhile (/= ',') xs in
                              Literal Neg name:clauseFromString (xs\\name)
clauseFromString xs = let   name = takeWhile (/= ',') xs
                                in
                              Literal Pos name:clauseFromString (xs\\name)

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