module Exercise09 where

import Data.List (delete, nub, sort, sortOn)
import Data.Ord (Down (Down))
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 [] = 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 (delete np cp ++ delete nn cn)
  where
    np = Literal Pos n
    nn = Literal Neg n

-- feel free to change behaviour and type
resolvants :: KeyClause -> KeyClause -> [(Resolve, Clause)]
resolvants (pk, cp) (nk, cn) = map (\(Literal _ n) -> (Resolve n pk nk, resolve n cp cn)) bothP ++ map (\(Literal _ n) -> (Resolve n nk pk, resolve n cn cp)) bothN
  where
    bothP = [c | c <- cp, lIsPos c, lNegate c `elem` cn]
    bothN = [c | c <- cn, lIsPos c, lNegate c `elem` cp]

-- proof checking

-- don't change the type nor expected behaviour
notNull :: [a] -> Bool
notNull = not . null

-- getDuplicate :: ConjForm -> Clause
-- getDuplicate form = [l | c <- form, l <- c, lNegate l `elem` concat (delete c form)]

hasDuplicate :: Clause -> Bool
hasDuplicate c = any (`elem` c) nc
  where
    nc = map lNegate c

-- removeDuplicate :: ConjForm -> ConjForm
-- removeDuplicate = map (\c -> if hasDuplicate c then [] else c)

proofCheck :: ConjForm -> Proof -> Bool
proofCheck _ (Refutation []) = True
proofCheck form (Refutation ((Resolve n kp kn) : rs)) = w
  where
    l = length form
    cp = form !! kp
    cn = form !! kn
    has = lPos n `elem` cp && lNeg n `elem` cn
    nForm = form ++ [resolve n cp cn]
    w = kp < l && kn < l && has && proofCheck nForm (Refutation rs)
--
proofCheck form (Model m) = all or formB
  where
    formB = map (map (\l -> if lName l `elem` m then lIsPos l else lIsNeg l)) form

-- proofCheck form (Model (m : ms)) = notNull pfs && notNull nfs && proofCheck nnfs (Model ms)
--   where
--     mp = lPos m
--     mn = lNeg m
--     pfs = [c | c <- form, mp `elem` c]
--     npfs = delete pf form
--     pf = head pfs
--     nfs = [c | c <- npfs, mn `elem` c]
--     nnfs = delete nf npfs
--     nf = head nfs

-- feel free to change behaviour and type
selClause :: SelClauseStrategy
selClause [] = Nothing
selClause (u : _) = Just u

-- feel free to change behaviour and type
keys :: ConjForm -> Int -> KeyConjForm
keys [] _ = []
keys (f : fs) n = (n, f) : keys fs (n + 1)

sortKey :: KeyConjForm -> KeyConjForm
sortKey = sortOn (length . snd)

same :: EClause -> EClause -> Bool
same k g = length k == length g && all (`elem` g) k

-- removeDuplicate :: KeyConjForm -> KeyConjForm -> KeyConjForm
-- removeDuplicate [] _ = []
-- removeDuplicate (kc : kcs) ks = if there then removeDuplicate kcs ks else kc : removeDuplicate kcs (kc : ks)
--   where
--     c = snd kc
--     there = not (null kc) && any (incl c . snd) (ks ++ kcs)

removeAlready :: [(Resolve, Clause)] -> ConjForm -> [(Resolve, Clause)]
removeAlready [] _ = []
removeAlready (kc : kcs) ks = if there then removeAlready kcs ks else kc : removeAlready kcs (snd kc : ks)
  where
    there = not (null (snd kc)) && any (same (snd kc)) ks

resolutionParamHelper :: Int -> SelClauseStrategy -> KeyConjForm -> KeyConjForm -> (Proof, KeyConjForm)
resolutionParamHelper keyStart sel u p = result
  where
    (Just uc) = sel u
    resoAll = concatMap (resolvants uc) p
    reso = removeAlready (filter (not . hasDuplicate . snd) resoAll) (map snd (p ++ u))
    newUs = map snd reso
    keyNewUs = keys newUs keyStart
    sortKeyNewUs = sortKey keyNewUs
    r = map fst reso
    newU = sortKeyNewUs ++ tail u
    newP = uc : p
    emptyUc = null (snd uc)
    (proof, endU) = resolutionParamHelper (keyStart + length newUs) sel newU newP
    loopRestResult (Refutation rs) = (Refutation (r ++ rs), endU)
    loopRestResult (Model v) = (Model v, endU)
    loopResult = if emptyUc then (Refutation r, u) else loopRestResult proof
    result = if notNull u then loopResult else (Model (extractModel p), u)

resolutionParam :: SelClauseStrategy -> ConjForm -> (Proof, KeyConjForm)
resolutionParam sel form = resolutionParamHelper formLength sel filterForm []
  where
    formLength = length form
    keyForm = keys (map nub form) 0
    sortKeyForm = sortKey keyForm
    filterForm = filter (not . hasDuplicate . snd) sortKeyForm

{-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 :: KeyConjForm -> Valuation
extractModel = run [] . sort . map (sortOn Down . snd)
  where
    run val [] = val
    run val (c : cs)
      | evalClause val c = run val cs
      | otherwise = run (lName (head c) : val) cs

m :: (Proof, KeyConjForm)
m = resolution [[Literal Pos "1"]]

re :: (Proof, KeyConjForm)
re = resolution [[Literal Pos "1"], [Literal Neg "2", Literal Pos "2"], [Literal Neg "2"]]

s =
  [ [Literal Neg "8"],
    [Literal Neg "8", Literal Neg "4"],
    [Literal Pos "4", Literal Pos "8"]
  ]

small :: (Proof, KeyConjForm)
small = resolution s