module Exercises1 where

import List

{- datatype for agents -} 

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"

{- datatype for basic propositions -} 

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

{- datatype for epistemic models with sets of designates states
   (candidates for "the real world")                             -}

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

{- A type for relations, and an operator for relational composition -}

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 ]

{- Exercise 1: 

   implement a function 

     reflR :: Eq a => [a] -> Rel a -> Bool
   
   with the property that 

     reflR xs r
   
   yields True iff r is a reflexive
   relation on xs. 
-} 

{- Exercise 2: 

   implement a function 

     symR :: Eq a => Rel a -> Bool
   
   with the property that 

     symR r 
   
   yields True iff r is a symmetric relation. 
-} 


{- Exercise 3: 
   implement a function 
     
     transR :: Eq a => Rel a -> Bool

   with the property that 

     transR r

   yields True iff r is a transitive 
   relation. 

   (Hint: look at the method for checking euclideanness in 
   the course slides.)
-}

{- Exercise 4: 
   implement a function 
     
     isEquiv :: Eq a => [a] -> Rel a -> Bool

   with the property that 

     isEquiv xs r 

   yields True iff r is an equivalence relation on xs. 
-}   

{- Exercise 5: 

   use isEquiv to write a test

      isS5 :: Eq state => EpistM state -> Bool
   
   where 

      isS5 model 
 
   yields True iff model is an S5 model. 
-} 

{- Exercise 6: 

   A partition P of a set A is a set of subsets of A with the 
   following properties: 

   (i) every member of P is non-empty. 

   (ii) every element of A belongs to some member of P. 

   (iii) different members of P are disjoint. 

   If R is an equivalence relation on A, the equivalence
   class of a, notation |a|_R, is the set { b in A | bRa }.

   Show that the set of equivalence classes 

        { |a|_R | a in R } 

   of an equivalence relation R on A forms a partition of A. 

-}

{- Exercise 7:  HOMEWORK

   A list partition of a domain xs is a list of lists xxs
   with the following properties: 

   (1) no member of xxs is empty 

   (2) every member of xxs is in ascending order and without 
       duplicates

   (3) every element of xs occurs in exactly one element of xxs. 

   Write a function 

     list2partition :: (Eq a, Ord a) => [a] -> Rel a -> [[a]]

   with the property that 

     list2partition xs r

   gives an error message if r is not an equivalence on xs, 
   and otherwise gives the corresponding partition. 
-}