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

module SMCDEL.Examples.WhatSum where

import SMCDEL.Examples.SumAndProduct (nmbr)
import SMCDEL.Language
import SMCDEL.Internal.Help
import SMCDEL.Symbolic.S5

wsBound :: Int
wsBound :: Int
wsBound = Int
50

wsTriples :: [ (Int,Int,Int) ]
wsTriples :: [(Int, Int, Int)]
wsTriples = ((Int, Int, Int) -> Bool) -> [(Int, Int, Int)] -> [(Int, Int, Int)]
forall a. (a -> Bool) -> [a] -> [a]
filter
  ( \(Int
x,Int
y,Int
z) -> Int
xInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
yInt -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==Int
z Bool -> Bool -> Bool
|| Int
xInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
zInt -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==Int
y Bool -> Bool -> Bool
|| Int
yInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
zInt -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==Int
x )
  [ (Int
x,Int
y,Int
z) | Int
x <- [Int
1..Int
wsBound], Int
y <- [Int
1..Int
wsBound], Int
z <- [Int
1..Int
wsBound] ]

aProps,bProps,cProps :: [Prp]
([Prp]
aProps,[Prp]
bProps,[Prp]
cProps) = ([(Int -> Prp
P Int
1)..(Int -> Prp
P Int
k)],[(Int -> Prp
P (Int -> Prp) -> Int -> Prp
forall a b. (a -> b) -> a -> b
$ Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)..(Int -> Prp
P Int
l)],[(Int -> Prp
P (Int -> Prp) -> Int -> Prp
forall a b. (a -> b) -> a -> b
$ Int
lInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)..(Int -> Prp
P Int
m)]) where
  [Int
k,Int
l,Int
m] = (Int -> Int) -> [Int] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int
wsAmountInt -> Int -> Int
forall a. Num a => a -> a -> a
*) [Int
1,Int
2,Int
3]
  wsAmount :: Int
wsAmount = Double -> Int
forall b. Integral b => Double -> b
forall a b. (RealFrac a, Integral b) => a -> b
ceiling (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
wsBound) :: Double)

aIs, bIs, cIs :: Int -> Form
aIs :: Int -> Form
aIs Int
n = [Prp] -> [Prp] -> Form
booloutofForm ([Prp] -> [[Prp]]
forall a. [a] -> [[a]]
powerset [Prp]
aProps [[Prp]] -> Int -> [Prp]
forall a. HasCallStack => [a] -> Int -> a
!! Int
n) [Prp]
aProps
bIs :: Int -> Form
bIs Int
n = [Prp] -> [Prp] -> Form
booloutofForm ([Prp] -> [[Prp]]
forall a. [a] -> [[a]]
powerset [Prp]
bProps [[Prp]] -> Int -> [Prp]
forall a. HasCallStack => [a] -> Int -> a
!! Int
n) [Prp]
bProps
cIs :: Int -> Form
cIs Int
n = [Prp] -> [Prp] -> Form
booloutofForm ([Prp] -> [[Prp]]
forall a. [a] -> [[a]]
powerset [Prp]
cProps [[Prp]] -> Int -> [Prp]
forall a. HasCallStack => [a] -> Int -> a
!! Int
n) [Prp]
cProps

wsKnStruct :: KnowStruct
wsKnStruct :: KnowStruct
wsKnStruct = [Prp] -> Bdd -> [(Agent, [Prp])] -> KnowStruct
KnS [Prp]
wsAllProps Bdd
law [(Agent, [Prp])]
obs where
  wsAllProps :: [Prp]
wsAllProps = [Prp]
aProps[Prp] -> [Prp] -> [Prp]
forall a. [a] -> [a] -> [a]
++[Prp]
bProps[Prp] -> [Prp] -> [Prp]
forall a. [a] -> [a] -> [a]
++[Prp]
cProps
  law :: Bdd
law = Form -> Bdd
boolBddOf (Form -> Bdd) -> Form -> Bdd
forall a b. (a -> b) -> a -> b
$ [Form] -> Form
Disj [ [Form] -> Form
Conj [ Int -> Form
aIs Int
x, Int -> Form
bIs Int
y, Int -> Form
cIs Int
z ] | (Int
x,Int
y,Int
z) <- [(Int, Int, Int)]
wsTriples ]
  obs :: [(Agent, [Prp])]
obs = [ (Agent
alice, [Prp]
bProps[Prp] -> [Prp] -> [Prp]
forall a. [a] -> [a] -> [a]
++[Prp]
cProps), (Agent
bob, [Prp]
aProps[Prp] -> [Prp] -> [Prp]
forall a. [a] -> [a] -> [a]
++[Prp]
cProps), (Agent
carol, [Prp]
aProps[Prp] -> [Prp] -> [Prp]
forall a. [a] -> [a] -> [a]
++[Prp]
bProps) ]

wsKnowSelfA,wsKnowSelfB,wsKnowSelfC :: Form
wsKnowSelfA :: Form
wsKnowSelfA = [Form] -> Form
Disj [ Agent -> Form -> Form
K Agent
alice (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Int -> Form
aIs Int
x | Int
x <- [Int
1..Int
wsBound] ]
wsKnowSelfB :: Form
wsKnowSelfB = [Form] -> Form
Disj [ Agent -> Form -> Form
K Agent
bob   (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Int -> Form
bIs Int
x | Int
x <- [Int
1..Int
wsBound] ]
wsKnowSelfC :: Form
wsKnowSelfC = [Form] -> Form
Disj [ Agent -> Form -> Form
K Agent
carol (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Int -> Form
cIs Int
x | Int
x <- [Int
1..Int
wsBound] ]

wsResult :: KnowStruct
wsResult :: KnowStruct
wsResult = (KnowStruct -> Form -> KnowStruct)
-> KnowStruct -> [Form] -> KnowStruct
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl KnowStruct -> Form -> KnowStruct
forall a b. Update a b => a -> b -> a
update KnowStruct
wsKnStruct [ Form -> Form
Neg Form
wsKnowSelfA, Form -> Form
Neg Form
wsKnowSelfB, Form -> Form
Neg Form
wsKnowSelfC ]

wsSolutions :: [State]
wsSolutions :: [[Prp]]
wsSolutions = KnowStruct -> [[Prp]]
statesOf KnowStruct
wsResult

wsExplainState :: [Prp] -> [(Char,Int)]
wsExplainState :: [Prp] -> [(Char, Int)]
wsExplainState [Prp]
truths =
  [ (Char
'a', [Prp] -> Int
explain [Prp]
aProps), (Char
'b', [Prp] -> Int
explain [Prp]
bProps), (Char
'c', [Prp] -> Int
explain [Prp]
cProps) ] where
    explain :: [Prp] -> Int
explain = [Prp] -> [Prp] -> Int
nmbr [Prp]
truths