{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses #-}

{- |
This module defines the language of Dynamic Epistemic Logic (DEL).
Keeping the syntax definition separate from the semantics allows us to use
the same language throughout the whole report, for both the explicit and
the symbolic model checkers.
-}

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

-- * Propositions and Agents

{- $
Propositions are represented as integers in Haskell.
Agents are strings.
-}

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"

-- | Five default agents given by `"1"` to `"5"`.
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)

-- generate a random group, always including agent 1
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"]

{- * Formulas
-}

{- $
The language \( \mathcal{L}(V) \) for a set of propositions \(V\) and a finite set of agents \(I\) is given by
  \[ \phi ::=
          \top   \mid  \bot  \mid  p
    \mid  \lnot \phi
    \mid  \bigwedge \Phi  \mid  \bigvee \Phi  \mid  \bigoplus \Phi
    \mid  \phi \rightarrow \phi  \mid  \phi \leftrightarrow \phi
    \mid  \forall P \phi  \mid  \exists P \phi
    \mid  K_i \phi  \mid  C_\Delta \phi \mid D_\Delta \phi
    \mid  [!\phi] \phi  \mid  [\Delta ! \phi] \phi \]
where \(p \in V\), \(P \subseteq V\), \(|P|<\omega\), \(\Phi\subseteq\mathcal{L}(V)\), \(|\Phi|<\omega\), \(i \in I\) and \(\Delta \subset I\).
We also write \(\phi \land \psi\) for \(\bigwedge \{ \phi,\psi \}\) and \(\phi \lor \psi\) for \(\bigvee \{ \phi,\psi \}\).
The \emph{boolean} formulas are those without \(K_i\), \(C_\Delta\), \(D_\Delta\), \([!\phi]\) and \([\Delta!\phi]\).

Hence, a formula can be (in this order):
The constant top or bottom, an atomic proposition, a negation, a conjunction, a disjunction, an exclusive or, an implication, a bi-implication, a universal or existential quantification over a set of propositions, or a statement about knowledge, common-knowledge, distributed knowledge, a public announcement or an announcement to a group.

Some of these connectives are inter-definable, for example \(\phi\leftrightarrow\psi\) and \(\bigwedge \{ \psi\rightarrow\phi,\phi\rightarrow\psi \}\) are equivalent according to all semantics which we will use here.
Hence we could shorten Definition~\ref{def-dellang} and treat some connectives as abbreviations.
This would lead to brevity and clarity in the formal definitions, but also to a decrease in performance of our model checking implementations.
To continue with the first example: If we have Binary Decision Diagrams (BDDs) for \(\phi\) and \(\psi\), computing the BDD for \(\phi\leftrightarrow\psi\) in one operation by calling the appropriate method of a BDD package will be faster than rewriting it to a conjunction of two implications and then making three calls to these corresponding functions of the BDD package.

We extend our language with abbreviations for "knowing whether" and "announcing whether".

\[ K^?_i \phi := \bigvee \{ K_i \phi , K_i (\lnot \phi) \} \]

\[ D^?_i \phi := \bigvee \{ D_i \phi , D_i (\lnot \phi) \} \]

\[ [?! \phi] \psi := \bigwedge \{ \phi \rightarrow [!\phi]\psi , \lnot \phi \rightarrow [!\lnot\phi]\psi \} \]

\[ [I ?! \phi] \psi := \bigwedge \{ \phi \rightarrow [I ! \phi]\psi , \lnot \phi \rightarrow [I !\lnot\phi]\psi \} \]

Note that - also for performance reasons - the three "whether" operators
occur as primitives and not as abbreviations.
-}

-- | Formulas
data Form
  = Top                         -- ^ True Constant
  | Bot                         -- ^ False Constant
  | PrpF Prp                    -- ^ Atomic Proposition
  | Neg Form                    -- ^ Negation
  | Conj [Form]                 -- ^ Conjunction
  | Disj [Form]                 -- ^ Disjunction
  | Xor [Form]                  -- ^ n-ary X-OR
  | Impl Form Form              -- ^ Implication
  | Equi Form Form              -- ^ Bi-Implication
  | Forall [Prp] Form           -- ^ Boolean Universal Quantification
  | Exists [Prp] Form           -- ^ Boolean Existential Quantification
  | K Agent Form                -- ^ Knowing that
  | Ck [Agent] Form             -- ^ Common knowing that
  | Dk [Agent] Form             -- ^ Distributed knowing that
  | Kw Agent Form               -- ^ Knowing whether
  | Ckw [Agent] Form            -- ^ Common knowing whether
  | Dkw [Agent] Form            -- ^ Distributed knowing whether
  | PubAnnounce Form Form       -- ^ Public announcement that
  | PubAnnounceW Form Form      -- ^ Public announcement whether
  | Announce [Agent] Form Form  -- ^ (Semi-)Private announcement that
  | AnnounceW [Agent] Form Form -- ^ (Semi-)Private announcement whether
  | Dia DynamicOp Form          -- ^ Dynamic Diamond
  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)

