module SMCDEL.Examples.SumAndProduct where

import Data.List
import Data.Maybe

import SMCDEL.Language
import SMCDEL.Internal.Help
import SMCDEL.Symbolic.S5

-- possible pairs 1<x<y, x+y<=100
pairs :: [(Int, Int)]
pairs :: [(Int, Int)]
pairs = [(Int
x,Int
y) | Int
x<-[Int
2..Int
100], Int
y<-[Int
2..Int
100], Int
xInt -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<Int
y, Int
xInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
yInt -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<=Int
100]

-- 7 propositions to label [2..100], because 2^6 = 64 < 100 < 128 = 2^7
xProps, yProps, sProps, pProps :: [Prp]
xProps :: [Prp]
xProps = [(Int -> Prp
P  Int
1)..(Int -> Prp
P  Int
7)]
yProps :: [Prp]
yProps = [(Int -> Prp
P  Int
8)..(Int -> Prp
P Int
14)]
sProps :: [Prp]
sProps = [(Int -> Prp
P Int
15)..(Int -> Prp
P Int
21)]
-- 12 propositions for the product, because 2^11 = 2048 < 2500 < 4096 = 2^12
pProps :: [Prp]
pProps = [(Int -> Prp
P Int
22)..(Int -> Prp
P Int
33)]

sapAllProps :: [Prp]
sapAllProps :: [Prp]
sapAllProps = [Prp] -> [Prp]
forall a. Ord a => [a] -> [a]
sort ([Prp] -> [Prp]) -> [Prp] -> [Prp]
forall a b. (a -> b) -> a -> b
$ [Prp]
xProps [Prp] -> [Prp] -> [Prp]
forall a. [a] -> [a] -> [a]
++ [Prp]
yProps [Prp] -> [Prp] -> [Prp]
forall a. [a] -> [a] -> [a]
++ [Prp]
sProps [Prp] -> [Prp] -> [Prp]
forall a. [a] -> [a] -> [a]
++ [Prp]
pProps

xIs, yIs, sIs, pIs :: Int -> Form
xIs :: Int -> Form
xIs Int
n = [Prp] -> [Prp] -> Form
booloutofForm ([Prp] -> [[Prp]]
forall a. [a] -> [[a]]
powerset [Prp]
xProps [[Prp]] -> Int -> [Prp]
forall a. HasCallStack => [a] -> Int -> a
!! Int
n) [Prp]
xProps
yIs :: Int -> Form
yIs Int
n = [Prp] -> [Prp] -> Form
booloutofForm ([Prp] -> [[Prp]]
forall a. [a] -> [[a]]
powerset [Prp]
yProps [[Prp]] -> Int -> [Prp]
forall a. HasCallStack => [a] -> Int -> a
!! Int
n) [Prp]
yProps
sIs :: Int -> Form
sIs Int
n = [Prp] -> [Prp] -> Form
booloutofForm ([Prp] -> [[Prp]]
forall a. [a] -> [[a]]
powerset [Prp]
sProps [[Prp]] -> Int -> [Prp]
forall a. HasCallStack => [a] -> Int -> a
!! Int
n) [Prp]
sProps
pIs :: Int -> Form
pIs Int
n = [Prp] -> [Prp] -> Form
booloutofForm ([Prp] -> [[Prp]]
forall a. [a] -> [[a]]
powerset [Prp]
pProps [[Prp]] -> Int -> [Prp]
forall a. HasCallStack => [a] -> Int -> a
!! Int
n) [Prp]
pProps

xyAre :: (Int,Int) -> Form
xyAre :: (Int, Int) -> Form
xyAre (Int
n,Int
m) = [Form] -> Form
Conj [ Int -> Form
xIs Int
n, Int -> Form
yIs Int
m ]

sapKnStruct :: KnowStruct
sapKnStruct :: KnowStruct
sapKnStruct = [Prp] -> Bdd -> [(Agent, [Prp])] -> KnowStruct
KnS [Prp]
sapAllProps Bdd
law [(Agent, [Prp])]
obs where
  law :: Bdd
law = Form -> Bdd
boolBddOf (Form -> Bdd) -> Form -> Bdd
forall a b. (a -> b) -> a -> b
$ [Form] -> Form
Disj [ [Form] -> Form
Conj [ (Int, Int) -> Form
xyAre (Int
x,Int
y), Int -> Form
sIs (Int
xInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
y), Int -> Form
pIs (Int
xInt -> Int -> Int
forall a. Num a => a -> a -> a
*Int
y) ] | (Int
x,Int
y) <- [(Int, Int)]
pairs ]
  obs :: [(Agent, [Prp])]
obs = [ (Agent
alice, [Prp]
sProps), (Agent
bob, [Prp]
pProps) ]

sapKnows :: Agent -> Form
sapKnows :: Agent -> Form
sapKnows Agent
i = [Form] -> Form
Disj [ Agent -> Form -> Form
K Agent
i ((Int, Int) -> Form
xyAre (Int, Int)
p) | (Int, Int)
p <- [(Int, Int)]
pairs ]

sapForm1, sapForm2, sapForm3 :: Form
sapForm1 :: Form
sapForm1 = Agent -> Form -> Form
K Agent
alice (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Form -> Form
Neg (Agent -> Form
sapKnows Agent
bob) -- Sum: I knew that you didn't know the numbers.
sapForm2 :: Form
sapForm2 = Agent -> Form
sapKnows Agent
bob   -- Product: Now I know the two numbers
sapForm3 :: Form
sapForm3 = Agent -> Form
sapKnows Agent
alice -- Sum: Now I know the two numbers too

sapProtocol :: Form
sapProtocol :: Form
sapProtocol = [Form] -> Form
Conj [ Form
sapForm1
                   , Form -> Form -> Form
PubAnnounce Form
sapForm1 Form
sapForm2
                   , Form -> Form -> Form
PubAnnounce Form
sapForm1 (Form -> Form -> Form
PubAnnounce Form
sapForm2 Form
sapForm3) ]

sapSolutions :: [[Prp]]
sapSolutions :: [[Prp]]
sapSolutions = KnowStruct -> Form -> [[Prp]]
whereViaBdd KnowStruct
sapKnStruct Form
sapProtocol

sapExplainState :: [Prp] -> String
sapExplainState :: [Prp] -> Agent
sapExplainState [Prp]
truths = [Agent] -> Agent
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
  [ Agent
"x = ", [Prp] -> Agent
explain [Prp]
xProps
  , Agent
", y = ", [Prp] -> Agent
explain [Prp]
yProps
  , Agent
", x+y = ", [Prp] -> Agent
explain [Prp]
sProps
  , Agent
" and x*y = ", [Prp] -> Agent
explain [Prp]
pProps ] where
  explain :: [Prp] -> Agent
explain = Int -> Agent
forall a. Show a => a -> Agent
show (Int -> Agent) -> ([Prp] -> Int) -> [Prp] -> Agent
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Prp] -> [Prp] -> Int
nmbr [Prp]
truths

nmbr :: [Prp] -> [Prp] -> Int
nmbr :: [Prp] -> [Prp] -> Int
nmbr [Prp]
truths [Prp]
varProps = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe (Agent -> Int
forall a. HasCallStack => Agent -> a
error Agent
"Value not found") (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$
  [Prp] -> [[Prp]] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
elemIndex ([Prp]
varProps [Prp] -> [Prp] -> [Prp]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` [Prp]
truths) ([Prp] -> [[Prp]]
forall a. [a] -> [[a]]
powerset [Prp]
varProps)