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,Show)

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

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 ]