module Exercise09 where

import Types

import Data.List ((\\), nub, sort, sortOn)
import Data.Ord (Down(Down))
import Data.Maybe (fromJust)

import Test.QuickCheck ( (==>), Property )

-- Artemis output string parser
-- source: Georg Kreuzmayr on Zulip
-- https://zulip.in.tum.de/#narrow/stream/154-FPV-Exercise09/topic/Artemis.20Output.20to.20ConjForm/near/71096

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)


-- I need a set minus that deletes all occurences
(\\\) :: Eq a => [a] -> a -> [a]
xs \\\ x = filter (/= x) xs

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 $ (cp \\\ lp) ++ (cn \\\ ln)
  where
    lp = lPos n
    ln = lNeg n

resolveLit :: Literal -> Clause -> Clause -> Clause
resolveLit l cp cn = nub $ sort $ (cp \\\ lp) ++ (cn \\\ ln)
  where
    lp = l
    ln = lNegate l

-- feel free to change behaviour and type
-- type KeyClause = (Key, EClause)
-- type Resolve = Resolve EName Key Key
-- todo: make sure first param of Resolve is positive, second is negative
resolvants :: KeyClause -> KeyClause -> [(Resolve, Clause)]
resolvants (kx, cx) (ky, cy)
  = [(Resolve (lName l) (kp l) (kn l), resolveLit l cx cy) | l <- cx, l `hasOppositeIn` cy]
    where
      hasOppositeIn l c = lNegate l `elem` c
      isPositiveIn l c = lIsPos l && l `elem` c
      isNegativeIn l c = lIsNeg l && l `elem` c
      kp l = if l `isPositiveIn` cx then kx else ky
      kn l = if l `isNegativeIn` cx then kx else ky

clean :: ConjForm -> ConjForm
clean = map (nub . sort)

-- proof checking

-- don't change the type nor expected behaviour
-- type Proof = Refutation [EResolve] | Model EValuation
proofCheck :: ConjForm -> Proof -> Bool
proofCheck f (Model val)     = eval val f
proofCheck f (Refutation rs) = [] `elem` f || derive f rs

-- type ConjForm is [Clause]
derive :: ConjForm -> [Resolve] -> Bool
derive _ [] = False
derive f ((Resolve n kx ky):rs)
  | null gen    = True
  | otherwise = derive (f ++ [gen]) rs
  where
    gen = resolve n (f !! kx) (f !! ky)

-- feel free to change behaviour and type
-- is KeyConjForm -> Maybe KeyClause
-- always select the shortest clause to get [] immediately
selClause :: SelClauseStrategy 
selClause = head' . sortOn (length . snd)

head' :: [a] -> Maybe a
head' (f:_) = Just f
head' []    = Nothing

-- feel free to change behaviour and type
resolutionParam :: SelClauseStrategy -> ConjForm -> (Proof, KeyConjForm)
resolutionParam s f = resolveInternal s (zip [0 ..] (clean f)) [] [] (length f)

strip :: KeyConjForm -> ConjForm
strip = map snd

{-WETT-}
-- s  clause selection strategy
-- u  unprocessed clauses
-- p  processed clauses
-- r  taken resolution steps
-- i  next free index
resolveInternal :: SelClauseStrategy -> [KeyClause] -> [KeyClause] -> [Resolve] -> Int -> (Proof, KeyConjForm)
resolveInternal _ [] p _ _ = (Model $ extractModel $ strip p, p)
resolveInternal s u  p r i
  -- we have found the empty clause, so return it
  | null (snd uc) = (Refutation r, p ++ u)
  | otherwise     = resolveInternal s nu np nr ni     -- or with trace (dump u uc p r i) $
  where
    -- select the next-best clause from the unprocessed set
    uc = fromJust $ s u
    -- remove the selected clause from the unprocessed set
    ru = u \\\ uc
    -- get list of resolves and new clauses, removing ones that are already contained in u
    rc = concat [resolvants uc pc | pc <- p]
    -- extract the new clauses from the new resolvants
    cl = filter (\c -> c `notElem` map snd u && c `notElem` map snd p)
        $ map (nub . sort . snd) rc
    -- add new resolves to the resolution steps
    nr = r ++ map fst rc
    -- add new clauses to the unprocessed set
    nu = ru ++ zip [i ..] cl
    -- compute new starting index
    ni = i + length rc
    -- mark the clause uc as processed
    np = uc : p

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

-- examples for testing
basicModel :: ConjForm
basicModel = [[lPos "A"], [lNeg "B"]]

basicRef :: ConjForm
basicRef = [[lPos "A"], [lNeg "A"]]

timeout :: ConjForm
timeout = [[lPos "A"], [lNeg "A", lPos "A"], [lPos "A"], [lNeg "A", lPos "A", lNeg "A"]]

dump :: [KeyClause] -> KeyClause -> [KeyClause] -> [Resolve] -> Int -> String
dump u uc p r i = "u: " ++ show u ++ " uc: " ++ show uc ++ " p: " ++ show p -- ++ " r: " ++ show r ++ " i: " ++ show i

prop_checks :: ConjForm -> Property
prop_checks cf =
  length cf < 5 && all (\cl -> length cl < 5) cf
    ==> proofCheck cf $ fst $ resolution cf


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