-- Note: This is a modified version of DEMO-S5 by Jan van Eijck.
-- For the original, see http://homepages.cwi.nl/~jve/software/demo_s5/
module SMCDEL.Explicit.DEMO_S5 where

import Control.Arrow (first,second)
import Data.List (sortBy)

import SMCDEL.Internal.Help (apply,restrict,Erel,bl)

newtype Agent = Ag Int deriving (Agent -> Agent -> Bool
(Agent -> Agent -> Bool) -> (Agent -> Agent -> Bool) -> Eq Agent
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Agent -> Agent -> Bool
== :: Agent -> Agent -> Bool
$c/= :: Agent -> Agent -> Bool
/= :: Agent -> Agent -> Bool
Eq,Eq Agent
Eq Agent =>
(Agent -> Agent -> Ordering)
-> (Agent -> Agent -> Bool)
-> (Agent -> Agent -> Bool)
-> (Agent -> Agent -> Bool)
-> (Agent -> Agent -> Bool)
-> (Agent -> Agent -> Agent)
-> (Agent -> Agent -> Agent)
-> Ord Agent
Agent -> Agent -> Bool
Agent -> Agent -> Ordering
Agent -> Agent -> Agent
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Agent -> Agent -> Ordering
compare :: Agent -> Agent -> Ordering
$c< :: Agent -> Agent -> Bool
< :: Agent -> Agent -> Bool
$c<= :: Agent -> Agent -> Bool
<= :: Agent -> Agent -> Bool
$c> :: Agent -> Agent -> Bool
> :: Agent -> Agent -> Bool
$c>= :: Agent -> Agent -> Bool
>= :: Agent -> Agent -> Bool
$cmax :: Agent -> Agent -> Agent
max :: Agent -> Agent -> Agent
$cmin :: Agent -> Agent -> Agent
min :: Agent -> Agent -> Agent
Ord,Int -> Agent -> ShowS
[Agent] -> ShowS
Agent -> String
(Int -> Agent -> ShowS)
-> (Agent -> String) -> ([Agent] -> ShowS) -> Show Agent
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Agent -> ShowS
showsPrec :: Int -> Agent -> ShowS
$cshow :: Agent -> String
show :: Agent -> String
$cshowList :: [Agent] -> ShowS
showList :: [Agent] -> ShowS
Show)

data DemoPrp = DemoP Int | DemoQ Int | DemoR Int | DemoS Int deriving (DemoPrp -> DemoPrp -> Bool
(DemoPrp -> DemoPrp -> Bool)
-> (DemoPrp -> DemoPrp -> Bool) -> Eq DemoPrp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DemoPrp -> DemoPrp -> Bool
== :: DemoPrp -> DemoPrp -> Bool
$c/= :: DemoPrp -> DemoPrp -> Bool
/= :: DemoPrp -> DemoPrp -> Bool
Eq,Eq DemoPrp
Eq DemoPrp =>
(DemoPrp -> DemoPrp -> Ordering)
-> (DemoPrp -> DemoPrp -> Bool)
-> (DemoPrp -> DemoPrp -> Bool)
-> (DemoPrp -> DemoPrp -> Bool)
-> (DemoPrp -> DemoPrp -> Bool)
-> (DemoPrp -> DemoPrp -> DemoPrp)
-> (DemoPrp -> DemoPrp -> DemoPrp)
-> Ord DemoPrp
DemoPrp -> DemoPrp -> Bool
DemoPrp -> DemoPrp -> Ordering
DemoPrp -> DemoPrp -> DemoPrp
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: DemoPrp -> DemoPrp -> Ordering
compare :: DemoPrp -> DemoPrp -> Ordering
$c< :: DemoPrp -> DemoPrp -> Bool
< :: DemoPrp -> DemoPrp -> Bool
$c<= :: DemoPrp -> DemoPrp -> Bool
<= :: DemoPrp -> DemoPrp -> Bool
$c> :: DemoPrp -> DemoPrp -> Bool
> :: DemoPrp -> DemoPrp -> Bool
$c>= :: DemoPrp -> DemoPrp -> Bool
>= :: DemoPrp -> DemoPrp -> Bool
$cmax :: DemoPrp -> DemoPrp -> DemoPrp
max :: DemoPrp -> DemoPrp -> DemoPrp
$cmin :: DemoPrp -> DemoPrp -> DemoPrp
min :: DemoPrp -> DemoPrp -> DemoPrp
Ord)
instance Show DemoPrp where
  show :: DemoPrp -> String
