module Exercise09 where

import qualified Data.HashMap.Strict as M
import qualified Data.HashSet as S
import Data.List (delete, minimumBy, nub, sort, sortOn, (\\))
import Data.Maybe
import Data.Ord (Down (Down))
--import Debug.Trace
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

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 c = not (null c) && any (\l -> lNegate l `elem` c) c

-- homework starts here

-- feel free to change behaviour and type
resolveP :: Name -> Clause -> Clause -> Clause
resolveP na cp cn = nub (filter (\(Literal p n) -> p /= Pos || n /= na) cp ++ filter (\(Literal p n) -> p /= Neg || n /= na) cn)

resolveN :: Name -> Clause -> Clause -> Clause
resolveN na cp cn = nub (filter (\(Literal p n) -> p /= Neg || n /= na) cp ++ filter (\(Literal p n) -> p /= Pos || n /= na) cn)

--first HClause has positive, second negative
hresolve :: Name -> HClause -> HClause -> HClause
hresolve n (cpp, cpn) (cnp, cnn) = (S.union (S.delete n cpp) cnp, S.union cpn (S.delete n cnn))

-- feel free to change behaviour and type
resolvants :: KeyClause -> KeyClause -> [(Resolve, Clause)]
resolvants (k1, kc1) (k2, kc2) =
  [(Resolve name k1 k2, resolveP name kc1 kc2) | (Literal _ name) <- filter (\(Literal po na) -> po == Pos && (Literal Neg na `elem` kc2)) kc1]
    ++ [(Resolve name k2 k1, resolveN name kc1 kc2) | (Literal _ name) <- filter (\(Literal po na) -> po == Pos && (Literal Neg na `elem` kc1)) kc2]

hresolvants :: ([Resolve], HConjForm, KeyMap, Key) -> HConjForm -> HClause -> HClause -> ([Resolve], HConjForm, KeyMap, Key)
hresolvants (rs, up, km, key) pc c1 c2 = h (h (rs, up, km, key) c1 c2 k1 k2) c2 c1 k2 k1
  where
    k1 = fromJust $ M.lookup c1 km
    k2 = fromJust $ M.lookup c2 km
    h (srs, sup, skm, skey) sc1@(sc1p, _) sc2@(_, sc2n) sk1 sk2 =
      S.foldl'
        ( \a@(frs, fup, fkm, fkey) na ->
            if S.member na sc2n
              then
                let nc@(ncp, ncn) = hresolve na sc1 sc2
                 in if M.member nc fkm
                   -- || any (\(pcp, pcn) -> all (`S.member` pcp) ncp && all (`S.member` pcn) ncn) pc
                      then a
                      else (Resolve na sk1 sk2 : frs, S.insert nc fup, M.insert nc fkey fkm, fkey + 1)
              else a
        )
        (srs, sup, skm, skey)
        sc1p

-- proof checking

-- don't change the type nor expected behaviour
proofCheck :: ConjForm -> Proof -> Bool
proofCheck jf (Model ts) = all (rc ts) jf
  where
    --    rc tns [] | trace ("proof FALSE: " ++ show tns) False = undefined
    rc _ [] = False
    rc tns ((Literal Pos na) : cs) = (na `elem` tns) || rc tns cs
    rc tns ((Literal Neg na) : cs) = (na `notElem` tns) || rc tns cs
proofCheck jf (Refutation ref) = res jf ref
  where
    --    res cnf [] | trace ("\n PROOF FAILED !!!!!:" ++ show cnf) False = undefined
    res _ [] = False
    --    res cnf ((Resolve na k1 k2) : rs) | (k1 >= length cnf || k2 >= length cnf) && trace ("proof out of bound: k1:" ++ show k1 ++ " k2:" ++ show k2 ++ " cnf:" ++ show cnf) False = undefined
    res cnf ((Resolve na k1 k2) : rs) = let nc = resolveP na (cnf !! k1) (cnf !! k2) in null nc || res (cnf ++ [nc]) rs

-- feel free to change behaviour and type
selClause :: SelClauseStrategy
selClause [] = Nothing
selClause cf = Just (minimumBy (\(_, c1) (_, c2) -> compare (length c1) (length c2)) cf)

selClauseH :: HConjForm -> Maybe HClause
selClauseH ch = if S.null ch then Nothing else Just (minimumBy (\(c1p, c1n) (c2p, c2n) -> compare (length c1p + length c1n) (length c2p + length c2n)) ch)

