module Exerc1_Uitw 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 ]

containedIn :: Eq a => [a] -> [a] -> Bool
containedIn xs ys =  all (\x -> elem x ys) xs 

cnv :: Rel a -> Rel a
cnv r = [ (y,x) | (x,y) <- r ]

{- Exercise 1: 

   implement a function 

     reflR :: Eq a => [a] -> Rel a -> Bool 

   
   with the property that 

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

{- Solution -} 

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

{- Exercise 2: 

   implement a function 

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

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

{- Solution -} 

symR :: Eq a => Rel a -> Bool
symR r = containedIn (cnv r) r

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

   with the property that 

     transR pairs 

   yields True iff pairs is a transitive 
   relation. 
-}

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

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

   with the property that 

     isEquiv xs pairs 

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

{- solution -} 

isEquiv :: Eq a => [a] -> Rel a -> Bool
isEquiv xs r = reflR xs r && symR r && transR r

{- Exercise 5: 

   use isEquiv to write a test

      isS5 :: EpistM -> Bool
   
   where 

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

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

isS5 :: Eq a => EpistM a -> Bool
isS5 m@(Mo states agents val rels actual) = 
  all (isEquiv states) [ rel a m |  a <- agents ]

{- 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. 

Answer. We have to check the three properties of partitions. 

Since R is reflexive of A, we have that for each a in A
it holds that a in |a|_R. This takes care of (i) and (ii). 

Let |a|_R and |b|_R be two equivalence classes, and assume that 
they are not disjoint. Then we have c in |a|_R \cap |b|_R. 

This means that we have both aRc and bRc. Since R is symmetric, we 
have cRb, and by transitivity of R, aRb, and again by symmetry of R, 
bRa. 

We can show now that |a|_R = |b|_R, as follows: 

Assume d in |a|_R. Then dRa. From this and aRb, by transitivity of 
R, dRb, i.e. d in |b|_R. This shows:  |a|_R \subseteq |b|_R. 

Assume d in |b|_R. Then dRb. From this and bRa, by transitivity of R, 
dRa, i.e., d in |a|_R. This shows: |b|_R \subseteq |a|_R. 

So if two equivalence classes |a|_R and |b|_R are not disjoint, 
then they are in fact equal. This takes care of (iii).

-}

{- 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 pairs 

   gives an error mesage is pairs is not an equivalence on xs, 
   and otherwise gives the corresponding partition. 

-} 

{- Solution -} 

list2partition :: (Eq a, Ord a) => [a] -> Rel a -> [[a]]
list2partition xs pairs = 
  if not (isEquiv xs pairs) then error "not an equivalence"
  else genPartition xs pairs 
     where genPartition [] pairs = []
           genPartition (x:xs) pairs = 
               xclass : genPartition (xs \\ xclass) pairs
                 where xclass = x : [ y | y <- xs, elem (x,y) pairs ]

{- Note:

   The function list2partition can be used to write a display function for 
   S5 models that shows each accessibility relation as a partition, as 
   follows. 

-}

showS5 :: (Ord a,Show a) => EpistM a -> [String]
showS5 m@(Mo states agents val rels actual) = 
  show states : 
  show val    : 
  map show [ (a, (list2partition states) (rel a m)) | a <- agents ] 
  ++ 
  [show actual]
 

{- we get: 

Exerc1_Uitw> (putStrLn . unlines . showS5) s5example
[0,1,2,3]
[(0,[]),(1,[p]),(2,[q]),(3,[p,q])]
(a,[[0],[1],[2],[3]])
(b,[[0],[1],[2],[3]])
(c,[[0,1,2,3]])
[1]

-}