module Hermod.ReCon.LTL.Internal.Rewrite(
  rewriteHomogeneous,
  rewriteIdentity
  ) where

import           Hermod.ReCon.LTL.Formula
import           Hermod.ReCon.LTL.Internal.IR.HomogeneousFormula (normaliseHomogeneous)

import           Data.Maybe (fromMaybe)
import qualified Data.Set as Set

-- This file concerns applying rewrite rules to a formula.
-- The rewrite rules must be logical identities, hence all rewrites here produce logically equivalent formulas.

-- | Call the given function on all sub-expressions of the formula recursively
--   up to any temporal operator (= heterogeneous fragment), exclusively.
recurseHomogeneous :: (Formula event ty -> Maybe (Formula event ty)) -> Formula event ty -> Formula event ty
recurseHomogeneous :: forall event ty.
(Formula event ty -> Maybe (Formula event ty))
-> Formula event ty -> Formula event ty
recurseHomogeneous Formula event ty -> Maybe (Formula event ty)
_ self :: Formula event ty
self@(Atom {})     = Formula event ty
self
recurseHomogeneous Formula event ty -> Maybe (Formula event ty)
_ self :: Formula event ty
self@(Forall {})   = Formula event ty
self
recurseHomogeneous Formula event ty -> Maybe (Formula event ty)
_ self :: Formula event ty
self@(ExistsN {})  = Formula event ty
self
recurseHomogeneous Formula event ty -> Maybe (Formula event ty)
_ self :: Formula event ty
self@(ForallN {})  = Formula event ty
self
recurseHomogeneous Formula event ty -> Maybe (Formula event ty)
_ self :: Formula event ty
self@(UntilN {})   = Formula event ty
self
recurseHomogeneous Formula event ty -> Maybe (Formula event ty)
_ self :: Formula event ty
self@(NextN {})    = Formula event ty
self
recurseHomogeneous Formula event ty -> Maybe (Formula event ty)
_ self :: Formula event ty
self@(Next Formula event ty
_)      = Formula event ty
self
recurseHomogeneous Formula event ty -> Maybe (Formula event ty)
f self :: Formula event ty
self@(And Formula event ty
phi Formula event ty
psi) =
  Formula event ty -> Maybe (Formula event ty) -> Formula event ty
forall a. a -> Maybe a -> a
fromMaybe (Formula event ty -> Formula event ty -> Formula event ty
forall event ty.
Formula event ty -> Formula event ty -> Formula event ty
And ((Formula event ty -> Maybe (Formula event ty))
-> Formula event ty -> Formula event ty
forall event ty.
(Formula event ty -> Maybe (Formula event ty))
-> Formula event ty -> Formula event ty
recurseHomogeneous Formula event ty -> Maybe (Formula event ty)
f Formula event ty
phi) ((Formula event ty -> Maybe (Formula event ty))
-> Formula event ty -> Formula event ty
forall event ty.
(Formula event ty -> Maybe (Formula event ty))
-> Formula event ty -> Formula event ty
recurseHomogeneous Formula event ty -> Maybe (Formula event ty)
f Formula event ty
psi)) (Formula event ty -> Maybe (Formula event ty)
f Formula event ty
self)
recurseHomogeneous Formula event ty -> Maybe (Formula event ty)
f self :: Formula event ty
self@(Or Formula event ty
phi Formula event ty
psi) =
  Formula event ty -> Maybe (Formula event ty) -> Formula event ty
forall a. a -> Maybe a -> a
fromMaybe (Formula event ty -> Formula event ty -> Formula event ty
forall event ty.
Formula event ty -> Formula event ty -> Formula event ty
Or ((Formula event ty -> Maybe (Formula event ty))
-> Formula event ty -> Formula event ty
forall event ty.
(Formula event ty -> Maybe (Formula event ty))
-> Formula event ty -> Formula event ty
recurseHomogeneous Formula event ty -> Maybe (Formula event ty)
f Formula event ty
phi) ((Formula event ty -> Maybe (Formula event ty))
-> Formula event ty -> Formula event ty
forall event ty.
(Formula event ty -> Maybe (Formula event ty))
-> Formula event ty -> Formula event ty
recurseHomogeneous Formula event ty -> Maybe (Formula event ty)
f Formula event ty
psi)) (Formula event ty -> Maybe (Formula event ty)
f Formula event ty
self)
recurseHomogeneous Formula event ty -> Maybe (Formula event ty)
f self :: Formula event ty
self@(Implies Formula event ty
phi Formula event ty
psi) =
  Formula event ty -> Maybe (Formula event ty) -> Formula event ty