show (DemoP Int
0) = String
"p"; show (DemoP Int
i) = String
"p" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
  show (DemoQ Int
0) = String
"q"; show (DemoQ Int
i) = String
"q" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
  show (DemoR Int
0) = String
"r"; show (DemoR Int
i) = String
"r" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
  show (DemoS Int
0) = String
"s"; show (DemoS Int
i) = String
"s" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i

data EpistM state = Mo
             [state]
             [Agent]
             [(state,[DemoPrp])]
             [(Agent,Erel state)]
             [state]  deriving (EpistM state -> EpistM state -> Bool
(EpistM state -> EpistM state -> Bool)
-> (EpistM state -> EpistM state -> Bool) -> Eq (EpistM state)
forall state. Eq state => EpistM state -> EpistM state -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall state. Eq state => EpistM state -> EpistM state -> Bool
== :: EpistM state -> EpistM state -> Bool
$c/= :: forall state. Eq state => EpistM state -> EpistM state -> Bool
/= :: EpistM state -> EpistM state -> Bool
Eq)

instance Show state => Show (EpistM state) where
  show :: EpistM state -> String
show (Mo [state]
worlds [Agent]
ags [(state, [DemoPrp])]
val [(Agent, Erel state)]
accs [state]
points) = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
    [ String
"Mo\n  "
    , [state] -> String
forall a. Show a => a -> String
show [state]
worlds, String
"\n  "
    , [Agent] -> String
forall a. Show a => a -> String
show [Agent]
ags, String
"\n  "
    , [(state, [DemoPrp])] -> String
forall a. Show a => a -> String
show [(state, [DemoPrp])]
val, String
"\n  "
    , [(Agent, Erel state)] -> String
forall a. Show a => a -> String
show [(Agent, Erel state)]
accs, String
"\n  "
    , [state] -> String
forall a. Show a => a -> String
show [state]
points, String
"\n"
    ]

rel :: Show a => Agent -> EpistM a -> Erel a
rel :: forall a. Show a => Agent -> EpistM a -> Erel a
rel Agent
ag (Mo [a]
_ [Agent]
_ [(a, [DemoPrp])]
_ [(Agent, Erel a)]
rels [a]
_) = [(Agent, Erel a)] -> Agent -> Erel a
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
apply [(Agent, Erel a)]
rels Agent
ag

initM :: (Num state, Enum state) => [Agent] -> [DemoPrp] -> EpistM state
initM :: forall state.
(Num state, Enum state) =>
[Agent] -> [DemoPrp] -> EpistM state
initM [Agent]
ags [DemoPrp]
props = [state]
-> [Agent]
-> [(state, [DemoPrp])]
-> [(Agent, Erel state)]
-> [state]
-> EpistM state
forall state.
[state]
-> [Agent]
-> [(state, [DemoPrp])]
-> [(Agent, Erel state)]
-> [state]
-> EpistM state
Mo [state]
worlds [Agent]
ags [(state, [DemoPrp])]
val [(Agent, Erel state)]
accs [state]
points where
  worlds :: [state]
worlds  = [state
0..(state
2state -> Int -> state
forall a b. (Num a, Integral b) => a -> b -> a
^Int
kstate -> state -> state
forall a. Num a => a -> a -> a
-state
1)]
  k :: Int
k       = [DemoPrp] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [DemoPrp]
props
  val :: [(state, [DemoPrp])]
val     = [state] -> [[DemoPrp]] -> [(state, [DemoPrp])]
forall a b. [a] -> [b] -> [(a, b)]
zip [state]
worlds ([[DemoPrp]] -> [[DemoPrp]]
forall a. Ord a => [[a]] -> [[a]]
sortL ([DemoPrp] -> [[DemoPrp]]
forall a. [a] -> [[a]]
powerList [DemoPrp]
props))
  accs :: [(Agent, Erel state)]
accs    = [ (Agent
ag,[[state]
worlds]) | Agent
ag  <- [Agent]
ags        ]
  points :: [state]
points  = [state]
worlds

powerList  :: [a] -> [[a]]
powerList :: forall a. [a] -> [[a]]
powerList  [] = [[]]
powerList  (a
x:[a]
xs) =
  [a] -> [[a]]
forall a. [a] -> [[a]]
powerList [a]
xs [[a]] -> [[a]] -> [[a]]
forall a. [a] -> [a] -> [a]
++ ([a] -> [a]) -> [[a]] -> [[a]]
forall a b. (a -> b) -> [a] -> [b]
map (a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:) ([a] -> [[a]]
forall a. [a] -> [[a]]
powerList [a]
xs)

