{-# OPTIONS_GHC -fno-warn-incomplete-uni-patterns #-}

module SMCDEL.Examples.Cheryl where

import Data.HasCacBDD (Bdd,con,disSet)
import Data.List

import SMCDEL.Language
import SMCDEL.Symbolic.S5
import SMCDEL.Internal.Help (powerset)

type Possibility = (Int, String)

possibilities :: [Possibility]
possibilities :: [Possibility]
possibilities =
  [ (Int
15,String
"May"), (Int
16,String
"May"), (Int
19,String
"May")
  , (Int
17,String
"June"), (Int
18,String
"June")
  , (Int
14,String
"July"), (Int
16,String
"July")
  , (Int
14,String
"August"), (Int
15,String
"August"), (Int
17,String
"August") ]

dayIs :: Int -> Prp
dayIs :: Int -> Prp
dayIs = Int -> Prp
P

monthIs :: String -> Prp
monthIs :: String -> Prp
monthIs String
"May"    = Int -> Prp
P Int
5
monthIs String
"June"   = Int -> Prp
P Int
6
monthIs String
"July"   = Int -> Prp
P Int
7
monthIs String
"August" = Int -> Prp
P Int
8
monthIs String
_        = Prp
forall a. HasCallStack => a
undefined

thisPos :: Possibility -> Form
thisPos :: Possibility -> Form
thisPos (Int
d,String
m) = [Form] -> Form
Conj ([Form] -> Form) -> [Form] -> Form
forall a b. (a -> b) -> a -> b
$
  (Prp -> Form
PrpF (Int -> Prp
dayIs Int
d) Form -> [Form] -> [Form]
forall a. a -> [a] -> [a]
: [ Form -> Form
Neg (Prp -> Form
PrpF (Prp -> Form) -> Prp -> Form
forall a b. (a -> b) -> a -> b
$ Int -> Prp
dayIs Int
d') | Int
d' <- [Int] -> [Int]
forall a. Eq a => [a] -> [a]
nub ((Possibility -> Int) -> [Possibility] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Possibility -> Int
forall a b. (a, b) -> a
fst [Possibility]
possibilities) [Int] -> [Int] -> [Int]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Int
d] ]) [Form] -> [Form] -> [Form]
forall a. [a] -> [a] -> [a]
++
  (Prp -> Form
PrpF (String -> Prp
monthIs String
m) Form -> [Form] -> [Form]
forall a. a -> [a] -> [a]
: [ Form -> Form
Neg (Prp -> Form
PrpF (Prp -> Form) -> Prp -> Form
forall a b. (a -> b) -> a -> b
$ String -> Prp
monthIs String
m') | String
m' <- [String] -> [String]
forall a. Eq a => [a] -> [a]
nub ((Possibility -> String) -> [Possibility] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Possibility -> String
forall a b. (a, b) -> b
snd [Possibility]
possibilities) [String] -> [String] -> [String]
forall a. Eq a => [a] -> [a] -> [a]
\\ [String
m] ])

knWhich :: Agent -> Form
knWhich :: String -> Form
knWhich String
i = [Form] -> Form
Disj [ String -> Form -> Form
K String
i (Possibility -> Form
thisPos Possibility
pos) | Possibility
pos <- [Possibility]
possibilities ]

start :: KnowStruct
start :: KnowStruct
start = [Prp] -> Bdd -> [(String, [Prp])] -> KnowStruct
KnS [Prp]
allprops Bdd
statelaw [(String, [Prp])]
obs where
  allprops :: [Prp]
allprops = [Prp] -> [Prp]
forall a. Ord a => [a] -> [a]
sort ([Prp] -> [Prp]) -> [Prp] -> [Prp]
forall a b. (a -> b) -> a -> b
$ [Prp] -> [Prp]
forall a. Eq a => [a] -> [a]
nub ([Prp] -> [Prp]) -> [Prp] -> [Prp]
forall a b. (a -> b) -> a -> b
$ (Possibility -> Prp) -> [Possibility] -> [Prp]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Prp
dayIs (Int -> Prp) -> (Possibility -> Int) -> Possibility -> Prp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Possibility -> Int
forall a b. (a, b) -> a
fst) [Possibility]
possibilities [Prp] -> [Prp] -> [Prp]
forall a. [a] -> [a] -> [a]
++ (Possibility -> Prp) -> [Possibility] -> [Prp]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Prp
monthIs (String -> Prp) -> (Possibility -> String) -> Possibility -> Prp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Possibility -> String
forall a b. (a, b) -> b
snd) [Possibility]
possibilities
  statelaw :: Bdd
