module Exercise09 where

import Types

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

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


data Tree a = Node (Tree a) a (Tree a)| Leaf
  deriving (Eq, Show)

insertTree:: (Ord a) => a -> Tree a -> Tree a
insertTree a Leaf = Node Leaf a Leaf
insertTree a (Node l x r) = if x > a then Node (insertTree a l) x r  else Node l x (insertTree a r)

insertTreeL :: KeyClause -> Tree KeyClause -> Tree KeyClause
insertTreeL a Leaf = Node Leaf a Leaf
insertTreeL a (Node l x r)
                    | (fst x) == (fst a) = (Node l x r)
                    |(length $ snd x) > (length $ snd a) = Node (insertTreeL a l) x r
                    |otherwise = Node l x (insertTreeL a r)

insertTreeK :: KeyClause -> Tree KeyClause -> Tree KeyClause
insertTreeK a Leaf = Node Leaf a Leaf
insertTreeK a (Node l x r)
                        | (fst x) > (fst a) = Node (insertTreeK a l) x r
                        | (fst x) == (fst a) = (Node l x r)
                        |otherwise = Node l x (insertTreeK a r)

createTree :: (Ord a) => [a] -> Tree a -> Tree a
createTree [] tree = tree
createTree (x:xs)  tree = createTree xs (insertTree x tree)

createTreeL :: [KeyClause] -> Tree KeyClause -> Tree KeyClause
createTreeL [] tree = tree
createTreeL (x:xs)  tree = createTreeL xs (insertTreeL x tree)

createTreeK :: [KeyClause] -> Tree KeyClause -> Tree KeyClause
createTreeK [] tree = tree
createTreeK xs  tree = Node (createTreeK (take l xs ) Leaf) x (createTreeK (drop (l+1) xs) Leaf)
            where l = (length xs `div` 2)
                  x = xs !! l
--createTreeK xs  tree = Node createTreeK (take l xs ++ drop (l+1) xs) (insertTreeK x tree)
biggestChildRemove:: Tree KeyClause -> (KeyClause, Tree KeyClause)
biggestChildRemove Leaf = ((-1, []), Leaf)
biggestChildRemove (Node l x Leaf) = (x, l )
biggestChildRemove (Node l x r) = (fst next, Node l x (snd next))
              where next = biggestChildRemove r

smallestChildRemove:: Tree KeyClause -> (KeyClause, Tree KeyClause)
smallestChildRemove Leaf = ((-1, []), Leaf)
smallestChildRemove (Node Leaf x r) = (x, r)
smallestChildRemove (Node l x r) = (fst next, Node (snd next) x r)
              where next = smallestChildRemove l

removeNode:: Tree KeyClause -> KeyClause -> Tree KeyClause
removeNode Leaf _ = Leaf
removeNode (Node Leaf x Leaf) c | fst c == fst x = Leaf
                                | otherwise = (Node Leaf x Leaf)
removeNode (Node l x r) c
          | fst c == fst x  = if l /= Leaf then Node (snd bcr) (fst bcr) r else Node Leaf (fst scr) (snd scr)
          | fst c < fst x   = Node (removeNode l c) x r
          | otherwise       = Node l x (removeNode r c)
          where bcr = biggestChildRemove l
                scr = smallestChildRemove r

popRoot:: Tree KeyClause -> (KeyClause, Tree KeyClause)
popRoot Leaf = ((-1, []), Leaf)
popRoot tree@(Node l x r) = (x, removeNode tree x)


treeToList :: Tree a -> [a]
treeToList Leaf = []
treeToList (Node l x r) = x : treeToList l ++ treeToList r


filterSubs :: Tree KeyClause -> Tree KeyClause
filterSubs = undefined

--testet ob
isSubs :: Clause -> Clause -> Bool
isSubs c1 c2 = undefined


-- feel free to change behaviour and type
resolve :: Name -> Clause -> Clause -> Clause
resolve n cp cn = nub ([ l | l<-nub cp, l /= (Literal Pos n)] ++ [ l | l<-nub cn,  l /= (Literal Neg n) ])

-- feel free to change behaviour and typen (Key, EClause)
resolvants :: KeyClause -> KeyClause -> [(Resolve, Clause)]
resolvants (k1,xs) (k2,ys) = [if p == Pos then ((Resolve n k1 k2), (resolve n xs ys)) else ((Resolve n k2 k1), (resolve n ys xs)) | l@(Literal p n)<-(nub xs), (lNegate l) `elem` ys]