-- * Abbreviations

-- | If-Then-Else
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]

-- | Abbreviation for a sequence of announcements using.
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

-- | Abbreviation to say that exactly a given subset of a set of propositions is true.
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] ] ]


-- * Dynamic Operators

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
" _"

-- | The dynamic box operator
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))


-- * Typeclasses for Semantics

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

-- | The \(\vDash\) symbol for semantics.
(|=) :: 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

-- * Type classes for Updates

class HasPrecondition a where
  preOf :: a -> Form

-- | Formulas used as public announcements are their own precondition.
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 ]

-- | Execute a list of updates, return the final resulting state.
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

-- | Execute a list of updates, return the list of starting, intermediate and final result states.
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

-- | Check that two models/actions/etc. have the same agents.
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

-- * Pretty-printing

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)

-- | Pretty-print a formula.
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)

-- | Pretty-print a formula with a translation for atomic propositions.
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

-- | Generates LaTeX code for a formula.
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 and Shrinking

-- | List of subformulas, including the given formula itself.
-- In particular this is used in the `shrink` function for QuickCheck.
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
_ = []

-- * Substitution

-- | Substitute a formula for a proposition in a formula.
-- As a safety measure this method will fail whenever the proposition to be replaced occurs in a quantifier.
-- All other cases are done by recursion.
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."

-- | Apply multiple substitutions after each other.
-- Note: in general this is *not* the same as simultaneous substitution.
-- It is equivalent to simultaneous substitution if none of the
-- replaced propositions occurs in the replacement formulas.
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)

-- | The "out of" substitution \([A \sqsubseteq B]\phi\).
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)

-- | Replace propositions in a formula.
-- In contrast to the previous substitution function this *is* simultaneous.
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 -- TODO needs propsIn dynop!

-- * Vocabulary of a formula

-- | List of all propositions occurring in a formula.
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 -- TODO needs HasVocab dynop!

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

-- | List of all agents occurring in a formula.
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 -- TODO needs HasVocab dynop!

-- * Simplification

-- | Simplify a formula using boolean equivalences.
-- For example, remove double negations and ``bubble up'' \(\bot\)
-- and \(\top\) in conjunctions and disjunctions, respectively.
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 -- Not equivalent to Bot in K.
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 -- Not equivalent to Bot in K.
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)

{- $

==== __Example for simplify__

Consider this rather unnatural formula:

>>> let testForm = Forall [P 3] $ Equi (Disj [ Bot, PrpF $ P 3, Bot ]) (Conj [ Top , Xor [Top,Kw alice (PrpF (P 4))] , AnnounceW [alice,bob] (PrpF (P 5)) (Kw bob $ PrpF (P 5)) ])
>>> testForm
Forall [P 3] (Equi (Disj [Bot,PrpF (P 3),Bot]) (Conj [Top,Xor [Top,Kw "Alice" (PrpF (P 4))],AnnounceW ["Alice","Bob"] (PrpF (P 5)) (Kw "Bob" (PrpF (P 5)))]))
>>> simplify testForm
Forall [P 3] (Equi (PrpF (P 3)) (Conj [Xor [Top,Kw "Alice" (PrpF (P 4))],AnnounceW ["Alice","Bob"] (PrpF (P 5)) (Kw "Bob" (PrpF (P 5)))]))
-}

-- TODO: how to show TeX output in Haddock?

-- * Generating random formulas

-- | Boolean Formulas
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
                -- , (\p f -> Exists [p] f) <$> elements allprops <*> st
                -- , (\p f -> Forall [p] f) <$> elements allprops <*> 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)

-- | A general Arbitrary instance for formulas.
-- It is used heavily in the automated tests.
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)

-- | Simplified Formulas
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)