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

module SMCDEL.Examples.RussianCards where

import Control.Monad (replicateM)
import Data.HasCacBDD hiding (Top,Bot)
import Data.List ((\\),delete,intersect,nub,sort)
import Data.Map.Strict (fromList)

import SMCDEL.Internal.Help (powerset)
import SMCDEL.Language
import SMCDEL.Other.Planning
import SMCDEL.Symbolic.S5
import qualified SMCDEL.Symbolic.K as K

rcPlayers :: [Agent]
rcPlayers :: [Agent]
rcPlayers = [Agent
alice,Agent
bob,Agent
carol]

rcNumOf :: Agent -> Int
rcNumOf :: Agent -> Int
rcNumOf Agent
"Alice" = Int
0
rcNumOf Agent
"Bob"   = Int
1
rcNumOf Agent
"Carol" = Int
2
rcNumOf Agent
_ = Agent -> Int
forall a. HasCallStack => Agent -> a
error Agent
"Unknown Agent"

rcCards :: [Int]
rcCards :: [Int]
rcCards   = [Int
0..Int
6]

rcProps :: [Prp]
rcProps :: [Prp]
rcProps   = [ Int -> Prp
P Int
k | Int
k <-[Int
0..(([Agent] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Agent]
rcPlayers Int -> Int -> Int
forall a. Num a => a -> a -> a
* [Int] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
rcCards)Int -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)] ]

hasCard :: Agent -> Int -> Form
hasCard :: Agent -> Int -> Form
hasCard Agent
i Int
n = Prp -> Form
PrpF (Int -> Prp
P (Int
3 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Agent -> Int
rcNumOf Agent
i))

hasHand :: Agent -> [Int] -> Form
hasHand :: Agent -> [Int] -> Form
hasHand Agent
i [Int]
ns = [Form] -> Form
Conj ([Form] -> Form) -> [Form] -> Form
forall a b. (a -> b) -> a -> b
$ (Int -> Form) -> [Int] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map (Agent
i Agent -> Int -> Form
`hasCard`) [Int]
ns

rcExplain :: Prp -> String
rcExplain :: Prp -> Agent
rcExplain (P Int
k) = ([Agent]
rcPlayers [Agent] -> Int -> Agent
forall a. HasCallStack => [a] -> Int -> a
!! Int
i) Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ Agent
" has card " Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ Int -> Agent
forall a. Show a => a -> Agent
show Int
n where (Int
n,Int
i) = Int -> Int -> (Int, Int)
forall a. Integral a => a -> a -> (a, a)
divMod Int
k Int
3

allCardsGiven, allCardsUnique :: Form
allCardsGiven :: Form
allCardsGiven  = [Form] -> Form
Conj [ [Form] -> Form
Disj [ Agent
i Agent -> Int -> Form
`hasCard` Int
n | Agent
i <- [Agent]
rcPlayers ] | Int
n <- [Int]
rcCards ]
allCardsUnique :: Form
allCardsUnique = [Form] -> Form
Conj [ Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Int -> Form
isDouble Int
n | Int
n <- [Int]
rcCards ] where
  isDouble :: Int -> Form
isDouble Int
n = [Form] -> Form
Disj [ [Form] -> Form
Conj [ Agent
x Agent -> Int -> Form
`hasCard` Int
n, Agent
y Agent -> Int -> Form
`hasCard` Int
n ] | Agent
x <- [Agent]
rcPlayers, Agent
y <- [Agent]
rcPlayers, Agent
x Agent -> Agent -> Bool
forall a. Ord a => a -> a -> Bool
< Agent
y ]

distribute331 :: Form
distribute331 :: Form
distribute331 = [Form] -> Form
Conj [ Form
aliceAtLeastThree, Form
bobAtLeastThree, Form
carolAtLeastOne ] where
  triples :: [[Int]]
triples = [ [Int
x, Int
y, Int
z] | Int
x <- [Int]
rcCards, Int
y <- Int -> [Int] -> [Int]
forall a. Eq a => a -> [a] -> [a]
delete Int
x [Int]
rcCards, Int
z <- [Int]
rcCards [Int] -> [Int] -> [Int]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Int
x,Int
y] ]
  aliceAtLeastThree :: Form
aliceAtLeastThree = [Form] -> Form
Disj [ [Form] -> Form
Conj ((Int -> Form) -> [Int] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map (Agent
alice Agent -> Int -> Form
`hasCard`) [Int]
t) | [Int]
t <- [[Int]]
triples ]
  bobAtLeastThree :: Form
