module Exercise09 where

import Data.List (nub, sort, sortOn, (\\))
import Data.Ord (Down (Down))
import Types
import Data.Maybe (isNothing, fromJust)
import GHC.OldList (union)
--import Debug.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 (filter (\x -> lName x /= n) (cp `union` cn))

resolvants :: KeyClause -> KeyClause -> [(Resolve, Clause)]
resolvants (_ , []) _ = []
resolvants  _ (_ , []) = []
resolvants (k, xs) (l, ys) = concatMap (\ x -> resolvantsHelper x (k, xs) (l, ys)) xs

resolvantsHelper :: ELiteral -> KeyClause -> KeyClause -> [(Resolve, Clause)]
resolvantsHelper x (k, xs) (l, ys) 
  | lNegate x `elem` ys && lIsPos x = [(Resolve (lName x) k l, resolve (lName x) xs ys)]
  | lNegate x `elem` ys && lIsNeg x = [(Resolve (lName x) l k, resolve (lName x) xs ys)]
  | otherwise  = []


-- proof checking

-- [EClause] -> [[ELiteral]] -> [[Polarity EName]]
-- don't change the type nor expected behaviour
proofCheck :: ConjForm -> Proof -> Bool
proofCheck c (Model ev) = eval ev c
proofCheck c (Refutation []) = [] `elem` c
proofCheck c (Refutation ((Resolve n x y) : xs))
  | [] `elem` c = True
  | otherwise = {-trace (show c1 ++ " : " ++ show c2)-} proofCheck (c ++ [resolve n c1 c2]) (Refutation xs)
  where
    c1 = c !! x
    c2 = c !! y

-- feel free to change behaviour and type
-- KeyConjForm -> Maybe KeyClause
selClause :: SelClauseStrategy
selClause [] = Nothing 
selClause k 
  | not (null t) = Just (head t)
  | otherwise = Just (head k)
  where t = filter (null . snd) k

-- feel free to change behaviour and type
-- [EClause] -> [[ELiteral]] -> [[Polarity EName]]
resolutionParam :: SelClauseStrategy -> ConjForm -> (Proof, KeyConjForm)
resolutionParam f xs = resolutionHelper f filtered [] [] (length xs)
  where filtered = filter (not . clauseIsTauto . snd) (conToKeyCon xs)

resolutionHelper :: SelClauseStrategy -> KeyConjForm -> KeyConjForm -> [EResolve]-> Int -> (Proof, KeyConjForm)
resolutionHelper _ [] p _ _ =  (Model (extractModel (keyConToCon p)), [])
resolutionHelper f u p r k
  | isNothing uc || null (snd unziped_uc) = {-trace (show u ++ " | " ++ show p)-} (Refutation r, [])
  | otherwise  = {-trace (show (u' `union` nu') ++ " | " ++ show p')-} resolutionHelper f (u' ++ nu') p' (r ++ nr) (k + length nu')
  where 
    uc =  f u
    unziped_uc = fromJust uc
    u' = filter (/= unziped_uc) u
    resol = concat [resolvants unziped_uc x | x <- p]
    resolFiltered = filterResol resol u' p'
    nr = [fst x | x <- resolFiltered]
    nu' = {-trace ("U: " ++ show u ++ "\nU': " ++ show u'++ " \np: " ++ show p ++ " \np': " ++ show p'++ " \nuc: " ++ show uc ++ " \nresultsFiltered: " ++ show resolFiltered ++ " \nresults: " ++ show resol++ "\n")-} zip [k..] (map snd resolFiltered)
    p' = if any (\x -> equals (snd x) (snd unziped_uc)) p then p else unziped_uc:p

filterResol :: [(Resolve , Clause)] -> [KeyClause] -> [KeyClause] -> [(Resolve, Clause)]
filterResol resol u' p' =  third
  where sndU' = {-trace (show (map snd u')) -}map snd u'
        sndP' = {-trace (show (map snd p'))-} map snd p'
        first = nub ([x | x <- resol, not (clauseIsTauto (snd x))])
        second =  nub ([x | x <- first, not (any (equals (snd x)) sndU')])
        third =  nub ([x | x <- second,  not (any (equals (snd x)) sndP')])

filterResolTest :: [(Resolve, Clause)]
filterResolTest = filterResol [(Resolve "8" 7303 5, clauseFromString "~5,~6,~3,4,7")] [(0,clauseFromString "1,~4,7,3,3"),(2,clauseFromString "~1,~4,~4,~7")] [(9,clauseFromString "~5,~6,~3,4,~8"),(8,clauseFromString "~5,~6,~3,4,7"),(7,clauseFromString "~5,~6,~3,~8"),(4,clauseFromString "~5,~6,7,~3,~3"),(1,clauseFromString "~7,~8"),(5,clauseFromString "8,4,8,7,~6")] 

contains :: Clause  -> Clause  -> Bool
contains xs y = foldr (\ x -> (&&) (x `elem` y)) True xs

equals :: Clause -> Clause -> Bool
equals x y = contains x y && contains y x

conToKeyCon :: ConjForm -> KeyConjForm
conToKeyCon = zip [0..] 

keyConToCon :: KeyConjForm -> ConjForm
keyConToCon xs = [snd x | x <- xs] 

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

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