module LabExerc2 where

import List

data Agent = A | B | C | D | E deriving (Eq,Ord,Enum)

a, alice, b, bob, c, carol, d, dave, e, ernie  :: Agent
a = A; alice = A
b = B; bob   = B
c = C; carol = C
d = D; dave  = D
e = E; ernie = E

instance Show Agent where
  show A = "a"; show B = "b"; show C = "c"; show D = "d" ; show E = "e"

data Prop = P Int | Q Int | R Int deriving (Eq,Ord)

instance Show Prop where 
  show (P 0) = "p"; show (P i) = "p" ++ show i 
  show (Q 0) = "q"; show (Q i) = "q" ++ show i 
  show (R 0) = "r"; show (R i) = "r" ++ show i

data EpistM state = Mo 
             [state]
             [Agent]
             [(state,[Prop])]
             [(Agent,state,state)]
             [state]
             deriving Eq 

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])

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) 

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..])

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

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

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

type Rel a = [(a,a)]

infixr 5 @@

(@@) :: Eq a => Rel a -> Rel a -> Rel a
r @@ s = 
  nub [ (x,z) | (x,y) <- r, (w,z) <- s, y == w ]

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 ]

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

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

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


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 w (Conj fs) = and (map (isTrueAt m w) fs)
isTrueAt m w (Disj fs) = or  (map (isTrueAt m w) fs)
isTrueAt m@(Mo states agents val rels actual) 
         w (K ag form) =
         and [ isTrueAt m s form | 
                s <- rightS (rel ag m) w ] 
isTrueAt m@(Mo states agents val rels actual) 
         w (EK gr form) =
         and [ isTrueAt m s form | 
                s <- genAlts rels gr w ] 
isTrueAt m@(Mo states agents val rels actual) 
         w (CK gr form) =
         and [ isTrueAt m s form | 
                s <- commonAlts rels gr states w ]