module LAI10

where 
import List
import Char
import LAI9

s5example :: EpistM Integer
s5example = 
 Mo [0..3]
    [a..c]
    [(0,[]),(1,[P 0]),(2,[Q 0]),(3,[P 0, Q 0])]
    ([ (a,x,x) | x <- [0..3] ] ++
     [ (b,x,x) | x <- [0..3] ] ++
     [ (c,x,y) | x <- [0..3], y <- [0..3] ])
    [1]

rel :: Agent -> EpistM a -> Rel a
rel a (Mo states agents val rels actual) = 
      [ (x,y) | (agent,x,y) <- rels, a == agent ]

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

initM :: [Agent] -> [Prop] -> EpistM Integer
initM ags props = (Mo worlds ags val accs points) 
  where 
    worlds = [0..(2^k-1)]
    k      = length props
    val    = zip worlds (sortL (powerList props))
    accs   = [ (ag,st1,st2) | ag  <- ags, 
                              st1 <- worlds, 
                              st2 <- worlds      ]
    points = worlds

genK :: Ord state => [(Agent,state,state)] 
                      -> [Agent] -> Rel state
genK r ags = [ (x,y) | (a,x,y) <- r, a `elem` ags ]

rightS :: Ord a => Rel a -> a -> [a]
rightS r x = (sort.nub) [ z | (y,z) <- r, x == y ]

genAlts :: Ord state => [(Agent,state,state)] 
        -> [Agent] -> state -> [state]
genAlts r ags s = rightS (genK r ags) s

lfp :: Eq a => (a -> a) -> a -> a
lfp f x | x == f x  = x
        | otherwise = lfp f (f x)

rtc :: Ord a => [a] -> Rel a -> Rel a
rtc xs r = lfp (\ s -> (sort.nub) (s ++ (r@@s))) i
  where i = [(x,x) | x <- xs ]

tc :: Ord a => Rel a -> Rel a 
tc r = lfp (\ s -> (sort.nub) (s ++ (r @@ s))) r

commonK :: Ord state => [(Agent,state,state)] 
           -> [Agent] -> [state] -> Rel state
commonK r ags xs = rtc xs (genK r ags)

commonAlts :: Ord state => [(Agent,state,state)] 
        -> [Agent] -> [state] -> state -> [state]
commonAlts r ags xs s = rightS (commonK r ags xs) s

data Form = Top 
          | Prop Prop 
          | Neg Form 
          | Conj [Form]
          | Disj [Form]
          | K Agent Form 
          | EK [Agent] Form 
          | CK [Agent] Form 
          deriving (Eq,Ord)

p = Prop (P 0)
q = Prop (Q 0)

instance Show Form where 
  show Top           = "T" 
  show (Prop p)      = show p
  show (Neg f)       = '-':(show f)
  show (Conj fs)     = '&': show fs
  show (Disj fs)     = 'v': show fs
  show (K agent f)   = '[':show agent++"]"++show f 
  show (EK agents f) = 'E': show agents ++ show f
  show (CK agents f) = 'C': show agents ++ show f

test1 = isTrueAt 
  (initM [a..c] [P 0]) 0 
  (CK [a..c] (Neg (K a p)))

isTrue :: Ord state => EpistM state -> Form -> Bool
isTrue m@(Mo worlds agents val acc points) f = 
  and [ isTrueAt m s f | s <- points ]

test2 = isTrue 
        (initM [a..c] [P 0]) 
        (CK [a..c] (Neg (K a p)))

upd_pa :: Ord state => 
          EpistM state -> Form -> EpistM state
upd_pa m@(Mo states agents val rels actual) f = 
  (Mo states' agents val' rels' actual') 
   where 
   states' = [ s | s <- states, isTrueAt m s f ]
   val'    = [(s,p) | (s,p) <- val, 
                       s `elem` states'   ]
   rels'   = [(a,x,y) | (a,x,y) <- rels, 
                         x `elem` states',
                         y `elem` states' ]
   actual' = [ s | s <- actual, isTrueAt m s f ]

m0 = initM [a..c] [P 0,Q 0]

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 ]

powerList  :: [a] -> [[a]]
powerList  [] = [[]]
powerList  (x:xs) = (powerList xs) ++ (map (x:) (powerList xs))

sortL :: Ord a => [[a]] -> [[a]]
sortL  = sortBy (\ xs ys -> if length xs < length ys then LT
                               else if length xs > length ys then GT
                               else compare xs ys) 

alternatives :: Eq state => 
                [(Agent,state,state)] -> Agent -> state -> [state]
alternatives rel ag current = 
  [ s' | (a,s,s') <- rel, a == ag, s == current ] 

expand :: Ord state => 
          [(Agent,state,state)] -> [Agent] -> [state] -> [state]
expand rel agnts ys = 
      (nub . sort . concat) 
         [ alternatives rel ag state | ag    <- agnts, 
                                       state <- ys       ]
closure ::  Ord state => 
            [(Agent,state,state)] -> [Agent] -> [state] -> [state]
closure rel agents xs = lfp f xs 
  where f = \ ys -> (nub .sort) (ys ++ (expand rel agents ys))

isTrueAt :: Ord state =>
     EpistM state -> state -> Form -> Bool
isTrueAt m w Top = True 
isTrueAt
 m@(Mo worlds agents val acc points) w (Prop p) = 
 elem p (concat [props|(w',props) <- val, w'==w ])
isTrueAt m w (Neg f)   = not (isTrueAt m w f) 
isTrueAt m w (Conj fs) = and (map (isTrueAt m w) fs)
isTrueAt m w (Disj fs) = or  (map (isTrueAt m w) fs)

isTrueAt
 m@(Mo worlds agents val acc points) w (K ag f) = 
 and (map (flip (isTrueAt m) f) 
          (rightS (rel ag m) w))
isTrueAt 
 m@(Mo worlds agents val acc points) w (EK ags f) = 
 and (map (flip (isTrueAt m) f) 
          (genAlts acc ags w))
isTrueAt 
 m@(Mo worlds agents val acc points) w (CK ags f) = 
 and (map (flip (isTrueAt m) f) 
          (commonAlts acc ags worlds w))

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

convert :: Eq state => 
           EpistM state -> EpistM Integer
convert (Mo states agents val rels actual) = 
 Mo states' agents val' rels' actual'
   where 
    states' = map f states
    val'    = map (\ (x,y) -> (f x,y)) val
    rels'   = map (\ (x,y,z) -> (x, f y, f z)) rels
    actual' = map f actual
    f       = apply (zip states [0..])

ec :: Ord a => Rel a -> Rel a 
ec r = lfp (\ s -> (sort.nub) (s ++ (cnv s @@ s))) r