module LAI13 where 

import List
import Char
import LAI9
import LAI10
import LAI11
import LAI12

cartProduct :: [a] -> [a] -> Rel a

cartProduct xs ys = [ (x,y) | x <- xs, y <- ys]

composeR :: Eq a => Rel a -> Int -> Rel a

composeR r 1 = r
composeR r (n+1) = r @@ (composeR r n)

data AM state = Am
             [state]
             [Agent]
             [(state,Form)]
             [(Agent,state,state)]
             [state]  deriving (Eq,Show)

type FAM state = [Agent] -> AM state

up :: (Eq state, Ord state) => 
       EpistM state -> FAM state 
                    -> EpistM (state,state)

up m@(Mo worlds ags val rel points) fam = 
   Mo worlds' ags' val' rel' points'
   where 
   Am states ags' pre susp actuals = fam ags 
   worlds' = [ (w,s) | w <- worlds, s <- states, 
                    isTrueAt m w (apply pre s)    ]
   val'    = [ ((w,s),props) | (w,props) <- val, 
                                s        <- states, 
                                elem (w,s) worlds']
   rel'    = [ (ag1,(w1,s1),(w2,s2)) | 
                 (ag1,w1,w2) <- rel, 
                 (ag2,s1,s2) <- susp, 
                  ag1 == ag2, 
                  elem (w1,s1) worlds', 
                  elem (w2,s2) worlds'   ]
   points' = [ (p,a) | p <- points, a <- actuals, 
                       elem (p,a) worlds'         ]