bestResolvant :: KeyClause -> KeyClause -> (Resolve, Clause)
bestResolvant c1 c2 = (foldr (\x y -> if length (snd x) < length (snd y) then x else y) (head xs) (tail xs))
        where xs = (resolvants c1 c2)

resolvantsAll:: KeyClause -> [KeyClause] -> [(Resolve, Clause)]
resolvantsAll _ [] = []
resolvantsAll c (k:ks) = nubBy (\x y -> snd x == snd y )  [r| r<-(resolvants c k) ++ (resolvantsAll c ks), not(testTrue $ snd r)]

testTrue :: EClause -> Bool
testTrue [] = False
testTrue (l:c) = if lNegate l `elem` c then True else testTrue c

removeTrues:: [EClause] -> [EClause]
removeTrues [] = []
removeTrues (c:cs) = if testTrue c then removeTrues cs else c: removeTrues cs

removeTruesK:: [KeyClause] -> [KeyClause]
removeTruesK [] = []
removeTruesK (c:cs) = if testTrue $ snd c then removeTruesK cs else c: removeTruesK cs
-- proof checking
aa1 :: ConjForm
aa1 = makeInputAux "[[~7,8,1],[6,3,3,~1,~4,9],[~7,4,~8,4,5],[~1,5,6,~1],[6],[9,~4,~2,1,~4,8,~8,10],[9,~4,~3,3,2,~7,10,9],[7,~2,~5,3,~5],[~7,~8,10,~6],[6,~2,3,~8,~9,~2,5,~2],[1,5,6,8,~10,~10,~10],[6,~6,~8,5,2],[2,10,~7,9,~1,10,~5],[7,~7,5,~3,~5,~9,~5],[3,4,5,~1,~7],[3,~2],[~6,~5,4,6,~1,~1],[1,1,~4],[~3,6,~6,~8,2],[~7,~5,5,2,~8,1,~4],[~8],[4,~1,4,~3],[3,2],[~5,4,3,~8,~4,~6],[~2,9,4,6],[5,3,~8,1,5,~6,~4],[~5,1,1,~5,1,4,~10],[~7,6,3],[~3,9],[5,8,6,6,~8,~8],[6,5,2],[~2,1,~2,5,1,~1,~4,~4],[~7,7],[7,6,7],[6,9],[~5,~2,~9,~6,~8,2,~4],[2,~9],[8,~4],[~7,~4,~10,7],[2,2,~5,~6],[~1],[4,~2,~5,~4,10,4,6,~5],[2,~8,2,3,~2,~10],[6,~7,5,4,~3,2,~10,7],[~9,6,5,~1,2,~2],[~8,2],[8,8,~6],[~4,4,~2,~6,~2,9,~2],[4,8,7,6],[2,~6,~9,10,~3,6,4,8],[2,~5]]"
r1 = Refutation [Resolve "3" 22 28,Resolve "6" 4 46,Resolve "8" 52 20]

zipToKey xs = zip [0..(length xs)] xs

aa2 :: ConjForm
aa2 = makeInputAux "[[2,~10,10],[5,6,6,~2,~6,~5],[~2,7],[~7,1],[10,~10,10,2,3,~1,~10],[8],[~6,2]]"
r2 = Model ["8","2"]

aa3 :: ConjForm
aa3 = makeInputAux "[[2,~3,3],[1,~2],[2,4]]"
r3 = Model ["8","2"]

aa4 :: ConjForm
aa4 = makeInputAux "[[5,~1,~7,8],[~8],[~2,~8,5,~1,~1],[~3,~4,~5,~5],[8,~7],[3,7],[5],[7,~3,~5,~6],[~7],[8],[~6,5],[7,6,~3],[6,5],[2,1],[6],[3,~6],[5,~4,~1,~3,5],[3,7,~6,4],[7],[~4,~3,~4,5,6],[~4,3,~4,~1,5],[~4,~2],[~1,~7,~8,3],[~5,~5,~8,7,~3],[7,8],[~8,~5]]"


aa5 :: ConjForm
aa5 = makeInputAux "[[2],[~2,~3,1],[~2,3,1]]"