sortL :: Ord a => [[a]] -> [[a]]
sortL :: forall a. Ord a => [[a]] -> [[a]]
sortL  = ([a] -> [a] -> Ordering) -> [[a]] -> [[a]]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy
  (\ [a]
xs [a]
ys -> if [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
xs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
ys
                then Ordering
LT
              else if [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
xs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
ys
                then Ordering
GT
              else [a] -> [a] -> Ordering
forall a. Ord a => a -> a -> Ordering
compare [a]
xs [a]
ys)

data DemoForm a = Top
            | Info a
            | Prp DemoPrp
            | Ng (DemoForm a)
            | Conj [DemoForm a]
            | Disj [DemoForm a]
            | Kn Agent (DemoForm a)
            | PA (DemoForm a) (DemoForm a)
            | PAW (DemoForm a) (DemoForm a)
          deriving (DemoForm a -> DemoForm a -> Bool
(DemoForm a -> DemoForm a -> Bool)
-> (DemoForm a -> DemoForm a -> Bool) -> Eq (DemoForm a)
forall a. Eq a => DemoForm a -> DemoForm a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => DemoForm a -> DemoForm a -> Bool
== :: DemoForm a -> DemoForm a -> Bool
$c/= :: forall a. Eq a => DemoForm a -> DemoForm a -> Bool
/= :: DemoForm a -> DemoForm a -> Bool
Eq,Eq (DemoForm a)
Eq (DemoForm a) =>
(DemoForm a -> DemoForm a -> Ordering)
-> (DemoForm a -> DemoForm a -> Bool)
-> (DemoForm a -> DemoForm a -> Bool)
-> (DemoForm a -> DemoForm a -> Bool)
-> (DemoForm a -> DemoForm a -> Bool)
-> (DemoForm a -> DemoForm a -> DemoForm a)
-> (DemoForm a -> DemoForm a -> DemoForm a)
-> Ord (DemoForm a)
DemoForm a -> DemoForm a -> Bool
DemoForm a -> DemoForm a -> Ordering
DemoForm a -> DemoForm a -> DemoForm a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (DemoForm a)
forall a. Ord a => DemoForm a -> DemoForm a -> Bool
forall a. Ord a => DemoForm a -> DemoForm a -> Ordering
forall a. Ord a => DemoForm a -> DemoForm a -> DemoForm a
$ccompare :: forall a. Ord a => DemoForm a -> DemoForm a -> Ordering
compare :: DemoForm a -> DemoForm a -> Ordering
$c< :: forall a. Ord a => DemoForm a -> DemoForm a -> Bool
< :: DemoForm a -> DemoForm a -> Bool
$c<= :: forall a. Ord a => DemoForm a -> DemoForm a -> Bool
<= :: DemoForm a -> DemoForm a -> Bool
$c> :: forall a. Ord a => DemoForm a -> DemoForm a -> Bool
> :: DemoForm a -> DemoForm a -> Bool
$c>= :: forall a. Ord a => DemoForm a -> DemoForm a -> Bool
>= :: DemoForm a -> DemoForm a -> Bool
$cmax :: forall a. Ord a => DemoForm a -> DemoForm a -> DemoForm a
max :: DemoForm a -> DemoForm a -> DemoForm a
$cmin :: forall a. Ord a => DemoForm a -> DemoForm a -> DemoForm a
min :: DemoForm a -> DemoForm a -> DemoForm a
Ord,Int -> DemoForm a -> ShowS
[DemoForm a] -> ShowS
DemoForm a -> String
(Int -> DemoForm a -> ShowS)
-> (DemoForm a -> String)
-> ([DemoForm a] -> ShowS)
-> Show (DemoForm a)
forall a. Show a => Int -> DemoForm a -> ShowS
forall a. Show a => [DemoForm a] -> ShowS
forall a. Show a => DemoForm a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> DemoForm a -> ShowS
showsPrec :: Int -> DemoForm a -> ShowS
$cshow :: forall a. Show a => DemoForm a -> String
show :: DemoForm a -> String
$cshowList :: forall a. Show a => [DemoForm a] -> ShowS
showList :: [DemoForm a] -> ShowS
Show)

impl :: DemoForm a -> DemoForm a -> DemoForm a
impl :: forall a. DemoForm a -> DemoForm a -> DemoForm a
impl DemoForm a
form1 DemoForm a
form2 = [DemoForm a] -> DemoForm a
forall a. [DemoForm a] -> DemoForm a
Disj [DemoForm a -> DemoForm a
forall a. DemoForm a -> DemoForm a
Ng DemoForm a
form1, DemoForm a
form2]

-- | semantics: truth at a world in a model
isTrueAt :: (Show state, Ord state) => EpistM state -> state -> DemoForm state -> Bool
isTrueAt :: forall state.
(Show state, Ord state) =>
EpistM state -> state -> DemoForm state -> Bool
isTrueAt EpistM state
_ state
_ DemoForm state
Top = Bool
True
isTrueAt EpistM state
_ state
w (Info state
x) = state
w state -> state -> Bool
forall a. Eq a => a -> a -> Bool
== state
x
isTrueAt (Mo [state]
_ [Agent]
_ [(state, [DemoPrp])]
val [(Agent, Erel state)]
_ [state]
_) state
w (Prp DemoPrp
p) = DemoPrp
p DemoPrp -> [DemoPrp] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [(state, [DemoPrp])] -> state -> [DemoPrp]
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
apply [(state, [DemoPrp])]
val state
w
isTrueAt EpistM state
m state
w (Ng DemoForm state
f) = Bool -> Bool
not (EpistM state -> state -> DemoForm state -> Bool
forall state.
(Show state, Ord state) =>
EpistM state -> state -> DemoForm state -> Bool
isTrueAt EpistM state
m state
w DemoForm state
f)
isTrueAt EpistM state
m state
w (Conj [DemoForm state]
fs) = (DemoForm state -> Bool) -> [DemoForm state] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (EpistM state -> state -> DemoForm state -> Bool
forall state.
(Show state, Ord state) =>
EpistM state -> state -> DemoForm state -> Bool
isTrueAt EpistM state
m state
w) [DemoForm state]
fs
isTrueAt EpistM state
m state
w (Disj [DemoForm state]
fs) = (DemoForm state -> Bool) -> [DemoForm state] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (EpistM state -> state -> DemoForm state -> Bool
forall state.
(Show state, Ord state) =>
EpistM state -> state -> DemoForm state -> Bool
isTrueAt EpistM state
m state
w) [DemoForm state]
fs
isTrueAt EpistM state
m state
w (Kn Agent
ag DemoForm state
f) = (state -> Bool) -> [state] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((state -> DemoForm state -> Bool)
-> DemoForm state -> state -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip (EpistM state -> state -> DemoForm state -> Bool
forall state.
(Show state, Ord state) =>
EpistM state -> state -> DemoForm state -> Bool
isTrueAt EpistM state
m) DemoForm state
f) (Erel state -> state -> [state]
forall a. Eq a => Erel a -> a -> [a]
bl (Agent -> EpistM state -> Erel state
forall a. Show a => Agent -> EpistM a -> Erel a
rel Agent
ag EpistM state
m) state
w)
isTrueAt EpistM state
m state
w (PA DemoForm state
f DemoForm state
g) = Bool -> Bool
not (EpistM state -> state -> DemoForm state -> Bool
forall state.
(Show state, Ord state) =>
EpistM state -> state -> DemoForm state -> Bool
isTrueAt EpistM state
m state
w DemoForm state
f) Bool -> Bool -> Bool
|| EpistM state -> state -> DemoForm state -> Bool
forall state.
(Show state, Ord state) =>
EpistM state -> state -> DemoForm state -> Bool
isTrueAt (EpistM state -> DemoForm state -> EpistM state
forall state.
(Show state, Ord state) =>
EpistM state -> DemoForm state -> EpistM state
updPa EpistM state
m DemoForm state
f) state
w DemoForm state
g
isTrueAt EpistM state
m state
w (PAW DemoForm state
f DemoForm state
g) = Bool -> Bool
not (EpistM state -> state -> DemoForm state -> Bool
forall state.
(Show state, Ord state) =>
EpistM state -> state -> DemoForm state -> Bool
isTrueAt EpistM state
m state
w DemoForm state
f) Bool -> Bool -> Bool
|| EpistM state -> state -> DemoForm state -> Bool
forall state.
(Show state, Ord state) =>
EpistM state -> state -> DemoForm state -> Bool
isTrueAt (EpistM state -> DemoForm state -> EpistM state
forall state.
(Show state, Ord state) =>
EpistM state -> DemoForm state -> EpistM state
updPaW EpistM state
m DemoForm state
f) state
w DemoForm state
g

-- | global truth in a model
isTrue :: Show a => Ord a => EpistM a -> DemoForm a -> Bool
isTrue :: forall a. (Show a, Ord a) => EpistM a -> DemoForm a -> Bool
isTrue m :: EpistM a
m@(Mo [a]
_ [Agent]
_ [(a, [DemoPrp])]
_ [(Agent, Erel a)]
_ [a]
points) DemoForm a
f = (a -> Bool) -> [a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\a
w -> EpistM a -> a -> DemoForm a -> Bool
forall state.
(Show state, Ord state) =>
EpistM state -> state -> DemoForm state -> Bool
isTrueAt EpistM a
m a
w DemoForm a
f) [a]
points

-- | public announcement
updPa :: (Show state, Ord state) => EpistM state -> DemoForm state -> EpistM state
updPa :: forall state.
(Show state, Ord state) =>
EpistM state -> DemoForm state -> EpistM state
updPa m :: EpistM state
m@(Mo [state]
states [Agent]
agents [(state, [DemoPrp])]
val [(Agent, Erel state)]
rels [state]
actual) DemoForm state
f = [state]
-> [Agent]
-> [(state, [DemoPrp])]
-> [(Agent, Erel state)]
-> [state]
-> EpistM state
forall state.
[state]
-> [Agent]
-> [(state, [DemoPrp])]
-> [(Agent, Erel state)]
-> [state]
-> EpistM state
Mo [state]
states' [Agent]
agents [(state, [DemoPrp])]
val' [(Agent, Erel state)]
rels' [state]
actual' where
  states' :: [state]
states' = [ state
s | state
s <- [state]
states, EpistM state -> state -> DemoForm state -> Bool
forall state.
(Show state, Ord state) =>
EpistM state -> state -> DemoForm state -> Bool
isTrueAt EpistM state
m state
s DemoForm state
f ]
  val' :: [(state, [DemoPrp])]
val'    = [ (state
s, [DemoPrp]
ps) | (state
s,[DemoPrp]
ps) <- [(state, [DemoPrp])]
val, state
s state -> [state] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [state]
states' ]
  rels' :: [(Agent, Erel state)]