forall a. a -> Maybe a -> a
fromMaybe (Formula event ty -> Formula event ty -> Formula event ty
forall event ty.
Formula event ty -> Formula event ty -> Formula event ty
Implies ((Formula event ty -> Maybe (Formula event ty))
-> Formula event ty -> Formula event ty
forall event ty.
(Formula event ty -> Maybe (Formula event ty))
-> Formula event ty -> Formula event ty
recurseHomogeneous Formula event ty -> Maybe (Formula event ty)
f Formula event ty
phi) ((Formula event ty -> Maybe (Formula event ty))
-> Formula event ty -> Formula event ty
forall event ty.
(Formula event ty -> Maybe (Formula event ty))
-> Formula event ty -> Formula event ty
recurseHomogeneous Formula event ty -> Maybe (Formula event ty)
f Formula event ty
psi)) (Formula event ty -> Maybe (Formula event ty)
f Formula event ty
self)
recurseHomogeneous Formula event ty -> Maybe (Formula event ty)
f self :: Formula event ty
self@(Not Formula event ty
phi) =
  Formula event ty -> Maybe (Formula event ty) -> Formula event ty
forall a. a -> Maybe a -> a
fromMaybe (Formula event ty -> Formula event ty
forall event ty. Formula event ty -> Formula event ty
Not ((Formula event ty -> Maybe (Formula event ty))
-> Formula event ty -> Formula event ty
forall event ty.
(Formula event ty -> Maybe (Formula event ty))
-> Formula event ty -> Formula event ty
recurseHomogeneous Formula event ty -> Maybe (Formula event ty)
f Formula event ty
phi)) (Formula event ty -> Maybe (Formula event ty)
f Formula event ty
self)
recurseHomogeneous Formula event ty -> Maybe (Formula event ty)
f self :: Formula event ty
self@Formula event ty
Bottom                       = Formula event ty -> Maybe (Formula event ty) -> Formula event ty
forall a. a -> Maybe a -> a
fromMaybe Formula event ty
self (Formula event ty -> Maybe (Formula event ty)
f Formula event ty
self)
recurseHomogeneous Formula event ty -> Maybe (Formula event ty)
f self :: Formula event ty
self@Formula event ty
Top                          = Formula event ty -> Maybe (Formula event ty) -> Formula event ty
forall a. a -> Maybe a -> a
fromMaybe Formula event ty
self (Formula event ty -> Maybe (Formula event ty)
f Formula event ty
self)
recurseHomogeneous Formula event ty -> Maybe (Formula event ty)
f self :: Formula event ty
self@(PropIntBinRel {})           = Formula event ty -> Maybe (Formula event ty) -> Formula event ty
forall a. a -> Maybe a -> a
fromMaybe Formula event ty
self (Formula event ty -> Maybe (Formula event ty)
f Formula event ty
self)
recurseHomogeneous Formula event ty -> Maybe (Formula event ty)
f self :: Formula event ty
self@(PropTextEq {})              = Formula event ty -> Maybe (Formula event ty) -> Formula event ty
forall a. a -> Maybe a -> a
fromMaybe Formula event ty
self (Formula event ty -> Maybe (Formula event ty)
f Formula event ty
self)
recurseHomogeneous Formula event ty -> Maybe (Formula event ty)
f self :: Formula event ty
self@(PropIntForall VariableIdentifier
x Formula event ty
phi)        = Formula event ty -> Maybe (Formula event ty) -> Formula event ty
forall a. a -> Maybe a -> a
fromMaybe (VariableIdentifier -> Formula event ty -> Formula event ty
forall event ty.
VariableIdentifier -> Formula event ty -> Formula event ty
PropIntForall VariableIdentifier
x ((Formula event ty -> Maybe (Formula event ty))
-> Formula event ty -> Formula event ty
forall event ty.
(Formula event ty -> Maybe (Formula event ty))
-> Formula event ty -> Formula event ty
recurseHomogeneous Formula event ty -> Maybe (Formula event ty)
f Formula event ty
phi)) (Formula event ty -> Maybe (Formula event ty)
f Formula event ty
self)
recurseHomogeneous Formula event ty -> Maybe (Formula event ty)
f self :: Formula event ty
self@(PropTextForall VariableIdentifier
x Formula event ty
phi)       = Formula event ty -> Maybe (Formula event ty) -> Formula event ty
forall a. a -> Maybe a -> a
fromMaybe (VariableIdentifier -> Formula event ty -> Formula event ty
forall event ty.
VariableIdentifier -> Formula event ty -> Formula event ty
PropTextForall VariableIdentifier
x ((Formula event ty -> Maybe (Formula event ty))
-> Formula event ty -> Formula event ty
forall event ty.
(Formula event ty -> Maybe (Formula event ty))
-> Formula event ty -> Formula event ty
recurseHomogeneous Formula event ty -> Maybe (Formula event ty)
f Formula event ty
phi)) (Formula event ty -> Maybe (Formula event ty)
f Formula event ty
self)
recurseHomogeneous Formula event ty -> Maybe (Formula event ty)
f self :: Formula event ty
self@(PropIntForallN VariableIdentifier
x Set IntValue
dom Formula event ty
phi)   = Formula event ty -> Maybe (Formula event ty) -> Formula event ty
forall a. a -> Maybe a -> a
fromMaybe (VariableIdentifier
-> Set IntValue -> Formula event ty -> Formula event ty
forall event ty.
VariableIdentifier
-> Set IntValue -> Formula event ty -> Formula event ty
PropIntForallN VariableIdentifier
x Set IntValue
dom ((Formula event ty -> Maybe (Formula event ty))
-> Formula event ty -> Formula event ty
forall event ty.
(Formula event ty -> Maybe (Formula event ty))
-> Formula event ty -> Formula event ty
recurseHomogeneous Formula event ty -> Maybe (Formula event ty)
f Formula event ty
phi)) (Formula event ty -> Maybe (Formula event ty)
f Formula event ty
self)
recurseHomogeneous Formula event ty -> Maybe (Formula event ty)
f self :: Formula event ty
self@(PropTextForallN VariableIdentifier
x Set VariableIdentifier
dom Formula event ty
phi)  = Formula event ty -> Maybe (Formula event ty) -> Formula event ty
forall a. a -> Maybe a -> a
fromMaybe (VariableIdentifier
-> Set VariableIdentifier -> Formula event ty -> Formula event ty
forall event ty.
VariableIdentifier
-> Set VariableIdentifier -> Formula event ty -> Formula event ty
PropTextForallN VariableIdentifier
x Set VariableIdentifier
dom ((Formula event ty -> Maybe (Formula event ty))
-> Formula event ty -> Formula event ty
forall event ty.
(Formula event ty -> Maybe (Formula event ty))
-> Formula event ty -> Formula event ty
recurseHomogeneous Formula event ty -> Maybe (Formula event ty)
f Formula event ty
phi)) (Formula event ty -> Maybe (Formula event ty)
f Formula event ty
self)
recurseHomogeneous Formula event ty -> Maybe (Formula event ty)
f self :: Formula event ty
self@(PropIntExists VariableIdentifier
x Formula event ty
phi)        = Formula event ty -> Maybe (Formula event ty) -> Formula event ty
forall a. a -> Maybe a -> a
fromMaybe (VariableIdentifier -> Formula event ty -> Formula event ty
forall event ty.
VariableIdentifier -> Formula event ty -> Formula event ty
PropIntExists VariableIdentifier
x ((Formula event ty -> Maybe (Formula event ty))
-> Formula event ty -> Formula event ty
forall event ty.
(Formula event ty -> Maybe (Formula event ty))
-> Formula event ty -> Formula event ty
recurseHomogeneous Formula event ty -> Maybe (Formula event ty)
f Formula event ty
phi)) (Formula event ty -> Maybe (Formula event ty)
f Formula event ty
self)
recurseHomogeneous Formula event ty -> Maybe (Formula event ty)
f self :: Formula event ty
self@(PropTextExists VariableIdentifier
x Formula event ty
phi)       = Formula event ty -> Maybe (Formula event ty) -> Formula event ty
forall a. a -> Maybe a -> a
fromMaybe (VariableIdentifier -> Formula event ty -> Formula event ty
forall event ty.
VariableIdentifier -> Formula event ty -> Formula event ty
PropTextExists VariableIdentifier
x ((Formula event ty -> Maybe (Formula event ty))
-> Formula event ty -> Formula event ty
forall event ty.
(Formula event ty -> Maybe (Formula event ty))
-> Formula event ty -> Formula event ty
recurseHomogeneous Formula event ty -> Maybe (Formula event ty)
f Formula event ty
phi)) (Formula event ty -> Maybe (Formula event ty)
f Formula event ty
self)
recurseHomogeneous Formula event ty -> Maybe (Formula event ty)
f self :: Formula event ty
self@(PropIntExistsN VariableIdentifier
x Set IntValue
dom Formula event ty
phi)   = Formula event ty -> Maybe (Formula event ty) -> Formula event ty
forall a. a -> Maybe a -> a
fromMaybe (VariableIdentifier
-> Set IntValue -> Formula event ty -> Formula event ty
forall event ty.
VariableIdentifier
-> Set IntValue -> Formula event ty -> Formula event ty
PropIntExistsN VariableIdentifier
x Set IntValue
dom ((Formula event ty -> Maybe (Formula event ty))
-> Formula event ty -> Formula event ty
forall event ty.
(Formula event ty -> Maybe (Formula event ty))
-> Formula event ty -> Formula event ty
recurseHomogeneous Formula event ty -> Maybe (Formula event ty)
f Formula event ty
phi)) (Formula event ty -> Maybe (Formula event ty)
f Formula event ty
self)
recurseHomogeneous Formula event ty -> Maybe (Formula event ty)
f self :: Formula event ty
self@(PropTextExistsN VariableIdentifier
x Set VariableIdentifier
dom Formula event ty
phi)  = Formula event ty -> Maybe (Formula event ty) -> Formula event ty
forall a. a -> Maybe a -> a
fromMaybe (VariableIdentifier
-> Set VariableIdentifier -> Formula event ty -> Formula event ty
forall event ty.
VariableIdentifier
-> Set VariableIdentifier -> Formula event ty -> Formula event ty
PropTextExistsN VariableIdentifier
x Set VariableIdentifier
dom ((Formula event ty -> Maybe (Formula event ty))
-> Formula event ty -> Formula event ty
forall event ty.
(Formula event ty -> Maybe (Formula event ty))
-> Formula event ty -> Formula event ty
recurseHomogeneous Formula event ty -> Maybe (Formula event ty)
f Formula event ty
phi)) (Formula event ty -> Maybe (Formula event ty)
f Formula event ty
self)