aa6:: ConjForm
aa6 = makeInputAux "[[~2,~2,~6],[~2,1,2,~1,~2],[9,4,5,~5,4,3],[5,2,~7],[8],[1,5,~10,~4,~3,~5,~7],[~1,~6,2,~1,~6,6,4],[2],[1,~3,3,4,10,9,~5],[2,5,8,9,~2,~6,~7,6],[7,9,10,~7],[2,~3,6,~3,~1,4],[~9,5,~7,~3],[~6,5],[3,~6,7,~10],[~5],[9,8,~7,~7,~2,5],[~6,9],[~5,~1,~8,~4,~7],[~1,~3,~6,1,8,~2,5,7],[1,~3],[7,~3,~8],[~5,6,8,7,~1,~8],[7,~3,10,~5,~6,5,6],[3,~6,7,~10],[2,~1,8,~6],[5,1,7,~10,~4,~9],[6,~9,~9],[~9,~10,~6,~1,~8,~3,~9],[~5,~10],[~9,8,~7,9,~5,~9],[~1,~2,~8,~3,8],[5,~2],[~5,10,~2,~2],[10,~4,~7,7,~2,7],[~4,4,~5,7],[~2,6],[5,~10,1,~3,~10,~8,~9],[~3]]"

-- don't change the type nor expected behaviour
proofCheck :: ConjForm -> Proof -> Bool
proofCheck cnf (Refutation []) = True
proofCheck cnf (Refutation [(Resolve n k1 k2)]) = (resolve n (cnf!!k1) (cnf!!k2) )== []
proofCheck cnf (Refutation ((Resolve n k1 k2):rs)) = proofCheck (cnf ++ [resolve n (cnf!!k1) (cnf!!k2)]) (Refutation rs)
proofCheck [] (Model vs) = True
proofCheck (c:cnf) (Model vs) = if (checkClause c vs) then proofCheck cnf (Model vs) else False

checkClause :: Clause -> EValuation -> Bool
checkClause [] _ = False
checkClause ((Literal Pos n):ls) vs = if n `elem` vs then True else checkClause ls vs
checkClause ((Literal Neg n):ls) vs = if n `notElem` vs then True else checkClause ls vs

-- feel free to change behaviour and type  [EKeyClause] -> Maybe KeyClause
selClause :: SelClauseStrategy 
selClause [] = Nothing
selClause  xs = Just (head xs)

selClause2 :: SelClauseStrategy 
selClause2 [] = Nothing
selClause2  xs = Just (last xs)

getSmallest :: SelClauseStrategy
getSmallest [] = Nothing
getSmallest xs = Just (foldr (\x y -> if length (snd x) < length (snd y) then x else y) (head xs) (tail xs))

-- feel free to change behaviour and type  -> (proof, [EKeyClause])
resolutionParamX :: SelClauseStrategy -> ConjForm -> (Proof, KeyConjForm)
resolutionParamX _ cnf = resHelper [0..((length cnfU) - 1)] [] [] cnfU
                    where cnfU = removeTrues cnf

resolutionParam :: SelClauseStrategy -> ConjForm -> (Proof, KeyConjForm)
resolutionParam _ cnf = resolutionParamT cnf

resHelper :: [Int] -> [Int] -> [Resolve] -> ConjForm -> (Proof, KeyConjForm)
resHelper [] p r cnf = (Model (extractModel (mapNumbersToCNF cnf  p)), mapToKC cnf p)
resHelper u p r cnf 
        | uc == Nothing = (Refutation r, [])
        | otherwise = resUp u (mapToKC cnf p)  r cnf uc
        where uc = selClause (mapToKC cnf u)
                               
resUp :: [Int] -> [KeyClause] -> [Resolve] -> ConjForm -> Maybe KeyClause -> (Proof, KeyConjForm)
resUp u p r cnf Nothing = resHelper u (map fst p) r cnf
resUp u p r cnf (Just uc) 
        | testTrue $ snd uc  = resHelper (map fst uo) (map fst p) r cnf
        | otherwise = resHelper (nub u2) (map fst p2) r2 cnf2
        where uo = filter (\x -> x /= uc) (mapToKC cnf u)
              xs = resolvantsAll uc p
              nr = map fst xs
              nu = map snd xs
              r2 = r ++ nr
              u2a = [nC| nC <- nu, nC `notElem` map snd uo, not(testTrue nC)]
              u2 = (map fst uo) ++ map fst (zip [ulen..(ulen + length u2a)] u2a)
                    where ulen = length u
              p2 = p ++ [uc]
              cnf2 = cnf ++ u2a

resolutionParamT :: ConjForm -> (Proof, KeyConjForm)
resolutionParamT cnf = resHelperTree [] [] (createTreeK cnfU Leaf) (createTreeL cnfU Leaf) (length cnf)
                    where cnfU = removeTruesK kCnf
                          kCnf = zipToKey cnf
             -- [0..((length cnfU) - 1)]