rels'   = [ (Agent
ag,[state] -> Erel state -> Erel state
forall a. Ord a => [a] -> Erel a -> Erel a
restrict [state]
states' Erel state
r) | (Agent
ag,Erel state
r) <- [(Agent, Erel state)]
rels ]
  actual' :: [state]
actual' = [ state
s | state
s <- [state]
actual, state
s state -> [state] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [state]
states' ]

updsPa ::  (Show state, Ord state) => EpistM state -> [DemoForm state] -> EpistM state
updsPa :: forall state.
(Show state, Ord state) =>
EpistM state -> [DemoForm state] -> EpistM state
updsPa = (EpistM state -> DemoForm state -> EpistM state)
-> EpistM state -> [DemoForm state] -> EpistM state
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl EpistM state -> DemoForm state -> EpistM state
forall state.
(Show state, Ord state) =>
EpistM state -> DemoForm state -> EpistM state
updPa

-- | public announcement-whether
updPaW :: (Show state, Ord state) => EpistM state -> DemoForm state -> EpistM state
updPaW :: forall state.
(Show state, Ord state) =>
EpistM state -> DemoForm state -> EpistM state
updPaW m :: EpistM state
m@(Mo [state]
states [Agent]
agents [(state, [DemoPrp])]
val [(Agent, Erel state)]
rels [state]
actual) DemoForm state
f = [state]
-> [Agent]
-> [(state, [DemoPrp])]
-> [(Agent, Erel state)]
-> [state]
-> EpistM state
forall state.
[state]
-> [Agent]
-> [(state, [DemoPrp])]
-> [(Agent, Erel state)]
-> [state]
-> EpistM state
Mo [state]
states [Agent]
agents [(state, [DemoPrp])]
val [(Agent, Erel state)]
rels' [state]
actual where
  rels' :: [(Agent, Erel state)]