-- | Rewrite the formula by applying the homogeneous fragment retraction & normalisation recursively.
rewriteHomogeneous :: Formula event ty -> Formula event ty
rewriteHomogeneous :: forall event ty. Formula event ty -> Formula event ty
rewriteHomogeneous = (Formula event ty -> Maybe (Formula event ty))
-> Formula event ty -> Formula event ty
forall event ty.
(Formula event ty -> Maybe (Formula event ty))
-> Formula event ty -> Formula event ty
recurseHomogeneous Formula event ty -> Maybe (Formula event ty)
forall event ty. Formula event ty -> Maybe (Formula event ty)
normaliseHomogeneous

-- | Rewrites the formula by the following logical identities recursively:
--   ☐ ᪲ₖ ⊤ = ⊤
--   ☐ᵏ ⊤ = ⊤
--   ♢ᵏ ⊥ = ⊥
--   φ |ᵏ ⊤ = ⊤
--   φ ∧ ⊤ = φ
--   ⊤ ∧ φ = φ
--   φ ∧ ⊥ = ⊥
--   ⊥ ∧ φ = ⊥
--   ⊤ ∨ φ = ⊤
--   φ ∨ ⊤ = ⊤
--   ⊥ ∨ φ = φ
--   φ ∨ ⊥ = φ
--   ⊤ ⇒ φ = φ
--   ⊥ ⇒ φ = ⊤
--   φ ⇒ ⊤ = ⊤
--   φ ⇒ ⊥ = ¬ φ
--   ¬ (¬ φ) = φ
--   ¬ ⊥ = ⊤
--   ¬ ⊤ = ⊥
--   (t = t) = ⊤
--   (t ≤ t) = ⊤
--   (t ≥ t) = ⊤
--   (t < t) = ⊥
--   (t > t) = ⊥
--   (n = m) = ⊤ where n = m   (n, m integer constants)
--   (n = m) = ⊥ where n ≠ m
--   (n < m) = ⊤ where n < m
--   (n < m) = ⊥ where n ≥ m
--   (n ≤ m) = ⊤ where n ≤ m
--   (n ≤ m) = ⊥ where n > m
--   (n > m) = ⊤ where n > m
--   (n > m) = ⊥ where n ≤ m
--   (n ≥ m) = ⊤ where n ≥ m
--   (n ≥ m) = ⊥ where n < m
--   ∀x. ⊤ = ⊤
--   ∀x. ⊥ = ⊥
--   ∃x. ⊤ = ⊤
--   ∃x. ⊥ = ⊥
--   ∀(x ∈ ∅). φ       = ⊤
--   ∀(x ∈ {v} ⊔ v̄). ⊥ = ⊥
--   ∀(x ∈ {v} ⊔ v̄). ⊤ = ⊤
--   ∃(x ∈ ∅). φ       = ⊥
--   ∃(x ∈ {v} ⊔ v̄). ⊥ = ⊥
--   ∃(x ∈ {v} ⊔ v̄). ⊤ = ⊤
--   Additionally, unfolds base-cases of finite temporal operators.
rewriteIdentity :: Eq ty => Formula event ty -> Formula event ty
rewriteIdentity :: forall ty event. Eq ty => Formula event ty -> Formula event ty
rewriteIdentity (Forall Word
k Formula event ty
phi) =
  case Formula event ty -> Formula event ty
