module Sol2 
where 

import List 
import LabExerc2

containedIn :: Eq a => [a] -> [a] -> Bool
containedIn xs ys = all (\ x -> elem x ys) xs

cnv :: Rel a -> Rel a
cnv r = [ (y,x) | (x,y) <- r ]

reflR :: Eq a => [a] -> Rel a -> Bool
reflR xs r = containedIn [ (x,x) | x <- xs ] r 

symR :: Eq a => Rel a -> Bool
symR r = containedIn (cnv r) r

transR :: Eq a => Rel a -> Bool
transR r = (r @@ r) `containedIn` r

isEquiv :: Eq a => [a] -> Rel a -> Bool
isEquiv xs r = reflR xs r && symR r && transR r

list2partition :: (Eq a, Ord a) => [a] -> Rel a -> [[a]]
list2partition xs pairs = 
  if not (isEquiv xs pairs) then error "not an equivalence"
  else genPartition xs pairs 
     where genPartition [] pairs = []
           genPartition (x:xs) pairs = 
               xclass : genPartition (xs \\ xclass) pairs
                 where xclass = x : [ y | y <- xs, elem (x,y) pairs ]


showS5 :: (Ord a,Show a) => EpistM a -> [String]
showS5 m@(Mo states agents val rels actual) = 
  show states : 
  show val    : 
  map show [ (a, (list2partition states) (rel a m)) 
                                    | a <- agents ] 
  ++ 
  [show actual]

displayS5 ::  (Ord a,Show a) => EpistM a -> IO()
displayS5 = putStrLn . unlines . showS5

p,q :: Form
p = Prop (P 0)
q = Prop (Q 0) 

apply :: Eq a => [(a,b)] -> a -> b
apply [] _ = error "argument not in list"
apply ((x,z):xs) y | x == y    = z
                   | otherwise = apply xs y


isTrueAt :: Ord state =>
     EpistM state -> state -> Form -> Bool
isTrueAt m w Top = True 
isTrueAt m@(Mo states agents val rels actual) 
         w (Prop prop) = elem prop (apply val w)
isTrueAt m w (Neg form) = not (isTrueAt m w form)
isTrueAt m@(Mo states agents val rels actual) 
         w (CK gr form) =
         and [ isTrueAt m s form | 
                s <- commonAlts rels gr states w ]