module Exercise09 where

import Data.List
import Data.Maybe
import Data.Ord
import Types

-- things from the tutorial

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

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

instance Show KeyClause where
  show (KC k c) = show (k, c)

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 $ delete (Literal Pos n) (nub cp) ++ delete (Literal Neg n) (nub cn)

-- feel free to change behaviour and type
resolvants :: KeyClause -> KeyClause -> [(Resolve, Clause)]
resolvants (KC k1 c1) (KC k2 c2) =
  let rs =
        [ if lIsPos l1
            then (Resolve n k1 k2, resolve n c1 c2)
            else (Resolve n k2 k1, resolve n c2 c1)
          | l1@(Literal _ n) <- c1,
            l2 <- c2,
            complements l1 l2
        ]
   in if length rs <= 1 then rs else []

-- proof checking

-- don't change the type nor expected behaviour
proofCheck :: EConjForm -> Proof -> Bool
proofCheck cf (Refutation []) = [] `elem` cf
proofCheck cf (Refutation ((Resolve n k1 k2) : rs)) = proofCheck (cf ++ [resolve n (cf !! k1) (cf !! k2)]) (Refutation rs)
proofCheck cf (Model val) = eval val cf

-- feel free to change behaviour and type
selClause :: KeyConjForm -> Maybe KeyClause
selClause [] = Nothing
selClause kcf = Just $ head kcf

-- feel free to change behaviour and type
resolutionParam :: SelClauseStrategy -> ConjForm -> (Proof, KeyConjForm)
resolutionParam _ cf = res (filter (not . clauseIsTauto . clause) $ subsume $ sort $ indicate (map (nub . sort) cf) 0) [] [] (length cf)

res :: KeyConjForm -> KeyConjForm -> [Resolve] -> Int -> (Proof, KeyConjForm)
res [] p _ _ = (Model $ extractModel (map clause p), p)
res u p r c
  | null $ clause uc = (Refutation r, u ++ p)
  | otherwise =
    let ns = sortBy (comparing snd) $ filter ((`notElem` map clause p) . snd) $ concatMap (resolvants uc) p
     in res (subsume $ merge (delete uc u) (subsume $ indicate (map snd ns) c)) (subsume $ insert uc p) (r ++ map fst ns) (c + length ns)
  where
    uc = fromJust $ selClause u

indicate :: ConjForm -> Int -> KeyConjForm
indicate [] _ = []
indicate (x : xs) n = KC n x : indicate xs (n + 1)

subsume :: KeyConjForm -> KeyConjForm
subsume [] = []
subsume (kc : kcs) = kc : subsume (subsume' kc kcs)
  where
    subsume' _ [] = []
    subsume' kc1 (kc2 : kcs')
      | null (clause kc1 \\ clause kc2) = subsume' kc1 kcs'
      | otherwise = kc2 : subsume' kc1 kcs'

merge :: [KeyClause] -> [KeyClause] -> [KeyClause]
merge [] ys = ys
merge xs [] = xs
merge (x : xs) (y : ys)
  | x <= y = x : merge xs (y : ys)
  | otherwise = y : merge (x : xs) ys

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

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