bobAtLeastThree   = [Form] -> Form
Disj [ [Form] -> Form
Conj ((Int -> Form) -> [Int] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map (Agent
bob   Agent -> Int -> Form
`hasCard`) [Int]
t) | [Int]
t <- [[Int]]
triples ]
  carolAtLeastOne :: Form
carolAtLeastOne   = [Form] -> Form
Disj [ Agent
carol Agent -> Int -> Form
`hasCard` Int
k | Int
k<-[Int
0..Int
6] ]

rusSCN :: KnowScene
rusKNS :: KnowStruct
rusSCN :: KnowScene
rusSCN@(KnowStruct
rusKNS,[Prp]
_) = ([Prp] -> Bdd -> [(Agent, [Prp])] -> KnowStruct
KnS [Prp]
rcProps Bdd
law [ (Agent
i, Agent -> [Prp]
obs Agent
i) | Agent
i <- [Agent]
rcPlayers ], [Prp]
defaultDeal) where
  law :: Bdd
law = Form -> Bdd
boolBddOf (Form -> Bdd) -> Form -> Bdd
forall a b. (a -> b) -> a -> b
$ [Form] -> Form
Conj [ Form
allCardsGiven, Form
allCardsUnique, Form
distribute331 ]
  obs :: Agent -> [Prp]
obs Agent
i = [ Int -> Prp
P (Int
3 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Agent -> Int
rcNumOf Agent
i) | Int
k<-[Int
0..Int
6] ]
  defaultDeal :: [Prp]
defaultDeal = [Int -> Prp
P Int
0,Int -> Prp
P Int
3,Int -> Prp
P Int
6,Int -> Prp
P Int
10,Int -> Prp
P Int
13,Int -> Prp
P Int
16,Int -> Prp
P Int
20]

