module Exercise09 where

import Data.List (find, minimumBy, nub, nubBy, sort, sortOn, unionBy)
import Data.Maybe (fromJust)
import Data.Ord (Down (Down), comparing)
-- import Debug.Trace ( trace )
import Types

-- things from the tutorial

-- | extract the Name from a Literal
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 $ filter f cp ++ filter f cn
  where
    f = (/= n) . lName

-- feel free to change behaviour and type
resolvants :: KeyClause -> KeyClause -> [(Resolve, Clause)]
resolvants (k, c) (k', c') =
  [ (Resolve n k k', resolve n c c')
    | (Literal Pos n) <- c,
      Literal Neg n `elem` c'
  ]
    ++ [ (Resolve n k' k, resolve n c' c)
         | (Literal Pos n) <- c',
           Literal Neg n `elem` c
       ]

-- proof checking

findClause :: Key -> KeyConjForm -> Clause
findClause k = snd . fromJust . find ((== k) . fst)

resolveStep :: Resolve -> KeyConjForm -> KeyConjForm
resolveStep _ [] = [(0, [])]
resolveStep (Resolve n c1 c2) cs =
  cs ++ [(length cs, resolve n c1' c2')]
  where
    c1' = findClause c1 cs
    c2' = findClause c2 cs

-- don't change the type nor expected behaviour
proofCheck :: ConjForm -> Proof -> Bool
proofCheck f (Refutation res) = [] `elem` checked
  where
    checked = map snd $ foldr resolveStep (zip [0 ..] f) $ reverse res
proofCheck f (Model valuation) = eval valuation f

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

-- feel free to change behaviour and type
resolutionParam :: KeyConjForm -> [Resolve] -> KeyConjForm -> (Proof, KeyConjForm)
resolutionParam p r []
  | any (null . snd) p = (Refutation r, [])
  | otherwise = (Model $ extractModel $ map snd p, p)
resolutionParam p r u
  | null $ snd uc = trace "empty clause" (Refutation r, u ++ p)
  | any (clauseIsTauto . snd) u = trace "filtering tautologies" resolutionParam p r notTauto
  | snd uc `elem` unKeyP = trace "duplicate clause" resolutionParam p r u'
  | otherwise = trace "everything normal" resolutionParam p' (r ++ steps) u''
  where
    maxKey = maximum $ map fst $ u ++ p
    Just uc = selClause u
    (steps, clauses) = trace ("uc = " ++ show uc) trace ("p = " ++ show p) unzip $ concat [resolvants uc c | c <- p]
    u' = trace ("u = " ++ show u) u \\ [uc]
    u'' = unionBy (compare' snd) u' $ filter ((/= snd uc) . snd) $ zip [maxKey + 1 ..] clauses
    p' = unionBy (compare' snd) p [uc]
    notTauto = filter (not . clauseIsTauto . snd) u
    unKeyP = map snd p

{-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 [] []
    . nubBy (compare' snd)
    . filter (not . clauseIsTauto . snd)
    . zip [0 ..]
    . map nub

{-TTEW-}

-- extract a model as described on https://lara.epfl.ch/w/_media/sav08/gbtalk.pdf

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

(\\) :: Eq a => [a] -> [a] -> [a]
xs \\ ys = foldr (\x xs' -> filter (x /=) xs') xs ys

compare' :: Eq a => (b -> a) -> b -> b -> Bool
compare' f x y = f x == f y

trace :: String -> a -> a
trace = const id