module Exercise09 where

import Types

import Data.List (group, sort, sortOn, minimumBy)
import Data.Ord (Down(Down))
--import Debug.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

-- feel free to change behaviour and type
resolve :: Name -> Clause -> Clause -> Clause
resolve n cp cn = (map head . group . sort) (
      filter (\(Literal p' n')-> not( n'==n && p'==Pos ) ) cp 
  ++  filter (\(Literal p' n')-> not( n'==n && p'==Neg ) ) cn)


-- feel free to change behaviour and type
resolvants :: KeyClause -> KeyClause -> [(Resolve, Clause)]
resolvants (i1, k1) (i2, k2) = 
  [
    (
      if lIsPos l
      then Resolve (lName l) i1 i2
      else Resolve (lName l) i2 i1
      ,
      if lIsPos l 
      then resolve (lName l) k1 k2
      else resolve (lName l) k2 k1
    ) 
    | l <- filter (\x->
          lIsPos x && lNegate x `elem` k2 
      ||  lIsNeg x && lNegate x `elem` k2 
      ) k1
  ]


-- proof checking

-- don't change the type nor expected behaviour
proofCheck :: EConjForm -> Proof -> Bool
--proofCheck conj (Refutation proof) = proofCheck (snd (unzip (filter (\(i,c)->not(i == (head proof))) (zip [0..(length conj)] conj)))) (Refutation proof)
proofCheck [] (Refutation []) = True 
proofCheck [] _ = False 
proofCheck conj (Refutation []) = null(last conj)
proofCheck conj (Refutation proof) = proofCheck (resolveProofStep conj (head proof)) (Refutation (tail proof))
proofCheck conj (Model proof) = and [or [Literal Pos n `elem` clause | n<-proof] || or [lIsNeg l && notElem (lName l) proof | l<-clause]| clause <- conj]

resolveProofStep :: EConjForm -> EResolve -> EConjForm
resolveProofStep conj (Resolve n k1 k2) = 
  let numberedClauses = zip [0..(length conj)] conj in
  conj ++ 
  [
    resolve 
      n 
      (head (map snd (filter (\x->fst x == k1) numberedClauses)))
      (head (map snd (filter (\x->fst x == k2) numberedClauses)))
  ]

-- feel free to change behaviour and type
selClause :: SelClauseStrategy 
selClause conj
  | null conj = Nothing
  | otherwise = 
    let emptyClauses = filter (null . snd) conj in
    if not(null emptyClauses) then Just (head emptyClauses)
    else Just (minimumBy (\(a,x) (b,y)-> if length x > length y then GT else LT) conj)
    

-- feel free to change behaviour and type
resolutionParam :: SelClauseStrategy -> EConjForm -> (Proof, KeyConjForm)
resolutionParam strat conj = solve_iteration strat (zip [0..(length conj-1)] conj) [] [] (length conj)
  where 
    solve_iteration s c r p n = let uc = s c in
      maybe (Model (extractModel (map snd p)), p) iterate_c uc
      where
        iterate_c ac = let resolv_opts = filter (\x->snd x `notElem` map snd (p++c)) (concat [resolvants ac ap | ap <- p]) in
          if null (snd ac)
          then (Refutation r, c ++ p)
          else solve_iteration 
            s 
            (
              filter (\x->fst x /= fst ac) c 
              ++ 
              zip [n .. (n + length resolv_opts)] (map snd resolv_opts)
            )
            (r ++ map fst resolv_opts) 
            (ac : p)
            (n + length resolv_opts)
            --(trace ("n:" ++ show (n + length resolv_opts) ++ ": c:" ++ show c ++ " p:" ++ show p ++ " resolvOpts: " ++ show resolv_opts) (n + length resolv_opts))

--{-WETT-}
-- testing example: resolution [[Literal Pos "A"],[Literal Neg "B"]]

-- 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 :: EConjForm -> (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