forall ty event. Eq ty => Formula event ty -> Formula event ty
rewriteIdentity Formula event ty
phi of
    Formula event ty
Top  -> Formula event ty
forall event ty. Formula event ty
Top
    Formula event ty
phi' -> Word -> Formula event ty -> Formula event ty
forall event ty. Word -> Formula event ty -> Formula event ty
Forall Word
k Formula event ty
phi'
rewriteIdentity (ForallN Word
0 Formula event ty
phi) = Formula event ty -> Formula event ty
forall ty event. Eq ty => Formula event ty -> Formula event ty
rewriteIdentity (Word -> Formula event ty -> Formula event ty
forall event ty. Word -> Formula event ty -> Formula event ty
unfoldForallN Word
0 Formula event ty
phi)
rewriteIdentity (ForallN Word
k Formula event ty
phi) =
  case Formula event ty -> Formula event ty
forall ty event. Eq ty => Formula event ty -> Formula event ty
rewriteIdentity Formula event ty
phi of
    Formula event ty
Top  -> Formula event ty
forall event ty. Formula event ty
Top
    Formula event ty
phi' -> Word -> Formula event ty -> Formula event ty
forall event ty. Word -> Formula event ty -> Formula event ty
ForallN Word
k Formula event ty
phi'
rewriteIdentity (ExistsN Word
0 Formula event ty
phi) = Formula event ty -> Formula event ty
forall ty event. Eq ty => Formula event ty -> Formula event ty
rewriteIdentity (Word -> Formula event ty -> Formula event ty
forall event ty. Word -> Formula event ty -> Formula event ty
unfoldExistsN Word
0 Formula event ty
phi)
rewriteIdentity (ExistsN Word
k Formula event ty
phi) =
  case Formula event ty -> Formula event ty