resHelperTree :: [KeyClause] -> [Resolve] -> Tree KeyClause -> Tree KeyClause -> Int -> (Proof, KeyConjForm)
resHelperTree p res Leaf Leaf _ = (Model (extractModel $ map snd p), p)
resHelperTree p res ktree ltree count
            | snd uc0 == [] = (Refutation res, [uc0])
            | testTrue $ snd uc0  = resHelperTree p resU ktree0 ltree0 count
            | [] `elem` (map snd ns) = (Refutation resU, p)  --zip [1..20] (map snd ns)mapKeyTreeToConjForm ltree
            | otherwise           = resHelperTree pU resU ktree2 ltree2 (count+length ns)
            where (uc0,ltree0) = popRoot ltree
                  ktree0       = removeNode ktree uc0
                  ns     = filter (\x -> (snd x) `notElem` (map snd p) && notInTree (snd x) ltree) (resolvantsAll uc0 p)
                  resU    = res ++ map fst ns
                  (ktree2, ltree2) = insertAll ns ktree0 ltree0 count
                  pU      = p ++ [uc0]

insertAll:: [(Resolve, Clause)] -> Tree KeyClause -> Tree KeyClause -> Int -> (Tree KeyClause, Tree KeyClause)
insertAll [] ktree ltree _ = (ktree, ltree)
insertAll (x:xs) ktree ltree count = insertAll xs (insertTreeK (count,snd x) ktree) (insertTreeL (count,snd x) ltree) (count+1)

                 {- (uc1, ucR)   = getSecond uc0 ltree0
                  ktree1       = removeNode ktree0 uc1
                  ltree1       = removeNode ltree0 uc1
                  --ucR         = bestResolvant uc0 uc1
                  pU          = p ++ [uc0, uc1]
                  resU        = res ++ [fst ucR]
                  ktree2      = insertTreeK (count+1, snd ucR) ktree1
                  ltree2      = insertTreeL (count+1, snd ucR) ltree1-}


notInTree:: Clause -> Tree KeyClause -> Bool
notInTree _ Leaf = True
notInTree c (Node l x r)
          |snd x == c = False
          | (length $ snd x) > length c = notInTree c l
          |otherwise = notInTree c r


{-getSecond :: KeyClause -> Tree KeyClause -> (KeyClause, (Resolve, Clause))
getSecond uc0 (Node Leaf x Leaf) = if rs == [] then (x, x++uc0) else (x, (head rs))
            where rs = resolvants uc0 x
getSecond uc0 tree = if rs == [] then getSecond uc0 tree1 else (uc1, (head rs))
        where (uc1, tree1) = popRoot tree
              rs           = resolvants uc0 uc1-}


{-resolvantsAllT:: KeyClause -> Tree KeyClause -> [(Resolve, Clause)]
resolvantsAllT _ Leaf = []
resolvantsAllT c (Node l x r) = [res| res<-((resolvants c x) ++ (resolvantsAllT c l)++(resolvantsAllT c r)), not(testTrue $ snd res)]

resHelperTree p res ktree ltree count
            | snd uc0 == [] = (Refutation res, [])
            | otherwise           = resHelperTree pU resU ktree2 ltree2 (count+1)
            where (uc0,ltree0) = popRoot ltree
                  ktree0      = removeNode ktree uc0
                  --(uc1,ltree1) = popRoot ltree0
                  --ktree1      = removeNode ktree0 uc1
                  ucR         = resolvantsAllT uc0 ltree0
                  rl          = length ucR
                  pU          = p ++ [fst uc0]
                  resU        = res ++ map fst ucR
                  ktree2      = insertTreeK (count+rl, snd ucR) ktree0
                  ltree2      = insertTreeL (count+rl, snd ucR) ltree0

                  resHelperTree [] res ktree ltree _ = (Model (extractModel $ mapKeyTreeToConjForm ktree), treeToList ktree)-}

mapNumbersToCNF :: ConjForm -> [Int] -> ConjForm
mapNumbersToCNF cnf xs = map (\i -> cnf !! i)  xs

mapToKC :: ConjForm -> [Int] -> KeyConjForm
mapToKC cnf xs = map (\i -> (i,cnf !! i))  xs

mapKeyTreeToConjForm :: Tree KeyClause -> ConjForm
mapKeyTreeToConjForm Leaf = []
mapKeyTreeToConjForm (Node l x r) =  snd x : (mapKeyTreeToConjForm l ++ mapKeyTreeToConjForm r)
{-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


makeInputAux :: [Char] -> EConjForm
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] -> EClause
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)