module Exercise09 where

import Types

import Data.List
import Data.Ord (Down(Down))
import Data.Maybe

import qualified Data.HashSet as HS

type HashSet = HS.HashSet

{--import Debug.Trace (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

hasName :: Name -> Literal -> Bool
hasName n = (==n) . lName

-- feel free to change behaviour and type
resolve :: Name -> Clause -> Clause -> Clause
resolve n cp cn = sort $ nub (filter (/=Literal Pos n) cp ++ filter (/= Literal Neg n) cn)

test_resolve :: Bool
test_resolve = resolve "a" [Literal Pos "a", Literal Neg "b", Literal Neg "d"] [Literal Neg "a", Literal Neg "b", Literal Pos "c"]
    == [Literal Neg "b", Literal Neg "d", Literal Neg "b", Literal Pos "c"]

test_resolve2 :: Bool
test_resolve2 = resolve "3" [Literal Pos "3"] [Literal Neg "3", Literal Pos "3"] == [Literal Pos "3"]

-- feel free to change behaviour and type
resolvants :: KeyClause -> KeyClause -> [(Resolve, Clause)]
resolvants (a, ac) (b, bc) = resolvesAPos ++ resolvesBPos
  where
    resLiterals = nub $ filter ((`elem` bc) . lNegate) ac
    resolvesAPos = [(Resolve n a b, resolve n ac bc ) | n <- nub $ map lName $ filter lIsPos resLiterals]
    resolvesBPos = [(Resolve n b a, resolve n bc ac ) | n <- nub $ map lName $ filter lIsNeg resLiterals]

-- proof checking

-- don't change the type nor expected behaviour
proofCheck :: ConjForm -> Proof -> Bool
proofCheck cnf (Model v) = eval v cnf
proofCheck cnf rs = proofRef (zip (iterate (+1) 0) cnf) rs
  where
    proofRef kcnf (Refutation ((Resolve n ka kb) : rs)) 
      | ka `elem` idx kcnf && kb `elem` idx kcnf = proofRef (kcnf ++ [(length kcnf , resolve n (getClause ka kcnf) (getClause kb kcnf))]) (Refutation rs)
      | otherwise = False
    proofRef kcnf (Refutation []) = any (null . snd) kcnf {--trace (show kcnf ++"")--}
    getClause idx = snd . fromJust . find ((==idx) . fst)
    idx = map fst

-- feel free to change behaviour and type
selClause :: SelClauseStrategy 
selClause [] = Nothing
selClause cs = Just $ head . sortOn (length . snd) $ cs

-- feel free to change behaviour and type
resolutionParam :: SelClauseStrategy -> ConjForm -> (Proof, KeyConjForm)
resolutionParam selStrat cnf = resolveAlgo selStrat (addKeys (map (sort . nub) cnf)) [] (HS.fromList cnf) [] 
  where 
    addKeys = zip (nums 0)

resolveAlgo :: SelClauseStrategy -> KeyConjForm -> KeyConjForm -> HashSet Clause-> [Resolve] -> (Proof, KeyConjForm)
resolveAlgo _ [] ps _ _ = (Model $ extractModel (map snd ps), ps)
resolveAlgo selStrat us ps hs rs = 
    if null $ snd slcd
    then 
      (Refutation rs, us ++ ps)
    else 
      {--trace (show us ++ " ps: " ++ show ps) trace (show rts)--} resolveAlgo selStrat newUs newPs newHs (rs ++ resolves)
  where
    Just slcd = selStrat us
    rts = concatMap (resolvants slcd) ps
    (newHs, clauses, resolves) = foldr (\(r,c) (h, cs, rs) -> if not (HS.member c h) then (HS.insert c h, c:cs, r:rs) else (h, cs, rs)) (hs,[],[]) rts
    newUs = delete slcd us ++ zip (nums ({--trace (show (length us + length ps ))--} (length us + length ps))) clauses
    newPs = ps ++ [slcd]
    clauseEqual x y = snd x == snd y 
    allClauses = map snd (ps ++ us)

nums :: Int -> [Int]
nums = iterate (+1)


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

resolvable :: [ConjForm]
resolvable = [
  [[Literal Pos "a"]], 
  [[Literal Pos "a"],[Literal Pos "b"]],
  [[Literal Pos "a"],[Literal Neg "b"]],
  [[Literal Pos "3"],[Literal Pos "3", Literal Neg "3"], [Literal Neg "3", Literal Neg "2"]]]

rs :: Int -> ConjForm
rs = (!!) resolvable  

nrs :: Int ->ConjForm
nrs = (!!) notResolvable

notResolvable :: [ConjForm]
notResolvable = [
  [[Literal Pos "a"],[Literal Neg "a"]],
  [[Literal Pos "a", Literal Neg "b"], [Literal Neg "a", Literal Pos "b"]],
  [[Literal Pos "a", Literal Neg "b"],[Literal Neg "a"],[Literal Neg "a",Literal Pos "b"], [Literal Pos "a"] , [Literal Neg "b", Literal Pos "c", Literal Neg "a"]],
  map (map parseLiteral) [["9","~10","8","~5","~3","~6"],["8","~2"],["4"],["~5"],["~5","~6","10","~2","6","~5"],["~8","9","8"],["6","~8"],["6","10"],["5","8","~2","~8","~7","~9","8","4"],["3","~8","5","~9","~3"],["4","~5","~10","~7","6","~7","3"],["~7","6","~7","~4","3","1","6","9"],["9","2","3","~9","7","~1","6"],["~5","~5"],["~4"],["~8","10","~5"]],
  map ( (:[]). Literal Neg . show) [1..49],
  parseCnf "[[~5],[~10,7,~4,~2],[5,~3,6,8],[~10],[~4],[2,4,~2,~3,~4,~10],[~7,10,1,~2,5,5,4,6],[10,~2,9,10],[~10,~5,~3],[~6,2,2,~8,~2,~2,~7],[~2,~2,~2,4],[4,~9,8,~5],[~3,4,~5,9,~1],[8],[9,~9,8,5,~4],[~4],[~8,~1,3,~2],[4,5,1,9,6],[6],[~9,~10,~10,~8,10,~1],[~7,7],[1],[~4,9,~5,~8,~10,5,~7],[1],[9,2],[~5],[1,8,3,1,~8,2,3],[~1,1,~1,~9],[3,9,~6,~10,2,~8,~9,2],[~7,~9,7,~7,3],[~8,3,7,~10],[~1,~4,~9],[4,1,~8,~7,1],[1,~7],[~1,3,7,~9],[1,9],[~9,~9,9,~8,4,~8],[9,~8,5,~1],[1,3,~3,~9,~6,3,~8],[~1,2,9,~8,~10,~8],[~3,4,10,3,~1,3],[~10,~5,3,10,~9,~1],[6,9,9,~10],[~2],[~6,~6,~9,~10,7,4],[1,9],[2,~9],[3,10,1],[~6,~9,~3,10,5,2],[10,3,9,3],[2,5,~7,~7,~3,3,~3],[~2],[6,~6,1,~5,~2],[5,10,~3,~10,9,7,7,~3],[1,~9],[~9,~3],[~4,~7,10],[7,2,2,~5,3,8],[4,~5,~10,~10,2],[~10],[5,6,2,~1,~1,~6],[~9,6,~3,5,3,1],[~10,~9,~6,7],[~8,~8,2],[~10,10,3,~8,1,~10,4,~4],[~1,10],[7,8,~3,4,8]]",
  parseCnf "[[~3,4,~6,~3,2,8,8,~1],[8,~7],[~8,~1,8,~5,2]]",
  parseCnf "[[3],[~1],[~2,1,~2,5,~6],[7,4,~5,~4]]",
  parseCnf "[[3,~9],[10],[~8,7,~11,~8,2,~10],[~3,~9,5,~11,10,~11,~10,10,~10,~7,8]]",
  parseCnf "[[~3],[~2,~8,5,2],[~8,~1,3,4,~1,~6,~5],[5,2,2],[~5,7,~7,~5,3],[~4,~5,1,~4,~4,1,~2],[~6,~2,6]]"
  ] 

parseLiteral :: String -> Literal
parseLiteral ('~':xs) = Literal Neg xs
parseLiteral xs = Literal Pos xs 

parseClause :: [String] -> Clause
parseClause = map parseLiteral

parseCnf :: String -> ConjForm
parseCnf s = map parseClause ((map (splitOn ",") . splitOn "],[" . init . init . tail . tail) s)

splitOn :: String -> String -> [String]
splitOn pat s = aux s [] []
  where 
    aux [] rs acc = acc ++ [rs]
    aux (x:xs) rs acc | pat `isPrefixOf` (x:xs) = aux (drop (length pat) (x:xs)) [] (acc ++ [rs])
                      | otherwise = aux xs (rs ++ [x]) acc

test_res1 :: Bool
test_res1 = and [solveAndCheck cnf | cnf <- resolvable]

test_res2 :: Bool
test_res2 = and [solveAndCheck cnf | cnf <- notResolvable]

solveAndCheck :: ConjForm -> Bool
solveAndCheck cnf = let r@(p, kcnf) = resolution cnf in {--trace (show r)--} proofCheck cnf p 

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