module Hermod.ReCon.LTL.Internal.Subst (
    substIntTerm
  , substTextTerm
  , substIntPropConstraint
  , substTextPropConstraint
  , substIntFormula
  , substTextFormula
  ) where

import           Hermod.ReCon.LTL.Formula

import qualified Data.Set as Set

-- The file concerns capture-avoiding substitution of an integer or text value
-- for a `VariableIdentifier` in formulas and their constituents.

-- | t[v / x]  (integer)
substIntTerm :: IntValue -> VariableIdentifier -> IntTerm -> IntTerm
substIntTerm :: IntValue -> VariableIdentifier -> IntTerm -> IntTerm
substIntTerm IntValue
v VariableIdentifier
x (IntVar IntValue
k VariableIdentifier
x') | VariableIdentifier
x VariableIdentifier -> VariableIdentifier -> Bool
forall a. Eq a => a -> a -> Bool
== VariableIdentifier
x' = IntValue -> IntTerm
IntConst (IntValue
k IntValue -> IntValue -> IntValue
forall a. Num a => a -> a -> a
* IntValue
v)
substIntTerm IntValue
v VariableIdentifier
x (IntSum IntTerm
a IntTerm
b)             = IntTerm -> IntTerm -> IntTerm
IntSum (IntValue -> VariableIdentifier -> IntTerm -> IntTerm
substIntTerm IntValue
v VariableIdentifier
x IntTerm
a) (IntValue -> VariableIdentifier -> IntTerm -> IntTerm
substIntTerm IntValue
v VariableIdentifier
x IntTerm
b)
substIntTerm IntValue
_ VariableIdentifier
_ IntTerm
t                        = IntTerm
t

-- | t[v / x]  (text)
substTextTerm :: TextValue -> VariableIdentifier -> TextTerm -> TextTerm
substTextTerm :: VariableIdentifier -> VariableIdentifier -> TextTerm -> TextTerm
substTextTerm VariableIdentifier
v VariableIdentifier
x (TextVar VariableIdentifier
x') | VariableIdentifier
x VariableIdentifier -> VariableIdentifier -> Bool
forall a. Eq a => a -> a -> Bool
== VariableIdentifier
x' = VariableIdentifier -> TextTerm
TextConst VariableIdentifier
v
substTextTerm VariableIdentifier
_ VariableIdentifier
_ TextTerm
t = TextTerm
t

-- | c[v / x]  (integer, propagates only into IntPropConstraint)
substIntPropConstraint :: IntValue -> VariableIdentifier -> PropConstraint -> PropConstraint
substIntPropConstraint :: IntValue -> VariableIdentifier -> PropConstraint -> PropConstraint
substIntPropConstraint IntValue
v VariableIdentifier
x (IntPropConstraint VariableIdentifier
k IntTerm
t)   = VariableIdentifier -> IntTerm -> PropConstraint
IntPropConstraint VariableIdentifier
k (IntValue -> VariableIdentifier -> IntTerm -> IntTerm
substIntTerm IntValue
v VariableIdentifier
x IntTerm
t)
substIntPropConstraint IntValue
_ VariableIdentifier
_ c :: PropConstraint
c@(TextPropConstraint {}) = PropConstraint
c

-- | c[v / x]  (text, propagates only into TextPropConstraint)
substTextPropConstraint :: TextValue -> VariableIdentifier -> PropConstraint -> PropConstraint
substTextPropConstraint :: VariableIdentifier
-> VariableIdentifier -> PropConstraint -> PropConstraint
substTextPropConstraint VariableIdentifier
v VariableIdentifier
x (TextPropConstraint VariableIdentifier
k TextTerm
t) = VariableIdentifier -> TextTerm -> PropConstraint
TextPropConstraint VariableIdentifier
k (VariableIdentifier -> VariableIdentifier -> TextTerm -> TextTerm
substTextTerm VariableIdentifier
v VariableIdentifier
x TextTerm
t)
substTextPropConstraint VariableIdentifier
_ VariableIdentifier
_ c :: PropConstraint
c@(IntPropConstraint {}) = PropConstraint
c

-- | φ[v / x]  (integer)
substIntFormula :: IntValue -> VariableIdentifier -> Formula event a -> Formula event a
substIntFormula :: forall event a.
IntValue
-> VariableIdentifier -> Formula event a -> Formula event a
substIntFormula IntValue
v VariableIdentifier
x (Forall Word
k Formula event a
phi) = Word -> Formula event a -> Formula event a
forall event ty. Word -> Formula event ty -> Formula event ty
Forall Word
k (IntValue
-> VariableIdentifier -> Formula event a -> Formula event a
forall event a.
IntValue
-> VariableIdentifier -> Formula event a -> Formula event a
substIntFormula IntValue
v VariableIdentifier
x Formula event a
phi)
substIntFormula IntValue
v VariableIdentifier
x (ForallN Word
k Formula event a
phi) = Word -> Formula event a -> Formula event a
forall event ty. Word -> Formula event ty -> Formula event ty
ForallN Word
k (IntValue
-> VariableIdentifier -> Formula event a -> Formula event a
forall event a.
IntValue
-> VariableIdentifier -> Formula event a -> Formula event a
substIntFormula IntValue
v VariableIdentifier
x Formula event a
phi)
substIntFormula IntValue
v VariableIdentifier
x (ExistsN Word
k Formula event a
phi) = Word -> Formula event a -> Formula event a
forall event ty. Word -> Formula event ty -> Formula event ty
ExistsN Word
k (IntValue
-> VariableIdentifier -> Formula event a -> Formula event a
forall event a.
IntValue
-> VariableIdentifier -> Formula event a -> Formula event a
substIntFormula IntValue
v VariableIdentifier
x Formula event a
phi)
substIntFormula IntValue
v VariableIdentifier
x (Next Formula event a
phi) = Formula event a -> Formula event a
forall event ty. Formula event ty -> Formula event ty
Next (IntValue
-> VariableIdentifier -> Formula event a -> Formula event a
forall event a.
IntValue
-> VariableIdentifier -> Formula event a -> Formula event a
substIntFormula IntValue
v VariableIdentifier
x Formula event a
phi)
substIntFormula IntValue
v VariableIdentifier
x (NextN Word
k Formula event a
phi) = Word -> Formula event a -> Formula event a
forall event ty. Word -> Formula event ty -> Formula event ty
NextN Word
k (IntValue
-> VariableIdentifier -> Formula event a -> Formula event a
forall event a.
IntValue
-> VariableIdentifier -> Formula event a -> Formula event a
substIntFormula IntValue
v VariableIdentifier
x Formula event a
phi)
substIntFormula IntValue
v VariableIdentifier
x (UntilN Word
k Formula event a
phi Formula event a
psi) = Word -> Formula event a -> Formula event a -> Formula event a
forall event ty.
Word -> Formula event ty -> Formula event ty -> Formula event ty
UntilN Word
k (IntValue
-> VariableIdentifier -> Formula event a -> Formula event a
forall event a.
IntValue
-> VariableIdentifier -> Formula event a -> Formula event a
substIntFormula IntValue
v VariableIdentifier
x Formula event a
phi) (IntValue
-> VariableIdentifier -> Formula event a -> Formula event a
forall event a.
IntValue
-> VariableIdentifier -> Formula event a -> Formula event a
substIntFormula IntValue
v VariableIdentifier
x Formula event a
psi)
substIntFormula IntValue
v VariableIdentifier
x (Atom a
c Set PropConstraint
is) = a -> Set PropConstraint -> Formula event a
forall event ty. ty -> Set PropConstraint -> Formula event ty
Atom a
c ((PropConstraint -> PropConstraint)
-> Set PropConstraint -> Set PropConstraint
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (IntValue -> VariableIdentifier -> PropConstraint -> PropConstraint
substIntPropConstraint IntValue
v VariableIdentifier
x) Set PropConstraint
is)
substIntFormula IntValue
v VariableIdentifier
x (And Formula event a
phi Formula event a
psi) = Formula event a -> Formula event a -> Formula event a
forall event ty.
Formula event ty -> Formula event ty -> Formula event ty
And (IntValue
-> VariableIdentifier -> Formula event a -> Formula event a
forall event a.
IntValue
-> VariableIdentifier -> Formula event a -> Formula event a
substIntFormula IntValue
v VariableIdentifier
x Formula event a
phi) (IntValue
-> VariableIdentifier -> Formula event a -> Formula event a
forall event a.
IntValue
-> VariableIdentifier -> Formula event a -> Formula event a
substIntFormula IntValue
v VariableIdentifier
x Formula event a
psi)
substIntFormula IntValue
v VariableIdentifier
x (Or Formula event a
phi Formula event a
psi) = Formula event a -> Formula event a -> Formula event a
forall event ty.
Formula event ty -> Formula event ty -> Formula event ty
Or (IntValue
-> VariableIdentifier -> Formula event a -> Formula event a
forall event a.
IntValue
-> VariableIdentifier -> Formula event a -> Formula event a
substIntFormula IntValue
v VariableIdentifier
x Formula event a
phi) (IntValue
-> VariableIdentifier -> Formula event a -> Formula event a
forall event a.
IntValue
-> VariableIdentifier -> Formula event a -> Formula event a
substIntFormula IntValue
v VariableIdentifier
x Formula event a
psi)
substIntFormula IntValue
v VariableIdentifier
x (Implies Formula event a
phi Formula event a
psi) = Formula event a -> Formula event a -> Formula event a
forall event ty.
Formula event ty -> Formula event ty -> Formula event ty
Implies (IntValue
-> VariableIdentifier -> Formula event a -> Formula event a
forall event a.
IntValue
-> VariableIdentifier -> Formula event a -> Formula event a
substIntFormula IntValue
v VariableIdentifier
x Formula event a
phi) (IntValue
-> VariableIdentifier -> Formula event a -> Formula event a
forall event a.
IntValue
-> VariableIdentifier -> Formula event a -> Formula event a
substIntFormula IntValue
v VariableIdentifier
x Formula event a
psi)
substIntFormula IntValue
v VariableIdentifier
x (Not Formula event a
phi) = Formula event a -> Formula event a
forall event ty. Formula event ty -> Formula event ty
Not (IntValue
-> VariableIdentifier -> Formula event a -> Formula event a
forall event a.
IntValue
-> VariableIdentifier -> Formula event a -> Formula event a
substIntFormula IntValue
v VariableIdentifier
x Formula event a
phi)
substIntFormula IntValue
_ VariableIdentifier
_ Formula event a
Bottom = Formula event a
forall event ty. Formula event ty
Bottom
substIntFormula IntValue
_ VariableIdentifier
_ Formula event a
Top = Formula event a
forall event ty. Formula event ty
Top
substIntFormula IntValue
_ VariableIdentifier
x (PropIntForall VariableIdentifier
x' Formula event a
e)  | VariableIdentifier
x VariableIdentifier -> VariableIdentifier -> Bool
forall a. Eq a => a -> a -> Bool
== VariableIdentifier
x' = VariableIdentifier -> Formula event a -> Formula event a
forall event ty.
VariableIdentifier -> Formula event ty -> Formula event ty
PropIntForall VariableIdentifier
x' Formula event a
e
substIntFormula IntValue
v VariableIdentifier
x (PropIntForall VariableIdentifier
x' Formula event a
e)             = VariableIdentifier -> Formula event a -> Formula event a
forall event ty.
VariableIdentifier -> Formula event ty -> Formula event ty
PropIntForall VariableIdentifier
x' (IntValue
-> VariableIdentifier -> Formula event a -> Formula event a
forall event a.
IntValue
-> VariableIdentifier -> Formula event a -> Formula event a
substIntFormula IntValue
v VariableIdentifier
x Formula event a
e)
substIntFormula IntValue
_ VariableIdentifier
x (PropTextForall VariableIdentifier
x' Formula event a
e) | VariableIdentifier
x VariableIdentifier -> VariableIdentifier -> Bool
forall a. Eq a => a -> a -> Bool
== VariableIdentifier
x' = VariableIdentifier -> Formula event a -> Formula event a
forall event ty.
VariableIdentifier -> Formula event ty -> Formula event ty
PropTextForall VariableIdentifier
x' Formula event a
e
substIntFormula IntValue
v VariableIdentifier
x (PropTextForall VariableIdentifier
x' Formula event a
e)            = VariableIdentifier -> Formula event a -> Formula event a
forall event ty.
VariableIdentifier -> Formula event ty -> Formula event ty
PropTextForall VariableIdentifier
x' (IntValue
-> VariableIdentifier -> Formula event a -> Formula event a
forall event a.
IntValue
-> VariableIdentifier -> Formula event a -> Formula event a
substIntFormula IntValue
v VariableIdentifier
x Formula event a
e)
substIntFormula IntValue
_ VariableIdentifier
x (PropIntForallN VariableIdentifier
x' Set IntValue
dom Formula event a
e)  | VariableIdentifier
x VariableIdentifier -> VariableIdentifier -> Bool
forall a. Eq a => a -> a -> Bool
== VariableIdentifier
x' = VariableIdentifier
-> Set IntValue -> Formula event a -> Formula event a
forall event ty.
VariableIdentifier
-> Set IntValue -> Formula event ty -> Formula event ty
PropIntForallN VariableIdentifier
x' Set IntValue
dom Formula event a
e
substIntFormula IntValue
v VariableIdentifier
x (PropIntForallN VariableIdentifier
x' Set IntValue
dom Formula event a
e)             = VariableIdentifier
-> Set IntValue -> Formula event a -> Formula event a
forall event ty.
VariableIdentifier
-> Set IntValue -> Formula event ty -> Formula event ty
PropIntForallN VariableIdentifier
x' Set IntValue
dom (IntValue
-> VariableIdentifier -> Formula event a -> Formula event a
forall event a.
IntValue
-> VariableIdentifier -> Formula event a -> Formula event a
substIntFormula IntValue
v VariableIdentifier
x Formula event a
e)
substIntFormula IntValue
_ VariableIdentifier
x (PropTextForallN VariableIdentifier
x' Set VariableIdentifier
dom Formula event a
e) | VariableIdentifier
x VariableIdentifier -> VariableIdentifier -> Bool
forall a. Eq a => a -> a -> Bool
== VariableIdentifier
x' = VariableIdentifier
-> Set VariableIdentifier -> Formula event a -> Formula event a
forall event ty.
VariableIdentifier
-> Set VariableIdentifier -> Formula event ty -> Formula event ty
PropTextForallN VariableIdentifier
x' Set VariableIdentifier
dom Formula event a
e
substIntFormula IntValue
v VariableIdentifier
x (PropTextForallN VariableIdentifier
x' Set VariableIdentifier
dom Formula event a
e)            = VariableIdentifier
-> Set VariableIdentifier -> Formula event a -> Formula event a
forall event ty.
VariableIdentifier
-> Set VariableIdentifier -> Formula event ty -> Formula event ty
PropTextForallN VariableIdentifier
x' Set VariableIdentifier
dom (IntValue
-> VariableIdentifier -> Formula event a -> Formula event a
forall event a.
IntValue
-> VariableIdentifier -> Formula event a -> Formula event a
substIntFormula IntValue
v VariableIdentifier
x Formula event a
e)
substIntFormula IntValue
_ VariableIdentifier
x (PropIntExists VariableIdentifier
x' Formula event a
e)  | VariableIdentifier
x VariableIdentifier -> VariableIdentifier -> Bool
forall a. Eq a => a -> a -> Bool
== VariableIdentifier
x' = VariableIdentifier -> Formula event a -> Formula event a
forall event ty.
VariableIdentifier -> Formula event ty -> Formula event ty
PropIntExists VariableIdentifier
x' Formula event a
e
substIntFormula IntValue
v VariableIdentifier
x (PropIntExists VariableIdentifier
x' Formula event a
e)             = VariableIdentifier -> Formula event a -> Formula event a
forall event ty.
VariableIdentifier -> Formula event ty -> Formula event ty
PropIntExists VariableIdentifier
x' (IntValue
-> VariableIdentifier -> Formula event a -> Formula event a
forall event a.
IntValue
-> VariableIdentifier -> Formula event a -> Formula event a
substIntFormula IntValue
v VariableIdentifier
x Formula event a
e)
substIntFormula IntValue
_ VariableIdentifier
x (PropTextExists VariableIdentifier
x' Formula event a
e) | VariableIdentifier
x VariableIdentifier -> VariableIdentifier -> Bool
forall a. Eq a => a -> a -> Bool
== VariableIdentifier
x' = VariableIdentifier -> Formula event a -> Formula event a
forall event ty.
VariableIdentifier -> Formula event ty -> Formula event ty
PropTextExists VariableIdentifier
x' Formula event a
e
substIntFormula IntValue
v VariableIdentifier
x (PropTextExists VariableIdentifier
x' Formula event a
e)            = VariableIdentifier -> Formula event a -> Formula event a
forall event ty.
VariableIdentifier -> Formula event ty -> Formula event ty
PropTextExists VariableIdentifier
x' (IntValue
-> VariableIdentifier -> Formula event a -> Formula event a
forall event a.
IntValue
-> VariableIdentifier -> Formula event a -> Formula event a
substIntFormula IntValue
v VariableIdentifier
x Formula event a
e)
substIntFormula IntValue
_ VariableIdentifier
x (PropIntExistsN VariableIdentifier
x' Set IntValue
dom Formula event a
e)  | VariableIdentifier
x VariableIdentifier -> VariableIdentifier -> Bool
forall a. Eq a => a -> a -> Bool
== VariableIdentifier
x' = VariableIdentifier
-> Set IntValue -> Formula event a -> Formula event a
forall event ty.
VariableIdentifier
-> Set IntValue -> Formula event ty -> Formula event ty
PropIntExistsN VariableIdentifier
x' Set IntValue
dom Formula event a
e
substIntFormula IntValue
v VariableIdentifier
x (PropIntExistsN VariableIdentifier
x' Set IntValue
dom Formula event a
e)             = VariableIdentifier
-> Set IntValue -> Formula event a -> Formula event a
forall event ty.
VariableIdentifier
-> Set IntValue -> Formula event ty -> Formula event ty
PropIntExistsN VariableIdentifier
x' Set IntValue
dom (IntValue
-> VariableIdentifier -> Formula event a -> Formula event a
forall event a.
IntValue
-> VariableIdentifier -> Formula event a -> Formula event a
substIntFormula IntValue
v VariableIdentifier
x Formula event a
e)
substIntFormula IntValue
_ VariableIdentifier
x (PropTextExistsN VariableIdentifier
x' Set VariableIdentifier
dom Formula event a
e) | VariableIdentifier
x VariableIdentifier -> VariableIdentifier -> Bool
forall a. Eq a => a -> a -> Bool
== VariableIdentifier
x' = VariableIdentifier
-> Set VariableIdentifier -> Formula event a -> Formula event a
forall event ty.
VariableIdentifier
-> Set VariableIdentifier -> Formula event ty -> Formula event ty
PropTextExistsN VariableIdentifier
x' Set VariableIdentifier
dom Formula event a
e
substIntFormula IntValue
v VariableIdentifier
x (PropTextExistsN VariableIdentifier
x' Set VariableIdentifier
dom Formula event a
e)            = VariableIdentifier
-> Set VariableIdentifier -> Formula event a -> Formula event a
forall event ty.
VariableIdentifier
-> Set VariableIdentifier -> Formula event ty -> Formula event ty
PropTextExistsN VariableIdentifier
x' Set VariableIdentifier
dom (IntValue
-> VariableIdentifier -> Formula event a -> Formula event a
forall event a.
IntValue
-> VariableIdentifier -> Formula event a -> Formula event a
substIntFormula IntValue
v VariableIdentifier
x Formula event a
e)
substIntFormula IntValue
v VariableIdentifier
x (PropIntBinRel BinRel
rel Relevance event a
r IntTerm
lhs IntTerm
rhs) = BinRel
-> Relevance event a -> IntTerm -> IntTerm -> Formula event a
forall event ty.
BinRel
-> Relevance event ty -> IntTerm -> IntTerm -> Formula event ty
PropIntBinRel BinRel
rel Relevance event a
r (IntValue -> VariableIdentifier -> IntTerm -> IntTerm
substIntTerm IntValue
v VariableIdentifier
x IntTerm
lhs) (IntValue -> VariableIdentifier -> IntTerm -> IntTerm
substIntTerm IntValue
v VariableIdentifier
x IntTerm
rhs)
substIntFormula IntValue
_ VariableIdentifier
_ (PropTextEq Relevance event a
rel TextTerm
t VariableIdentifier
rhs)        = Relevance event a
-> TextTerm -> VariableIdentifier -> Formula event a
forall event ty.
Relevance event ty
-> TextTerm -> VariableIdentifier -> Formula event ty
PropTextEq Relevance event a
rel TextTerm
t VariableIdentifier
rhs

