module SMCDEL.Examples.CherylDemo where

import Data.List

import SMCDEL.Explicit.DEMO_S5 as DEMO_S5

type MyWorld = (Int,Int,Int)

--  Cheryl: I have two younger brothers. The product of all our ages is 144.
allStates :: [MyWorld]
allStates :: [(Int, Int, Int)]
allStates = [ (Int
c,Int
b1,Int
b2) | Int
c  <- [Int
1..Int
144]
                        , Int
b1 <- [Int
1..(Int
cInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)]
                        , Int
b2 <- [Int
1..(Int
cInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)]
                        , Int
c Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
b1 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
b2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
144 ]

start,step1,step2,step3,step4,step5 :: DEMO_S5.EpistM MyWorld

start :: EpistM (Int, Int, Int)
start = [(Int, Int, Int)]
-> [Agent]
-> [((Int, Int, Int), [DemoPrp])]
-> [(Agent, Erel (Int, Int, Int))]
-> [(Int, Int, Int)]
-> EpistM (Int, Int, Int)
forall state.
[state]
-> [Agent]
-> [(state, [DemoPrp])]
-> [(Agent, Erel state)]
-> [state]
-> EpistM state
DEMO_S5.Mo [(Int, Int, Int)]
states [Agent]
agents [] [(Agent, Erel (Int, Int, Int))]
rels [(Int, Int, Int)]
points where
  states :: [(Int, Int, Int)]
states = [(Int, Int, Int)]
allStates
  agents :: [Agent]
agents = [Int -> Agent
DEMO_S5.Ag Int
1] -- a single observer agent
  rels :: [(Agent, Erel (Int, Int, Int))]
rels = [ (Int -> Agent
DEMO_S5.Ag Int
1, [[(Int, Int, Int)]
states]) ] -- nothing known
  points :: [(Int, Int, Int)]
points = [(Int, Int, Int)]
allStates

cherylIs :: Int -> DemoForm MyWorld
cherylIs :: Int -> DemoForm (Int, Int, Int)
cherylIs Int
n = [DemoForm (Int, Int, Int)] -> DemoForm (Int, Int, Int)
forall a. [DemoForm a] -> DemoForm a
Disj [ (Int, Int, Int) -> DemoForm (Int, Int, Int)
forall a. a -> DemoForm a
Info (Int
n,Int
b1,Int
b2) | Int
b1 <- [Int
1..Int
144], Int
b2 <- [Int
1..Int
144], (Int
n,Int
b1,Int
b2) (Int, Int, Int) -> [(Int, Int, Int)] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [(Int, Int, Int)]
allStates ]

weKnowIt :: DemoForm MyWorld
weKnowIt :: DemoForm (Int, Int, Int)
weKnowIt = [DemoForm (Int, Int, Int)] -> DemoForm (Int, Int, Int)
forall a. [DemoForm a] -> DemoForm a
Disj [ Agent -> DemoForm (Int, Int, Int) -> DemoForm (Int, Int, Int)
forall a. Agent -> DemoForm a -> DemoForm a
Kn (Int -> Agent
Ag Int
1) (Int -> DemoForm (Int, Int, Int)
cherylIs Int
n) | Int
n <- [Int
1..Int
144]]

-- Albert: We still don't know your age. What other hints can you give us?
step1 :: EpistM (Int, Int, Int)
step1 = EpistM (Int, Int, Int)
start EpistM (Int, Int, Int)
-> DemoForm (Int, Int, Int) -> EpistM (Int, Int, Int)
forall state.
(Show state, Ord state) =>
EpistM state -> DemoForm state -> EpistM state
`updPa` DemoForm (Int, Int, Int) -> DemoForm (Int, Int, Int)
forall a. DemoForm a -> DemoForm a
Ng DemoForm (Int, Int, Int)
weKnowIt