forall ty event. Eq ty => Formula event ty -> Formula event ty
rewriteIdentity Formula event ty
phi of
    Formula event ty
Bottom -> Formula event ty
forall event ty. Formula event ty
Bottom
    Formula event ty
phi'   -> Word -> Formula event ty -> Formula event ty
forall event ty. Word -> Formula event ty -> Formula event ty
ExistsN Word
k Formula event ty
phi'
rewriteIdentity (Next Formula event ty
phi) = Formula event ty -> Formula event ty
forall event ty. Formula event ty -> Formula event ty
Next (Formula event ty -> Formula event ty
forall ty event. Eq ty => Formula event ty -> Formula event ty
rewriteIdentity Formula event ty
phi)
rewriteIdentity (NextN Word
0 Formula event ty
phi) = Formula event ty -> Formula event ty
forall ty event. Eq ty => Formula event ty -> Formula event ty
rewriteIdentity (Word -> Formula event ty -> Formula event ty
forall event ty. Word -> Formula event ty -> Formula event ty
unfoldNextN Word
0 Formula event ty
phi)
rewriteIdentity (NextN Word
k Formula event ty
phi) = Word -> Formula event ty -> Formula event ty
forall event ty. Word -> Formula event ty -> Formula event ty
NextN Word
k (Formula event ty -> Formula event ty
forall ty event. Eq ty => Formula event ty -> Formula event ty
rewriteIdentity Formula event ty
phi)
rewriteIdentity (UntilN Word
0 Formula event ty
phi Formula event ty
psi) = Formula event ty -> Formula event ty
forall ty event. Eq ty => Formula event ty -> Formula event ty
rewriteIdentity (Word -> Formula event ty -> Formula event ty -> Formula event ty
forall event ty.
Word -> Formula event ty -> Formula event ty -> Formula event ty
unfoldUntilN Word
0 Formula event ty
phi Formula event ty
psi)
rewriteIdentity (UntilN Word
k Formula event ty
phi Formula event ty
psi) =
  case Formula event ty -> Formula event ty
forall ty event. Eq ty => Formula event ty -> Formula event ty
rewriteIdentity Formula event ty
psi of
    Formula event ty
Top -> Formula event ty
forall event ty. Formula event ty
Top
    Formula event ty
