{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses #-}
module SMCDEL.Language where
import Data.List (nub,intercalate,(\\))
import Data.Dynamic
import Data.Maybe (fromMaybe)
import Test.QuickCheck
import SMCDEL.Internal.Help (powerset)
import SMCDEL.Internal.TexDisplay
newtype Prp = P Int deriving (Prp -> Prp -> Bool
(Prp -> Prp -> Bool) -> (Prp -> Prp -> Bool) -> Eq Prp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Prp -> Prp -> Bool
== :: Prp -> Prp -> Bool
$c/= :: Prp -> Prp -> Bool
/= :: Prp -> Prp -> Bool
Eq,Eq Prp
Eq Prp =>
(Prp -> Prp -> Ordering)
-> (Prp -> Prp -> Bool)
-> (Prp -> Prp -> Bool)
-> (Prp -> Prp -> Bool)
-> (Prp -> Prp -> Bool)
-> (Prp -> Prp -> Prp)
-> (Prp -> Prp -> Prp)
-> Ord Prp
Prp -> Prp -> Bool
Prp -> Prp -> Ordering
Prp -> Prp -> Prp
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 :: Prp -> Prp -> Ordering
compare :: Prp -> Prp -> Ordering
$c< :: Prp -> Prp -> Bool
< :: Prp -> Prp -> Bool
$c<= :: Prp -> Prp -> Bool
<= :: Prp -> Prp -> Bool
$c> :: Prp -> Prp -> Bool
> :: Prp -> Prp -> Bool
$c>= :: Prp -> Prp -> Bool
>= :: Prp -> Prp -> Bool
$cmax :: Prp -> Prp -> Prp
max :: Prp -> Prp -> Prp
$cmin :: Prp -> Prp -> Prp
min :: Prp -> Prp -> Prp
Ord,Int -> Prp -> ShowS
[Prp] -> ShowS
Prp -> Agent
(Int -> Prp -> ShowS)
-> (Prp -> Agent) -> ([Prp] -> ShowS) -> Show Prp
forall a.
(Int -> a -> ShowS) -> (a -> Agent) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Prp -> ShowS
showsPrec :: Int -> Prp -> ShowS
$cshow :: Prp -> Agent
show :: Prp -> Agent
$cshowList :: [Prp] -> ShowS
showList :: [Prp] -> ShowS
Show)
instance Enum Prp where
toEnum :: Int -> Prp
toEnum = Int -> Prp
P
fromEnum :: Prp -> Int
fromEnum (P Int
n) = Int
n
defaultVocabulary :: [Prp]
defaultVocabulary :: [Prp]
defaultVocabulary = (Int -> Prp) -> [Int] -> [Prp]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Prp
P [Int
0..Int
4]
instance Arbitrary Prp where
arbitrary :: Gen Prp
arbitrary = [Prp] -> Gen Prp
forall a. [a] -> Gen a
elements [Prp]
defaultVocabulary
freshp :: [Prp] -> Prp
freshp :: [Prp] -> Prp
freshp [] = Int -> Prp
P Int
1
freshp [Prp]
prps = Int -> Prp
P ([Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ((Prp -> Int) -> [Prp] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Prp -> Int
forall a. Enum a => a -> Int
fromEnum [Prp]
prps) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
class HasVocab a where
vocabOf :: a -> [Prp]
type Agent = String
alice,bob,carol :: Agent
alice :: Agent
alice = Agent
"Alice"
bob :: Agent
bob = Agent
"Bob"
carol :: Agent
carol = Agent
"Carol"
defaultAgents :: [Agent]
defaultAgents :: [Agent]
defaultAgents = (Integer -> Agent) -> [Integer] -> [Agent]
forall a b. (a -> b) -> [a] -> [b]
map Integer -> Agent
forall a. Show a => a -> Agent
show [(Integer
1::Integer)..Integer
5]
newtype AgAgent = Ag Agent deriving (AgAgent -> AgAgent -> Bool
(AgAgent -> AgAgent -> Bool)
-> (AgAgent -> AgAgent -> Bool) -> Eq AgAgent
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: AgAgent -> AgAgent -> Bool
== :: AgAgent -> AgAgent -> Bool
$c/= :: AgAgent -> AgAgent -> Bool
/= :: AgAgent -> AgAgent -> Bool
Eq,Eq AgAgent
Eq AgAgent =>
(AgAgent -> AgAgent -> Ordering)
-> (AgAgent -> AgAgent -> Bool)
-> (AgAgent -> AgAgent -> Bool)
-> (AgAgent -> AgAgent -> Bool)
-> (AgAgent -> AgAgent -> Bool)
-> (AgAgent -> AgAgent -> AgAgent)
-> (AgAgent -> AgAgent -> AgAgent)
-> Ord AgAgent
AgAgent -> AgAgent -> Bool
AgAgent -> AgAgent -> Ordering
AgAgent -> AgAgent -> AgAgent
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 :: AgAgent -> AgAgent -> Ordering
compare :: AgAgent -> AgAgent -> Ordering
$c< :: AgAgent -> AgAgent -> Bool
< :: AgAgent -> AgAgent -> Bool
$c<= :: AgAgent -> AgAgent -> Bool
<= :: AgAgent -> AgAgent -> Bool
$c> :: AgAgent -> AgAgent -> Bool
> :: AgAgent -> AgAgent -> Bool
$c>= :: AgAgent -> AgAgent -> Bool
>= :: AgAgent -> AgAgent -> Bool
$cmax :: AgAgent -> AgAgent -> AgAgent
max :: AgAgent -> AgAgent -> AgAgent
$cmin :: AgAgent -> AgAgent -> AgAgent
min :: AgAgent -> AgAgent -> AgAgent
Ord,Int -> AgAgent -> ShowS
[AgAgent] -> ShowS
AgAgent -> Agent
(Int -> AgAgent -> ShowS)
-> (AgAgent -> Agent) -> ([AgAgent] -> ShowS) -> Show AgAgent
forall a.
(Int -> a -> ShowS) -> (a -> Agent) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> AgAgent -> ShowS
showsPrec :: Int -> AgAgent -> ShowS
$cshow :: AgAgent -> Agent
show :: AgAgent -> Agent
$cshowList :: [AgAgent] -> ShowS
showList :: [AgAgent] -> ShowS
Show)
instance Arbitrary AgAgent where
arbitrary :: Gen AgAgent
arbitrary = [AgAgent] -> Gen AgAgent
forall a. [a] -> Gen a
elements ([AgAgent] -> Gen AgAgent) -> [AgAgent] -> Gen AgAgent
forall a b. (a -> b) -> a -> b
$ (Agent -> AgAgent) -> [Agent] -> [AgAgent]
forall a b. (a -> b) -> [a] -> [b]
map Agent -> AgAgent
Ag [Agent]
defaultAgents
newtype Group = Group [Agent] deriving (Group -> Group -> Bool
(Group -> Group -> Bool) -> (Group -> Group -> Bool) -> Eq Group
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Group -> Group -> Bool
== :: Group -> Group -> Bool
$c/= :: Group -> Group -> Bool
/= :: Group -> Group -> Bool
Eq,Eq Group
Eq Group =>
(Group -> Group -> Ordering)
-> (Group -> Group -> Bool)
-> (Group -> Group -> Bool)
-> (Group -> Group -> Bool)
-> (Group -> Group -> Bool)
-> (Group -> Group -> Group)
-> (Group -> Group -> Group)
-> Ord Group
Group -> Group -> Bool
Group -> Group -> Ordering
Group -> Group -> Group
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 :: Group -> Group -> Ordering
compare :: Group -> Group -> Ordering
$c< :: Group -> Group -> Bool
< :: Group -> Group -> Bool
$c<= :: Group -> Group -> Bool
<= :: Group -> Group -> Bool
$c> :: Group -> Group -> Bool
> :: Group -> Group -> Bool
$c>= :: Group -> Group -> Bool
>= :: Group -> Group -> Bool
$cmax :: Group -> Group -> Group
max :: Group -> Group -> Group
$cmin :: Group -> Group -> Group
min :: Group -> Group -> Group
Ord,Int -> Group -> ShowS
[Group] -> ShowS
Group -> Agent
(Int -> Group -> ShowS)
-> (Group -> Agent) -> ([Group] -> ShowS) -> Show Group
forall a.
(Int -> a -> ShowS) -> (a -> Agent) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Group -> ShowS
showsPrec :: Int -> Group -> ShowS
$cshow :: Group -> Agent
show :: Group -> Agent
$cshowList :: [Group] -> ShowS
showList :: [Group] -> ShowS
Show)
instance Arbitrary Group where
arbitrary :: Gen Group
arbitrary = ([Agent] -> Group) -> Gen [Agent] -> Gen Group
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Agent] -> Group
Group([Agent] -> Group) -> ([Agent] -> [Agent]) -> [Agent] -> Group
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Agent
"1"Agent -> [Agent] -> [Agent]
forall a. a -> [a] -> [a]
:)) (Gen [Agent] -> Gen Group) -> Gen [Agent] -> Gen Group
forall a b. (a -> b) -> a -> b
$ [Agent] -> Gen [Agent]
forall a. [a] -> Gen [a]
sublistOf ([Agent] -> Gen [Agent]) -> [Agent] -> Gen [Agent]
forall a b. (a -> b) -> a -> b
$ [Agent]
defaultAgents [Agent] -> [Agent] -> [Agent]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Agent
"1"]
data Form
= Top
| Bot
| PrpF Prp
| Neg Form
| Conj [Form]
| Disj [Form]
| Xor [Form]
| Impl Form Form
| Equi Form Form
| Forall [Prp] Form
| Exists [Prp] Form
| K Agent Form
| Ck [Agent] Form
| Dk [Agent] Form
| Kw Agent Form
| Ckw [Agent] Form
| Dkw [Agent] Form
| PubAnnounce Form Form
| PubAnnounceW Form Form
| Announce [Agent] Form Form
| AnnounceW [Agent] Form Form
| Dia DynamicOp Form
deriving (Form -> Form -> Bool
(Form -> Form -> Bool) -> (Form -> Form -> Bool) -> Eq Form
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Form -> Form -> Bool
== :: Form -> Form -> Bool
$c/= :: Form -> Form -> Bool
/= :: Form -> Form -> Bool
Eq,Eq Form
Eq Form =>
(Form -> Form -> Ordering)
-> (Form -> Form -> Bool)
-> (Form -> Form -> Bool)
-> (Form -> Form -> Bool)
-> (Form -> Form -> Bool)
-> (Form -> Form -> Form)
-> (Form -> Form -> Form)
-> Ord Form
Form -> Form -> Bool
Form -> Form -> Ordering
Form -> Form -> Form
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 :: Form -> Form -> Ordering
compare :: Form -> Form -> Ordering
$c< :: Form -> Form -> Bool
< :: Form -> Form -> Bool
$c<= :: Form -> Form -> Bool
<= :: Form -> Form -> Bool
$c> :: Form -> Form -> Bool
> :: Form -> Form -> Bool
$c>= :: Form -> Form -> Bool
>= :: Form -> Form -> Bool
$cmax :: Form -> Form -> Form
max :: Form -> Form -> Form
$cmin :: Form -> Form -> Form
min :: Form -> Form -> Form
Ord,Int -> Form -> ShowS
[Form] -> ShowS
Form -> Agent
(Int -> Form -> ShowS)
-> (Form -> Agent) -> ([Form] -> ShowS) -> Show Form
forall a.
(Int -> a -> ShowS) -> (a -> Agent) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Form -> ShowS
showsPrec :: Int -> Form -> ShowS
$cshow :: Form -> Agent
show :: Form -> Agent
$cshowList :: [Form] -> ShowS
showList :: [Form] -> ShowS
Show)
ite :: Form -> Form -> Form -> Form
ite :: Form -> Form -> Form -> Form
ite Form
f Form
g Form
h = [Form] -> Form
Conj [Form
f Form -> Form -> Form
`Impl` Form
g, Form -> Form
Neg Form
f Form -> Form -> Form
`Impl` Form
h]
pubAnnounceStack :: [Form] -> Form -> Form
pubAnnounceStack :: [Form] -> Form -> Form
pubAnnounceStack = (Form -> [Form] -> Form) -> [Form] -> Form -> Form
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Form -> [Form] -> Form) -> [Form] -> Form -> Form)
-> (Form -> [Form] -> Form) -> [Form] -> Form -> Form
forall a b. (a -> b) -> a -> b
$ (Form -> Form -> Form) -> Form -> [Form] -> Form
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Form -> Form -> Form
PubAnnounce
pubAnnounceWhetherStack :: [Form] -> Form -> Form
pubAnnounceWhetherStack :: [Form] -> Form -> Form
pubAnnounceWhetherStack = (Form -> [Form] -> Form) -> [Form] -> Form -> Form
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Form -> [Form] -> Form) -> [Form] -> Form -> Form)
-> (Form -> [Form] -> Form) -> [Form] -> Form -> Form
forall a b. (a -> b) -> a -> b
$ (Form -> Form -> Form) -> Form -> [Form] -> Form
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Form -> Form -> Form
PubAnnounceW
booloutofForm :: [Prp] -> [Prp] -> Form
booloutofForm :: [Prp] -> [Prp] -> Form
booloutofForm [Prp]
ps [Prp]
qs = [Form] -> Form
Conj ([Form] -> Form) -> [Form] -> Form
forall a b. (a -> b) -> a -> b
$ [ Prp -> Form
PrpF Prp
p | Prp
p <- [Prp]
ps ] [Form] -> [Form] -> [Form]
forall a. [a] -> [a] -> [a]
++ [ Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Prp -> Form
PrpF Prp
r | Prp
r <- [Prp]
qs [Prp] -> [Prp] -> [Prp]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Prp]
ps ]
oneOf :: [Form] -> Form
oneOf :: [Form] -> Form
oneOf [Form]
fs = [Form] -> Form
Conj [ [Form] -> Form
Disj [Form]
fs, [Form] -> Form
Conj [ Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ [Form] -> Form
Conj [Form
f1, Form
f2] | Form
f1 <- [Form]
fs, Form
f2 <- [Form]
fs [Form] -> [Form] -> [Form]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Form
f1] ] ]
data DynamicOp = Dyn !String !Dynamic
instance Eq DynamicOp where
Dyn Agent
a Dynamic
_ == :: DynamicOp -> DynamicOp -> Bool
== Dyn Agent
b Dynamic
_ = Agent
a Agent -> Agent -> Bool
forall a. Eq a => a -> a -> Bool
== Agent
b
instance Ord DynamicOp where
compare :: DynamicOp -> DynamicOp -> Ordering
compare (Dyn Agent
a Dynamic
_) (Dyn Agent
b Dynamic
_) = Agent -> Agent -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Agent
a Agent
b
instance Show DynamicOp where
show :: DynamicOp -> Agent
show (Dyn Agent
a Dynamic
_) = Agent
"Dyn " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> Agent
show Agent
a Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
" _"
box :: DynamicOp -> Form -> Form
box :: DynamicOp -> Form -> Form
box DynamicOp
op Form
f = Form -> Form
Neg (DynamicOp -> Form -> Form
Dia DynamicOp
op (Form -> Form
Neg Form
f))
class HasAgents a where
agentsOf :: a -> [Agent]
class Pointed a b
instance (HasVocab a, Pointed a b) => HasVocab (a,b) where vocabOf :: (a, b) -> [Prp]
vocabOf = a -> [Prp]
forall a. HasVocab a => a -> [Prp]
vocabOf (a -> [Prp]) -> ((a, b) -> a) -> (a, b) -> [Prp]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, b) -> a
forall a b. (a, b) -> a
fst
instance (HasAgents a, Pointed a b) => HasAgents (a,b) where agentsOf :: (a, b) -> [Agent]
agentsOf = a -> [Agent]
forall a. HasAgents a => a -> [Agent]
agentsOf (a -> [Agent]) -> ((a, b) -> a) -> (a, b) -> [Agent]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, b) -> a
forall a b. (a, b) -> a
fst
class HasVocab a => Semantics a where
isTrue :: a -> Form -> Bool
(|=) :: Semantics a => a -> Form -> Bool
|= :: forall a. Semantics a => a -> Form -> Bool
(|=) = a -> Form -> Bool
forall a. Semantics a => a -> Form -> Bool
isTrue
class Optimizable a where
optimize :: [Prp] -> a -> a
class HasPrecondition a where
preOf :: a -> Form
instance HasPrecondition Form where
preOf :: Form -> Form
preOf = Form -> Form
forall a. a -> a
id
class (Show a, Show b, HasAgents a, Semantics a, HasPrecondition b) => Update a b where
{-# MINIMAL unsafeUpdate #-}
unsafeUpdate :: a -> b -> a
checks :: [a -> b -> Bool]
checks = [a -> b -> Bool
forall a b. Update a b => a -> b -> Bool
preCheck]
preCheck :: a -> b -> Bool
preCheck a
x b
y = a -> Form -> Bool
forall a. Semantics a => a -> Form -> Bool
isTrue a
x (b -> Form
forall a. HasPrecondition a => a -> Form
preOf b
y)
update :: a -> b -> a
update a
x b
y = if [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
checkResults
then a -> b -> a
forall a b. Update a b => a -> b -> a
unsafeUpdate a
x b
y
else Agent -> a
forall a. HasCallStack => Agent -> a
error (Agent -> a) -> ([Agent] -> Agent) -> [Agent] -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Agent] -> Agent
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([Agent] -> a) -> [Agent] -> a
forall a b. (a -> b) -> a -> b
$
[ Agent
"Update failed."
, Agent
"\n x = ", a -> Agent
forall a. Show a => a -> Agent
show a
x
, Agent
"\n y = ", b -> Agent
forall a. Show a => a -> Agent
show b
y
, Agent
"\n preOf y = ", Form -> Agent
forall a. Show a => a -> Agent
show (b -> Form
forall a. HasPrecondition a => a -> Form
preOf b
y)
, Agent
"\n preCheck y = ", Bool -> Agent
forall a. Show a => a -> Agent
show (a -> b -> Bool
forall a b. Update a b => a -> b -> Bool
preCheck a
x b
y)
, Agent
"\n checkResults: ", [Bool] -> Agent
forall a. Show a => a -> Agent
show [Bool]
checkResults ]
where checkResults :: [Bool]
checkResults = [ a -> b -> Bool
c a
x b
y | a -> b -> Bool
c <- [a -> b -> Bool]
forall a b. Update a b => [a -> b -> Bool]
checks ]
updates :: Update a b => a -> [b] -> a
updates :: forall a b. Update a b => a -> [b] -> a
updates = (a -> b -> a) -> a -> [b] -> a
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl a -> b -> a
forall a b. Update a b => a -> b -> a
update
updateSequence :: Update a b => a -> [b] -> [a]
updateSequence :: forall a b. Update a b => a -> [b] -> [a]
updateSequence a
x [] = [a
x]
updateSequence a
x (b
y:[b]
ys) = let next :: a
next = a
x a -> b -> a
forall a b. Update a b => a -> b -> a
`update` b
y in a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: a -> [b] -> [a]
forall a b. Update a b => a -> [b] -> [a]
updateSequence a
next [b]
ys
haveSameAgents :: (HasAgents a, HasAgents b) => a -> b -> Bool
haveSameAgents :: forall a b. (HasAgents a, HasAgents b) => a -> b -> Bool
haveSameAgents a
x b
y = a -> [Agent]
forall a. HasAgents a => a -> [Agent]
agentsOf a
x [Agent] -> [Agent] -> Bool
forall a. Eq a => a -> a -> Bool
== b -> [Agent]
forall a. HasAgents a => a -> [Agent]
agentsOf b
y
showSet :: Show a => [a] -> String
showSet :: forall a. Show a => [a] -> Agent
showSet [a]
xs = Agent -> [Agent] -> Agent
forall a. [a] -> [[a]] -> [a]
intercalate Agent
"," ((a -> Agent) -> [a] -> [Agent]
forall a b. (a -> b) -> [a] -> [b]
map a -> Agent
forall a. Show a => a -> Agent
show [a]
xs)
ppForm :: Form -> String
ppForm :: Form -> Agent
ppForm = (Prp -> Agent) -> Form -> Agent
ppFormWith (\(P Int
n) -> Int -> Agent
forall a. Show a => a -> Agent
show Int
n)
ppFormWith :: (Prp -> String)-> Form -> String
ppFormWith :: (Prp -> Agent) -> Form -> Agent
ppFormWith Prp -> Agent
_ Form
Top = Agent
"T"
ppFormWith Prp -> Agent
_ Form
Bot = Agent
"F"
ppFormWith Prp -> Agent
trans (PrpF Prp
p) = Prp -> Agent
trans Prp
p
ppFormWith Prp -> Agent
trans (Neg Form
f) = Agent
"~" Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ (Prp -> Agent) -> Form -> Agent
ppFormWith Prp -> Agent
trans Form
f
ppFormWith Prp -> Agent
trans (Conj [Form]
fs) = Agent
"(" Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent -> [Agent] -> Agent
forall a. [a] -> [[a]] -> [a]
intercalate Agent
" & " ((Form -> Agent) -> [Form] -> [Agent]
forall a b. (a -> b) -> [a] -> [b]
map ((Prp -> Agent) -> Form -> Agent
ppFormWith Prp -> Agent
trans) [Form]
fs) Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
")"
ppFormWith Prp -> Agent
trans (Disj [Form]
fs) = Agent
"(" Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent -> [Agent] -> Agent
forall a. [a] -> [[a]] -> [a]
intercalate Agent
" | " ((Form -> Agent) -> [Form] -> [Agent]
forall a b. (a -> b) -> [a] -> [b]
map ((Prp -> Agent) -> Form -> Agent
ppFormWith Prp -> Agent
trans) [Form]
fs) Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
")"
ppFormWith Prp -> Agent
trans (Xor [Form]
fs) = Agent
"XOR{" Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ [Agent] -> Agent
forall a. Show a => [a] -> Agent
showSet ((Form -> Agent) -> [Form] -> [Agent]
forall a b. (a -> b) -> [a] -> [b]
map ((Prp -> Agent) -> Form -> Agent
ppFormWith Prp -> Agent
trans) [Form]
fs) Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
"}"
ppFormWith Prp -> Agent
trans (Impl Form
f Form
g) = Agent
"(" Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ (Prp -> Agent) -> Form -> Agent
ppFormWith Prp -> Agent
trans Form
f Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
"->" Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ (Prp -> Agent) -> Form -> Agent
ppFormWith Prp -> Agent
trans Form
g Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
")"
ppFormWith Prp -> Agent
trans (Equi Form
f Form
g) = (Prp -> Agent) -> Form -> Agent
ppFormWith Prp -> Agent
trans Form
f Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
"=" Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ (Prp -> Agent) -> Form -> Agent
ppFormWith Prp -> Agent
trans Form
g
ppFormWith Prp -> Agent
trans (Forall [Prp]
ps Form
f) = Agent
"Forall {" Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ [Prp] -> Agent
forall a. Show a => [a] -> Agent
showSet [Prp]
ps Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
"}: " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ (Prp -> Agent) -> Form -> Agent
ppFormWith Prp -> Agent
trans Form
f
ppFormWith Prp -> Agent
trans (Exists [Prp]
ps Form
f) = Agent
"Exists {" Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ [Prp] -> Agent
forall a. Show a => [a] -> Agent
showSet [Prp]
ps Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
"}: " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ (Prp -> Agent) -> Form -> Agent
ppFormWith Prp -> Agent
trans Form
f
ppFormWith Prp -> Agent
trans (K Agent
i Form
f) = Agent
"K " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
i Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
" " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ (Prp -> Agent) -> Form -> Agent
ppFormWith Prp -> Agent
trans Form
f
ppFormWith Prp -> Agent
trans (Ck [Agent]
is Form
f) = Agent
"Ck " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ [Agent] -> Agent
forall a. Show a => [a] -> Agent
showSet [Agent]
is Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
" " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ (Prp -> Agent) -> Form -> Agent
ppFormWith Prp -> Agent
trans Form
f
ppFormWith Prp -> Agent
trans (Dk [Agent]
is Form
f) = Agent
"Dk " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ [Agent] -> Agent
forall a. Show a => [a] -> Agent
showSet [Agent]
is Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
" " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ (Prp -> Agent) -> Form -> Agent
ppFormWith Prp -> Agent
trans Form
f
ppFormWith Prp -> Agent
trans (Kw Agent
i Form
f) = Agent
"Kw " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
i Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
" " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ (Prp -> Agent) -> Form -> Agent
ppFormWith Prp -> Agent
trans Form
f
ppFormWith Prp -> Agent
trans (Ckw [Agent]
is Form
f) = Agent
"Ckw " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ [Agent] -> Agent
forall a. Show a => [a] -> Agent
showSet [Agent]
is Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
" " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ (Prp -> Agent) -> Form -> Agent
ppFormWith Prp -> Agent
trans Form
f
ppFormWith Prp -> Agent
trans (Dkw [Agent]
is Form
f) = Agent
"Dkw " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ [Agent] -> Agent
forall a. Show a => [a] -> Agent
showSet [Agent]
is Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
" " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ (Prp -> Agent) -> Form -> Agent
ppFormWith Prp -> Agent
trans Form
f
ppFormWith Prp -> Agent
trans (PubAnnounce Form
f Form
g) = Agent
"[! " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ (Prp -> Agent) -> Form -> Agent
ppFormWith Prp -> Agent
trans Form
f Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
"] " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ (Prp -> Agent) -> Form -> Agent
ppFormWith Prp -> Agent
trans Form
g
ppFormWith Prp -> Agent
trans (PubAnnounceW Form
f Form
g) = Agent
"[?! " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ (Prp -> Agent) -> Form -> Agent
ppFormWith Prp -> Agent
trans Form
f Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
"] " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ (Prp -> Agent) -> Form -> Agent
ppFormWith Prp -> Agent
trans Form
g
ppFormWith Prp -> Agent
trans (Announce [Agent]
is Form
f Form
g) = Agent
"[" Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent -> [Agent] -> Agent
forall a. [a] -> [[a]] -> [a]
intercalate Agent
", " [Agent]
is Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
" ! " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ (Prp -> Agent) -> Form -> Agent
ppFormWith Prp -> Agent
trans Form
f Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
"]" Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ (Prp -> Agent) -> Form -> Agent
ppFormWith Prp -> Agent
trans Form
g
ppFormWith Prp -> Agent
trans (AnnounceW [Agent]
is Form
f Form
g) = Agent
"[" Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent -> [Agent] -> Agent
forall a. [a] -> [[a]] -> [a]
intercalate Agent
", " [Agent]
is Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
" ?! " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ (Prp -> Agent) -> Form -> Agent
ppFormWith Prp -> Agent
trans Form
f Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
"]" Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ (Prp -> Agent) -> Form -> Agent
ppFormWith Prp -> Agent
trans Form
g
ppFormWith Prp -> Agent
trans (Dia (Dyn Agent
s Dynamic
_) Form
f) = Agent
"<" Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
s Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
">" Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ (Prp -> Agent) -> Form -> Agent
ppFormWith Prp -> Agent
trans Form
f
texForm :: Form -> String
texForm :: Form -> Agent
texForm Form
Top = Agent
"\\top "
texForm Form
Bot = Agent
"\\bot "
texForm (PrpF Prp
p) = Prp -> Agent
forall a. TexAble a => a -> Agent
tex Prp
p
texForm (Neg (PubAnnounce Form
f (Neg Form
g))) = Agent
"\\langle !" Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Form -> Agent
texForm Form
f Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
" \\rangle " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Form -> Agent
texForm Form
g
texForm (Neg Form
f) = Agent
"\\lnot " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Form -> Agent
texForm Form
f
texForm (Conj []) = Agent
"\\top "
texForm (Conj [Form
f]) = Form -> Agent
texForm Form
f
texForm (Conj [Form
f,Form
g]) = Agent
" ( " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Form -> Agent
texForm Form
f Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
" \\land " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Form -> Agent
texForm Form
g Agent -> ShowS
forall a. [a] -> [a] -> [a]
++Agent
" ) "
texForm (Conj [Form]
fs) = Agent
"\\bigwedge \\{\n" Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent -> [Agent] -> Agent
forall a. [a] -> [[a]] -> [a]
intercalate Agent
"," ((Form -> Agent) -> [Form] -> [Agent]
forall a b. (a -> b) -> [a] -> [b]
map Form -> Agent
texForm [Form]
fs) Agent -> ShowS
forall a. [a] -> [a] -> [a]
++Agent
" \\} "
texForm (Disj []) = Agent
"\\bot "
texForm (Disj [Form
f]) = Form -> Agent
texForm Form
f
texForm (Disj [Form
f,Form
g]) = Agent
" ( " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Form -> Agent
texForm Form
f Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
" \\lor "Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Form -> Agent
texForm Form
g Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
" ) "
texForm (Disj [Form]
fs) = Agent
"\\bigvee \\{\n " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent -> [Agent] -> Agent
forall a. [a] -> [[a]] -> [a]
intercalate Agent
"," ((Form -> Agent) -> [Form] -> [Agent]
forall a b. (a -> b) -> [a] -> [b]
map Form -> Agent
texForm [Form]
fs) Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
" \\} "
texForm (Xor []) = Agent
"\\bot "
texForm (Xor [Form
f]) = Form -> Agent
texForm Form
f
texForm (Xor [Form
f,Form
g]) = Agent
" ( " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Form -> Agent
texForm Form
f Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
" \\oplus " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Form -> Agent
texForm Form
g Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
" ) "
texForm (Xor [Form]
fs) = Agent
"\\bigoplus \\{\n" Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent -> [Agent] -> Agent
forall a. [a] -> [[a]] -> [a]
intercalate Agent
"," ((Form -> Agent) -> [Form] -> [Agent]
forall a b. (a -> b) -> [a] -> [b]
map Form -> Agent
texForm [Form]
fs) Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
" \\} "
texForm (Equi Form
f Form
g) = Agent
" ( "Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Form -> Agent
texForm Form
f Agent -> ShowS
forall a. [a] -> [a] -> [a]
++Agent
" \\leftrightarrow "Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Form -> Agent
texForm Form
g Agent -> ShowS
forall a. [a] -> [a] -> [a]
++Agent
" ) "
texForm (Impl Form
f Form
g) = Agent
" ( "Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Form -> Agent
texForm Form
f Agent -> ShowS
forall a. [a] -> [a] -> [a]
++Agent
" \\rightarrow "Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Form -> Agent
texForm Form
g Agent -> ShowS
forall a. [a] -> [a] -> [a]
++Agent
" ) "
texForm (Forall [Prp]
ps Form
f) = Agent
" \\forall " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ [Prp] -> Agent
forall a. TexAble a => a -> Agent
tex [Prp]
ps Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
" " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Form -> Agent
texForm Form
f
texForm (Exists [Prp]
ps Form
f) = Agent
" \\exists " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ [Prp] -> Agent
forall a. TexAble a => a -> Agent
tex [Prp]
ps Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
" " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Form -> Agent
texForm Form
f
texForm (K Agent
i Form
f) = Agent
"K_{\\text{" Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
i Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
"}} " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Form -> Agent
texForm Form
f
texForm (Kw Agent
i Form
f) = Agent
"K^?_{\\text{" Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
i Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
"}} " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Form -> Agent
texForm Form
f
texForm (Ck [Agent]
ags Form
f) = Agent
"Ck_{\\{\n" Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent -> [Agent] -> Agent
forall a. [a] -> [[a]] -> [a]
intercalate Agent
"," [Agent]
ags Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
"\n\\}} " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Form -> Agent
texForm Form
f
texForm (Dk [Agent]
ags Form
f) = Agent
"Dk_{\\{\n" Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent -> [Agent] -> Agent
forall a. [a] -> [[a]] -> [a]
intercalate Agent
"," [Agent]
ags Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
"\n\\}} " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Form -> Agent
texForm Form
f
texForm (Ckw [Agent]
ags Form
f) = Agent
"Ck^?_{\\{\n" Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent -> [Agent] -> Agent
forall a. [a] -> [[a]] -> [a]
intercalate Agent
"," [Agent]
ags Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
"\n\\}} " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Form -> Agent
texForm Form
f
texForm (Dkw [Agent]
ags Form
f) = Agent
"Dk^?_{\\{\n" Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent -> [Agent] -> Agent
forall a. [a] -> [[a]] -> [a]
intercalate Agent
"," [Agent]
ags Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
"\n\\}} " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Form -> Agent
texForm Form
f
texForm (PubAnnounce Form
f Form
g) = Agent
"[!" Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Form -> Agent
texForm Form
f Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
"] " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Form -> Agent
texForm Form
g
texForm (PubAnnounceW Form
f Form
g) = Agent
"[?!" Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Form -> Agent
texForm Form
f Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
"] " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Form -> Agent
texForm Form
g
texForm (Announce [Agent]
ags Form
f Form
g) = Agent
"[" Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent -> [Agent] -> Agent
forall a. [a] -> [[a]] -> [a]
intercalate Agent
"," [Agent]
ags Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
"!" Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Form -> Agent
texForm Form
f Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
"] " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Form -> Agent
texForm Form
g
texForm (AnnounceW [Agent]
ags Form
f Form
g) = Agent
"[" Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent -> [Agent] -> Agent
forall a. [a] -> [[a]] -> [a]
intercalate Agent
"," [Agent]
ags Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
"?!" Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Form -> Agent
texForm Form
f Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
"] " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Form -> Agent
texForm Form
g
texForm (Dia (Dyn Agent
s Dynamic
_) Form
f) = Agent
" \\langle " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
s Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
" \\rangle " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Form -> Agent
texForm Form
f
instance TexAble Prp where
tex :: Prp -> Agent
tex (P Int
0) = Agent
" p "
tex (P Int
n) = Agent
" p_{" Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Agent
forall a. Show a => a -> Agent
show Int
n Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
"} "
instance TexAble [Prp] where
tex :: [Prp] -> Agent
tex [] = Agent
" \\varnothing "
tex [Prp]
ps = Agent
"\\{" Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent -> [Agent] -> Agent
forall a. [a] -> [[a]] -> [a]
intercalate Agent
"," ((Prp -> Agent) -> [Prp] -> [Agent]
forall a b. (a -> b) -> [a] -> [b]
map Prp -> Agent
forall a. TexAble a => a -> Agent
tex [Prp]
ps) Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
"\\}"
instance TexAble Form where
tex :: Form -> Agent
tex = ShowS
removeDoubleSpaces ShowS -> (Form -> Agent) -> Form -> Agent
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Form -> Agent
texForm
subformulas :: Form -> [Form]
subformulas :: Form -> [Form]
subformulas Form
Top = [Form
Top]
subformulas Form
Bot = [Form
Bot]
subformulas (PrpF Prp
p) = [Prp -> Form
PrpF Prp
p]
subformulas (Neg Form
f) = Form -> Form
Neg Form
f Form -> [Form] -> [Form]
forall a. a -> [a] -> [a]
: Form -> [Form]
subformulas Form
f
subformulas (Conj [Form]
fs) = [Form] -> Form
Conj [Form]
fs Form -> [Form] -> [Form]
forall a. a -> [a] -> [a]
: [Form] -> [Form]
forall a. Eq a => [a] -> [a]
nub ((Form -> [Form]) -> [Form] -> [Form]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Form -> [Form]
subformulas [Form]
fs)
subformulas (Disj [Form]
fs) = [Form] -> Form
Disj [Form]
fs Form -> [Form] -> [Form]
forall a. a -> [a] -> [a]
: [Form] -> [Form]
forall a. Eq a => [a] -> [a]
nub ((Form -> [Form]) -> [Form] -> [Form]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Form -> [Form]
subformulas [Form]
fs)
subformulas (Xor [Form]
fs) = [Form] -> Form
Xor [Form]
fs Form -> [Form] -> [Form]
forall a. a -> [a] -> [a]
: [Form] -> [Form]
forall a. Eq a => [a] -> [a]
nub ((Form -> [Form]) -> [Form] -> [Form]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Form -> [Form]
subformulas [Form]
fs)
subformulas (Impl Form
f Form
g) = Form -> Form -> Form
Impl Form
f Form
g Form -> [Form] -> [Form]
forall a. a -> [a] -> [a]
: [Form] -> [Form]
forall a. Eq a => [a] -> [a]
nub ((Form -> [Form]) -> [Form] -> [Form]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Form -> [Form]
subformulas [Form
f,Form
g])
subformulas (Equi Form
f Form
g) = Form -> Form -> Form
Equi Form
f Form
g Form -> [Form] -> [Form]
forall a. a -> [a] -> [a]
: [Form] -> [Form]
forall a. Eq a => [a] -> [a]
nub ((Form -> [Form]) -> [Form] -> [Form]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Form -> [Form]
subformulas [Form
f,Form
g])
subformulas (Forall [Prp]
ps Form
f) = [Prp] -> Form -> Form
Forall [Prp]
ps Form
f Form -> [Form] -> [Form]
forall a. a -> [a] -> [a]
: Form -> [Form]
subformulas Form
f
subformulas (Exists [Prp]
ps Form
f) = [Prp] -> Form -> Form
Exists [Prp]
ps Form
f Form -> [Form] -> [Form]
forall a. a -> [a] -> [a]
: Form -> [Form]
subformulas Form
f
subformulas (K Agent
i Form
f) = Agent -> Form -> Form
K Agent
i Form
f Form -> [Form] -> [Form]
forall a. a -> [a] -> [a]
: Form -> [Form]
subformulas Form
f
subformulas (Ck [Agent]
is Form
f) = [Agent] -> Form -> Form
Ck [Agent]
is Form
f Form -> [Form] -> [Form]
forall a. a -> [a] -> [a]
: Form -> [Form]
subformulas Form
f
subformulas (Dk [Agent]
is Form
f) = [Agent] -> Form -> Form
Dk [Agent]
is Form
f Form -> [Form] -> [Form]
forall a. a -> [a] -> [a]
: Form -> [Form]
subformulas Form
f
subformulas (Kw Agent
i Form
f) = Agent -> Form -> Form
Kw Agent
i Form
f Form -> [Form] -> [Form]
forall a. a -> [a] -> [a]
: Form -> [Form]
subformulas Form
f
subformulas (Ckw [Agent]
is Form
f) = [Agent] -> Form -> Form
Ckw [Agent]
is Form
f Form -> [Form] -> [Form]
forall a. a -> [a] -> [a]
: Form -> [Form]
subformulas Form
f
subformulas (Dkw [Agent]
is Form
f) = [Agent] -> Form -> Form
Dkw [Agent]
is Form
f Form -> [Form] -> [Form]
forall a. a -> [a] -> [a]
: Form -> [Form]
subformulas Form
f
subformulas (PubAnnounce Form
f Form
g) = Form -> Form -> Form
PubAnnounce Form
f Form
g Form -> [Form] -> [Form]
forall a. a -> [a] -> [a]
: [Form] -> [Form]
forall a. Eq a => [a] -> [a]
nub (Form -> [Form]
subformulas Form
f [Form] -> [Form] -> [Form]
forall a. [a] -> [a] -> [a]
++ Form -> [Form]
subformulas Form
g)
subformulas (PubAnnounceW Form
f Form
g) = Form -> Form -> Form
PubAnnounceW Form
f Form
g Form -> [Form] -> [Form]
forall a. a -> [a] -> [a]
: [Form] -> [Form]
forall a. Eq a => [a] -> [a]
nub (Form -> [Form]
subformulas Form
f [Form] -> [Form] -> [Form]
forall a. [a] -> [a] -> [a]
++ Form -> [Form]
subformulas Form
g)
subformulas (Announce [Agent]
is Form
f Form
g) = [Agent] -> Form -> Form -> Form
Announce [Agent]
is Form
f Form
g Form -> [Form] -> [Form]
forall a. a -> [a] -> [a]
: [Form] -> [Form]
forall a. Eq a => [a] -> [a]
nub (Form -> [Form]
subformulas Form
f [Form] -> [Form] -> [Form]
forall a. [a] -> [a] -> [a]
++ Form -> [Form]
subformulas Form
g)
subformulas (AnnounceW [Agent]
is Form
f Form
g) = [Agent] -> Form -> Form -> Form
AnnounceW [Agent]
is Form
f Form
g Form -> [Form] -> [Form]
forall a. a -> [a] -> [a]
: [Form] -> [Form]
forall a. Eq a => [a] -> [a]
nub (Form -> [Form]
subformulas Form
f [Form] -> [Form] -> [Form]
forall a. [a] -> [a] -> [a]
++ Form -> [Form]
subformulas Form
g)
subformulas (Dia DynamicOp
dynop Form
f) = DynamicOp -> Form -> Form
Dia DynamicOp
dynop Form
f Form -> [Form] -> [Form]
forall a. a -> [a] -> [a]
: Form -> [Form]
subformulas Form
f
shrinkform :: Form -> [Form]
shrinkform :: Form -> [Form]
shrinkform Form
f = [ Form -> Form
simplify Form
f | Form
f Form -> Form -> Bool
forall a. Eq a => a -> a -> Bool
/= Form -> Form
simplify Form
f ] [Form] -> [Form] -> [Form]
forall a. [a] -> [a] -> [a]
++ (Form -> [Form]
subformulas Form
f [Form] -> [Form] -> [Form]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Form
f]) [Form] -> [Form] -> [Form]
forall a. [a] -> [a] -> [a]
++ Form -> [Form]
otherShrinks Form
f
where
otherShrinks :: Form -> [Form]
otherShrinks (Conj [Form]
fs) = [[Form] -> Form
Conj [Form]
gs | [Form]
gs <- [Form] -> [[Form]]
forall a. [a] -> [[a]]
powerset [Form]
fs [[Form]] -> [[Form]] -> [[Form]]
forall a. Eq a => [a] -> [a] -> [a]
\\ [[Form]
fs]]
otherShrinks (Disj [Form]
fs) = [[Form] -> Form
Disj [Form]
gs | [Form]
gs <- [Form] -> [[Form]]
forall a. [a] -> [[a]]
powerset [Form]
fs [[Form]] -> [[Form]] -> [[Form]]
forall a. Eq a => [a] -> [a] -> [a]
\\ [[Form]
fs]]
otherShrinks (Xor [Form]
fs) = [[Form] -> Form
Xor [Form]
gs | [Form]
gs <- [Form] -> [[Form]]
forall a. [a] -> [[a]]
powerset [Form]
fs [[Form]] -> [[Form]] -> [[Form]]
forall a. Eq a => [a] -> [a] -> [a]
\\ [[Form]
fs]]
otherShrinks (Ck [Agent]
is Form
g) = [[Agent] -> Form -> Form
Ck [Agent]
js Form
g | [Agent]
js <- [Agent] -> [[Agent]]
forall a. [a] -> [[a]]
powerset [Agent]
is [[Agent]] -> [[Agent]] -> [[Agent]]
forall a. Eq a => [a] -> [a] -> [a]
\\ [[Agent]
is]]
otherShrinks (Ckw [Agent]
is Form
g) = [[Agent] -> Form -> Form
Ckw [Agent]
js Form
g | [Agent]
js <- [Agent] -> [[Agent]]
forall a. [a] -> [[a]]
powerset [Agent]
is [[Agent]] -> [[Agent]] -> [[Agent]]
forall a. Eq a => [a] -> [a] -> [a]
\\ [[Agent]
is]]
otherShrinks (Dk [Agent]
is Form
g) = [[Agent] -> Form -> Form
Dk [Agent]
js Form
g | [Agent]
js <- [Agent] -> [[Agent]]
forall a. [a] -> [[a]]
powerset [Agent]
is [[Agent]] -> [[Agent]] -> [[Agent]]
forall a. Eq a => [a] -> [a] -> [a]
\\ [[Agent]
is]]
otherShrinks (Dkw [Agent]
is Form
g) = [[Agent] -> Form -> Form
Dkw [Agent]
js Form
g | [Agent]
js <- [Agent] -> [[Agent]]
forall a. [a] -> [[a]]
powerset [Agent]
is [[Agent]] -> [[Agent]] -> [[Agent]]
forall a. Eq a => [a] -> [a] -> [a]
\\ [[Agent]
is]]
otherShrinks (Forall [Prp]
ps Form
g) = [[Prp] -> Form -> Form
Forall [Prp]
qs Form
g | [Prp]
qs <- [Prp] -> [[Prp]]
forall a. [a] -> [[a]]
powerset [Prp]
ps [[Prp]] -> [[Prp]] -> [[Prp]]
forall a. Eq a => [a] -> [a] -> [a]
\\ [[Prp]
ps]]
otherShrinks (Exists [Prp]
ps Form
g) = [[Prp] -> Form -> Form
Exists [Prp]
qs Form
g | [Prp]
qs <- [Prp] -> [[Prp]]
forall a. [a] -> [[a]]
powerset [Prp]
ps [[Prp]] -> [[Prp]] -> [[Prp]]
forall a. Eq a => [a] -> [a] -> [a]
\\ [[Prp]
ps]]
otherShrinks Form
_ = []
substit :: Prp -> Form -> Form -> Form
substit :: Prp -> Form -> Form -> Form
substit Prp
_ Form
_ Form
Top = Form
Top
substit Prp
_ Form
_ Form
Bot = Form
Bot
substit Prp
q Form
psi (PrpF Prp
p) = if Prp
pPrp -> Prp -> Bool
forall a. Eq a => a -> a -> Bool
==Prp
q then Form
psi else Prp -> Form
PrpF Prp
p
substit Prp
q Form
psi (Neg Form
form) = Form -> Form
Neg (Prp -> Form -> Form -> Form
substit Prp
q Form
psi Form
form)
substit Prp
q Form
psi (Conj [Form]
forms) = [Form] -> Form
Conj ((Form -> Form) -> [Form] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map (Prp -> Form -> Form -> Form
substit Prp
q Form
psi) [Form]
forms)
substit Prp
q Form
psi (Disj [Form]
forms) = [Form] -> Form
Disj ((Form -> Form) -> [Form] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map (Prp -> Form -> Form -> Form
substit Prp
q Form
psi) [Form]
forms)
substit Prp
q Form
psi (Xor [Form]
forms) = [Form] -> Form
Xor ((Form -> Form) -> [Form] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map (Prp -> Form -> Form -> Form
substit Prp
q Form
psi) [Form]
forms)
substit Prp
q Form
psi (Impl Form
f Form
g) = Form -> Form -> Form
Impl (Prp -> Form -> Form -> Form
substit Prp
q Form
psi Form
f) (Prp -> Form -> Form -> Form
substit Prp
q Form
psi Form
g)
substit Prp
q Form
psi (Equi Form
f Form
g) = Form -> Form -> Form
Equi (Prp -> Form -> Form -> Form
substit Prp
q Form
psi Form
f) (Prp -> Form -> Form -> Form
substit Prp
q Form
psi Form
g)
substit Prp
q Form
psi (Forall [Prp]
ps Form
f) = if Prp
q Prp -> [Prp] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Prp]
ps
then Agent -> Form
forall a. HasCallStack => Agent -> a
error (Agent
"substit failed: Substituens "Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Prp -> Agent
forall a. Show a => a -> Agent
show Prp
q Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
" in 'Forall " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ [Prp] -> Agent
forall a. Show a => a -> Agent
show [Prp]
ps Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
" " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Form -> Agent
forall a. Show a => a -> Agent
show Form
f)
else [Prp] -> Form -> Form
Forall [Prp]
ps (Prp -> Form -> Form -> Form
substit Prp
q Form
psi Form
f)
substit Prp
q Form
psi (Exists [Prp]
ps Form
f) = if Prp
q Prp -> [Prp] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Prp]
ps
then Agent -> Form
forall a. HasCallStack => Agent -> a
error (Agent
"substit failed: Substituens " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Prp -> Agent
forall a. Show a => a -> Agent
show Prp
q Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
" in 'Exists " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ [Prp] -> Agent
forall a. Show a => a -> Agent
show [Prp]
ps Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
" " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Form -> Agent
forall a. Show a => a -> Agent
show Form
f)
else [Prp] -> Form -> Form
Exists [Prp]
ps (Prp -> Form -> Form -> Form
substit Prp
q Form
psi Form
f)
substit Prp
q Form
psi (K Agent
i Form
f) = Agent -> Form -> Form
K Agent
i (Prp -> Form -> Form -> Form
substit Prp
q Form
psi Form
f)
substit Prp
q Form
psi (Kw Agent
i Form
f) = Agent -> Form -> Form
Kw Agent
i (Prp -> Form -> Form -> Form
substit Prp
q Form
psi Form
f)
substit Prp
q Form
psi (Ck [Agent]
ags Form
f) = [Agent] -> Form -> Form
Ck [Agent]
ags (Prp -> Form -> Form -> Form
substit Prp
q Form
psi Form
f)
substit Prp
q Form
psi (Ckw [Agent]
ags Form
f) = [Agent] -> Form -> Form
Ckw [Agent]
ags (Prp -> Form -> Form -> Form
substit Prp
q Form
psi Form
f)
substit Prp
q Form
psi (Dk [Agent]
ags Form
f) = [Agent] -> Form -> Form
Dk [Agent]
ags (Prp -> Form -> Form -> Form
substit Prp
q Form
psi Form
f)
substit Prp
q Form
psi (Dkw [Agent]
ags Form
f) = [Agent] -> Form -> Form
Dkw [Agent]
ags (Prp -> Form -> Form -> Form
substit Prp
q Form
psi Form
f)
substit Prp
q Form
psi (PubAnnounce Form
f Form
g) = Form -> Form -> Form
PubAnnounce (Prp -> Form -> Form -> Form
substit Prp
q Form
psi Form
f) (Prp -> Form -> Form -> Form
substit Prp
q Form
psi Form
g)
substit Prp
q Form
psi (PubAnnounceW Form
f Form
g) = Form -> Form -> Form
PubAnnounceW (Prp -> Form -> Form -> Form
substit Prp
q Form
psi Form
f) (Prp -> Form -> Form -> Form
substit Prp
q Form
psi Form
g)
substit Prp
q Form
psi (Announce [Agent]
ags Form
f Form
g) = [Agent] -> Form -> Form -> Form
Announce [Agent]
ags (Prp -> Form -> Form -> Form
substit Prp
q Form
psi Form
f) (Prp -> Form -> Form -> Form
substit Prp
q Form
psi Form
g)
substit Prp
q Form
psi (AnnounceW [Agent]
ags Form
f Form
g) = [Agent] -> Form -> Form -> Form
AnnounceW [Agent]
ags (Prp -> Form -> Form -> Form
substit Prp
q Form
psi Form
f) (Prp -> Form -> Form -> Form
substit Prp
q Form
psi Form
g)
substit Prp
_ Form
_ (Dia DynamicOp
_ Form
_) = Agent -> Form
forall a. HasCallStack => Agent -> a
error Agent
"Cannot substitute in dynamic diamonds."
substitSet :: [(Prp,Form)] -> Form -> Form
substitSet :: [(Prp, Form)] -> Form -> Form
substitSet [] Form
f = Form
f
substitSet ((Prp
q,Form
psi):[(Prp, Form)]
rest) Form
f = [(Prp, Form)] -> Form -> Form
substitSet [(Prp, Form)]
rest (Prp -> Form -> Form -> Form
substit Prp
q Form
psi Form
f)
substitOutOf :: [Prp] -> [Prp] -> Form -> Form
substitOutOf :: [Prp] -> [Prp] -> Form -> Form
substitOutOf [Prp]
truths [Prp]
allps = [(Prp, Form)] -> Form -> Form
substitSet [(Prp
p, if Prp
p Prp -> [Prp] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Prp]
truths then Form
Top else Form
Bot) | Prp
p <- [Prp]
allps]
replPsInP :: [(Prp,Prp)] -> Prp -> Prp
replPsInP :: [(Prp, Prp)] -> Prp -> Prp
replPsInP [(Prp, Prp)]
repl Prp
p = Prp -> Maybe Prp -> Prp
forall a. a -> Maybe a -> a
fromMaybe Prp
p (Prp -> [(Prp, Prp)] -> Maybe Prp
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Prp
p [(Prp, Prp)]
repl)
replPsInF :: [(Prp,Prp)] -> Form -> Form
replPsInF :: [(Prp, Prp)] -> Form -> Form
replPsInF [(Prp, Prp)]
_ Form
Top = Form
Top
replPsInF [(Prp, Prp)]
_ Form
Bot = Form
Bot
replPsInF [(Prp, Prp)]
repl (PrpF Prp
p) = Prp -> Form
PrpF (Prp -> Form) -> Prp -> Form
forall a b. (a -> b) -> a -> b
$ [(Prp, Prp)] -> Prp -> Prp
replPsInP [(Prp, Prp)]
repl Prp
p
replPsInF [(Prp, Prp)]
repl (Neg Form
f) = Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ [(Prp, Prp)] -> Form -> Form
replPsInF [(Prp, Prp)]
repl Form
f
replPsInF [(Prp, Prp)]
repl (Conj [Form]
fs) = [Form] -> Form
Conj ([Form] -> Form) -> [Form] -> Form
forall a b. (a -> b) -> a -> b
$ (Form -> Form) -> [Form] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map ([(Prp, Prp)] -> Form -> Form
replPsInF [(Prp, Prp)]
repl) [Form]
fs
replPsInF [(Prp, Prp)]
repl (Disj [Form]
fs) = [Form] -> Form
Disj ([Form] -> Form) -> [Form] -> Form
forall a b. (a -> b) -> a -> b
$ (Form -> Form) -> [Form] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map ([(Prp, Prp)] -> Form -> Form
replPsInF [(Prp, Prp)]
repl) [Form]
fs
replPsInF [(Prp, Prp)]
repl (Xor [Form]
fs) = [Form] -> Form
Xor ([Form] -> Form) -> [Form] -> Form
forall a b. (a -> b) -> a -> b
$ (Form -> Form) -> [Form] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map ([(Prp, Prp)] -> Form -> Form
replPsInF [(Prp, Prp)]
repl) [Form]
fs
replPsInF [(Prp, Prp)]
repl (Impl Form
f Form
g) = Form -> Form -> Form
Impl ([(Prp, Prp)] -> Form -> Form
replPsInF [(Prp, Prp)]
repl Form
f) ([(Prp, Prp)] -> Form -> Form
replPsInF [(Prp, Prp)]
repl Form
g)
replPsInF [(Prp, Prp)]
repl (Equi Form
f Form
g) = Form -> Form -> Form
Equi ([(Prp, Prp)] -> Form -> Form
replPsInF [(Prp, Prp)]
repl Form
f) ([(Prp, Prp)] -> Form -> Form
replPsInF [(Prp, Prp)]
repl Form
g)
replPsInF [(Prp, Prp)]
repl (Forall [Prp]
ps Form
f) = [Prp] -> Form -> Form
Forall ((Prp -> Prp) -> [Prp] -> [Prp]
forall a b. (a -> b) -> [a] -> [b]
map ([(Prp, Prp)] -> Prp -> Prp
replPsInP [(Prp, Prp)]
repl) [Prp]
ps) ([(Prp, Prp)] -> Form -> Form
replPsInF [(Prp, Prp)]
repl Form
f)
replPsInF [(Prp, Prp)]
repl (Exists [Prp]
ps Form
f) = [Prp] -> Form -> Form
Exists ((Prp -> Prp) -> [Prp] -> [Prp]
forall a b. (a -> b) -> [a] -> [b]
map ([(Prp, Prp)] -> Prp -> Prp
replPsInP [(Prp, Prp)]
repl) [Prp]
ps) ([(Prp, Prp)] -> Form -> Form
replPsInF [(Prp, Prp)]
repl Form
f)
replPsInF [(Prp, Prp)]
repl (K Agent
i Form
f) = Agent -> Form -> Form
K Agent
i ([(Prp, Prp)] -> Form -> Form
replPsInF [(Prp, Prp)]
repl Form
f)
replPsInF [(Prp, Prp)]
repl (Kw Agent
i Form
f) = Agent -> Form -> Form
Kw Agent
i ([(Prp, Prp)] -> Form -> Form
replPsInF [(Prp, Prp)]
repl Form
f)
replPsInF [(Prp, Prp)]
repl (Ck [Agent]
ags Form
f) = [Agent] -> Form -> Form
Ck [Agent]
ags ([(Prp, Prp)] -> Form -> Form
replPsInF [(Prp, Prp)]
repl Form
f)
replPsInF [(Prp, Prp)]
repl (Ckw [Agent]
ags Form
f) = [Agent] -> Form -> Form
Ckw [Agent]
ags ([(Prp, Prp)] -> Form -> Form
replPsInF [(Prp, Prp)]
repl Form
f)
replPsInF [(Prp, Prp)]
repl (Dk [Agent]
ags Form
f) = [Agent] -> Form -> Form
Dk [Agent]
ags ([(Prp, Prp)] -> Form -> Form
replPsInF [(Prp, Prp)]
repl Form
f)
replPsInF [(Prp, Prp)]
repl (Dkw [Agent]
ags Form
f) = [Agent] -> Form -> Form
Dkw [Agent]
ags ([(Prp, Prp)] -> Form -> Form
replPsInF [(Prp, Prp)]
repl Form
f)
replPsInF [(Prp, Prp)]
repl (PubAnnounce Form
f Form
g) = Form -> Form -> Form
PubAnnounce ([(Prp, Prp)] -> Form -> Form
replPsInF [(Prp, Prp)]
repl Form
f) ([(Prp, Prp)] -> Form -> Form
replPsInF [(Prp, Prp)]
repl Form
g)
replPsInF [(Prp, Prp)]
repl (PubAnnounceW Form
f Form
g) = Form -> Form -> Form
PubAnnounceW ([(Prp, Prp)] -> Form -> Form
replPsInF [(Prp, Prp)]
repl Form
f) ([(Prp, Prp)] -> Form -> Form
replPsInF [(Prp, Prp)]
repl Form
g)
replPsInF [(Prp, Prp)]
repl (Announce [Agent]
ags Form
f Form
g) = [Agent] -> Form -> Form -> Form
Announce [Agent]
ags ([(Prp, Prp)] -> Form -> Form
replPsInF [(Prp, Prp)]
repl Form
f) ([(Prp, Prp)] -> Form -> Form
replPsInF [(Prp, Prp)]
repl Form
g)
replPsInF [(Prp, Prp)]
repl (AnnounceW [Agent]
ags Form
f Form
g) = [Agent] -> Form -> Form -> Form
AnnounceW [Agent]
ags ([(Prp, Prp)] -> Form -> Form
replPsInF [(Prp, Prp)]
repl Form
f) ([(Prp, Prp)] -> Form -> Form
replPsInF [(Prp, Prp)]
repl Form
g)
replPsInF [(Prp, Prp)]
_ (Dia DynamicOp
_ Form
_) = Form
forall a. HasCallStack => a
undefined
propsInForm :: Form -> [Prp]
propsInForm :: Form -> [Prp]
propsInForm Form
Top = []
propsInForm Form
Bot = []
propsInForm (PrpF Prp
p) = [Prp
p]
propsInForm (Neg Form
f) = Form -> [Prp]
propsInForm Form
f
propsInForm (Conj [Form]
fs) = [Prp] -> [Prp]
forall a. Eq a => [a] -> [a]
nub ([Prp] -> [Prp]) -> [Prp] -> [Prp]
forall a b. (a -> b) -> a -> b
$ (Form -> [Prp]) -> [Form] -> [Prp]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Form -> [Prp]
propsInForm [Form]
fs
propsInForm (Disj [Form]
fs) = [Prp] -> [Prp]
forall a. Eq a => [a] -> [a]
nub ([Prp] -> [Prp]) -> [Prp] -> [Prp]
forall a b. (a -> b) -> a -> b
$ (Form -> [Prp]) -> [Form] -> [Prp]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Form -> [Prp]
propsInForm [Form]
fs
propsInForm (Xor [Form]
fs) = [Prp] -> [Prp]
forall a. Eq a => [a] -> [a]
nub ([Prp] -> [Prp]) -> [Prp] -> [Prp]
forall a b. (a -> b) -> a -> b
$ (Form -> [Prp]) -> [Form] -> [Prp]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Form -> [Prp]
propsInForm [Form]
fs
propsInForm (Impl Form
f Form
g) = [Prp] -> [Prp]
forall a. Eq a => [a] -> [a]
nub ([Prp] -> [Prp]) -> [Prp] -> [Prp]
forall a b. (a -> b) -> a -> b
$ (Form -> [Prp]) -> [Form] -> [Prp]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Form -> [Prp]
propsInForm [Form
f,Form
g]
propsInForm (Equi Form
f Form
g) = [Prp] -> [Prp]
forall a. Eq a => [a] -> [a]
nub ([Prp] -> [Prp]) -> [Prp] -> [Prp]
forall a b. (a -> b) -> a -> b
$ (Form -> [Prp]) -> [Form] -> [Prp]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Form -> [Prp]
propsInForm [Form
f,Form
g]
propsInForm (Forall [Prp]
ps Form
f) = [Prp] -> [Prp]
forall a. Eq a => [a] -> [a]
nub ([Prp] -> [Prp]) -> [Prp] -> [Prp]
forall a b. (a -> b) -> a -> b
$ [Prp]
ps [Prp] -> [Prp] -> [Prp]
forall a. [a] -> [a] -> [a]
++ Form -> [Prp]
propsInForm Form
f
propsInForm (Exists [Prp]
ps Form
f) = [Prp] -> [Prp]
forall a. Eq a => [a] -> [a]
nub ([Prp] -> [Prp]) -> [Prp] -> [Prp]
forall a b. (a -> b) -> a -> b
$ [Prp]
ps [Prp] -> [Prp] -> [Prp]
forall a. [a] -> [a] -> [a]
++ Form -> [Prp]
propsInForm Form
f
propsInForm (K Agent
_ Form
f) = Form -> [Prp]
propsInForm Form
f
propsInForm (Kw Agent
_ Form
f) = Form -> [Prp]
propsInForm Form
f
propsInForm (Ck [Agent]
_ Form
f) = Form -> [Prp]
propsInForm Form
f
propsInForm (Ckw [Agent]
_ Form
f) = Form -> [Prp]
propsInForm Form
f
propsInForm (Dk [Agent]
_ Form
f) = Form -> [Prp]
propsInForm Form
f
propsInForm (Dkw [Agent]
_ Form
f) = Form -> [Prp]
propsInForm Form
f
propsInForm (Announce [Agent]
_ Form
f Form
g) = [Prp] -> [Prp]
forall a. Eq a => [a] -> [a]
nub ([Prp] -> [Prp]) -> [Prp] -> [Prp]
forall a b. (a -> b) -> a -> b
$ Form -> [Prp]
propsInForm Form
f [Prp] -> [Prp] -> [Prp]
forall a. [a] -> [a] -> [a]
++ Form -> [Prp]
propsInForm Form
g
propsInForm (AnnounceW [Agent]
_ Form
f Form
g) = [Prp] -> [Prp]
forall a. Eq a => [a] -> [a]
nub ([Prp] -> [Prp]) -> [Prp] -> [Prp]
forall a b. (a -> b) -> a -> b
$ Form -> [Prp]
propsInForm Form
f [Prp] -> [Prp] -> [Prp]
forall a. [a] -> [a] -> [a]
++ Form -> [Prp]
propsInForm Form
g
propsInForm (PubAnnounce Form
f Form
g) = [Prp] -> [Prp]
forall a. Eq a => [a] -> [a]
nub ([Prp] -> [Prp]) -> [Prp] -> [Prp]
forall a b. (a -> b) -> a -> b
$ Form -> [Prp]
propsInForm Form
f [Prp] -> [Prp] -> [Prp]
forall a. [a] -> [a] -> [a]
++ Form -> [Prp]
propsInForm Form
g
propsInForm (PubAnnounceW Form
f Form
g) = [Prp] -> [Prp]
forall a. Eq a => [a] -> [a]
nub ([Prp] -> [Prp]) -> [Prp] -> [Prp]
forall a b. (a -> b) -> a -> b
$ Form -> [Prp]
propsInForm Form
f [Prp] -> [Prp] -> [Prp]
forall a. [a] -> [a] -> [a]
++ Form -> [Prp]
propsInForm Form
g
propsInForm (Dia DynamicOp
_dynOp Form
_f) = [Prp]
forall a. HasCallStack => a
undefined
propsInForms :: [Form] -> [Prp]
propsInForms :: [Form] -> [Prp]
propsInForms [Form]
fs = [Prp] -> [Prp]
forall a. Eq a => [a] -> [a]
nub ([Prp] -> [Prp]) -> [Prp] -> [Prp]
forall a b. (a -> b) -> a -> b
$ (Form -> [Prp]) -> [Form] -> [Prp]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Form -> [Prp]
propsInForm [Form]
fs
agentsInForm :: Form -> [Agent]
agentsInForm :: Form -> [Agent]
agentsInForm Form
Top = []
agentsInForm Form
Bot = []
agentsInForm (PrpF Prp
_) = []
agentsInForm (Neg Form
f) = Form -> [Agent]
agentsInForm Form
f
agentsInForm (Conj [Form]
fs) = [Agent] -> [Agent]
forall a. Eq a => [a] -> [a]
nub ([Agent] -> [Agent]) -> [Agent] -> [Agent]
forall a b. (a -> b) -> a -> b
$ (Form -> [Agent]) -> [Form] -> [Agent]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Form -> [Agent]
agentsInForm [Form]
fs
agentsInForm (Disj [Form]
fs) = [Agent] -> [Agent]
forall a. Eq a => [a] -> [a]
nub ([Agent] -> [Agent]) -> [Agent] -> [Agent]
forall a b. (a -> b) -> a -> b
$ (Form -> [Agent]) -> [Form] -> [Agent]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Form -> [Agent]
agentsInForm [Form]
fs
agentsInForm (Xor [Form]
fs) = [Agent] -> [Agent]
forall a. Eq a => [a] -> [a]
nub ([Agent] -> [Agent]) -> [Agent] -> [Agent]
forall a b. (a -> b) -> a -> b
$ (Form -> [Agent]) -> [Form] -> [Agent]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Form -> [Agent]
agentsInForm [Form]
fs
agentsInForm (Impl Form
f Form
g) = [Agent] -> [Agent]
forall a. Eq a => [a] -> [a]
nub ([Agent] -> [Agent]) -> [Agent] -> [Agent]
forall a b. (a -> b) -> a -> b
$ (Form -> [Agent]) -> [Form] -> [Agent]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Form -> [Agent]
agentsInForm [Form
f,Form
g]
agentsInForm (Equi Form
f Form
g) = [Agent] -> [Agent]
forall a. Eq a => [a] -> [a]
nub ([Agent] -> [Agent]) -> [Agent] -> [Agent]
forall a b. (a -> b) -> a -> b
$ (Form -> [Agent]) -> [Form] -> [Agent]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Form -> [Agent]
agentsInForm [Form
f,Form
g]
agentsInForm (Forall [Prp]
_ Form
f) = Form -> [Agent]
agentsInForm Form
f
agentsInForm (Exists [Prp]
_ Form
f) = Form -> [Agent]
agentsInForm Form
f
agentsInForm (K Agent
i Form
f) = [Agent] -> [Agent]
forall a. Eq a => [a] -> [a]
nub ([Agent] -> [Agent]) -> [Agent] -> [Agent]
forall a b. (a -> b) -> a -> b
$ Agent
i Agent -> [Agent] -> [Agent]
forall a. a -> [a] -> [a]
: Form -> [Agent]
agentsInForm Form
f
agentsInForm (Kw Agent
i Form
f) = [Agent] -> [Agent]
forall a. Eq a => [a] -> [a]
nub ([Agent] -> [Agent]) -> [Agent] -> [Agent]
forall a b. (a -> b) -> a -> b
$ Agent
i Agent -> [Agent] -> [Agent]
forall a. a -> [a] -> [a]
: Form -> [Agent]
agentsInForm Form
f
agentsInForm (Ck [Agent]
is Form
f) = [Agent] -> [Agent]
forall a. Eq a => [a] -> [a]
nub ([Agent] -> [Agent]) -> [Agent] -> [Agent]
forall a b. (a -> b) -> a -> b
$ [Agent]
is [Agent] -> [Agent] -> [Agent]
forall a. [a] -> [a] -> [a]
++ Form -> [Agent]
agentsInForm Form
f
agentsInForm (Ckw [Agent]
is Form
f) = [Agent] -> [Agent]
forall a. Eq a => [a] -> [a]
nub ([Agent] -> [Agent]) -> [Agent] -> [Agent]
forall a b. (a -> b) -> a -> b
$ [Agent]
is [Agent] -> [Agent] -> [Agent]
forall a. [a] -> [a] -> [a]
++ Form -> [Agent]
agentsInForm Form
f
agentsInForm (Dk [Agent]
is Form
f) = [Agent] -> [Agent]
forall a. Eq a => [a] -> [a]
nub ([Agent] -> [Agent]) -> [Agent] -> [Agent]
forall a b. (a -> b) -> a -> b
$ [Agent]
is [Agent] -> [Agent] -> [Agent]
forall a. [a] -> [a] -> [a]
++ Form -> [Agent]
agentsInForm Form
f
agentsInForm (Dkw [Agent]
is Form
f) = [Agent] -> [Agent]
forall a. Eq a => [a] -> [a]
nub ([Agent] -> [Agent]) -> [Agent] -> [Agent]
forall a b. (a -> b) -> a -> b
$ [Agent]
is [Agent] -> [Agent] -> [Agent]
forall a. [a] -> [a] -> [a]
++ Form -> [Agent]
agentsInForm Form
f
agentsInForm (Announce [Agent]
is Form
f Form
g) = [Agent] -> [Agent]
forall a. Eq a => [a] -> [a]
nub ([Agent] -> [Agent]) -> [Agent] -> [Agent]
forall a b. (a -> b) -> a -> b
$ [Agent]
is [Agent] -> [Agent] -> [Agent]
forall a. [a] -> [a] -> [a]
++ Form -> [Agent]
agentsInForm Form
f [Agent] -> [Agent] -> [Agent]
forall a. [a] -> [a] -> [a]
++ Form -> [Agent]
agentsInForm Form
g
agentsInForm (AnnounceW [Agent]
is Form
f Form
g) = [Agent] -> [Agent]
forall a. Eq a => [a] -> [a]
nub ([Agent] -> [Agent]) -> [Agent] -> [Agent]
forall a b. (a -> b) -> a -> b
$ [Agent]
is [Agent] -> [Agent] -> [Agent]
forall a. [a] -> [a] -> [a]
++ Form -> [Agent]
agentsInForm Form
f [Agent] -> [Agent] -> [Agent]
forall a. [a] -> [a] -> [a]
++ Form -> [Agent]
agentsInForm Form
g
agentsInForm (PubAnnounce Form
f Form
g) = [Agent] -> [Agent]
forall a. Eq a => [a] -> [a]
nub ([Agent] -> [Agent]) -> [Agent] -> [Agent]
forall a b. (a -> b) -> a -> b
$ Form -> [Agent]
agentsInForm Form
f [Agent] -> [Agent] -> [Agent]
forall a. [a] -> [a] -> [a]
++ Form -> [Agent]
agentsInForm Form
g
agentsInForm (PubAnnounceW Form
f Form
g) = [Agent] -> [Agent]
forall a. Eq a => [a] -> [a]
nub ([Agent] -> [Agent]) -> [Agent] -> [Agent]
forall a b. (a -> b) -> a -> b
$ Form -> [Agent]
agentsInForm Form
f [Agent] -> [Agent] -> [Agent]
forall a. [a] -> [a] -> [a]
++ Form -> [Agent]
agentsInForm Form
g
agentsInForm (Dia DynamicOp
_dynOp Form
_f) = [Agent]
forall a. HasCallStack => a
undefined
simplify :: Form -> Form
simplify :: Form -> Form
simplify Form
f = if Form -> Form
simStep Form
f Form -> Form -> Bool
forall a. Eq a => a -> a -> Bool
== Form
f then Form
f else Form -> Form
simplify (Form -> Form
simStep Form
f)
simStep :: Form -> Form
simStep :: Form -> Form
simStep Form
Top = Form
Top
simStep Form
Bot = Form
Bot
simStep (PrpF Prp
p) = Prp -> Form
PrpF Prp
p
simStep (Neg Form
Top) = Form
Bot
simStep (Neg Form
Bot) = Form
Top
simStep (Neg (Neg Form
f)) = Form -> Form
simStep Form
f
simStep (Neg Form
f) = Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Form -> Form
simStep Form
f
simStep (Conj []) = Form
Top
simStep (Conj [Form
f]) = Form -> Form
simStep Form
f
simStep (Conj [Form]
fs) | Form
Bot Form -> [Form] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Form]
fs = Form
Bot
| [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [ Form -> Form
Neg Form
f Form -> [Form] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Form]
fs | Form
f <- [Form]
fs ] = Form
Bot
| Bool
otherwise = [Form] -> Form
Conj ([Form] -> [Form]
forall a. Eq a => [a] -> [a]
nub ([Form] -> [Form]) -> [Form] -> [Form]
forall a b. (a -> b) -> a -> b
$ (Form -> [Form]) -> [Form] -> [Form]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Form -> [Form]
unpack [Form]
fs) where
unpack :: Form -> [Form]
unpack Form
Top = []
unpack (Conj [Form]
subfs) = (Form -> Form) -> [Form] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map Form -> Form
simStep ([Form] -> [Form]) -> [Form] -> [Form]
forall a b. (a -> b) -> a -> b
$ (Form -> Bool) -> [Form] -> [Form]
forall a. (a -> Bool) -> [a] -> [a]
filter (Form
Top Form -> Form -> Bool
forall a. Eq a => a -> a -> Bool
/=) [Form]
subfs
unpack Form
f = [Form -> Form
simStep Form
f]
simStep (Disj []) = Form
Bot
simStep (Disj [Form
f]) = Form -> Form
simStep Form
f
simStep (Disj [Form]
fs) | Form
Top Form -> [Form] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Form]
fs = Form
Top
| [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [ Form -> Form
Neg Form
f Form -> [Form] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Form]
fs | Form
f <- [Form]
fs ] = Form
Top
| Bool
otherwise = [Form] -> Form
Disj ([Form] -> [Form]
forall a. Eq a => [a] -> [a]
nub ([Form] -> [Form]) -> [Form] -> [Form]
forall a b. (a -> b) -> a -> b
$ (Form -> [Form]) -> [Form] -> [Form]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Form -> [Form]
unpack [Form]
fs) where
unpack :: Form -> [Form]
unpack Form
Bot = []
unpack (Disj [Form]
subfs) = (Form -> Form) -> [Form] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map Form -> Form
simStep ([Form] -> [Form]) -> [Form] -> [Form]
forall a b. (a -> b) -> a -> b
$ (Form -> Bool) -> [Form] -> [Form]
forall a. (a -> Bool) -> [a] -> [a]
filter (Form
Bot Form -> Form -> Bool
forall a. Eq a => a -> a -> Bool
/=) [Form]
subfs
unpack Form
f = [Form -> Form
simStep Form
f]
simStep (Xor []) = Form
Bot
simStep (Xor [Form
Bot]) = Form
Bot
simStep (Xor [Form
f]) = Form -> Form
simStep Form
f
simStep (Xor [Form]
fs) = [Form] -> Form
Xor ((Form -> Form) -> [Form] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map Form -> Form
simStep ([Form] -> [Form]) -> [Form] -> [Form]
forall a b. (a -> b) -> a -> b
$ (Form -> Bool) -> [Form] -> [Form]
forall a. (a -> Bool) -> [a] -> [a]
filter (Form
Bot Form -> Form -> Bool
forall a. Eq a => a -> a -> Bool
/=) [Form]
fs)
simStep (Impl Form
Bot Form
_) = Form
Top
simStep (Impl Form
_ Form
Top) = Form
Top
simStep (Impl Form
Top Form
f) = Form -> Form
simStep Form
f
simStep (Impl Form
f Form
Bot) = Form -> Form
Neg (Form -> Form
simStep Form
f)
simStep (Impl Form
f Form
g) | Form
fForm -> Form -> Bool
forall a. Eq a => a -> a -> Bool
==Form
g = Form
Top
| Bool
otherwise = Form -> Form -> Form
Impl (Form -> Form
simStep Form
f) (Form -> Form
simStep Form
g)
simStep (Equi Form
Top Form
f) = Form -> Form
simStep Form
f
simStep (Equi Form
Bot Form
f) = Form -> Form
Neg (Form -> Form
simStep Form
f)
simStep (Equi Form
f Form
Top) = Form -> Form
simStep Form
f
simStep (Equi Form
f Form
Bot) = Form -> Form
Neg (Form -> Form
simStep Form
f)
simStep (Equi Form
f Form
g) | Form
fForm -> Form -> Bool
forall a. Eq a => a -> a -> Bool
==Form
g = Form
Top
| Bool
otherwise = Form -> Form -> Form
Equi (Form -> Form
simStep Form
f) (Form -> Form
simStep Form
g)
simStep (Forall [] Form
f) = Form -> Form
simStep Form
f
simStep (Forall [Prp]
ps Form
f) = [Prp] -> Form -> Form
Forall [Prp]
ps (Form -> Form
simStep Form
f)
simStep (Exists [] Form
f) = Form -> Form
simStep Form
f
simStep (Exists [Prp]
ps Form
f) = [Prp] -> Form -> Form
Exists [Prp]
ps (Form -> Form
simStep Form
f)
simStep (K Agent
a Form
f) = Agent -> Form -> Form
K Agent
a (Form -> Form
simStep Form
f)
simStep (Kw Agent
a Form
f) = Agent -> Form -> Form
Kw Agent
a (Form -> Form
simStep Form
f)
simStep (Ck [Agent]
_ Form
Top) = Form
Top
simStep (Ck [Agent]
ags Form
Bot) = [Agent] -> Form -> Form
Ck [Agent]
ags Form
Bot
simStep (Ck [Agent]
ags Form
f) = [Agent] -> Form -> Form
Ck [Agent]
ags (Form -> Form
simStep Form
f)
simStep (Ckw [Agent]
_ Form
Top) = Form
Top
simStep (Ckw [Agent]
_ Form
Bot) = Form
Top
simStep (Ckw [Agent]
ags Form
f) = [Agent] -> Form -> Form
Ckw [Agent]
ags (Form -> Form
simStep Form
f)
simStep (Dk [Agent]
_ Form
Top) = Form
Top
simStep (Dk [Agent]
ags Form
Bot) = [Agent] -> Form -> Form
Dk [Agent]
ags Form
Bot
simStep (Dk [Agent]
ags Form
f) = [Agent] -> Form -> Form
Dk [Agent]
ags (Form -> Form
simStep Form
f)
simStep (Dkw [Agent]
_ Form
Top) = Form
Top
simStep (Dkw [Agent]
_ Form
Bot) = Form
Top
simStep (Dkw [Agent]
ags Form
f) = [Agent] -> Form -> Form
Dkw [Agent]
ags (Form -> Form
simStep Form
f)
simStep (PubAnnounce Form
Top Form
f) = Form -> Form
simStep Form
f
simStep (PubAnnounce Form
Bot Form
_) = Form
Top
simStep (PubAnnounce Form
f Form
g) = Form -> Form -> Form
PubAnnounce (Form -> Form
simStep Form
f) (Form -> Form
simStep Form
g)
simStep (PubAnnounceW Form
f Form
g) = Form -> Form -> Form
PubAnnounceW (Form -> Form
simStep Form
f) (Form -> Form
simStep Form
g)
simStep (Announce [Agent]
ags Form
f Form
g) = [Agent] -> Form -> Form -> Form
Announce [Agent]
ags (Form -> Form
simStep Form
f) (Form -> Form
simStep Form
g)
simStep (AnnounceW [Agent]
ags Form
f Form
g) = [Agent] -> Form -> Form -> Form
AnnounceW [Agent]
ags (Form -> Form
simStep Form
f) (Form -> Form
simStep Form
g)
simStep (Dia DynamicOp
dynop Form
f) = DynamicOp -> Form -> Form
Dia DynamicOp
dynop (Form -> Form
simStep Form
f)
newtype BF = BF Form deriving (BF -> BF -> Bool
(BF -> BF -> Bool) -> (BF -> BF -> Bool) -> Eq BF
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BF -> BF -> Bool
== :: BF -> BF -> Bool
$c/= :: BF -> BF -> Bool
/= :: BF -> BF -> Bool
Eq,Eq BF
Eq BF =>
(BF -> BF -> Ordering)
-> (BF -> BF -> Bool)
-> (BF -> BF -> Bool)
-> (BF -> BF -> Bool)
-> (BF -> BF -> Bool)
-> (BF -> BF -> BF)
-> (BF -> BF -> BF)
-> Ord BF
BF -> BF -> Bool
BF -> BF -> Ordering
BF -> BF -> BF
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 :: BF -> BF -> Ordering
compare :: BF -> BF -> Ordering
$c< :: BF -> BF -> Bool
< :: BF -> BF -> Bool
$c<= :: BF -> BF -> Bool
<= :: BF -> BF -> Bool
$c> :: BF -> BF -> Bool
> :: BF -> BF -> Bool
$c>= :: BF -> BF -> Bool
>= :: BF -> BF -> Bool
$cmax :: BF -> BF -> BF
max :: BF -> BF -> BF
$cmin :: BF -> BF -> BF
min :: BF -> BF -> BF
Ord,Int -> BF -> ShowS
[BF] -> ShowS
BF -> Agent
(Int -> BF -> ShowS) -> (BF -> Agent) -> ([BF] -> ShowS) -> Show BF
forall a.
(Int -> a -> ShowS) -> (a -> Agent) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BF -> ShowS
showsPrec :: Int -> BF -> ShowS
$cshow :: BF -> Agent
show :: BF -> Agent
$cshowList :: [BF] -> ShowS
showList :: [BF] -> ShowS
Show)
instance Arbitrary BF where
arbitrary :: Gen BF
arbitrary = (Int -> Gen BF) -> Gen BF
forall a. (Int -> Gen a) -> Gen a
sized ((Int -> Gen BF) -> Gen BF) -> (Int -> Gen BF) -> Gen BF
forall a b. (a -> b) -> a -> b
$ [Prp] -> Int -> Gen BF
randomboolformWith [Int -> Prp
P Int
1 .. Int -> Prp
P Int
100]
shrink :: BF -> [BF]
shrink (BF Form
f) = (Form -> BF) -> [Form] -> [BF]
forall a b. (a -> b) -> [a] -> [b]
map Form -> BF
BF ([Form] -> [BF]) -> [Form] -> [BF]
forall a b. (a -> b) -> a -> b
$ Form -> [Form]
shrinkform Form
f
randomboolformWith :: [Prp] -> Int -> Gen BF
randomboolformWith :: [Prp] -> Int -> Gen BF
randomboolformWith [Prp]
allprops Int
sz = Form -> BF
BF (Form -> BF) -> Gen Form -> Gen BF
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Gen Form
forall {a}. Integral a => a -> Gen Form
bf' Int
sz where
bf' :: a -> Gen Form
bf' a
0 = Prp -> Form
PrpF (Prp -> Form) -> Gen Prp -> Gen Form
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Prp] -> Gen Prp
forall a. [a] -> Gen a
elements [Prp]
allprops
bf' a
n = [Gen Form] -> Gen Form
forall a. [Gen a] -> Gen a
oneof [ Form -> Gen Form
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Form
SMCDEL.Language.Top
, Form -> Gen Form
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Form
SMCDEL.Language.Bot
, Prp -> Form
PrpF (Prp -> Form) -> Gen Prp -> Gen Form
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Prp] -> Gen Prp
forall a. [a] -> Gen a
elements [Prp]
allprops
, Form -> Form
Neg (Form -> Form) -> Gen Form -> Gen Form
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Form
st
, (\Form
x Form
y -> [Form] -> Form
Conj [Form
x,Form
y]) (Form -> Form -> Form) -> Gen Form -> Gen (Form -> Form)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Form
st Gen (Form -> Form) -> Gen Form -> Gen Form
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen Form
st
, (\Form
x Form
y Form
z -> [Form] -> Form
Conj [Form
x,Form
y,Form
z]) (Form -> Form -> Form -> Form)
-> Gen Form -> Gen (Form -> Form -> Form)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Form
st Gen (Form -> Form -> Form) -> Gen Form -> Gen (Form -> Form)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen Form
st Gen (Form -> Form) -> Gen Form -> Gen Form
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen Form
st
, (\Form
x Form
y -> [Form] -> Form
Disj [Form
x,Form
y]) (Form -> Form -> Form) -> Gen Form -> Gen (Form -> Form)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Form
st Gen (Form -> Form) -> Gen Form -> Gen Form
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen Form
st
, (\Form
x Form
y Form
z -> [Form] -> Form
Disj [Form
x,Form
y,Form
z]) (Form -> Form -> Form -> Form)
-> Gen Form -> Gen (Form -> Form -> Form)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Form
st Gen (Form -> Form -> Form) -> Gen Form -> Gen (Form -> Form)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen Form
st Gen (Form -> Form) -> Gen Form -> Gen Form
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen Form
st
, Form -> Form -> Form
Impl (Form -> Form -> Form) -> Gen Form -> Gen (Form -> Form)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Form
st Gen (Form -> Form) -> Gen Form -> Gen Form
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen Form
st
, Form -> Form -> Form
Equi (Form -> Form -> Form) -> Gen Form -> Gen (Form -> Form)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Form
st Gen (Form -> Form) -> Gen Form -> Gen Form
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen Form
st
, (\Form
x -> [Form] -> Form
Xor [Form
x]) (Form -> Form) -> Gen Form -> Gen Form
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Form
st
, (\Form
x Form
y -> [Form] -> Form
Xor [Form
x,Form
y]) (Form -> Form -> Form) -> Gen Form -> Gen (Form -> Form)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Form
st Gen (Form -> Form) -> Gen Form -> Gen Form
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen Form
st
, (\Form
x Form
y Form
z -> [Form] -> Form
Xor [Form
x,Form
y,Form
z]) (Form -> Form -> Form -> Form)
-> Gen Form -> Gen (Form -> Form -> Form)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Form
st Gen (Form -> Form -> Form) -> Gen Form -> Gen (Form -> Form)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen Form
st Gen (Form -> Form) -> Gen Form -> Gen Form
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen Form
st
]
where
st :: Gen Form
st = a -> Gen Form
bf' (a
n a -> a -> a
forall a. Integral a => a -> a -> a
`div` a
3)
instance Arbitrary Form where
arbitrary :: Gen Form
arbitrary = (Int -> Gen Form) -> Gen Form
forall a. (Int -> Gen a) -> Gen a
sized Int -> Gen Form
forall {a}. Integral a => a -> Gen Form
form where
form :: t -> Gen Form
form t
0 = [Gen Form] -> Gen Form
forall a. [Gen a] -> Gen a
oneof [ Form -> Gen Form
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Form
Top
, Form -> Gen Form
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Form
Bot
, Prp -> Form
PrpF (Prp -> Form) -> Gen Prp -> Gen Form
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Prp
forall a. Arbitrary a => Gen a
arbitrary ]
form t
n = [Gen Form] -> Gen Form
forall a. [Gen a] -> Gen a
oneof [ Form -> Gen Form
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Form
SMCDEL.Language.Top
, Form -> Gen Form
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Form
SMCDEL.Language.Bot
, Prp -> Form
PrpF (Prp -> Form) -> Gen Prp -> Gen Form
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Prp
forall a. Arbitrary a => Gen a
arbitrary
, Form -> Form
Neg (Form -> Form) -> Gen Form -> Gen Form
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t -> Gen Form
form t
n'
, [Form] -> Form
Conj ([Form] -> Form) -> Gen [Form] -> Gen Form
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Form -> Gen [Form]
forall a. Gen a -> Gen [a]
listOf (t -> Gen Form
form t
n')
, [Form] -> Form
Disj ([Form] -> Form) -> Gen [Form] -> Gen Form
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Form -> Gen [Form]
forall a. Gen a -> Gen [a]
listOf (t -> Gen Form
form t
n')
, [Form] -> Form
Xor ([Form] -> Form) -> Gen [Form] -> Gen Form
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Form -> Gen [Form]
forall a. Gen a -> Gen [a]
listOf (t -> Gen Form
form t
n')
, Form -> Form -> Form
Impl (Form -> Form -> Form) -> Gen Form -> Gen (Form -> Form)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t -> Gen Form
form t
n' Gen (Form -> Form) -> Gen Form -> Gen Form
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> t -> Gen Form
form t
n'
, Form -> Form -> Form
Equi (Form -> Form -> Form) -> Gen Form -> Gen (Form -> Form)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t -> Gen Form
form t
n' Gen (Form -> Form) -> Gen Form -> Gen Form
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> t -> Gen Form
form t
n'
, Agent -> Form -> Form
K (Agent -> Form -> Form) -> Gen Agent -> Gen (Form -> Form)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Agent
arbitraryAg Gen (Form -> Form) -> Gen Form -> Gen Form
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> t -> Gen Form
form t
n'
, [Agent] -> Form -> Form
Ck ([Agent] -> Form -> Form) -> Gen [Agent] -> Gen (Form -> Form)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen [Agent]
arbitraryAgs Gen (Form -> Form) -> Gen Form -> Gen Form
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> t -> Gen Form
form t
n'
, [Agent] -> Form -> Form
Dk ([Agent] -> Form -> Form) -> Gen [Agent] -> Gen (Form -> Form)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen [Agent]
arbitraryAgs Gen (Form -> Form) -> Gen Form -> Gen Form
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> t -> Gen Form
form t
n'
, Agent -> Form -> Form
Kw (Agent -> Form -> Form) -> Gen Agent -> Gen (Form -> Form)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Agent
arbitraryAg Gen (Form -> Form) -> Gen Form -> Gen Form
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> t -> Gen Form
form t
n'
, [Agent] -> Form -> Form
Ckw ([Agent] -> Form -> Form) -> Gen [Agent] -> Gen (Form -> Form)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen [Agent]
arbitraryAgs Gen (Form -> Form) -> Gen Form -> Gen Form
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> t -> Gen Form
form t
n'
, [Agent] -> Form -> Form
Dkw ([Agent] -> Form -> Form) -> Gen [Agent] -> Gen (Form -> Form)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen [Agent]
arbitraryAgs Gen (Form -> Form) -> Gen Form -> Gen Form
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> t -> Gen Form
form t
n'
, Form -> Form -> Form
PubAnnounce (Form -> Form -> Form) -> Gen Form -> Gen (Form -> Form)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t -> Gen Form
form t
n' Gen (Form -> Form) -> Gen Form -> Gen Form
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> t -> Gen Form
form t
n'
, Form -> Form -> Form
PubAnnounceW (Form -> Form -> Form) -> Gen Form -> Gen (Form -> Form)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t -> Gen Form
form t
n' Gen (Form -> Form) -> Gen Form -> Gen Form
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> t -> Gen Form
form t
n'
, [Agent] -> Form -> Form -> Form
Announce ([Agent] -> Form -> Form -> Form)
-> Gen [Agent] -> Gen (Form -> Form -> Form)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen [Agent]
arbitraryAgs Gen (Form -> Form -> Form) -> Gen Form -> Gen (Form -> Form)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> t -> Gen Form
form t
n' Gen (Form -> Form) -> Gen Form -> Gen Form
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> t -> Gen Form
form t
n'
, [Agent] -> Form -> Form -> Form
AnnounceW ([Agent] -> Form -> Form -> Form)
-> Gen [Agent] -> Gen (Form -> Form -> Form)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen [Agent]
arbitraryAgs Gen (Form -> Form -> Form) -> Gen Form -> Gen (Form -> Form)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> t -> Gen Form
form t
n' Gen (Form -> Form) -> Gen Form -> Gen Form
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> t -> Gen Form
form t
n' ]
where
n' :: t
n' = t
n t -> t -> t
forall a. Integral a => a -> a -> a
`div` t
5
arbitraryAg :: Gen Agent
arbitraryAg = (\(Ag Agent
i) -> Agent
i) (AgAgent -> Agent) -> Gen AgAgent -> Gen Agent
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen AgAgent
forall a. Arbitrary a => Gen a
arbitrary
arbitraryAgs :: Gen [Agent]
arbitraryAgs = [Agent] -> Gen [Agent]
forall a. [a] -> Gen [a]
sublistOf ((Integer -> Agent) -> [Integer] -> [Agent]
forall a b. (a -> b) -> [a] -> [b]
map Integer -> Agent
forall a. Show a => a -> Agent
show [Integer
1..(Integer
5::Integer)]) Gen [Agent] -> ([Agent] -> Bool) -> Gen [Agent]
forall a. Gen a -> (a -> Bool) -> Gen a
`suchThat` (Bool -> Bool
not (Bool -> Bool) -> ([Agent] -> Bool) -> [Agent] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Agent] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null)
shrink :: Form -> [Form]
shrink = Form -> [Form]
shrinkform
newtype SimplifiedForm = SF Form deriving (SimplifiedForm -> SimplifiedForm -> Bool
(SimplifiedForm -> SimplifiedForm -> Bool)
-> (SimplifiedForm -> SimplifiedForm -> Bool) -> Eq SimplifiedForm
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SimplifiedForm -> SimplifiedForm -> Bool
== :: SimplifiedForm -> SimplifiedForm -> Bool
$c/= :: SimplifiedForm -> SimplifiedForm -> Bool
/= :: SimplifiedForm -> SimplifiedForm -> Bool
Eq,Eq SimplifiedForm
Eq SimplifiedForm =>
(SimplifiedForm -> SimplifiedForm -> Ordering)
-> (SimplifiedForm -> SimplifiedForm -> Bool)
-> (SimplifiedForm -> SimplifiedForm -> Bool)
-> (SimplifiedForm -> SimplifiedForm -> Bool)
-> (SimplifiedForm -> SimplifiedForm -> Bool)
-> (SimplifiedForm -> SimplifiedForm -> SimplifiedForm)
-> (SimplifiedForm -> SimplifiedForm -> SimplifiedForm)
-> Ord SimplifiedForm
SimplifiedForm -> SimplifiedForm -> Bool
SimplifiedForm -> SimplifiedForm -> Ordering
SimplifiedForm -> SimplifiedForm -> SimplifiedForm
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 :: SimplifiedForm -> SimplifiedForm -> Ordering
compare :: SimplifiedForm -> SimplifiedForm -> Ordering
$c< :: SimplifiedForm -> SimplifiedForm -> Bool
< :: SimplifiedForm -> SimplifiedForm -> Bool
$c<= :: SimplifiedForm -> SimplifiedForm -> Bool
<= :: SimplifiedForm -> SimplifiedForm -> Bool
$c> :: SimplifiedForm -> SimplifiedForm -> Bool
> :: SimplifiedForm -> SimplifiedForm -> Bool
$c>= :: SimplifiedForm -> SimplifiedForm -> Bool
>= :: SimplifiedForm -> SimplifiedForm -> Bool
$cmax :: SimplifiedForm -> SimplifiedForm -> SimplifiedForm
max :: SimplifiedForm -> SimplifiedForm -> SimplifiedForm
$cmin :: SimplifiedForm -> SimplifiedForm -> SimplifiedForm
min :: SimplifiedForm -> SimplifiedForm -> SimplifiedForm
Ord,Int -> SimplifiedForm -> ShowS
[SimplifiedForm] -> ShowS
SimplifiedForm -> Agent
(Int -> SimplifiedForm -> ShowS)
-> (SimplifiedForm -> Agent)
-> ([SimplifiedForm] -> ShowS)
-> Show SimplifiedForm
forall a.
(Int -> a -> ShowS) -> (a -> Agent) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SimplifiedForm -> ShowS
showsPrec :: Int -> SimplifiedForm -> ShowS
$cshow :: SimplifiedForm -> Agent
show :: SimplifiedForm -> Agent
$cshowList :: [SimplifiedForm] -> ShowS
showList :: [SimplifiedForm] -> ShowS
Show)
instance Arbitrary SimplifiedForm where
arbitrary :: Gen SimplifiedForm
arbitrary = Form -> SimplifiedForm
SF (Form -> SimplifiedForm)
-> (Form -> Form) -> Form -> SimplifiedForm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Form -> Form
simplify (Form -> SimplifiedForm) -> Gen Form -> Gen SimplifiedForm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Form
forall a. Arbitrary a => Gen a
arbitrary
shrink :: SimplifiedForm -> [SimplifiedForm]
shrink (SF Form
f) = [SimplifiedForm] -> [SimplifiedForm]
forall a. Eq a => [a] -> [a]
nub ([SimplifiedForm] -> [SimplifiedForm])
-> [SimplifiedForm] -> [SimplifiedForm]
forall a b. (a -> b) -> a -> b
$ (Form -> SimplifiedForm) -> [Form] -> [SimplifiedForm]
forall a b. (a -> b) -> [a] -> [b]
map (Form -> SimplifiedForm
SF (Form -> SimplifiedForm)
-> (Form -> Form) -> Form -> SimplifiedForm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Form -> Form
simplify) (Form -> [Form]
shrinkform Form
f)