statelaw = Form -> Bdd
boolBddOf (Form -> Bdd) -> Form -> Bdd
forall a b. (a -> b) -> a -> b
$ [Form] -> Form
Conj
    [ [Form] -> Form
Disj ((Possibility -> Form) -> [Possibility] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map Possibility -> Form
thisPos [Possibility]
possibilities)
    , [Form] -> Form
Conj [ Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ [Form] -> Form
Conj [Possibility -> Form
thisPos Possibility
p1, Possibility -> Form
thisPos Possibility
p2] | Possibility
p1 <- [Possibility]
possibilities, Possibility
p2 <- [Possibility]
possibilities, Possibility
p1 Possibility -> Possibility -> Bool
forall a. Eq a => a -> a -> Bool
/= Possibility
p2 ] ]
  obs :: [(String, [Prp])]
obs = [ (String
"Albert" , [Prp] -> [Prp]
forall a. Eq a => [a] -> [a]
nub ([Prp] -> [Prp]) -> [Prp] -> [Prp]
forall a b. (a -> b) -> a -> b
$ (Possibility -> Prp) -> [Possibility] -> [Prp]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Prp
monthIs (String -> Prp) -> (Possibility -> String) -> Possibility -> Prp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Possibility -> String
forall a b. (a, b) -> b
snd) [Possibility]
possibilities)
        , (String
"Bernard", [Prp] -> [Prp]
forall a. Eq a => [a] -> [a]
nub ([Prp] -> [Prp]) -> [Prp] -> [Prp]
forall a b. (a -> b) -> a -> b
$ (Possibility -> Prp) -> [Possibility] -> [Prp]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Prp
dayIs   (Int -> Prp) -> (Possibility -> Int) -> Possibility -> Prp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Possibility -> Int
forall a b. (a, b) -> a
fst) [Possibility]
possibilities) ]

round1,round2,round3 :: KnowStruct
round1 :: KnowStruct
round1 = KnowStruct -> Form -> KnowStruct
forall a b. Update a b => a -> b -> a
update KnowStruct
start ([Form] -> Form
Conj [Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ String -> Form
knWhich String
"Albert", String -> Form -> Form
K String
"Albert" (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Form -> Form
Neg (String -> Form
knWhich String
"Bernard")])
round2 :: KnowStruct
round2 = KnowStruct -> Form -> KnowStruct
forall a b. Update a b => a -> b -> a
update KnowStruct
round1 (String -> Form
knWhich String
"Bernard")
round3 :: KnowStruct
round3 = KnowStruct -> Form -> KnowStruct
forall a b. Update a b => a -> b -> a
update KnowStruct
round2 (String -> Form
knWhich String
"Albert")

cherylsBirthday :: String
cherylsBirthday :: String
cherylsBirthday = String
m String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
d String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"th" where
  [(Int
d,String
m)] = (Possibility -> Bool) -> [Possibility] -> [Possibility]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Int
d',String
m') -> [String -> Prp
monthIs String
m', Int -> Prp
dayIs Int
d'] [Prp] -> [[Prp]] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` KnowStruct -> [[Prp]]
statesOf KnowStruct
round3) [Possibility]
possibilities

newtype Variable = Var [Prp] deriving (Variable -> Variable -> Bool
(Variable -> Variable -> Bool)
-> (Variable -> Variable -> Bool) -> Eq Variable
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Variable -> Variable -> Bool
== :: Variable -> Variable -> Bool
$c/= :: Variable -> Variable -> Bool
/= :: Variable -> Variable -> Bool
Eq,Eq Variable
Eq Variable =>
(Variable -> Variable -> Ordering)
-> (Variable -> Variable -> Bool)
-> (Variable -> Variable -> Bool)
-> (Variable -> Variable -> Bool)
-> (Variable -> Variable -> Bool)
-> (Variable -> Variable -> Variable)
-> (Variable -> Variable -> Variable)
-> Ord Variable
Variable -> Variable -> Bool
Variable -> Variable -> Ordering
Variable -> Variable -> Variable
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 :: Variable -> Variable -> Ordering
compare :: Variable -> Variable -> Ordering
$c< :: Variable -> Variable -> Bool
< :: Variable -> Variable -> Bool
$c<= :: Variable -> Variable -> Bool
<= :: Variable -> Variable -> Bool
$c> :: Variable -> Variable -> Bool
> :: Variable -> Variable -> Bool
$c>= :: Variable -> Variable -> Bool
>= :: Variable -> Variable -> Bool
$cmax :: Variable -> Variable -> Variable
max :: Variable -> Variable -> Variable
$cmin :: Variable -> Variable -> Variable
min :: Variable -> Variable -> Variable
Ord,Int -> Variable -> String -> String
[Variable] -> String -> String
Variable -> String
(Int -> Variable -> String -> String)
-> (Variable -> String)
-> ([Variable] -> String -> String)
-> Show Variable
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> Variable -> String -> String
showsPrec :: Int -> Variable -> String -> String
$cshow :: Variable -> String
show :: Variable -> String
$cshowList :: [Variable] -> String -> String
showList :: [Variable] -> String -> String
Show)