psi' -> Word -> Formula event ty -> Formula event ty -> Formula event ty
forall event ty.
Word -> Formula event ty -> Formula event ty -> Formula event ty
UntilN Word
k (Formula event ty -> Formula event ty
forall ty event. Eq ty => Formula event ty -> Formula event ty
rewriteIdentity Formula event ty
phi) Formula event ty
psi'
rewriteIdentity (And Formula event ty
phi Formula event ty
psi) =
  case (Formula event ty -> Formula event ty
forall ty event. Eq ty => Formula event ty -> Formula event ty
rewriteIdentity Formula event ty
phi, Formula event ty -> Formula event ty
forall ty event. Eq ty => Formula event ty -> Formula event ty
rewriteIdentity Formula event ty
psi) of
    (Formula event ty
Bottom, Formula event ty
_)   -> Formula event ty
forall event ty. Formula event ty
Bottom
    (Formula event ty
Top, Formula event ty
psi')   -> Formula event ty
psi'
    (Formula event ty
_, Formula event ty
Bottom)   -> Formula event ty
forall event ty. Formula event ty
Bottom
    (Formula event ty
phi', Formula event ty
Top)   -> Formula event ty
phi'
    (Formula event ty
phi', Formula event ty
psi')  -> Formula event ty -> Formula event ty -> Formula event ty
forall event ty.
Formula event ty -> Formula event ty -> Formula event ty
And Formula event ty
phi' Formula event ty
psi'
rewriteIdentity (Or Formula event ty
phi Formula event ty
psi) =
  case (Formula event ty -> Formula event ty
forall ty event. Eq ty => Formula event ty -> Formula event ty
rewriteIdentity Formula event ty
phi, Formula event ty -> Formula event ty
forall ty event. Eq ty => Formula event ty -> Formula event ty
rewriteIdentity Formula event ty
psi) of
    (Formula event ty
Bottom, Formula event ty
psi') -> Formula event ty
psi'
    (Formula event ty
Top, Formula event ty
_)       -> Formula event ty
forall event ty. Formula event ty
Top
    (Formula event ty
phi', Formula event ty
Bottom) -> Formula event ty
phi'
    (Formula event ty
_, Formula event ty
Top)       -> Formula event ty
forall event ty. Formula event ty
Top
    (Formula event ty
phi', Formula event ty
psi')   -> Formula event ty -> Formula event ty -> Formula event ty
forall event ty.
Formula event ty -> Formula event ty -> Formula event ty
Or Formula event ty
phi' Formula event ty
psi'
rewriteIdentity (Implies Formula event ty
phi Formula event ty
psi) =
  case (Formula event ty -> Formula event ty
forall ty event. Eq ty => Formula event ty -> Formula event ty
rewriteIdentity Formula event ty
phi, Formula event ty -> Formula event ty
forall ty event. Eq ty => Formula event ty -> Formula event ty
rewriteIdentity Formula event ty
psi) of
    (Formula event ty
Top, Formula event ty
psi')     -> Formula event ty
psi'
    (Formula event ty
Bottom, Formula event ty
_)     -> Formula event ty
forall event ty. Formula event ty
Top
    (Formula event ty
_, Formula event ty
Top)        -> Formula event ty
forall event ty. Formula event ty
Top
    (Formula event ty
phi', Formula event ty
Bottom)  -> Formula event ty -> Formula event ty
forall ty event. Eq ty => Formula event ty -> Formula event ty
rewriteIdentity (Formula event ty -> Formula event ty
forall event ty. Formula event ty -> Formula event ty
Not Formula event ty
phi')
    (Formula event ty
phi', Formula event ty
psi')    -> Formula event ty -> Formula event ty -> Formula event ty
forall event ty.
Formula event ty -> Formula event ty -> Formula event ty
Implies Formula event ty
phi' Formula event ty
psi'
rewriteIdentity (Not Formula event ty
phi) =
  case Formula event ty -> Formula event ty
forall ty event. Eq ty => Formula event ty -> Formula event ty
rewriteIdentity Formula event ty
phi of
    Not Formula event ty
phi' -> Formula event ty
phi'
    Formula event ty
Top      -> Formula event ty
forall event ty. Formula event ty
Bottom
    Formula event ty
Bottom   -> Formula event ty
forall event ty. Formula event ty
Top
    Formula event ty
phi'      -> Formula event ty -> Formula event ty
forall event ty. Formula event ty -> Formula event ty
Not Formula event ty
phi'
rewriteIdentity Formula event ty
Bottom = Formula event ty
forall event ty. Formula event ty
Bottom
rewriteIdentity Formula event ty
Top = Formula event ty
forall event ty. Formula event ty
Top
rewriteIdentity (PropIntBinRel BinRel
rel Relevance event ty
_ IntTerm
lhs IntTerm
rhs) | IntTerm
lhs IntTerm -> IntTerm -> Bool
forall a. Eq a => a -> a -> Bool
== IntTerm
rhs =
  case BinRel
rel of
    BinRel
Eq  -> Formula event ty
forall event ty. Formula event ty
Top
    BinRel
Lte -> Formula event ty
forall event ty. Formula event ty
Top
    BinRel
Gte -> Formula event ty
forall event ty. Formula event ty
Top
    BinRel
Lt  -> Formula event ty
forall event ty. Formula event ty
Bottom
    BinRel
Gt  -> Formula event ty
forall event ty. Formula event ty
Bottom
rewriteIdentity (PropIntBinRel BinRel
rel Relevance event ty
_ (IntConst IntValue
a) (IntConst IntValue
b)) =
  case BinRel
rel of
    BinRel
Eq  -> if IntValue
a IntValue -> IntValue -> Bool
forall a. Eq a => a -> a -> Bool
== IntValue
b  then Formula event ty
forall event ty. Formula event ty
Top else Formula event ty
forall event ty. Formula event ty
Bottom
    BinRel
Lt  -> if IntValue
a IntValue -> IntValue -> Bool
forall a. Ord a => a -> a -> Bool
<  IntValue
b  then Formula event ty
forall event ty. Formula event ty
Top else Formula event ty
forall event ty. Formula event ty
Bottom
    BinRel
Lte -> if IntValue
a IntValue -> IntValue -> Bool
forall a. Ord a => a -> a -> Bool
<= IntValue
b  then Formula event ty
forall event ty. Formula event ty
Top else Formula event ty
forall event ty. Formula event ty
Bottom
    BinRel
Gt  -> if IntValue
a IntValue -> IntValue -> Bool
forall a. Ord a => a -> a -> Bool
>  IntValue
b  then Formula event ty
forall event ty. Formula event ty
Top else Formula event ty
forall event ty. Formula event ty
Bottom
    BinRel
Gte -> if IntValue
a IntValue -> IntValue -> Bool
forall a. Ord a => a -> a -> Bool
>= IntValue
b  then Formula event ty
forall event ty. Formula event ty
Top else Formula event ty
forall event ty. Formula event ty
Bottom
rewriteIdentity p :: Formula event ty
p@(PropIntBinRel {}) = Formula event ty
p
rewriteIdentity (PropTextEq Relevance event ty
_ (TextConst VariableIdentifier
v) VariableIdentifier
v') | VariableIdentifier
v VariableIdentifier -> VariableIdentifier -> Bool
forall a. Eq a => a -> a -> Bool
== VariableIdentifier
v' = Formula event ty
forall event ty. Formula event ty
Top
rewriteIdentity (PropTextEq Relevance event ty
_ (TextConst VariableIdentifier
_) VariableIdentifier
_)            = Formula event ty
forall event ty. Formula event ty
Bottom
rewriteIdentity p :: Formula event ty
p@(PropTextEq {}) = Formula event ty
p
rewriteIdentity p :: Formula event ty
p@(Atom {}) = Formula event ty
p
rewriteIdentity (PropIntForall VariableIdentifier
x Formula event ty
phi) =
  case Formula event ty -> Formula event ty
forall ty event. Eq ty => Formula event ty -> Formula event ty
rewriteIdentity Formula event ty
phi of
    Formula event ty
Top    -> Formula event ty
forall event ty. Formula event ty
Top
    Formula event ty
Bottom -> Formula event ty
forall event ty. Formula event ty
Bottom
    Formula event ty
phi'   -> VariableIdentifier -> Formula event ty -> Formula event ty
forall event ty.
VariableIdentifier -> Formula event ty -> Formula event ty
PropIntForall VariableIdentifier
x Formula event ty
phi'
rewriteIdentity (PropTextForall VariableIdentifier
x Formula event ty
phi) =
  case Formula event ty -> Formula event ty
forall ty event. Eq ty => Formula event ty -> Formula event ty
rewriteIdentity Formula event ty
phi of
    Formula event ty
Top    -> Formula event ty
forall event ty. Formula event ty
Top
    Formula event ty
Bottom -> Formula event ty
forall event ty. Formula event ty
Bottom
    Formula event ty
phi'   -> VariableIdentifier -> Formula event ty -> Formula event ty
forall event ty.
VariableIdentifier -> Formula event ty -> Formula event ty
PropTextForall VariableIdentifier
x Formula event ty
phi'
rewriteIdentity (PropIntExists VariableIdentifier
x Formula event ty
phi) =
  case Formula event ty -> Formula event ty
forall ty event. Eq ty => Formula event ty -> Formula event ty
rewriteIdentity Formula event ty
phi of
    Formula event ty
Top    -> Formula event ty
forall event ty. Formula event ty
Top
    Formula event ty
Bottom -> Formula event ty
forall event ty. Formula event ty
Bottom
    Formula event ty
phi'   -> VariableIdentifier -> Formula event ty -> Formula event ty
forall event ty.
VariableIdentifier -> Formula event ty -> Formula event ty
PropIntExists VariableIdentifier
x Formula event ty
phi'
rewriteIdentity (PropTextExists VariableIdentifier
x Formula event ty
phi) =
  case Formula event ty -> Formula event ty
forall ty event. Eq ty => Formula event ty -> Formula event ty
rewriteIdentity Formula event ty
phi of
    Formula event ty
Top    -> Formula event ty
forall event ty. Formula event ty
Top
    Formula event ty
Bottom -> Formula event ty
forall event ty. Formula event ty
Bottom
    Formula event ty
phi'   -> VariableIdentifier -> Formula event ty -> Formula event ty
forall event ty.
VariableIdentifier -> Formula event ty -> Formula event ty
PropTextExists VariableIdentifier
x Formula event ty
phi'
rewriteIdentity (PropIntForallN  VariableIdentifier
_ Set IntValue
dom Formula event ty
_) | Set IntValue -> Bool
forall a. Set a -> Bool
Set.null Set IntValue
dom = Formula event ty
forall event ty. Formula event ty
Top
rewriteIdentity (PropIntForallN  VariableIdentifier
x Set IntValue
dom Formula event ty
phi) =
  case Formula event ty -> Formula event ty
forall ty event. Eq ty => Formula event ty -> Formula event ty
rewriteIdentity Formula event ty
phi of
    Formula event ty
Top    -> Formula event ty
forall event ty. Formula event ty
Top
    Formula event ty
Bottom -> Formula event ty
forall event ty. Formula event ty
Bottom
    Formula event ty
phi'   -> VariableIdentifier
-> Set IntValue -> Formula event ty -> Formula event ty
forall event ty.
VariableIdentifier
-> Set IntValue -> Formula event ty -> Formula event ty
PropIntForallN VariableIdentifier
x Set IntValue
dom Formula event ty
phi'
rewriteIdentity (PropTextForallN VariableIdentifier
_ Set VariableIdentifier
dom Formula event ty
_) | Set VariableIdentifier -> Bool
forall a. Set a -> Bool
Set.null Set VariableIdentifier
dom = Formula event ty
forall event ty. Formula event ty
Top
rewriteIdentity (PropTextForallN VariableIdentifier
x Set VariableIdentifier
dom Formula event ty
phi) =
  case Formula event ty -> Formula event ty
forall ty event. Eq ty => Formula event ty -> Formula event ty
rewriteIdentity Formula event ty
phi of
    Formula event ty
Top    -> Formula event ty
forall event ty. Formula event ty
Top
    Formula event ty
Bottom -> Formula event ty
forall event ty. Formula event ty
Bottom
    Formula event ty
phi'   -> VariableIdentifier
-> Set VariableIdentifier -> Formula event ty -> Formula event ty
forall event ty.
VariableIdentifier
-> Set VariableIdentifier -> Formula event ty -> Formula event ty
PropTextForallN VariableIdentifier
x Set VariableIdentifier
dom Formula event ty
phi'
rewriteIdentity (PropIntExistsN  VariableIdentifier
_ Set IntValue
dom Formula event ty
_) | Set IntValue -> Bool
forall a. Set a -> Bool
Set.null Set IntValue
dom = Formula event ty
forall event ty. Formula event ty
Bottom
rewriteIdentity (PropIntExistsN  VariableIdentifier
x Set IntValue
dom Formula event ty
phi) =
  case Formula event ty -> Formula event ty
forall ty event. Eq ty => Formula event ty -> Formula event ty
rewriteIdentity Formula event ty
phi of
    Formula event ty
Top    -> Formula event ty
forall event ty. Formula event ty
Top
    Formula event ty
Bottom -> Formula event ty
forall event ty. Formula event ty
Bottom
    Formula event ty
phi'   -> VariableIdentifier
-> Set IntValue -> Formula event ty -> Formula event ty
forall event ty.
VariableIdentifier
-> Set IntValue -> Formula event ty -> Formula event ty
PropIntExistsN VariableIdentifier
x Set IntValue
dom Formula event ty
phi'
rewriteIdentity (PropTextExistsN VariableIdentifier
_ Set VariableIdentifier
dom Formula event ty
_) | Set VariableIdentifier -> Bool
forall a. Set a -> Bool
Set.null Set VariableIdentifier
dom = Formula event ty
forall event ty. Formula event ty
Bottom
rewriteIdentity (PropTextExistsN VariableIdentifier
x Set VariableIdentifier
dom Formula event ty
phi) =
  case Formula event ty -> Formula event ty
forall ty event. Eq ty => Formula event ty -> Formula event ty
rewriteIdentity Formula event ty
phi of
    Formula event ty
Top    -> Formula event ty
forall event ty. Formula event ty
Top
    Formula event ty
Bottom -> Formula event ty
forall event ty. Formula event ty
Bottom
    Formula event ty
phi'   -> VariableIdentifier
-> Set VariableIdentifier -> Formula event ty -> Formula event ty
forall event ty.
VariableIdentifier
-> Set VariableIdentifier -> Formula event ty -> Formula event ty
PropTextExistsN VariableIdentifier
x Set VariableIdentifier
dom Formula event ty
phi'