module Exercise09 where

import Types

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

import Test.QuickCheck as QC





-- 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 nm cl1 cl2 = nub $ nCl1 ++ nCl2
    where nCl1 = [lt |lt <- cl1, lt /= (Literal Pos nm)]
          nCl2 = [lt | lt <- cl2, lt /= (Literal Neg nm)]



-- feel free to change behaviour and type
resolvants :: KeyClause -> KeyClause -> [(Resolve, Clause)]
resolvants (kOn, ltOns) kyClTw = frmMaybe [resolvantsAux lt (kOn, ltOns) kyClTw  | lt <- ltOns]


frmMaybe :: [Maybe (Resolve , Clause)] -> [(Resolve, Clause )]
frmMaybe [] = []
frmMaybe (Nothing:rs) = frmMaybe rs
frmMaybe ((Just rC):rs) = rC:(frmMaybe rs)

resolvantsAux :: Literal -> KeyClause -> KeyClause -> Maybe (Resolve, Clause)  --KeyClause : (Key, EClause) = (Int , [Eliteral]) = (Int, [Literal Polarity EName])
resolvantsAux (Literal Pos nm) (kOn, (ltOns)) (kTw, ltTws) =
   if  ngtd `elem` ltTws  && isPure rsltCls then  Just (rsl, rsltCls) else Nothing
    where ngtd = Literal Neg nm
          rsl = Resolve nm kOn kTw
          rsltCls = resolve nm ltOns ltTws
resolvantsAux (Literal Neg nm) (kOn, (ltOns)) (kTw, ltTws) = 
  if pstd `elem` ltTws && isPure rsltRevCls then Just (rslRev, rsltRevCls) else Nothing 
    where pstd = Literal Pos nm 
          rslRev = Resolve nm kTw kOn 
          rsltRevCls = resolve nm ltTws ltOns

isPure :: Clause -> Bool
isPure cl = and [isPrAux lt cl | lt <- cl]

isPrAux :: Literal  -> Clause -> Bool
isPrAux lt cls = not $ (lNegate lt) `elem` cls


-- proof checking

-- don't change the type nor expected behaviour
proofCheck :: ConjForm -> Proof -> Bool
proofCheck cnjFrm (Model vl) = eval vl cnjFrm 
proofCheck cnjFrm (Refutation rls) = isEmptyPart allCnjFrm 
     where allCnjFrm = auxRslv cnjFrm rls

isEmptyPart :: ConjForm -> Bool 
isEmptyPart [] = False
isEmptyPart (x:xs) = null x || isEmptyPart xs

allRslEmpty :: ConjForm -> Bool
allRslEmpty cnjForm = and [cla `elem` cnjForm | cla <- allCls]
      where kyCl = toKyCl cnjForm 
            allRsl = concat [resolvants clOn clTw | clOn <- kyCl, clTw <- kyCl]
            allCls = map snd allRsl 

toKyCl :: ConjForm -> [KeyClause]
toKyCl cls = zip [0.. ((length cls) - 1)] cls

--ConjForm = [EClause] = [[Literal Polarity EName]]
--test

auxRslv :: ConjForm -> [EResolve] -> ConjForm 
auxRslv clss [] = clss 
auxRslv clss ((Resolve nm kOn kTw):rsls) = auxRslv (clss ++ [resolve nm (clss !! kOn) (clss !! kTw)]) rsls

-- feel free to change behaviour and type
selClause :: SelClauseStrategy 
selClause xs = Just (head mins)
   where mini = minimum $ map length xs
         mins = filter (\x-> (length x) == mini) xs 
selClause [] = Nothing


-- feel free to change behaviour and type
resolutionParam :: SelClauseStrategy -> ConjForm -> (Proof, KeyConjForm)
resolutionParam stra cnjFr = resAux stra kyCf kyCf [] []
      where kyCf = zip [0 .. ((length cnjFr)-1)] cnjFr

sngls :: KeyConjForm -> [Literal]
sngls kyClss = nub [head cl | (_, cl) <- kyClss, length cl == 1]

sbsmptn :: KeyConjForm -> [Literal] -> KeyConjForm 
sbsmptn kyCnF lts = foldr (\lt kC -> sbsAux lt kC) kyCnF lts
         
sbsAux :: Literal -> KeyConjForm -> KeyConjForm
sbsAux lt kClss = [(ky, cl) | (ky, cl) <- kClss, notElem lt cl || length cl == 1]
 
-- sbsAuxCl :: Literal -> 


resAux :: SelClauseStrategy -> KeyConjForm -> KeyConjForm ->  KeyConjForm  ->[EResolve] -> (Proof, KeyConjForm)
resAux sel uB all pB r 
     | null u = (Model $ nub $ extractModel $ keyToNo all, all)
     | otherwise  = if null uc then (Refutation r, all) else resAux sel uu alll pp rr
    where sinls = sngls (uB ++ pB)
          u = sbsmptn uB sinls 
          p = sbsmptn pB sinls
          (ky, uc) = frmMb $ selClause u
          uTmp = auxDel u ky
          nrNU = allRslvnt (ky, uc) p all 
          (nr, nu) = nrnu nrNU ([], [])
          nuK = zip [length all .. (length all) + (length nu) -1] nu
          rr = r ++ nr 
          uu = uTmp ++ nuK
          pp = p ++ [(ky, uc)]
          alll = all ++ nuK 

allRslvnt :: KeyClause -> KeyConjForm -> KeyConjForm -> [(Resolve, Clause)]
allRslvnt uc p all= [(rs, cl) | (rs, cl) <- dupls, null cl || (not (clElemCls cl allCnF))]
   where dupls = concat (map (resolvants uc) p)
         allCnF = keyToNo all

clElemCls :: Clause -> ConjForm -> Bool 
clElemCls lts cls = or (map (eql lts) cls)

eql :: Clause -> Clause -> Bool 
eql ltsOne clT = (and [lt `elem` clT | lt <- ltsOne]) && (and [ltT `elem` ltsOne | ltT <- clT])

nrnu :: [(Resolve, Clause)] -> ([Resolve], [Clause]) -> ([Resolve], [Clause])
nrnu ((re, cl):rst) (rs, cls) =  nrnu rst (rs ++ [re], cls ++ [cl])
nrnu [] (rs, cls) = (rs, cls)

frmMb :: Maybe KeyClause -> KeyClause
frmMb (Just kcl) = kcl

auxDel :: KeyConjForm -> Int -> KeyConjForm 
auxDel ((n, cl):kyCls)  nd = if n == nd then kyCls else (n, cl):auxDel kyCls nd

keyToNo :: KeyConjForm -> ConjForm
keyToNo cj = map snd cj



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