bitsOf :: Int -> [Int]
bitsOf :: Int -> [Int]
bitsOf Int
0 = []
bitsOf Int
n = Int
k Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: Int -> [Int]
bitsOf (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
2Int -> Int -> Int
forall a b. (Num a, Integral b) => a -> b -> a
^Int
k) where
  k :: Int
  k :: Int
k = Double -> Int
forall b. Integral b => Double -> b
forall a b. (RealFrac a, Integral b) => a -> b
floor (Double -> Double -> Double
forall a. Floating a => a -> a -> a
logBase Double
2 (Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n) :: Double)

-- alternative to:  booloutofForm (powerset props !! n) props
is :: Variable -> Int -> Form
is :: Variable -> Int -> Form
is (Var [Prp]
props) Int
n = [Form] -> Form
Conj [ (if Int
i Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Int -> [Int]
bitsOf Int
n then Form -> Form
forall a. a -> a
id else Form -> Form
Neg) (Prp -> Form
PrpF Prp
k)
                        | (Prp
k,Int
i) <- [Prp] -> [Int] -> [(Prp, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Prp]
props [(Int
0::Int)..] ]

isBdd :: Variable -> Int -> Bdd
isBdd :: Variable -> Int -> Bdd
isBdd Variable
v = Form -> Bdd
boolBddOf (Form -> Bdd) -> (Int -> Form) -> Int -> Bdd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Variable -> Int -> Form
is Variable
v

-- inverse of "is":
valueIn :: Variable -> State -> Int
valueIn :: Variable -> [Prp] -> Int
valueIn (Var [Prp]
props) [Prp]
s = [Int] -> Int
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [ Int
2Int -> Int -> Int
forall a b. (Num a, Integral b) => a -> b -> a
^Int
i | (Prp
k,Int
i) <- [Prp] -> [Int] -> [(Prp, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Prp]
props [(Int
0::Int)..], Prp
k Prp -> [Prp] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Prp]
s ]

explainState :: [Variable] -> State -> [Int]
explainState :: [Variable] -> [Prp] -> [Int]
explainState [Variable]
vs [Prp]
s = (Variable -> Int) -> [Variable] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Variable -> [Prp] -> Int
`valueIn` [Prp]
s) [Variable]
vs

-- an agent knows the value iff they know-whether all bits
kv :: Agent -> Variable -> Form
kv :: String -> Variable -> Form
kv String
i (Var [Prp]
props) = [Form] -> Form
Conj [ String -> Form -> Form
Kw String
i (Prp -> Form
PrpF Prp
k) | Prp
k <- [Prp]
props ]

--  Cheryl: I have two younger brothers. The product of all our ages is 144.
allStates :: [(Int,Int,Int)]
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 ]

cheryl, broOne :: Variable
cheryl :: Variable
cheryl = [Prp] -> Variable
Var [Int -> Prp
P (Int
2Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
k   ) | Int
k <- [Int
0..Int
7] ]
broOne :: Variable
broOne = [Prp] -> Variable
Var [Int -> Prp
P (Int
2Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) | Int
k <- [Int
0..Int
7] ]

ageKnsStart :: KnowStruct
ageKnsStart :: KnowStruct
ageKnsStart = [Prp] -> Bdd -> [(String, [Prp])] -> KnowStruct
KnS [Prp]
allprops Bdd
statelaw [(String, [Prp])]
forall {a}. [(String, [a])]
obs where
  allprops :: [Prp]
allprops = let (Var [Prp]
cs, Var [Prp]
bs) = (Variable
cheryl, Variable
broOne) in [Prp] -> [Prp]
forall a. Ord a => [a] -> [a]
sort ([Prp] -> [Prp]) -> [Prp] -> [Prp]
forall a b. (a -> b) -> a -> b
$ [Prp]
cs [Prp] -> [Prp] -> [Prp]
forall a. [a] -> [a] -> [a]
++ [Prp]
bs
  statelaw :: Bdd