-- Cheryl: The sum of all our ages is the bus number of this bus that we are on.
step2 :: EpistM (Int, Int, Int)
step2 = EpistM (Int, Int, Int)
-> [DemoForm (Int, Int, Int)] -> EpistM (Int, Int, Int)
forall state.
(Show state, Ord state) =>
EpistM state -> [DemoForm state] -> EpistM state
updsPaW EpistM (Int, Int, Int)
step1 [ Int -> DemoForm (Int, Int, Int)
sumIs Int
n | Int
n <- [Int]
possibleSums ] where
  possibleSums :: [Int]
possibleSums = [Int] -> [Int]
forall a. Ord a => [a] -> [a]
sort ([Int] -> [Int]) -> ([Int] -> [Int]) -> [Int] -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Int] -> [Int]
forall a. Eq a => [a] -> [a]
nub ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ ((Int, Int, Int) -> Int) -> [(Int, Int, Int)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (\(Int
c, Int
b1, Int
b2) -> Int
cInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
b1Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
b2) [(Int, Int, Int)]
allStates
  sumIs :: Int -> DemoForm (Int, Int, Int)
sumIs Int
n = [DemoForm (Int, Int, Int)] -> DemoForm (Int, Int, Int)
forall a. [DemoForm a] -> DemoForm a
Disj (((Int, Int, Int) -> DemoForm (Int, Int, Int))
-> [(Int, Int, Int)] -> [DemoForm (Int, Int, Int)]
forall a b. (a -> b) -> [a] -> [b]
map (Int, Int, Int) -> DemoForm (Int, Int, Int)
forall a. a -> DemoForm a
Info (((Int, Int, Int) -> Bool) -> [(Int, Int, Int)] -> [(Int, Int, Int)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Int
c, Int
b1, Int
b2) -> Int
cInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
b1Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
b2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n) [(Int, Int, Int)]
allStates))

-- Bernard: Of course we know the bus number, but we still don't know your age.
step3 :: EpistM (Int, Int, Int)
step3 = EpistM (Int, Int, Int)
step2 EpistM (Int, Int, Int)
-> DemoForm (Int, Int, Int) -> EpistM (Int, Int, Int)
forall state.
(Show state, Ord state) =>
EpistM state -> DemoForm state -> EpistM state
`updPa` DemoForm (Int, Int, Int) -> DemoForm (Int, Int, Int)
forall a. DemoForm a -> DemoForm a
Ng DemoForm (Int, Int, Int)
weKnowIt

-- Cheryl: Oh, I forgot to tell you that my brothers have the same age.
step4 :: EpistM (Int, Int, Int)
step4 = EpistM (Int, Int, Int)
step3 EpistM (Int, Int, Int)
-> DemoForm (Int, Int, Int) -> EpistM (Int, Int, Int)
forall state.
(Show state, Ord state) =>
EpistM state -> DemoForm state -> EpistM state
`updPa` DemoForm (Int, Int, Int)
broSame where
  broSame :: DemoForm (Int, Int, Int)
broSame = [DemoForm (Int, Int, Int)] -> DemoForm (Int, Int, Int)
forall a. [DemoForm a] -> DemoForm a
Disj (((Int, Int, Int) -> DemoForm (Int, Int, Int))
-> [(Int, Int, Int)] -> [DemoForm (Int, Int, Int)]
forall a b. (a -> b) -> [a] -> [b]
map (Int, Int, Int) -> DemoForm (Int, Int, Int)
forall a. a -> DemoForm a
Info (((Int, Int, Int) -> Bool) -> [(Int, Int, Int)] -> [(Int, Int, Int)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Int
_, Int
b1, Int
b2) -> Int
b1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
b2) [(Int, Int, Int)]
allStates))

-- Albert and Bernard: Oh, now we know your age.
step5 :: EpistM (Int, Int, Int)
step5 = EpistM (Int, Int, Int)
step4 EpistM (Int, Int, Int)
-> DemoForm (Int, Int, Int) -> EpistM (Int, Int, Int)
forall state.
(Show state, Ord state) =>
EpistM state -> DemoForm state -> EpistM state
`updPa` DemoForm (Int, Int, Int)
weKnowIt