rels'    = [ (Agent
ag, Erel state -> Erel state
forall a. Ord a => [[a]] -> [[a]]
sortL (Erel state -> Erel state) -> Erel state -> Erel state
forall a b. (a -> b) -> a -> b
$ ([state] -> Erel state) -> Erel state -> Erel state
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap [state] -> Erel state
split Erel state
r) | (Agent
ag,Erel state
r) <- [(Agent, Erel state)]
rels ]
  split :: [state] -> Erel state
split [state]
ws = ([state] -> Bool) -> Erel state -> Erel state
forall a. (a -> Bool) -> [a] -> [a]
filter ([state] -> [state] -> Bool
forall a. Eq a => a -> a -> Bool
/= []) [ (state -> Bool) -> [state] -> [state]
forall a. (a -> Bool) -> [a] -> [a]
filter (\state
w -> EpistM state -> state -> DemoForm state -> Bool
forall state.
(Show state, Ord state) =>
EpistM state -> state -> DemoForm state -> Bool
isTrueAt EpistM state
m state
w DemoForm state
f) [state]
ws, (state -> Bool) -> [state] -> [state]
forall a. (a -> Bool) -> [a] -> [a]
filter (\state
w -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ EpistM state -> state -> DemoForm state -> Bool
forall state.
(Show state, Ord state) =>
EpistM state -> state -> DemoForm state -> Bool
isTrueAt EpistM state
m state
w DemoForm state
f) [state]
ws ]

