module RPAU

where 
import List
import HFKR

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

symmR :: Eq a => Rel a -> Bool
symmR r = cnv r `containedIn` r

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

isS5 :: Eq a => [a] -> Rel a -> Bool
isS5 xs r = reflR xs r && transR r && symmR r 

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]

dom :: EpistM a -> [a]
dom (Mo states _ _ _ _) = states

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

valuation ::  EpistM a -> [(a,[Prop])]
valuation (Mo _ _ val  _ _ ) = val

rel2partition :: Ord a => [a] -> Rel a -> [[a]]
rel2partition [] r = []
rel2partition (x:xs) r = 
   xclass :  rel2partition (xs \\ xclass) r
     where 
       xclass = x : [ y | y <- xs, elem (x,y) r ]

showS5 :: (Ord a,Show a) => EpistM a -> [String]
showS5 m@(Mo states agents val rels actual) = 
  show states : 
  show val    : 
  map show [ (a, (rel2partition 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

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) 

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 
          | 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 (CK agents f) = 'C': show agents ++ show f

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

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, s `elem` states' ]

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

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

gsm :: Ord state => EpistM state ->  EpistM state
gsm (Mo states ags val rel points) = (Mo states' ags val' rel' points)
   where 
   states' = closure rel ags points
   val'    = [(s,props) | (s,props)     <- val, 
                           elem s states'                   ]
   rel'    = [(ag,s,s') | (ag,s,s') <- rel, 
                           elem s states', 
                           elem s' states'                  ]

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

expand :: Ord state => 
           [(Agent,state,state)] -> [Agent] -> [state] -> [state]
expand rel agnts ys = 
      (nub . sort . concat) 
         [ alternatives rel ag state | ag    <- agnts, 
                                       state <- ys       ]

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

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 (CK ags f) = 
 and (map (flip (isTrueAt m) f) 
          (commonAlts acc ags worlds w))

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