module LAI16 where 

import List
import Char
import LAI9
import LAI10
import LAI11
import LAI12
import LAI13
import LAI14
import LAI15

data Frm = Bot  
         | Prp Prop 
         | Ng Frm 
         | Cnj [Frm]
         | Dsj [Frm]
         | Rl Rl Frm 
         | Publ Frm Frm
         deriving (Eq,Ord)

top = Ng Bot

imp f1 f2 = Ng (Cnj[f1,Ng f2])

data Rl = Ag Agent
        | Test Frm
        | Cmp [Rl]
        | Cup [Rl]
        | Star Rl
        deriving (Eq,Ord)

instance Show Frm where 
  show Bot = "B" ; show (Prp p) = show p
  show (Ng Bot) = "T"
  show (Ng (Cnj [f,Ng g])) = 
       '(' : show f ++ "=>" ++ show g ++ ")"
  show (Ng f) = '-':(show f)
  show (Cnj fs)   = '&': show fs
  show (Dsj fs)   = 'v': show fs
  show (Rl r f)   = '[': show r ++ "]" ++ show f 
  show (Publ f f')= '[': show f ++ "!]" ++ show f'

instance Show Rl where 
  show (Ag ag) = show ag
  show (Test f)= show f ++ "?"
  show (Cmp []) = ""
  show (Cmp [r]) = show r
  show (Cmp (r:rs)) = 
    show r ++ ";" ++ show (Cmp rs)
  show (Cup []) = ""
  show (Cup [r]) = show r
  show (Cup (r:rs)) = 
    show r  ++ " U " ++ show (Cup rs)
  show (Star r) = '(' : show r ++ ")*"

isTrAt :: Ord state =>
     EpistM state -> state -> Frm -> Bool
isTrAt m w Bot = False  
isTrAt  m@(Mo _ _ val _ _) w (Prp p) = 
  elem p (apply val w) 
isTrAt m w (Ng f)   = not (isTrAt m w f) 
isTrAt m w (Cnj fs) = and (map (isTrAt m w) fs)
isTrAt m w (Dsj fs) = or  (map (isTrAt m w) fs)
isTrAt m w (Rl r f) = 
   and [ isTrAt m v f | v <- rightS (semRl m r) w ]
isTrAt m w (Publ f1 f2) =  not (isTrAt m w f1) 
                     || isTrAt (upd_publ m f1) w f2

upd_publ :: Ord state => 
          EpistM state -> Frm -> EpistM state
upd_publ m@(Mo states agents val rels actual) f = 
  (Mo states' agents val' rels' actual') 
   where 
   states' = [ s | s <- states, isTrAt 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, isTrAt m s f ]

semRl :: Ord state => 
         EpistM state -> Rl -> Rel state

semRl (Mo _ _ _ rel _) (Ag b) = 
   [(x,y) | (ag,x,y) <- rel, ag == b ]

semRl m@(Mo worlds _ _ _ _) (Test f) = 
   [(x,x) | x <- worlds, isTrAt m x f ]

semRl m (Cmp [])  = []   
semRl m (Cmp [r]) = semRl m r
semRl m (Cmp (r:rs)) = 
   (semRl m r) @@ (semRl m (Cmp rs))

semRl m (Cup [])  = []
semRl m (Cup [r]) = semRl m r
semRl m (Cup (r:rs)) = 
   (nub.sort) ((semRl m r) ++ (semRl m (Cup rs)))

semRl m@(Mo worlds _ _ _ _) (Star r) = 
   rtc worlds (semRl m r)

tr :: Frm -> Frm
tr Bot = Bot
tr (Prp p) = Prp p
tr (Ng f)  = Ng (tr f)
tr (Cnj fs) = Cnj (map tr fs)
tr (Dsj fs) = Dsj (map tr fs)
tr (Rl r f) = Rl (trr r) (tr f)

tr (Publ f (Bot)) = Ng (tr f)
tr (Publ f (Prp p)) = imp (tr f) (Prp p)
tr (Publ f (Ng f')) = 
   imp (tr f) (Ng (tr (Publ f f')))
tr (Publ f (Cnj fs)) = 
   Cnj (map tr [ Publ f f' | f' <- fs ])
tr (Publ f (Dsj fs)) = 
   Dsj (map tr [ Publ f f' | f' <- fs ])
tr (Publ f (Rl r f')) = 
   Rl (transform f r) (tr (Publ f f'))
tr (Publ f (Publ f2 f3)) = 
   tr (Publ f (tr (Publ f2 f3)))

trr :: Rl -> Rl
trr (Ag a) = Ag a
trr (Test f) = Test (tr f)
trr (Cmp rs) = Cmp (map trr rs)
trr (Cup rs) = Cup (map trr rs)
trr (Star r) = Star (trr r)

transform :: Frm -> Rl -> Rl
transform f (Ag a)    = Cmp [Test (tr f), Ag a]
transform f (Test f') = 
  Test (Cnj [tr f,tr(Publ f f')])
transform f (Cmp rs)  = 
  Cmp (map (transform f) rs)
transform f (Cup rs)  = 
  Cup (map (transform f) rs)
transform f (Star r)  = Star (transform f r)

frm1 = Publ (Prp (P 0)) 
   (Rl (Star (Cup [Ag a,Ag b])) (Prp (Q 0)))

frm2 = Publ (Prp (P 0)) 
   (Rl (Star (Cup [Ag a,Ag b])) (Prp (P 0)))

initm = initM [a,b,c] [P 0,Q 0]

am ags = 
  Am [0,1,2] 
     ags 
     [(0,p),(1,p),(2,Top)] 
     ([(ag,x,x) | ag <- ags, x <- [0,1,2]] ++ 
            [(a,0,1),(a,1,0),(c,1,2),(c,2,1)])
     [0]

secret :: [Agent] -> Form -> FAM State
secret gr form agents = 
  if sort gr == sort agents 
    then public form agents
    else 
      (Am 
       [0,1] 
        agents
       [(0,form),(1,Top)] 
        ([ (a,0,0) | a <- gr ] 
          ++ [ (a,0,1) | a <- agents \\ gr ] 
          ++ [ (a,1,1) | a <- agents       ])
       [0])