updsPaW ::  (Show state, Ord state) => EpistM state -> [DemoForm state] -> EpistM state
updsPaW :: forall state.
(Show state, Ord state) =>
EpistM state -> [DemoForm state] -> EpistM state
updsPaW = (EpistM state -> DemoForm state -> EpistM state)
-> EpistM state -> [DemoForm state] -> EpistM state
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl EpistM state -> DemoForm state -> EpistM state
forall state.
(Show state, Ord state) =>
EpistM state -> DemoForm state -> EpistM state
updPaW

-- | safe substitutions
sub :: Show a => [(DemoPrp,DemoForm a)] -> DemoPrp -> DemoForm a
sub :: forall a.
Show a =>
[(DemoPrp, DemoForm a)] -> DemoPrp -> DemoForm a
sub [(DemoPrp, DemoForm a)]
subst DemoPrp
p | DemoPrp
p DemoPrp -> [DemoPrp] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ((DemoPrp, DemoForm a) -> DemoPrp)
-> [(DemoPrp, DemoForm a)] -> [DemoPrp]
forall a b. (a -> b) -> [a] -> [b]
map (DemoPrp, DemoForm a) -> DemoPrp
forall a b. (a, b) -> a
fst [(DemoPrp, DemoForm a)]
subst = [(DemoPrp, DemoForm a)] -> DemoPrp -> DemoForm a
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
apply [(DemoPrp, DemoForm a)]
subst DemoPrp
p
            | Bool
otherwise              = DemoPrp -> DemoForm a
forall a. DemoPrp -> DemoForm a
Prp DemoPrp
p

-- | public factual change
updPc :: (Show state, Ord state) => [DemoPrp] -> EpistM state -> [(DemoPrp,DemoForm state)] -> EpistM state
updPc :: forall state.
(Show state, Ord state) =>
[DemoPrp]
-> EpistM state -> [(DemoPrp, DemoForm state)] -> EpistM state
updPc [DemoPrp]
ps m :: EpistM state
m@(Mo [state]
states [Agent]
agents [(state, [DemoPrp])]
_ [(Agent, Erel state)]
rels [state]
actual) [(DemoPrp, DemoForm state)]
sb = [state]
-> [Agent]
-> [(state, [DemoPrp])]
-> [(Agent, Erel state)]
-> [state]
-> EpistM state
forall state.
[state]
-> [Agent]
-> [(state, [DemoPrp])]
-> [(Agent, Erel state)]
-> [state]
-> EpistM state
Mo [state]
states [Agent]
agents [(state, [DemoPrp])]
val' [(Agent, Erel state)]
rels [state]
actual where
   val' :: [(state, [DemoPrp])]
val' = [ (state
s, [DemoPrp
p | DemoPrp
p <- [DemoPrp]
ps, EpistM state -> state -> DemoForm state -> Bool
forall state.
(Show state, Ord state) =>
EpistM state -> state -> DemoForm state -> Bool
isTrueAt EpistM state
m state
s ([(DemoPrp, DemoForm state)] -> DemoPrp -> DemoForm state
forall a.
Show a =>
[(DemoPrp, DemoForm a)] -> DemoPrp -> DemoForm a
sub [(DemoPrp, DemoForm state)]
sb DemoPrp
p)]) | state
s <- [state]
states ]

updsPc :: Show state => Ord state => [DemoPrp] -> EpistM state
                     -> [[(DemoPrp,DemoForm state)]] -> EpistM state