statelaw = [Bdd] -> Bdd
disSet [ Bdd -> Bdd -> Bdd
con (Variable
cheryl Variable -> Int -> Bdd
`isBdd` Int
c) (Variable
broOne Variable -> Int -> Bdd
`isBdd` Int
b) | (Int
c,Int
b,Int
_) <- [(Int, Int, Int)]
allStates ]
  obs :: [(String, [a])]
obs = [(String
"albernard",[])]

step1,step2,step3,step4,step5 :: KnowStruct

-- Albert: We still don't know your age. What other hints can you give us?
step1 :: KnowStruct
step1 = KnowStruct
ageKnsStart KnowStruct -> Form -> KnowStruct
forall a b. Update a b => a -> b -> a
`update` Form -> Form
Neg (String -> Variable -> Form
kv String
"albernard" Variable
cheryl)

-- Cheryl: The sum of all our ages is the bus number of this bus that we are on.
step2 :: KnowStruct
step2 = KnowStruct
step1 KnowStruct -> KnowTransformer -> KnowStruct
forall a b. Update a b => a -> b -> a
`update` KnowTransformer
revealTransformer
-- For this we need a way to reveal the sum, hence we use a knowledge transformer
revealTransformer :: KnowTransformer
revealTransformer :: KnowTransformer
revealTransformer = ([Prp]
 -> Form -> [(Prp, Bdd)] -> [(String, [Prp])] -> KnowTransformer)
-> [Prp] -> Form -> [(String, [Prp])] -> KnowTransformer
noChange [Prp]
-> Form -> [(Prp, Bdd)] -> [(String, [Prp])] -> KnowTransformer
KnTrf [Prp]
addProps Form
addLaw [(String, [Prp])]
addObs where
  addProps :: [Prp]
addProps = (Int -> Prp) -> [Int] -> [Prp]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Prp
P [Int
1001..Int
1008] -- 8 bits to label all sums
  addLaw :: Form
addLaw = Form -> Form
simplify (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ [Form] -> Form
Conj [ [Form] -> Form
Disj [ Int -> Form
label (Int
c Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
b Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
a) | (Int
c,Int
b,Int
a) <- [(Int, Int, Int)]
allStates ]
                           , [Form] -> Form
Conj [ Int -> Form
sumIs Int
s Form -> Form -> Form
`Equi` Int -> Form
label Int
s | Int
s <- [Int
1..Int
144] ] ] where
    label :: Int -> Form
label Int
s = [Prp] -> [Prp] -> Form
booloutofForm ([Prp] -> [[Prp]]
forall a. [a] -> [[a]]
powerset ((Int -> Prp) -> [Int] -> [Prp]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Prp
P [Int
1001..Int
1008]) [[Prp]] -> Int -> [Prp]
forall a. HasCallStack => [a] -> Int -> a
!! Int
s) ((Int -> Prp) -> [Int] -> [Prp]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Prp
P [Int
1001..Int
1008])
    sumIs :: Int -> Form
sumIs Int
n = [Form] -> Form
Disj [ [Form] -> Form
Conj [ Variable
cheryl Variable -> Int -> Form
`is` Int
c, Variable
broOne Variable -> Int -> Form
`is` Int
b ]
                   | (Int
c,Int
b,Int
a) <- [(Int, Int, Int)]
allStates, Int
c Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
b Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n ]
  addObs :: [(String, [Prp])]
addObs = [(String
"albernard",[Prp]
addProps)]

-- Bernard: Of course we know the bus number, but we still don't know your age.
step3 :: KnowStruct
step3 = KnowStruct
step2 KnowStruct -> Form -> KnowStruct
forall a b. Update a b => a -> b -> a
`update` Form -> Form
Neg (String -> Variable -> Form
kv String
"albernard" Variable
cheryl)

-- Cheryl: Oh, I forgot to tell you that my brothers have the same age.
step4 :: KnowStruct
step4 = KnowStruct
step3 KnowStruct -> Form -> KnowStruct
forall a b. Update a b => a -> b -> a
`update` Form
sameAge where
  sameAge :: Form
sameAge = [Form] -> Form
Disj [ [Form] -> Form
Conj [Variable
cheryl Variable -> Int -> Form
`is` Int
c, Variable
broOne Variable -> Int -> Form
`is` Int
b ]
                 | (Int
c,Int
b,Int
a) <- [(Int, Int, Int)]
allStates
                 , Int
b Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
a ]

-- Albert and Bernard: Oh, now we know your age.
step5 :: KnowStruct
step5 = KnowStruct
step4 KnowStruct -> Form -> KnowStruct
forall a b. Update a b => a -> b -> a
`update` String -> Variable -> Form
kv String
"albernard" Variable
cheryl