-- | φ[v / x]  (text)
substTextFormula :: TextValue -> VariableIdentifier -> Formula event a -> Formula event a
substTextFormula :: forall event a.
VariableIdentifier
-> VariableIdentifier -> Formula event a -> Formula event a
substTextFormula VariableIdentifier
v VariableIdentifier
x (Forall Word
k Formula event a
phi) = Word -> Formula event a -> Formula event a
forall event ty. Word -> Formula event ty -> Formula event ty
Forall Word
k (VariableIdentifier
-> VariableIdentifier -> Formula event a -> Formula event a
forall event a.
VariableIdentifier
-> VariableIdentifier -> Formula event a -> Formula event a
substTextFormula VariableIdentifier
v VariableIdentifier
x Formula event a
phi)
substTextFormula VariableIdentifier
v VariableIdentifier
x (ForallN Word
k Formula event a
phi) = Word -> Formula event a -> Formula event a
forall event ty. Word -> Formula event ty -> Formula event ty
ForallN Word
k (VariableIdentifier
-> VariableIdentifier -> Formula event a -> Formula event a
forall event a.
VariableIdentifier
-> VariableIdentifier -> Formula event a -> Formula event a
substTextFormula VariableIdentifier
v VariableIdentifier
x Formula event a
phi)
substTextFormula VariableIdentifier
v VariableIdentifier
x (ExistsN Word
k Formula event a
phi) = Word -> Formula event a -> Formula event a
forall event ty. Word -> Formula event ty -> Formula event ty
ExistsN Word
k (VariableIdentifier
-> VariableIdentifier -> Formula event a -> Formula event a
forall event a.
VariableIdentifier
-> VariableIdentifier -> Formula event a -> Formula event a
substTextFormula VariableIdentifier
v VariableIdentifier
x Formula event a
phi)
substTextFormula VariableIdentifier
v VariableIdentifier
x (Next Formula event a
phi) = Formula event a -> Formula event a
forall event ty. Formula event ty -> Formula event ty
Next (VariableIdentifier
-> VariableIdentifier -> Formula event a -> Formula event a
forall event a.
VariableIdentifier
-> VariableIdentifier -> Formula event a -> Formula event a
substTextFormula VariableIdentifier
v VariableIdentifier
x Formula event a
phi)
substTextFormula VariableIdentifier
v VariableIdentifier
x (NextN Word
k Formula event a
phi) = Word -> Formula event a -> Formula event a
forall event ty. Word -> Formula event ty -> Formula event ty
NextN Word
k (VariableIdentifier
-> VariableIdentifier -> Formula event a -> Formula event a
forall event a.
VariableIdentifier
-> VariableIdentifier -> Formula event a -> Formula event a
substTextFormula VariableIdentifier
v VariableIdentifier
x Formula event a
phi)
substTextFormula VariableIdentifier
v VariableIdentifier
x (UntilN Word
k Formula event a
phi Formula event a
psi) = Word -> Formula event a -> Formula event a -> Formula event a
forall event ty.
Word -> Formula event ty -> Formula event ty -> Formula event ty
UntilN Word
k (VariableIdentifier
-> VariableIdentifier -> Formula event a -> Formula event a
forall event a.
VariableIdentifier
-> VariableIdentifier -> Formula event a -> Formula event a
substTextFormula VariableIdentifier
v VariableIdentifier
x Formula event a
phi) (VariableIdentifier
-> VariableIdentifier -> Formula event a -> Formula event a
forall event a.
VariableIdentifier
-> VariableIdentifier -> Formula event a -> Formula event a
substTextFormula VariableIdentifier
v VariableIdentifier
x Formula event a
psi)
substTextFormula VariableIdentifier
v VariableIdentifier
x (Atom a
c Set PropConstraint
is) = a -> Set PropConstraint -> Formula event a
forall event ty. ty -> Set PropConstraint -> Formula event ty
Atom a
c ((PropConstraint -> PropConstraint)
-> Set PropConstraint -> Set PropConstraint
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (VariableIdentifier
-> VariableIdentifier -> PropConstraint -> PropConstraint
substTextPropConstraint VariableIdentifier
v VariableIdentifier
x) Set PropConstraint
is)
substTextFormula VariableIdentifier
v VariableIdentifier
x (And Formula event a
phi Formula event a
psi) = Formula event a -> Formula event a -> Formula event a
forall event ty.
Formula event ty -> Formula event ty -> Formula event ty
And (VariableIdentifier
-> VariableIdentifier -> Formula event a -> Formula event a
forall event a.
VariableIdentifier
-> VariableIdentifier -> Formula event a -> Formula event a
substTextFormula VariableIdentifier
v VariableIdentifier
x Formula event a
phi) (VariableIdentifier
-> VariableIdentifier -> Formula event a -> Formula event a
forall event a.
VariableIdentifier
-> VariableIdentifier -> Formula event a -> Formula event a
substTextFormula VariableIdentifier
v VariableIdentifier
x Formula event a
psi)
substTextFormula VariableIdentifier
v VariableIdentifier
x (Or Formula event a
phi Formula event a
psi) = Formula event a -> Formula event a -> Formula event a
forall event ty.
Formula event ty -> Formula event ty -> Formula event ty
Or (VariableIdentifier
-> VariableIdentifier -> Formula event a -> Formula event a
forall event a.
VariableIdentifier
-> VariableIdentifier -> Formula event a -> Formula event a
substTextFormula VariableIdentifier
v VariableIdentifier
x Formula event a
phi) (VariableIdentifier
-> VariableIdentifier -> Formula event a -> Formula event a
forall event a.
VariableIdentifier
-> VariableIdentifier -> Formula event a -> Formula event a
substTextFormula VariableIdentifier
v VariableIdentifier
x Formula event a
psi)
substTextFormula VariableIdentifier
v VariableIdentifier
x (Implies Formula event a
phi Formula event a
psi) = Formula event a -> Formula event a -> Formula event a
forall event ty.
Formula event ty -> Formula event ty -> Formula event ty
Implies (VariableIdentifier
-> VariableIdentifier -> Formula event a -> Formula event a
forall event a.
VariableIdentifier
-> VariableIdentifier -> Formula event a -> Formula event a
substTextFormula VariableIdentifier
v VariableIdentifier
x Formula event a
phi) (VariableIdentifier
-> VariableIdentifier -> Formula event a -> Formula event a
forall event a.
VariableIdentifier
-> VariableIdentifier -> Formula event a -> Formula event a
substTextFormula VariableIdentifier
v VariableIdentifier
x Formula event a
psi)
substTextFormula VariableIdentifier
v VariableIdentifier
x (Not Formula event a
phi) = Formula event a -> Formula event a
forall event ty. Formula event ty -> Formula event ty
Not (VariableIdentifier
-> VariableIdentifier -> Formula event a -> Formula event a
forall event a.
VariableIdentifier
-> VariableIdentifier -> Formula event a -> Formula event a
substTextFormula VariableIdentifier
v VariableIdentifier
x Formula event a
phi)
substTextFormula VariableIdentifier
_ VariableIdentifier
_ Formula event a
Bottom = Formula event a
forall event ty. Formula event ty
Bottom
substTextFormula VariableIdentifier
_ VariableIdentifier
_ Formula event a
Top = Formula event a
forall event ty. Formula event ty
Top
substTextFormula VariableIdentifier
_ VariableIdentifier
x (PropIntForall VariableIdentifier
x' Formula event a
e)  | VariableIdentifier
x VariableIdentifier -> VariableIdentifier -> Bool
forall a. Eq a => a -> a -> Bool
== VariableIdentifier
x' = VariableIdentifier -> Formula event a -> Formula event a
forall event ty.
VariableIdentifier -> Formula event ty -> Formula event ty
PropIntForall VariableIdentifier
x' Formula event a
e
substTextFormula VariableIdentifier
v VariableIdentifier
x (PropIntForall VariableIdentifier
x' Formula event a
e)             = VariableIdentifier -> Formula event a -> Formula event a
forall event ty.
VariableIdentifier -> Formula event ty -> Formula event ty
PropIntForall VariableIdentifier
x' (VariableIdentifier
-> VariableIdentifier -> Formula event a -> Formula event a
forall event a.
VariableIdentifier
-> VariableIdentifier -> Formula event a -> Formula event a
substTextFormula VariableIdentifier
v VariableIdentifier
x Formula event a
e)
substTextFormula VariableIdentifier
_ VariableIdentifier
x (PropTextForall VariableIdentifier
x' Formula event a
e) | VariableIdentifier
x VariableIdentifier -> VariableIdentifier -> Bool
forall a. Eq a => a -> a -> Bool
== VariableIdentifier
x' = VariableIdentifier -> Formula event a -> Formula event a
forall event ty.
VariableIdentifier -> Formula event ty -> Formula event ty
PropTextForall VariableIdentifier
x' Formula event a
e
substTextFormula VariableIdentifier
v VariableIdentifier
x (PropTextForall VariableIdentifier
x' Formula event a
e)            = VariableIdentifier -> Formula event a -> Formula event a
forall event ty.
VariableIdentifier -> Formula event ty -> Formula event ty
PropTextForall VariableIdentifier
x' (VariableIdentifier
-> VariableIdentifier -> Formula event a -> Formula event a
forall event a.
VariableIdentifier
-> VariableIdentifier -> Formula event a -> Formula event a
substTextFormula VariableIdentifier
v VariableIdentifier
x Formula event a
e)
substTextFormula VariableIdentifier
_ VariableIdentifier
x (PropIntForallN VariableIdentifier
x' Set IntValue
dom Formula event a
e)  | VariableIdentifier
x VariableIdentifier -> VariableIdentifier -> Bool
forall a. Eq a => a -> a -> Bool
== VariableIdentifier
x' = VariableIdentifier
-> Set IntValue -> Formula event a -> Formula event a
forall event ty.
VariableIdentifier
-> Set IntValue -> Formula event ty -> Formula event ty
PropIntForallN VariableIdentifier
x' Set IntValue
dom Formula event a
e
substTextFormula VariableIdentifier
v VariableIdentifier
x (PropIntForallN VariableIdentifier
x' Set IntValue
dom Formula event a
e)             = VariableIdentifier
-> Set IntValue -> Formula event a -> Formula event a
forall event ty.
VariableIdentifier
-> Set IntValue -> Formula event ty -> Formula event ty
PropIntForallN VariableIdentifier
x' Set IntValue
dom (VariableIdentifier
-> VariableIdentifier -> Formula event a -> Formula event a
forall event a.
VariableIdentifier
-> VariableIdentifier -> Formula event a -> Formula event a
substTextFormula VariableIdentifier
v VariableIdentifier
x Formula event a
e)
substTextFormula VariableIdentifier
_ VariableIdentifier
x (PropTextForallN VariableIdentifier
x' Set VariableIdentifier
dom Formula event a
e) | VariableIdentifier
x VariableIdentifier -> VariableIdentifier -> Bool
forall a. Eq a => a -> a -> Bool
== VariableIdentifier
x' = VariableIdentifier
-> Set VariableIdentifier -> Formula event a -> Formula event a
forall event ty.
VariableIdentifier
-> Set VariableIdentifier -> Formula event ty -> Formula event ty
PropTextForallN VariableIdentifier
x' Set VariableIdentifier
dom Formula event a
e
substTextFormula VariableIdentifier
v VariableIdentifier
x (PropTextForallN VariableIdentifier
x' Set VariableIdentifier
dom Formula event a
e)            = VariableIdentifier
-> Set VariableIdentifier -> Formula event a -> Formula event a
forall event ty.
VariableIdentifier
-> Set VariableIdentifier -> Formula event ty -> Formula event ty
PropTextForallN VariableIdentifier
x' Set VariableIdentifier
dom (VariableIdentifier
-> VariableIdentifier -> Formula event a -> Formula event a
forall event a.
VariableIdentifier
-> VariableIdentifier -> Formula event a -> Formula event a
substTextFormula VariableIdentifier
v VariableIdentifier
x Formula event a
e)
substTextFormula VariableIdentifier
_ VariableIdentifier
x (PropIntExists VariableIdentifier
x' Formula event a
e)  | VariableIdentifier
x VariableIdentifier -> VariableIdentifier -> Bool
forall a. Eq a => a -> a -> Bool
== VariableIdentifier
x' = VariableIdentifier -> Formula event a -> Formula event a
forall event ty.
VariableIdentifier -> Formula event ty -> Formula event ty
PropIntExists VariableIdentifier
x' Formula event a
e
substTextFormula VariableIdentifier
v VariableIdentifier
x (PropIntExists VariableIdentifier
x' Formula event a
e)             = VariableIdentifier -> Formula event a -> Formula event a
forall event ty.
VariableIdentifier -> Formula event ty -> Formula event ty
PropIntExists VariableIdentifier
x' (VariableIdentifier
-> VariableIdentifier -> Formula event a -> Formula event a
forall event a.
VariableIdentifier
-> VariableIdentifier -> Formula event a -> Formula event a
substTextFormula VariableIdentifier
v VariableIdentifier
x Formula event a
e)
substTextFormula VariableIdentifier
_ VariableIdentifier
x (PropTextExists VariableIdentifier
x' Formula event a
e) | VariableIdentifier
x VariableIdentifier -> VariableIdentifier -> Bool
forall a. Eq a => a -> a -> Bool
== VariableIdentifier
x' = VariableIdentifier -> Formula event a -> Formula event a
forall event ty.
VariableIdentifier -> Formula event ty -> Formula event ty
PropTextExists VariableIdentifier
x' Formula event a
e
substTextFormula VariableIdentifier
v VariableIdentifier
x (PropTextExists VariableIdentifier
x' Formula event a
e)            = VariableIdentifier -> Formula event a -> Formula event a
forall event ty.
VariableIdentifier -> Formula event ty -> Formula event ty
PropTextExists VariableIdentifier
x' (VariableIdentifier
-> VariableIdentifier -> Formula event a -> Formula event a
forall event a.
VariableIdentifier
-> VariableIdentifier -> Formula event a -> Formula event a
substTextFormula VariableIdentifier
v VariableIdentifier
x Formula event a
e)
substTextFormula VariableIdentifier
_ VariableIdentifier
x (PropIntExistsN VariableIdentifier
x' Set IntValue
dom Formula event a
e)  | VariableIdentifier
x VariableIdentifier -> VariableIdentifier -> Bool
forall a. Eq a => a -> a -> Bool
== VariableIdentifier
x' = VariableIdentifier
-> Set IntValue -> Formula event a -> Formula event a
forall event ty.
VariableIdentifier
-> Set IntValue -> Formula event ty -> Formula event ty
PropIntExistsN VariableIdentifier
x' Set IntValue
dom Formula event a
e
substTextFormula VariableIdentifier
v VariableIdentifier
x (PropIntExistsN VariableIdentifier
x' Set IntValue
dom Formula event a
e)             = VariableIdentifier
-> Set IntValue -> Formula event a -> Formula event a
forall event ty.
VariableIdentifier
-> Set IntValue -> Formula event ty -> Formula event ty
PropIntExistsN VariableIdentifier
x' Set IntValue
dom (VariableIdentifier
-> VariableIdentifier -> Formula event a -> Formula event a
forall event a.
VariableIdentifier
-> VariableIdentifier -> Formula event a -> Formula event a
substTextFormula VariableIdentifier
v VariableIdentifier
x Formula event a
e)
substTextFormula VariableIdentifier
_ VariableIdentifier
x (PropTextExistsN VariableIdentifier
x' Set VariableIdentifier
dom Formula event a
e) | VariableIdentifier
x VariableIdentifier -> VariableIdentifier -> Bool
forall a. Eq a => a -> a -> Bool
== VariableIdentifier
x' = VariableIdentifier
-> Set VariableIdentifier -> Formula event a -> Formula event a
forall event ty.
VariableIdentifier
-> Set VariableIdentifier -> Formula event ty -> Formula event ty
PropTextExistsN VariableIdentifier
x' Set VariableIdentifier
dom Formula event a
e
substTextFormula VariableIdentifier
v VariableIdentifier
x (PropTextExistsN VariableIdentifier
x' Set VariableIdentifier
dom Formula event a
e)            = VariableIdentifier
-> Set VariableIdentifier -> Formula event a -> Formula event a
forall event ty.
VariableIdentifier
-> Set VariableIdentifier -> Formula event ty -> Formula event ty
PropTextExistsN VariableIdentifier
x' Set VariableIdentifier
dom (VariableIdentifier
-> VariableIdentifier -> Formula event a -> Formula event a
forall event a.
VariableIdentifier
-> VariableIdentifier -> Formula event a -> Formula event a
substTextFormula VariableIdentifier
v VariableIdentifier
x Formula event a
e)
substTextFormula VariableIdentifier
_ VariableIdentifier
_ (PropIntBinRel BinRel
rel Relevance event a
r IntTerm
t IntTerm
rhs) = BinRel
-> Relevance event a -> IntTerm -> IntTerm -> Formula event a
forall event ty.
BinRel
-> Relevance event ty -> IntTerm -> IntTerm -> Formula event ty
PropIntBinRel BinRel
rel Relevance event a
r IntTerm
t IntTerm
rhs
substTextFormula VariableIdentifier
v VariableIdentifier
x (PropTextEq Relevance event a
rel TextTerm
t VariableIdentifier
rhs)      = Relevance event a
-> TextTerm -> VariableIdentifier -> Formula event a
forall event ty.
Relevance event ty
-> TextTerm -> VariableIdentifier -> Formula event ty
PropTextEq Relevance event a
rel (VariableIdentifier -> VariableIdentifier -> TextTerm -> TextTerm
substTextTerm VariableIdentifier
v VariableIdentifier
x TextTerm
t) VariableIdentifier
rhs