updsPc :: forall state.
(Show state, Ord state) =>
[DemoPrp]
-> EpistM state -> [[(DemoPrp, DemoForm state)]] -> EpistM state
updsPc [DemoPrp]
ps = (EpistM state -> [(DemoPrp, DemoForm state)] -> EpistM state)
-> EpistM state -> [[(DemoPrp, DemoForm state)]] -> EpistM state
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ([DemoPrp]
-> EpistM state -> [(DemoPrp, DemoForm state)] -> EpistM state
forall state.
(Show state, Ord state) =>
[DemoPrp]
-> EpistM state -> [(DemoPrp, DemoForm state)] -> EpistM state
updPc [DemoPrp]
ps)

updPi :: (state1 -> state2) -> EpistM state1 -> EpistM state2
updPi :: forall state1 state2.
(state1 -> state2) -> EpistM state1 -> EpistM state2
updPi state1 -> state2
f (Mo [state1]
states [Agent]
agents [(state1, [DemoPrp])]
val [(Agent, Erel state1)]
rels [state1]
actual) =
  [state2]
-> [Agent]
-> [(state2, [DemoPrp])]
-> [(Agent, Erel state2)]
-> [state2]
-> EpistM state2
forall state.
[state]
-> [Agent]
-> [(state, [DemoPrp])]
-> [(Agent, Erel state)]
-> [state]
-> EpistM state
Mo
  ((state1 -> state2) -> [state1] -> [state2]
forall a b. (a -> b) -> [a] -> [b]
map state1 -> state2
f [state1]
states)
  [Agent]
agents
  (((state1, [DemoPrp]) -> (state2, [DemoPrp]))
-> [(state1, [DemoPrp])] -> [(state2, [DemoPrp])]
forall a b. (a -> b) -> [a] -> [b]
map ((state1 -> state2) -> (state1, [DemoPrp]) -> (state2, [DemoPrp])
forall b c d. (b -> c) -> (b, d) -> (c, d)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first state1 -> state2
f) [(state1, [DemoPrp])]
val)
  (((Agent, Erel state1) -> (Agent, Erel state2))
-> [(Agent, Erel state1)] -> [(Agent, Erel state2)]
forall a b. (a -> b) -> [a] -> [b]
map ((Erel state1 -> Erel state2)
-> (Agent, Erel state1) -> (Agent, Erel state2)
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (([state1] -> [state2]) -> Erel state1 -> Erel state2
forall a b. (a -> b) -> [a] -> [b]
map ((state1 -> state2) -> [state1] -> [state2]
forall a b. (a -> b) -> [a] -> [b]
map state1 -> state2
f))) [(Agent, Erel state1)]
rels)
  ((state1 -> state2) -> [state1] -> [state2]
forall a b. (a -> b) -> [a] -> [b]
map state1 -> state2
f [state1]
actual)

bTables :: Int -> [[Bool]]
bTables :: Int -> [[Bool]]
bTables Int
0 = [[]]
bTables Int
n = ([Bool] -> [Bool]) -> [[Bool]] -> [[Bool]]
forall a b. (a -> b) -> [a] -> [b]
map (Bool
TrueBool -> [Bool] -> [Bool]
forall a. a -> [a] -> [a]
:) (Int -> [[Bool]]
bTables (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)) [[Bool]] -> [[Bool]] -> [[Bool]]
forall a. [a] -> [a] -> [a]
++ ([Bool] -> [Bool]) -> [[Bool]] -> [[Bool]]
forall a b. (a -> b) -> [a] -> [b]
map (Bool
FalseBool -> [Bool] -> [Bool]
forall a. a -> [a] -> [a]
:) (Int -> [[Bool]]
bTables (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1))

initN :: Int -> EpistM [Bool]
initN :: Int -> EpistM [Bool]
initN Int
n = [[Bool]]
-> [Agent]
-> [([Bool], [DemoPrp])]
-> [(Agent, Erel [Bool])]
-> [[Bool]]
-> EpistM [Bool]
forall state.
[state]
-> [Agent]
-> [(state, [DemoPrp])]
-> [(Agent, Erel state)]
-> [state]
-> EpistM state
Mo [[Bool]]
states [Agent]
agents [] [(Agent, Erel [Bool])]
rels [[Bool]]
points where
  states :: [[Bool]]
states = Int -> [[Bool]]
bTables Int
n
  agents :: [Agent]
agents = (Int -> Agent) -> [Int] -> [Agent]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Agent
Ag [Int
1..Int
n]
  rels :: [(Agent, Erel [Bool])]