-- feel free to change behaviour and type
resolutionParam :: SelClauseStrategy -> ConjForm -> (Proof, KeyConjForm)
resolutionParam _ cj = undefined

resu :: KeyConjForm -> KeyConjForm -> [EResolve] -> Maybe KeyClause -> Int -> (Proof, KeyConjForm)
resu _ p _ Nothing _ = (Model (extractModel [c | (_, c) <- p]), p)
resu u p rs (Just (_, [])) _ = (Refutation rs, u ++ p)
resu u p rs (Just c) k = resu nu (c : p) (rs ++ nars) (selClause nu) (l + k)
  where
    npu = delete c u
    (nars, nuu) = unzip (concat [resolvants c pc | pc <- p])
    nfu = filter (\fc -> not (any (\(_, cl) -> cl == fc) p)) nuu
    l = length nfu
    nu = npu ++ [(i + k, nuu !! i) | i <- [0 .. l -1]]

--t = []
--t = if trace ("resu c:"++show c++" nuu:"++show nuu++" p:"++show p) True then [] else undefined
--t = if trace ("resu last: u:" ++ show u ++ " p:" ++ show p ++ " rs:" ++ show rs ++ " c:" ++ show c ++ " k;" ++ show k ++ " npu:" ++ show npu ++ " nars:" ++ show nars ++ " nuu:" ++ show nuu ++ " l:" ++ show l ++ " nu:" ++ show nu) True then [] else []

hresu :: [Resolve] -> HConjForm -> KeyMap -> Key -> Maybe HClause -> HConjForm -> Proof
--hresu rs uc km key mc pc | trace ("hresu: rs:" ++ show rs ++ " uc:" ++ show uc ++ " km:" ++ show km ++ " key:" ++ show key ++ " mc:" ++ show mc ++ " pc:" ++ show pc) False = undefined
--hresu rs uc km key (Just cc) pc | trace ("hresu: " ++ " cc:" ++ show cc ++ " rs:" ++ show [0] ++ " key:" ++ show key ++ " rnrs:" ++ show (nrs \\ rs) ++ " rnuc:" ++ show (S.difference nuc uc) ++ " rnkm:" ++ show (M.difference nkm km) ++ " rnkey:" ++ show nkey) False = undefined
--  where
--    (nrs, nuc, nkm, nkey) = S.foldl' (`hresolvants` cc) (rs, uc, km, key) pc
hresu _ _ _ _ Nothing pc = Model (extractModel (toEConjFormH pc))
hresu rs uc km key (Just cc@(ccp, ccn)) pc =
  if S.null ccp && S.null ccn
    then Refutation (reverse rs)
    else hresu nrs nnuc nkm nkey (selClauseH nnuc) (S.insert cc pc)
  where
    nnuc = S.delete cc nuc
    (nrs, nuc, nkm, nkey) = S.foldl' (\upa ncl -> hresolvants upa pc cc ncl) (rs, uc, km, key) pc

fillKeyMap :: ConjForm -> KeyMap -> Int -> (KeyMap, Int)
fillKeyMap [] km key = (km, key)
fillKeyMap (c : cs) km key = if M.member hc km then fillKeyMap cs km (key + 1) else fillKeyMap cs nkm (key + 1)
  where
    hc = toClauseH c
    nkm = M.insert hc key km

{-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 :')

-- The Code is trivially self explaining
-- Proof by contradiction:
--  Assume code is not trivially self explanatory
--  This is a contradiction, because the compiler is able to understand the code
--                                                          □ QED
resolution :: ConjForm -> (Proof, KeyConjForm)
resolution cj = (hresu [] hc km key (selClauseH hc) S.empty, [])
  where
    (km, key) = fillKeyMap cj M.empty 0
    hc = toConjFormH cj

resolutionFA :: String -> (Proof, Bool)
resolutionFA str = let (pr, _) = resolution inp in (pr, proofCheck inp pr)
  where
    inp = makeInputAux str

exh :: HClause
exh = (S.fromList [], S.fromList ["1"])

{-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 m | trace ("extractModel: " ++ show m) False = undefined
extractModel m = (run [] . sort . map (sortOn Down)) m
  where
    run val [] = val
    run val (c : cs)
      | evalClause val c = run val cs
      | otherwise = run (lName (head c) : val) cs

-- Georg Kreuzmayr
-- Help Method to generate ConjForm
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)