aAnnounce :: Form
aAnnounce :: Form
aAnnounce = Agent -> Form -> Form
K Agent
alice (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ [Form] -> Form
Disj [ [Form] -> Form
Conj ((Int -> Form) -> [Int] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map (Agent
alice Agent -> Int -> Form
`hasCard`) [Int]
hand) |
  [Int]
hand <- [ [Int
0,Int
1,Int
2], [Int
0,Int
3,Int
4], [Int
0,Int
5,Int
6], [Int
1,Int
3,Int
5], [Int
2,Int
4,Int
6] ] ]

bAnnounce :: Form
bAnnounce :: Form
bAnnounce = Agent -> Form -> Form
K Agent
bob (Agent
carol Agent -> Int -> Form
`hasCard` Int
6)

aKnowsBs, bKnowsAs, cIgnorant :: Form
aKnowsBs :: Form
aKnowsBs = [Form] -> Form
Conj [ Agent
alice Agent -> Form -> Form
`Kw` (Agent
bob   Agent -> Int -> Form
`hasCard` Int
k) | Int
k<-[Int]
rcCards ]
bKnowsAs :: Form
bKnowsAs = [Form] -> Form
Conj [ Agent
bob   Agent -> Form -> Form
`Kw` (Agent
alice Agent -> Int -> Form
`hasCard` Int
k) | Int
k<-[Int]
rcCards ]
cIgnorant :: Form
cIgnorant = [Form] -> Form
Conj ([Form] -> Form) -> [Form] -> Form
forall a b. (a -> b) -> a -> b
$ [[Form]] -> [Form]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [ Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Agent -> Form -> Form
K Agent
carol (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Agent
alice Agent -> Int -> Form
`hasCard` Int
i
                            , Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Agent -> Form -> Form
K Agent
carol (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Agent
bob   Agent -> Int -> Form
`hasCard` Int
i ] | Int
i<-[Int]
rcCards ]

rcCheck :: Int -> Form
rcCheck :: Int -> Form
rcCheck Int
0 = Form
aAnnounce

rcCheck Int
1 = Form -> Form -> Form
PubAnnounce Form
aAnnounce Form
bKnowsAs
rcCheck Int
2 = Form -> Form -> Form
PubAnnounce Form
aAnnounce ([Agent] -> Form -> Form
Ck [Agent
alice,Agent
bob] Form
bKnowsAs)

rcCheck Int
3 = Form -> Form -> Form
PubAnnounce Form
aAnnounce (Agent -> Form -> Form
K Agent
bob (Prp -> Form
PrpF (Int -> Prp
P Int
20)))

rcCheck Int
4 = Form -> Form -> Form
PubAnnounce Form
aAnnounce ([Agent] -> Form -> Form
Ck [Agent
alice,Agent
bob,Agent
carol] Form
cIgnorant)

rcCheck Int
5 = Form -> Form -> Form
PubAnnounce Form
aAnnounce (Form -> Form -> Form
PubAnnounce Form
bAnnounce ([Agent] -> Form -> Form
Ck [Agent
alice,Agent
bob] Form
aKnowsBs))
rcCheck Int
6 = Form -> Form -> Form
PubAnnounce Form
aAnnounce (Form -> Form -> Form
PubAnnounce Form
bAnnounce ([Agent] -> Form -> Form
Ck [Agent
alice,Agent
bob] Form
bKnowsAs))
rcCheck Int
_ = Form -> Form -> Form
PubAnnounce Form
aAnnounce (Form -> Form -> Form
PubAnnounce Form
bAnnounce ([Agent] -> Form -> Form
Ck [Agent]
rcPlayers Form
cIgnorant))

rcAllChecks :: Bool
rcAllChecks :: Bool
rcAllChecks = KnowScene -> Form -> Bool
evalViaBdd KnowScene
rusSCN ([Form] -> Form
Conj ((Int -> Form) -> [Int] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Form
rcCheck [Int
0..Int
7]))

checkSet :: [[Int]] -> Bool
checkSet :: [[Int]] -> Bool
checkSet [[Int]]
set = (Form -> Bool) -> [Form] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (KnowScene -> Form -> Bool
evalViaBdd KnowScene
rusSCN) [Form]
fs where
  aliceSays :: Form
aliceSays = Agent -> Form -> Form
K Agent
alice ([Form] -> Form
Disj [ [Form] -> Form
Conj ([Form] -> Form) -> [Form] -> Form
forall a b. (a -> b) -> a -> b
$ (Int -> Form) -> [Int] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map (Agent
alice Agent -> Int -> Form
`hasCard`) [Int]
h | [Int]
h <- [[Int]]
set ])
  bobSays :: Form
bobSays = Agent -> Form -> Form
K Agent
bob (Agent
carol Agent -> Int -> Form
`hasCard` Int
6)
  fs :: [Form]
fs = [ Form
aliceSays
       , Form -> Form -> Form
PubAnnounce Form
aliceSays Form
bKnowsAs
       , Form -> Form -> Form
PubAnnounce Form
aliceSays ([Agent] -> Form -> Form
Ck [Agent
alice,Agent
bob] Form
bKnowsAs)
       , Form -> Form -> Form
PubAnnounce Form
aliceSays ([Agent] -> Form -> Form
Ck [Agent
alice,Agent
bob,Agent
carol] Form
cIgnorant)
       , Form -> Form -> Form
PubAnnounce Form
aliceSays (Form -> Form -> Form
PubAnnounce Form
bobSays ([Agent] -> Form -> Form
Ck [Agent
alice,Agent
bob] (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ [Form] -> Form
Conj [Form
aKnowsBs, Form
bKnowsAs]))
       , Form -> Form -> Form
PubAnnounce Form
aliceSays (Form -> Form -> Form
PubAnnounce Form
bobSays ([Agent] -> Form -> Form
Ck [Agent]
rcPlayers Form
cIgnorant)) ]

possibleHands :: [[Int]]
possibleHands :: [[Int]]
possibleHands = [ [Int
x,Int
y,Int
z] | Int
x <- [Int]
rcCards, Int
y <- (Int -> Bool) -> [Int] -> [Int]
forall a. (a -> Bool) -> [a] -> [a]
filter (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
x) [Int]
rcCards, Int
z <-(Int -> Bool) -> [Int] -> [Int]
forall a. (a -> Bool) -> [a] -> [a]
filter (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
y) [Int]
rcCards ]

pickHandsNoCrossing :: [ [Int] ] -> Int -> [ [ [Int] ] ]
pickHandsNoCrossing :: [[Int]] -> Int -> [[[Int]]]
pickHandsNoCrossing [[Int]]
_ Int
0 = [ [ [ ] ] ]
pickHandsNoCrossing [[Int]]
unused Int
1 = [ [[Int]
h] | [Int]
h <- [[Int]]
unused ]
pickHandsNoCrossing [[Int]]
unused Int
n = [[[[Int]]]] -> [[[Int]]]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [ [Int]
h[Int] -> [[Int]] -> [[Int]]
forall a. a -> [a] -> [a]
:[[Int]]
hs | [[Int]]
hs <- [[Int]] -> Int -> [[[Int]]]
pickHandsNoCrossing ([Int] -> [[Int]] -> [[Int]]
forall {a}. Ord a => [a] -> [[a]] -> [[a]]
myfilter [Int]
h [[Int]]
unused) (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) ]  | [Int]
h <- [[Int]]
unused ] where
  myfilter :: [a] -> [[a]] -> [[a]]
myfilter [a]
h = ([a] -> Bool) -> [[a]] -> [[a]]
forall a. (a -> Bool) -> [a] -> [a]
filter (\[a]
xs -> [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([a]
h [a] -> [a] -> [a]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` [a]
xs) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
2 Bool -> Bool -> Bool
&& [a]
h [a] -> [a] -> Bool
forall a. Ord a => a -> a -> Bool
< [a]
xs) -- do not allow intersection > 2

allHandLists, safeHandLists :: [ [ [Int] ] ]
allHandLists :: [[[Int]]]
allHandLists = (Int -> [[[Int]]]) -> [Int] -> [[[Int]]]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([[Int]] -> Int -> [[[Int]]]
pickHandsNoCrossing [[Int]]
possibleHands) [Int
5,Int
6,Int
7]
safeHandLists :: [[[Int]]]
safeHandLists = [[[Int]]] -> [[[Int]]]
forall a. Ord a => [a] -> [a]
sort (([[Int]] -> Bool) -> [[[Int]]] -> [[[Int]]]
forall a. (a -> Bool) -> [a] -> [a]
filter [[Int]] -> Bool
checkSet [[[Int]]]
allHandLists)

alicesActions :: [Form]
alicesActions :: [Form]
alicesActions = [ [Form] -> Form
Disj ([Form] -> Form) -> [Form] -> Form
forall a b. (a -> b) -> a -> b
$ ([Int] -> Form) -> [[Int]] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map (Agent
alice Agent -> [Int] -> Form
`hasHand`) ([Int
0,Int
1,Int
2][Int] -> [[Int]] -> [[Int]]
forall a. a -> [a] -> [a]
:[[Int]]
otherHands) | [[Int]]
otherHands <- [[[Int]]]
handLists ] where
  handLists :: [ [ [Int] ] ]
  handLists :: [[[Int]]]
handLists = [[Int]] -> Int -> [[[Int]]]
pickHands ([Int] -> [[Int]] -> [[Int]]
forall a. Eq a => a -> [a] -> [a]
delete [Int
0,Int
1,Int
2] [[Int]]
possibleHands) Int
4
  pickHands :: [ [Int] ] -> Int -> [ [ [Int] ] ]
  pickHands :: [[Int]] -> Int -> [[[Int]]]
pickHands [[Int]]
_     Int
0 = [ [ [ ] ] ]
  pickHands [[Int]]
hands Int
1 = [ [ [Int]
h   ] | [Int]
h <- [[Int]]
hands ]
  pickHands [[Int]]
hands Int
n = [ [Int]
h[Int] -> [[Int]] -> [[Int]]
forall a. a -> [a] -> [a]
:[[Int]]
hs    | [Int]
h <- [[Int]]
hands, [[Int]]
hs <- [[Int]] -> Int -> [[[Int]]]
pickHands (([Int] -> Bool) -> [[Int]] -> [[Int]]
forall a. (a -> Bool) -> [a] -> [a]
filter ([Int]
h [Int] -> [Int] -> Bool
forall a. Ord a => a -> a -> Bool
<) [[Int]]
hands) (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) ]

bobsActions :: [Form]
bobsActions :: [Form]
bobsActions = [ Agent
carol Agent -> Int -> Form
`hasCard` Int
n | Int
n <- [Int] -> [Int]
forall a. [a] -> [a]
reverse [Int
4..Int
6] ]

rcSolutions :: [ [Form] ]
rcSolutions :: [[Form]]
rcSolutions = [ [Form
a, Form
b] | Form
a <- [Form]
alicesActions, Form
b <- [Form]
bobsActions, Form -> Form -> Bool
testPlan Form
a Form
b ] where
  testPlan :: Form -> Form -> Bool
  testPlan :: Form -> Form -> Bool
testPlan Form
aSays Form
bSays = (Form -> Bool) -> [Form] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (KnowScene -> Form -> Bool
evalViaBdd KnowScene
rusSCN)
    -- NOTE: increasing checks are faster than one big conjunction!
    [ Form
aSays
    , Form -> Form -> Form
PubAnnounce Form
aSays Form
bKnowsAs
    , Form -> Form -> Form
PubAnnounce Form
aSays Form
cIgnorant
    , Form -> Form -> Form
PubAnnounce Form
aSays Form
bSays
    , Form -> Form -> Form
PubAnnounce Form
aSays (Form -> Form -> Form
PubAnnounce Form
bSays Form
aKnowsBs)
    , Form -> Form -> Form
PubAnnounce Form
aSays (Form -> Form -> Form
PubAnnounce Form
bSays ([Agent] -> Form -> Form
Ck [Agent
alice,Agent
bob] (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ [Form] -> Form
Conj [Form
cIgnorant,Form
aKnowsBs,Form
bKnowsAs])) ]

rcPlan :: OfflinePlan
rcPlan :: [Form]
rcPlan = [ Form
aAnnounce, Form
bAnnounce ]

rcGoal :: Form
rcGoal :: Form
rcGoal = [Form] -> Form
Conj [ Form
aKnowsBs
              , Form
bKnowsAs
              , [Agent] -> Form -> Form
Ck [Agent
alice,Agent
bob] ([Form] -> Form
Conj [Form
aKnowsBs, Form
bKnowsAs])
              , [Agent] -> Form -> Form
Ck [Agent
alice,Agent
bob,Agent
carol] Form
cIgnorant ]

rcSolutionsViaPlanning :: [OfflinePlan]
rcSolutionsViaPlanning :: [[Form]]
rcSolutionsViaPlanning = Int -> KnowScene -> [Form] -> [Form] -> Form -> [[Form]]
forall a.
(Eq a, Semantics a, Update a Form) =>
Int -> a -> [Form] -> [Form] -> Form -> [[Form]]
offlineSearch Int
maxSteps KnowScene
start [Form]
actions [Form]
constraints Form
goal where
  maxSteps :: Int
maxSteps    = Int
2 -- We need two steps!
  start :: KnowScene
start       = RusCardProblem -> KnowScene
rusSCNfor (Int
3,Int
3,Int
1)
  actions :: [Form]
actions     = [Form]
alicesActions [Form] -> [Form] -> [Form]
forall a. [a] -> [a] -> [a]
++ [Form]
bobsActions
  constraints :: [Form]
constraints = [Form
cIgnorant,Form
bKnowsAs]
  goal :: Form
goal        = [Form] -> Form
Conj [Form
aKnowsBs, Form
bKnowsAs]

type RusCardProblem = (Int,Int,Int)

distribute :: RusCardProblem -> Form
distribute :: RusCardProblem -> Form
distribute (Int
na,Int
nb,Int
nc) = [Form] -> Form
Conj [ Agent
alice Agent -> Int -> Form
`hasAtLeast` Int
na
                             , Agent
bob   Agent -> Int -> Form
`hasAtLeast` Int
nb
                             , Agent
carol Agent -> Int -> Form
`hasAtLeast` Int
nc ] where
  n :: Int
n = Int
na Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
nb Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
nc
  hasAtLeast :: Agent -> Int -> Form
  hasAtLeast :: Agent -> Int -> Form
hasAtLeast Agent
_ Int
0 = Form
Top
  hasAtLeast Agent
i Int
1 = [Form] -> Form
Disj [ Agent
i Agent -> Int -> Form
`hasCard` Int
k | Int
k <- Int -> [Int]
nCards Int
n ]
  hasAtLeast Agent
i Int
k = [Form] -> Form
Disj [ [Form] -> Form
Conj ((Int -> Form) -> [Int] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map (Agent
i Agent -> Int -> Form
`hasCard`) ([Int] -> [Int]
forall a. Ord a => [a] -> [a]
sort [Int]
set))
                        | [Int]
set <- [Int] -> [[Int]]
forall a. [a] -> [[a]]
powerset (Int -> [Int]
nCards Int
n), [Int] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
set Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
k ]

nCards :: Int -> [Int]
nCards :: Int -> [Int]
nCards Int
n = [Int
0..(Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)]

nCardsGiven, nCardsUnique :: Int -> Form
nCardsGiven :: Int -> Form
nCardsGiven  Int
n = [Form] -> Form
Conj [ [Form] -> Form
Disj [ Agent
i Agent -> Int -> Form
`hasCard` Int
k | Agent
i <- [Agent]
rcPlayers ] | Int
k <- Int -> [Int]
nCards Int
n ]
nCardsUnique :: Int -> Form
nCardsUnique Int
n = [Form] -> Form
Conj [ Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Int -> Form
isDouble Int
k | Int
k <- Int -> [Int]
nCards Int
n ] where
  isDouble :: Int -> Form
isDouble Int
k = [Form] -> Form
Disj [ [Form] -> Form
Conj [ Agent
x Agent -> Int -> Form
`hasCard` Int
k, Agent
y Agent -> Int -> Form
`hasCard` Int
k ] | Agent
x <- [Agent]
rcPlayers, Agent
y <- [Agent]
rcPlayers, Agent
xAgent -> Agent -> Bool
forall a. Eq a => a -> a -> Bool
/=Agent
y, Agent
x Agent -> Agent -> Bool
forall a. Ord a => a -> a -> Bool
< Agent
y ]

rusSCNfor :: RusCardProblem -> KnowScene
rusSCNfor :: RusCardProblem -> KnowScene
rusSCNfor (Int
na,Int
nb,Int
nc) = ([Prp] -> Bdd -> [(Agent, [Prp])] -> KnowStruct
KnS [Prp]
props Bdd
law [ (Agent
i, Agent -> [Prp]
obs Agent
i) | Agent
i <- [Agent]
rcPlayers ], [Prp]
defaultDeal) where
  n :: Int
n = Int
na Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
nb Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
nc
  props :: [Prp]
props   = [ Int -> Prp
P Int
k | Int
k <-[Int
0..(([Agent] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Agent]
rcPlayers Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
n)Int -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)] ]
  law :: Bdd
law = Form -> Bdd
boolBddOf (Form -> Bdd) -> Form -> Bdd
forall a b. (a -> b) -> a -> b
$ [Form] -> Form
Conj [ Int -> Form
nCardsGiven Int
n, Int -> Form
nCardsUnique Int
n, RusCardProblem -> Form
distribute (Int
na,Int
nb,Int
nc)  ]
  obs :: Agent -> [Prp]
obs Agent
i = [ Int -> Prp
P (Int
3 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Agent -> Int
rcNumOf Agent
i) | Int
k<-[Int
0..Int
6] ]
  defaultDeal :: [Prp]
defaultDeal =  [ let (PrpF Prp
p) = Agent
i Agent -> Int -> Form
`hasCard` Int
k in Prp
p | Agent
i <- [Agent]
rcPlayers, Int
k <- Agent -> [Int]
cardsFor Agent
i ]
  cardsFor :: Agent -> [Int]
cardsFor Agent
"Alice" = [Int
0..(Int
naInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)]
  cardsFor Agent
"Bob"   = [Int
na..(Int
naInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
nbInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)]
  cardsFor Agent
"Carol" = [(Int
naInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
nb)..(Int
naInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
nbInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
ncInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)]
  cardsFor Agent
_       = Agent -> [Int]
forall a. HasCallStack => Agent -> a
error Agent
"Who is that?"

possibleHandsN :: Int -> Int -> [[Int]]
possibleHandsN :: Int -> Int -> [[Int]]
possibleHandsN Int
n Int
na = ([Int] -> Bool) -> [[Int]] -> [[Int]]
forall a. (a -> Bool) -> [a] -> [a]
filter [Int] -> Bool
forall {a}. Eq a => [a] -> Bool
alldiff ([[Int]] -> [[Int]]) -> [[Int]] -> [[Int]]
forall a b. (a -> b) -> a -> b
$ [[Int]] -> [[Int]]
forall a. Eq a => [a] -> [a]
nub ([[Int]] -> [[Int]]) -> [[Int]] -> [[Int]]
forall a b. (a -> b) -> a -> b
$ ([Int] -> [Int]) -> [[Int]] -> [[Int]]
forall a b. (a -> b) -> [a] -> [b]
map [Int] -> [Int]
forall a. Ord a => [a] -> [a]
sort ([[Int]] -> [[Int]]) -> [[Int]] -> [[Int]]
forall a b. (a -> b) -> a -> b
$ Int -> [Int] -> [[Int]]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
na (Int -> [Int]
nCards Int
n) where
  alldiff :: [a] -> Bool
alldiff [] = Bool
True
  alldiff (a
x:[a]
xs) = a
x a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [a]
xs Bool -> Bool -> Bool
&& [a] -> Bool
alldiff [a]
xs

allHandListsN :: Int -> Int -> [ [ [Int] ] ]
allHandListsN :: Int -> Int -> [[[Int]]]
allHandListsN Int
n Int
na = (Int -> [[[Int]]]) -> [Int] -> [[[Int]]]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([[Int]] -> Int -> [[[Int]]]
pickHandsNoCrossing (Int -> Int -> [[Int]]
possibleHandsN Int
n Int
na)) [Int
5,Int
6,Int
7] -- FIXME how to adapt the number of hands for larger n?

aKnowsBsN, bKnowsAsN, cIgnorantN :: Int -> Form
aKnowsBsN :: Int -> Form
aKnowsBsN Int
n = [Form] -> Form
Conj [ Agent
alice Agent -> Form -> Form
`Kw` (Agent
bob Agent -> Int -> Form
`hasCard` Int
k) | Int
k <- Int -> [Int]
nCards Int
n ]
bKnowsAsN :: Int -> Form
bKnowsAsN Int
n = [Form] -> Form
Conj [ Agent
bob Agent -> Form -> Form
`Kw` (Agent
alice Agent -> Int -> Form
`hasCard` Int
k) | Int
k <- Int -> [Int]
nCards Int
n ]
cIgnorantN :: Int -> Form
cIgnorantN Int
n = [Form] -> Form
Conj ([Form] -> Form) -> [Form] -> Form
forall a b. (a -> b) -> a -> b
$ [[Form]] -> [Form]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [ Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Agent -> Form -> Form
K Agent
carol (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Agent
alice Agent -> Int -> Form
`hasCard` Int
i
                            , Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Agent -> Form -> Form
K Agent
carol (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Agent
bob   Agent -> Int -> Form
`hasCard` Int
i ] | Int
i <- Int -> [Int]
nCards Int
n ]

checkSetFor :: RusCardProblem -> [[Int]] -> Bool
checkSetFor :: RusCardProblem -> [[Int]] -> Bool
checkSetFor (Int
na,Int
nb,Int
nc) [[Int]]
set = [Form] -> Form -> KnowScene -> Bool
forall o. Semantics o => [Form] -> Form -> o -> Bool
forall a o. (IsPlan a, Semantics o) => a -> Form -> o -> Bool
reachesOn [Form]
plan Form
rcGoal (RusCardProblem -> KnowScene
rusSCNfor (Int
na,Int
nb,Int
nc)) where
  n :: Int
n = Int
na Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
nb Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
nc
  aliceSays :: Form
aliceSays = Agent -> Form -> Form
K Agent
alice ([Form] -> Form
Disj [ [Form] -> Form
Conj ([Form] -> Form) -> [Form] -> Form
forall a b. (a -> b) -> a -> b
$ (Int -> Form) -> [Int] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map (Agent
alice Agent -> Int -> Form
`hasCard`) [Int]
h | [Int]
h <- [[Int]]
set ])
  bobSays :: Form
bobSays = Agent -> Form -> Form
K Agent
bob (Agent
carol Agent -> Int -> Form
`hasCard` [Int] -> Int
forall a. HasCallStack => [a] -> a
last (Int -> [Int]
nCards Int
n))
  plan :: [Form]
plan = [ Form
aliceSays, Form
bobSays ]

checkHandsFor :: RusCardProblem -> [ ( [[Int]], Bool) ]
checkHandsFor :: RusCardProblem -> [([[Int]], Bool)]
checkHandsFor (Int
na,Int
nb,Int
nc) = ([[Int]] -> ([[Int]], Bool)) -> [[[Int]]] -> [([[Int]], Bool)]
forall a b. (a -> b) -> [a] -> [b]
map (\[[Int]]
hs -> ([[Int]]
hs, RusCardProblem -> [[Int]] -> Bool
checkSetFor (Int
na,Int
nb,Int
nc) [[Int]]
hs)) (Int -> Int -> [[[Int]]]
allHandListsN Int
n Int
na) where
  n :: Int
n = Int
na Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
nb Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
nc

allCasesUpTo :: Int -> [RusCardProblem]
allCasesUpTo :: Int -> [RusCardProblem]
allCasesUpTo Int
bound = [ (Int
na,Int
nb,Int
nc) | Int
na <- [Int
1..Int
bound]
                                  , Int
nb <- [Int
1..(Int
boundInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
na)]
                                  , Int
nc <- [Int
1..(Int
boundInt -> Int -> Int
forall a. Num a => a -> a -> a
-(Int
naInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
nb))]
                                  -- these restrictions are only proven
                                  -- for two announcement plans!
                                  , Int
nc Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< (Int
na Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
                                  , Int
nc Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
nb ]

dontChange :: [Form] -> K.RelBDD
dontChange :: [Form] -> RelBDD
dontChange [Form]
fs = [Bdd] -> Bdd
conSet ([Bdd] -> Bdd) -> Tagged Dubbel [Bdd] -> RelBDD
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RelBDD] -> Tagged Dubbel [Bdd]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [ Bdd -> Bdd -> Bdd
equ (Bdd -> Bdd -> Bdd) -> RelBDD -> Tagged Dubbel (Bdd -> Bdd)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bdd -> RelBDD
K.mvBdd Bdd
b Tagged Dubbel (Bdd -> Bdd) -> RelBDD -> RelBDD
forall a b.
Tagged Dubbel (a -> b) -> Tagged Dubbel a -> Tagged Dubbel b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Bdd -> RelBDD
K.cpBdd Bdd
b | Bdd
b <- (Form -> Bdd) -> [Form] -> [Bdd]
forall a b. (a -> b) -> [a] -> [b]
map Form -> Bdd
boolBddOf [Form]
fs ]

noDoubles :: Int -> Form
noDoubles :: Int -> Form
noDoubles Int
n = Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ [Form] -> Form
Disj [ Int -> Form
notDouble Int
k | Int
k <- Int -> [Int]
nCards Int
n ] where
  notDouble :: Int -> Form
notDouble Int
k = [Form] -> Form
Conj [Agent
alice Agent -> Int -> Form
`hasCard` Int
k, Agent
bob Agent -> Int -> Form
`hasCard` Int
k]

rusBelScnfor :: RusCardProblem -> K.BelScene
rusBelScnfor :: RusCardProblem -> BelScene
rusBelScnfor (Int
na,Int
nb,Int
nc) = ([Prp] -> Bdd -> Map Agent RelBDD -> BelStruct
K.BlS [Prp]
props Bdd
law ([(Agent, RelBDD)] -> Map Agent RelBDD
forall k a. Ord k => [(k, a)] -> Map k a
fromList [ (Agent
i, Agent -> RelBDD
obsbdd Agent
i) | Agent
i <- [Agent]
rcPlayers ]), [Prp]
defaultDeal) where
  n :: Int
n = Int
na Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
nb Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
nc
  props :: [Prp]
props   = [ Int -> Prp
P Int
k | Int
k <-[Int
0..((Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
n)Int -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)] ]
  law :: Bdd
law = Form -> Bdd
boolBddOf (Form -> Bdd) -> Form -> Bdd
forall a b. (a -> b) -> a -> b
$ [Form] -> Form
Conj [ Int -> Form
noDoubles Int
n, RusCardProblem -> Form
distribute (Int
na,Int
nb,Int
nc)  ]
  obsbdd :: Agent -> RelBDD
obsbdd Agent
"Alice" = [Form] -> RelBDD
dontChange [ Prp -> Form
PrpF (Int -> Prp
P (Int -> Prp) -> Int -> Prp
forall a b. (a -> b) -> a -> b
$ Int
2Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
k) | Int
k <- [Int
0..(Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)] ]
  obsbdd Agent
"Bob"   = [Form] -> RelBDD
dontChange [ Prp -> Form
PrpF (Int -> Prp
P (Int -> Prp) -> Int -> Prp
forall a b. (a -> b) -> a -> b
$ (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
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)] ]
  obsbdd Agent
"Carol" = [Form] -> RelBDD
dontChange [ [Form] -> Form
Disj [Prp -> Form
PrpF (Int -> Prp
P (Int -> Prp) -> Int -> Prp
forall a b. (a -> b) -> a -> b
$ Int
2Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
k), Prp -> Form
PrpF (Int -> Prp
P (Int -> Prp) -> Int -> Prp
forall a b. (a -> b) -> a -> b
$ (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
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)] ]
  obsbdd Agent
_       = Agent -> RelBDD
forall a. HasCallStack => Agent -> a
error Agent
"Unkown Agent"
  defaultDeal :: [Prp]
defaultDeal =  [ let (PrpF Prp
p) = Agent
i Agent -> Int -> Form
`hasCard` Int
k in Prp
p | Agent
i <- [Agent
alice,Agent
bob], Int
k <- Agent -> [Int]
cardsFor Agent
i ] where
    cardsFor :: Agent -> [Int]
cardsFor Agent
"Alice" = [Int
0..(Int
naInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)]
    cardsFor Agent
"Bob"   = [Int
na..(Int
naInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
nbInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)]
    cardsFor Agent
"Carol" = [(Int
naInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
nb)..(Int
naInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
nbInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
ncInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)]
    cardsFor Agent
_       = Agent -> [Int]
forall a. HasCallStack => Agent -> a
error Agent
"Unkown Agent"