rels = [(Int -> Agent
Ag Int
i, [[[Bool]
tab1[Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++[Bool
True][Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++[Bool]
tab2,[Bool]
tab1[Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++[Bool
False][Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++[Bool]
tab2] |
                   [Bool]
tab1 <- Int -> [[Bool]]
bTables (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1),
                   [Bool]
tab2 <- Int -> [[Bool]]
bTables (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
i) ]) | Int
i <- [Int
1..Int
n] ]
  points :: [[Bool]]
points = [Bool
FalseBool -> [Bool] -> [Bool]
forall a. a -> [a] -> [a]
: Int -> Bool -> [Bool]
forall a. Int -> a -> [a]
replicate (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Bool
True]

fatherN :: Int -> DemoForm [Bool]
fatherN :: Int -> DemoForm [Bool]
fatherN Int
n = DemoForm [Bool] -> DemoForm [Bool]
forall a. DemoForm a -> DemoForm a
Ng ([Bool] -> DemoForm [Bool]
forall a. a -> DemoForm a
Info (Int -> Bool -> [Bool]
forall a. Int -> a -> [a]
replicate Int
n Bool
False))

kn :: Int -> Int -> DemoForm [Bool]
kn :: Int -> Int -> DemoForm [Bool]
kn Int
n Int
i = [DemoForm [Bool]] -> DemoForm [Bool]
forall a. [DemoForm a] -> DemoForm a
Disj [Agent -> DemoForm [Bool] -> DemoForm [Bool]
forall a. Agent -> DemoForm a -> DemoForm a
Kn (Int -> Agent
Ag Int
i) ([DemoForm [Bool]] -> DemoForm [Bool]
forall a. [DemoForm a] -> DemoForm a
Disj [ [Bool] -> DemoForm [Bool]
forall a. a -> DemoForm a
Info ([Bool]
tab1[Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++[Bool
True][Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++[Bool]
tab2)
                               | [Bool]
tab1 <- Int -> [[Bool]]
bTables (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)
                               , [Bool]
tab2 <- Int -> [[Bool]]
bTables (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
i)
                               ] ),
               Agent -> DemoForm [Bool] -> DemoForm [Bool]
forall a. Agent -> DemoForm a -> DemoForm a
Kn (Int -> Agent
Ag Int
i) ([DemoForm [Bool]] -> DemoForm [Bool]
forall a. [DemoForm a] -> DemoForm a
Disj [ [Bool] -> DemoForm [Bool]
forall a. a -> DemoForm a
Info ([Bool]
tab1[Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++[Bool
False][Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++[Bool]
tab2)
                               | [Bool]
tab1 <- Int -> [[Bool]]
bTables (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)
                               , [Bool]
tab2 <- Int -> [[Bool]]
bTables (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
i)
                               ] )
              ]

dont :: Int -> DemoForm [Bool]
dont :: Int -> DemoForm [Bool]
dont Int
n = [DemoForm [Bool]] -> DemoForm [Bool]
forall a. [DemoForm a] -> DemoForm a
Conj [DemoForm [Bool] -> DemoForm [Bool]
forall a. DemoForm a -> DemoForm a
Ng (Int -> Int -> DemoForm [Bool]
kn Int
n Int
i) | Int
i <- [Int
1..Int
n] ]

knowN :: Int -> DemoForm [Bool]
knowN :: Int -> DemoForm [Bool]
knowN Int
n = [DemoForm [Bool]] -> DemoForm [Bool]
forall a. [DemoForm a] -> DemoForm a
Conj [Int -> Int -> DemoForm [Bool]
kn Int
n Int
i | Int
i <- [Int
2..Int
n] ]

solveN :: Int -> EpistM [Bool]
solveN :: Int -> EpistM [Bool]
solveN Int
n = EpistM [Bool] -> [DemoForm [Bool]] -> EpistM [Bool]
forall state.
(Show state, Ord state) =>
EpistM state -> [DemoForm state] -> EpistM state
updsPa (Int -> EpistM [Bool]
initN Int
n) (DemoForm [Bool]
fDemoForm [Bool] -> [DemoForm [Bool]] -> [DemoForm [Bool]]
forall a. a -> [a] -> [a]
:[DemoForm [Bool]]
istatements [DemoForm [Bool]] -> [DemoForm [Bool]] -> [DemoForm [Bool]]
forall a. [a] -> [a] -> [a]
++ [Int -> DemoForm [Bool]
knowN Int
n]) where
  f :: DemoForm [Bool]
f = Int -> DemoForm [Bool]
fatherN Int
n
  istatements :: [DemoForm [Bool]]
istatements = Int -> DemoForm [Bool] -> [DemoForm [Bool]]
forall a. Int -> a -> [a]
replicate (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
2) (Int -> DemoForm [Bool]
dont Int
n)