module Hermod.ReCon.LTL.Internal.IR.HomogeneousFormula (
    HomogeneousFormula(..)
  , Extended(..)
  , toFormula
  , lower
  , eval
  , quote
  , equiv
  , retract
  , normaliseHomogeneous) where

import           Hermod.ReCon.Common.Types (BinRel (..))
import           Hermod.ReCon.LTL.Formula (Formula, IntTerm (..), IntValue, TextTerm (..),
                   VariableIdentifier)
import qualified Hermod.ReCon.LTL.Formula as F
import           Hermod.ReCon.LTL.Internal.IR.HomogeneousFormula.FinFree (Extended (..))
import qualified Hermod.ReCon.LTL.Internal.IR.HomogeneousFormula.FinFree as FinFree

import           Data.Function (on)
import           Data.Set (Set)
import qualified Data.Set as Set
import           Data.Text (Text)

-- | A `Formula` with no temporal operators and no atoms.
--   Equivalence of two `HomogeneousFormula`s is decidable.
data HomogeneousFormula =
   ------------ Connective -------------
     Or HomogeneousFormula HomogeneousFormula
   | And HomogeneousFormula HomogeneousFormula
   | Not HomogeneousFormula
   | Implies HomogeneousFormula HomogeneousFormula
   | Top
   | Bottom
   -------------------------------------

   ----------- Event property ----------
   | PropIntForall   VariableIdentifier HomogeneousFormula
   | PropTextForall  VariableIdentifier HomogeneousFormula
   | PropIntForallN  VariableIdentifier (Set IntValue)  HomogeneousFormula
   | PropTextForallN VariableIdentifier (Set Text) HomogeneousFormula
   | PropIntExists   VariableIdentifier HomogeneousFormula
   | PropTextExists  VariableIdentifier HomogeneousFormula
   | PropIntExistsN  VariableIdentifier (Set IntValue)  HomogeneousFormula
   | PropTextExistsN VariableIdentifier (Set Text) HomogeneousFormula
   | PropIntBinRel BinRel IntTerm  IntTerm
   | PropTextEq    TextTerm  Text
   deriving (Int -> HomogeneousFormula -> ShowS
[HomogeneousFormula] -> ShowS
HomogeneousFormula -> String
(Int -> HomogeneousFormula -> ShowS)
-> (HomogeneousFormula -> String)
-> ([HomogeneousFormula] -> ShowS)
-> Show HomogeneousFormula
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> HomogeneousFormula -> ShowS
showsPrec :: Int -> HomogeneousFormula -> ShowS
$cshow :: HomogeneousFormula -> String
show :: HomogeneousFormula -> String
$cshowList :: [HomogeneousFormula] -> ShowS
showList :: [HomogeneousFormula] -> ShowS
Show, HomogeneousFormula -> HomogeneousFormula -> Bool
(HomogeneousFormula -> HomogeneousFormula -> Bool)
-> (HomogeneousFormula -> HomogeneousFormula -> Bool)
-> Eq HomogeneousFormula
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: HomogeneousFormula -> HomogeneousFormula -> Bool
== :: HomogeneousFormula -> HomogeneousFormula -> Bool
$c/= :: HomogeneousFormula -> HomogeneousFormula -> Bool
/= :: HomogeneousFormula -> HomogeneousFormula -> Bool
Eq, Eq HomogeneousFormula
Eq HomogeneousFormula =>
(HomogeneousFormula -> HomogeneousFormula -> Ordering)
-> (HomogeneousFormula -> HomogeneousFormula -> Bool)
-> (HomogeneousFormula -> HomogeneousFormula -> Bool)
-> (HomogeneousFormula -> HomogeneousFormula -> Bool)
-> (HomogeneousFormula -> HomogeneousFormula -> Bool)
-> (HomogeneousFormula -> HomogeneousFormula -> HomogeneousFormula)
-> (HomogeneousFormula -> HomogeneousFormula -> HomogeneousFormula)
-> Ord HomogeneousFormula
HomogeneousFormula -> HomogeneousFormula -> Bool
HomogeneousFormula -> HomogeneousFormula -> Ordering
HomogeneousFormula -> HomogeneousFormula -> HomogeneousFormula
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 :: HomogeneousFormula -> HomogeneousFormula -> Ordering
compare :: HomogeneousFormula -> HomogeneousFormula -> Ordering
$c< :: HomogeneousFormula -> HomogeneousFormula -> Bool
< :: HomogeneousFormula -> HomogeneousFormula -> Bool
$c<= :: HomogeneousFormula -> HomogeneousFormula -> Bool
<= :: HomogeneousFormula -> HomogeneousFormula -> Bool
$c> :: HomogeneousFormula -> HomogeneousFormula -> Bool
> :: HomogeneousFormula -> HomogeneousFormula -> Bool
$c>= :: HomogeneousFormula -> HomogeneousFormula -> Bool
>= :: HomogeneousFormula -> HomogeneousFormula -> Bool
$cmax :: HomogeneousFormula -> HomogeneousFormula -> HomogeneousFormula
max :: HomogeneousFormula -> HomogeneousFormula -> HomogeneousFormula
$cmin :: HomogeneousFormula -> HomogeneousFormula -> HomogeneousFormula
min :: HomogeneousFormula -> HomogeneousFormula -> HomogeneousFormula
Ord)
   -------------------------------------

toFormula :: HomogeneousFormula -> Formula event ty
toFormula :: forall event ty. HomogeneousFormula -> Formula event ty
toFormula (And HomogeneousFormula
a HomogeneousFormula
b)                    = Formula event ty -> Formula event ty -> Formula event ty
forall event ty.
Formula event ty -> Formula event ty -> Formula event ty
F.And (HomogeneousFormula -> Formula event ty
forall event ty. HomogeneousFormula -> Formula event ty
toFormula HomogeneousFormula
a) (HomogeneousFormula -> Formula event ty
forall event ty. HomogeneousFormula -> Formula event ty
toFormula HomogeneousFormula
b)
toFormula (Or HomogeneousFormula
a HomogeneousFormula
b)                     = Formula event ty -> Formula event ty -> Formula event ty
forall event ty.
Formula event ty -> Formula event ty -> Formula event ty
F.Or (HomogeneousFormula -> Formula event ty
forall event ty. HomogeneousFormula -> Formula event ty
toFormula HomogeneousFormula
a) (HomogeneousFormula -> Formula event ty
forall event ty. HomogeneousFormula -> Formula event ty
toFormula HomogeneousFormula
b)
toFormula (Implies HomogeneousFormula
a HomogeneousFormula
b)                = Formula event ty -> Formula event ty -> Formula event ty
forall event ty.
Formula event ty -> Formula event ty -> Formula event ty
F.Implies (HomogeneousFormula -> Formula event ty
forall event ty. HomogeneousFormula -> Formula event ty
toFormula HomogeneousFormula
a) (HomogeneousFormula -> Formula event ty
forall event ty. HomogeneousFormula -> Formula event ty
toFormula HomogeneousFormula
b)
toFormula (Not HomogeneousFormula
a)                      = Formula event ty -> Formula event ty
forall event ty. Formula event ty -> Formula event ty
F.Not (HomogeneousFormula -> Formula event ty
forall event ty. HomogeneousFormula -> Formula event ty
toFormula HomogeneousFormula
a)
toFormula HomogeneousFormula
Bottom                       = Formula event ty
forall event ty. Formula event ty
F.Bottom
toFormula HomogeneousFormula
Top                          = Formula event ty
forall event ty. Formula event ty
F.Top
toFormula (PropIntBinRel BinRel
rel IntTerm
a IntTerm
b)       = BinRel
-> Relevance event ty -> IntTerm -> IntTerm -> Formula event ty
forall event ty.
BinRel
-> Relevance event ty -> IntTerm -> IntTerm -> Formula event ty
F.PropIntBinRel BinRel
rel Relevance event ty
forall a. Set a
Set.empty IntTerm
a IntTerm
b
toFormula (PropTextEq TextTerm
a VariableIdentifier
b)             = Relevance event ty
-> TextTerm -> VariableIdentifier -> Formula event ty
forall event ty.
Relevance event ty
-> TextTerm -> VariableIdentifier -> Formula event ty
F.PropTextEq Relevance event ty
forall a. Set a
Set.empty TextTerm
a VariableIdentifier
b
toFormula (PropIntForall VariableIdentifier
x HomogeneousFormula
phi)        = VariableIdentifier -> Formula event ty -> Formula event ty
forall event ty.
VariableIdentifier -> Formula event ty -> Formula event ty
F.PropIntForall VariableIdentifier
x (HomogeneousFormula -> Formula event ty
forall event ty. HomogeneousFormula -> Formula event ty
toFormula HomogeneousFormula
phi)
toFormula (PropTextForall VariableIdentifier
x HomogeneousFormula
phi)       = VariableIdentifier -> Formula event ty -> Formula event ty
forall event ty.
VariableIdentifier -> Formula event ty -> Formula event ty
F.PropTextForall VariableIdentifier
x (HomogeneousFormula -> Formula event ty
forall event ty. HomogeneousFormula -> Formula event ty
toFormula HomogeneousFormula
phi)
toFormula (PropIntForallN VariableIdentifier
x Set IntValue
dom HomogeneousFormula
phi)   = VariableIdentifier
-> Set IntValue -> Formula event ty -> Formula event ty
forall event ty.
VariableIdentifier
-> Set IntValue -> Formula event ty -> Formula event ty
F.PropIntForallN VariableIdentifier
x Set IntValue
dom (HomogeneousFormula -> Formula event ty
forall event ty. HomogeneousFormula -> Formula event ty
toFormula HomogeneousFormula
phi)
toFormula (PropTextForallN VariableIdentifier
x Set VariableIdentifier
dom HomogeneousFormula
phi)  = VariableIdentifier
-> Set VariableIdentifier -> Formula event ty -> Formula event ty
forall event ty.
VariableIdentifier
-> Set VariableIdentifier -> Formula event ty -> Formula event ty
F.PropTextForallN VariableIdentifier
x Set VariableIdentifier
dom (HomogeneousFormula -> Formula event ty
forall event ty. HomogeneousFormula -> Formula event ty
toFormula HomogeneousFormula
phi)
toFormula (PropIntExists VariableIdentifier
x HomogeneousFormula
phi)        = VariableIdentifier -> Formula event ty -> Formula event ty
forall event ty.
VariableIdentifier -> Formula event ty -> Formula event ty
F.PropIntExists VariableIdentifier
x (HomogeneousFormula -> Formula event ty
forall event ty. HomogeneousFormula -> Formula event ty
toFormula HomogeneousFormula
phi)
toFormula (PropTextExists VariableIdentifier
x HomogeneousFormula
phi)       = VariableIdentifier -> Formula event ty -> Formula event ty
forall event ty.
VariableIdentifier -> Formula event ty -> Formula event ty
F.PropTextExists VariableIdentifier
x (HomogeneousFormula -> Formula event ty
forall event ty. HomogeneousFormula -> Formula event ty
toFormula HomogeneousFormula
phi)
toFormula (PropIntExistsN VariableIdentifier
x Set IntValue
dom HomogeneousFormula
phi)   = VariableIdentifier
-> Set IntValue -> Formula event ty -> Formula event ty
forall event ty.
VariableIdentifier
-> Set IntValue -> Formula event ty -> Formula event ty
F.PropIntExistsN VariableIdentifier
x Set IntValue
dom (HomogeneousFormula -> Formula event ty
forall event ty. HomogeneousFormula -> Formula event ty
toFormula HomogeneousFormula
phi)
toFormula (PropTextExistsN VariableIdentifier
x Set VariableIdentifier
dom HomogeneousFormula
phi)  = VariableIdentifier
-> Set VariableIdentifier -> Formula event ty -> Formula event ty
forall event ty.
VariableIdentifier
-> Set VariableIdentifier -> Formula event ty -> Formula event ty
F.PropTextExistsN VariableIdentifier
x Set VariableIdentifier
dom (HomogeneousFormula -> Formula event ty
forall event ty. HomogeneousFormula -> Formula event ty
toFormula HomogeneousFormula
phi)

-- | Lower a `HomogeneousFormula` to `FinFree` by eliminating all finite-domain
--   quantifiers.  Finite universal (∀x ∈ dom) unfolds to a conjunction; finite
--   existential (∃x ∈ dom) unfolds to a disjunction.
--
--   @'eval' = 'FinFree.eval' . 'lower'@
lower :: HomogeneousFormula -> FinFree.FinFree
lower :: HomogeneousFormula -> FinFree
lower (Or HomogeneousFormula
phi HomogeneousFormula
psi)      = FinFree -> FinFree -> FinFree
FinFree.Or (HomogeneousFormula -> FinFree
lower HomogeneousFormula
phi) (HomogeneousFormula -> FinFree
lower HomogeneousFormula
psi)
lower (And HomogeneousFormula
phi HomogeneousFormula
psi)     = FinFree -> FinFree -> FinFree
FinFree.And (HomogeneousFormula -> FinFree
lower HomogeneousFormula
phi) (HomogeneousFormula -> FinFree
lower HomogeneousFormula
psi)
lower (Not HomogeneousFormula
phi)         = FinFree -> FinFree
FinFree.Not (HomogeneousFormula -> FinFree
lower HomogeneousFormula
phi)
lower (Implies HomogeneousFormula
phi HomogeneousFormula
psi) = FinFree -> FinFree -> FinFree
FinFree.Implies (HomogeneousFormula -> FinFree
lower HomogeneousFormula
phi) (HomogeneousFormula -> FinFree
lower HomogeneousFormula
psi)
lower HomogeneousFormula
Top               = FinFree
FinFree.Top
lower HomogeneousFormula
Bottom            = FinFree
FinFree.Bottom
lower (PropIntForall  VariableIdentifier
x HomogeneousFormula
phi) = VariableIdentifier -> FinFree -> FinFree
FinFree.PropIntForall  VariableIdentifier
x (HomogeneousFormula -> FinFree
lower HomogeneousFormula
phi)
lower (PropTextForall VariableIdentifier
x HomogeneousFormula
phi) = VariableIdentifier -> FinFree -> FinFree
FinFree.PropTextForall VariableIdentifier
x (HomogeneousFormula -> FinFree
lower HomogeneousFormula
phi)
lower (PropIntExists  VariableIdentifier
x HomogeneousFormula
phi) = VariableIdentifier -> FinFree -> FinFree
FinFree.PropIntExists  VariableIdentifier
x (HomogeneousFormula -> FinFree
lower HomogeneousFormula
phi)
lower (PropTextExists VariableIdentifier
x HomogeneousFormula
phi) = VariableIdentifier -> FinFree -> FinFree
FinFree.PropTextExists VariableIdentifier
x (HomogeneousFormula -> FinFree
lower HomogeneousFormula
phi)
lower (PropIntBinRel BinRel
rel IntTerm
t IntTerm
v) = BinRel -> IntTerm -> IntTerm -> FinFree
FinFree.PropIntBinRel BinRel
rel IntTerm
t IntTerm
v
lower (PropTextEq TextTerm
t VariableIdentifier
v)        = TextTerm -> VariableIdentifier -> FinFree
FinFree.PropTextEq TextTerm
t VariableIdentifier
v
-- ∀x ∈ {v₁,...,vₙ}. φ  ≡  φ[v₁/x] ∧ ... ∧ φ[vₙ/x]   (⊤ when dom is empty)
lower (PropIntForallN VariableIdentifier
x Set IntValue
dom HomogeneousFormula
phi) =
  (IntValue -> FinFree -> FinFree)
-> FinFree -> [IntValue] -> FinFree
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (FinFree -> FinFree -> FinFree
FinFree.And (FinFree -> FinFree -> FinFree)
-> (IntValue -> FinFree) -> IntValue -> FinFree -> FinFree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \IntValue
v -> IntValue -> VariableIdentifier -> FinFree -> FinFree
FinFree.substInt  IntValue
v VariableIdentifier
x (HomogeneousFormula -> FinFree
lower HomogeneousFormula
phi)) FinFree
FinFree.Top    (Set IntValue -> [IntValue]
forall a. Set a -> [a]
Set.toList Set IntValue
dom)
lower (PropTextForallN VariableIdentifier
x Set VariableIdentifier
dom HomogeneousFormula
phi) =
  (VariableIdentifier -> FinFree -> FinFree)
-> FinFree -> [VariableIdentifier] -> FinFree
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (FinFree -> FinFree -> FinFree
FinFree.And (FinFree -> FinFree -> FinFree)
-> (VariableIdentifier -> FinFree)
-> VariableIdentifier
-> FinFree
-> FinFree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \VariableIdentifier
v -> Extended VariableIdentifier
-> VariableIdentifier -> FinFree -> FinFree
FinFree.substText (VariableIdentifier -> Extended VariableIdentifier
forall a. a -> Extended a
Val VariableIdentifier
v) VariableIdentifier
x (HomogeneousFormula -> FinFree
lower HomogeneousFormula
phi)) FinFree
FinFree.Top    (Set VariableIdentifier -> [VariableIdentifier]
forall a. Set a -> [a]
Set.toList Set VariableIdentifier
dom)
-- ∃x ∈ {v₁,...,vₙ}. φ  ≡  φ[v₁/x] ∨ ... ∨ φ[vₙ/x]   (⊥ when dom is empty)
lower (PropIntExistsN VariableIdentifier
x Set IntValue
dom HomogeneousFormula
phi) =
  (IntValue -> FinFree -> FinFree)
-> FinFree -> [IntValue] -> FinFree
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (FinFree -> FinFree -> FinFree
FinFree.Or  (FinFree -> FinFree -> FinFree)
-> (IntValue -> FinFree) -> IntValue -> FinFree -> FinFree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \IntValue
v -> IntValue -> VariableIdentifier -> FinFree -> FinFree
FinFree.substInt  IntValue
v VariableIdentifier
x (HomogeneousFormula -> FinFree
lower HomogeneousFormula
phi)) FinFree
FinFree.Bottom (Set IntValue -> [IntValue]
forall a. Set a -> [a]
Set.toList Set IntValue
dom)
lower (PropTextExistsN VariableIdentifier
x Set VariableIdentifier
dom HomogeneousFormula
phi) =
  (VariableIdentifier -> FinFree -> FinFree)
-> FinFree -> [VariableIdentifier] -> FinFree
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (FinFree -> FinFree -> FinFree
FinFree.Or  (FinFree -> FinFree -> FinFree)
-> (VariableIdentifier -> FinFree)
-> VariableIdentifier
-> FinFree
-> FinFree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \VariableIdentifier
v -> Extended VariableIdentifier
-> VariableIdentifier -> FinFree -> FinFree
FinFree.substText (VariableIdentifier -> Extended VariableIdentifier
forall a. a -> Extended a
Val VariableIdentifier
v) VariableIdentifier
x (HomogeneousFormula -> FinFree
lower HomogeneousFormula
phi)) FinFree
FinFree.Bottom (Set VariableIdentifier -> [VariableIdentifier]
forall a. Set a -> [a]
Set.toList Set VariableIdentifier
dom)

-- | Evaluate the `HomogeneousFormula` onto `Bool`.
eval :: HomogeneousFormula -> Bool
eval :: HomogeneousFormula -> Bool
eval = FinFree -> Bool
FinFree.eval (FinFree -> Bool)
-> (HomogeneousFormula -> FinFree) -> HomogeneousFormula -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HomogeneousFormula -> FinFree
lower

-- | This is the "easy" part of the iso: `HomogeneousFormula` ≅ `Bool`
quote :: Bool -> HomogeneousFormula
quote :: Bool -> HomogeneousFormula
quote Bool
True  = HomogeneousFormula
Top
quote Bool
False = HomogeneousFormula
Bottom

-- | Check equivalence of two `HomogeneousFormula`s.
equiv :: HomogeneousFormula -> HomogeneousFormula -> Bool
equiv :: HomogeneousFormula -> HomogeneousFormula -> Bool
equiv = (Bool -> Bool -> Bool)
-> (HomogeneousFormula -> Bool)
-> HomogeneousFormula
-> HomogeneousFormula
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
on Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
(==) HomogeneousFormula -> Bool
eval

retract :: Formula event ty -> Maybe HomogeneousFormula
retract :: forall event ty. Formula event ty -> Maybe HomogeneousFormula
retract = Set VariableIdentifier
-> Formula event ty -> Maybe HomogeneousFormula
forall event ty.
Set VariableIdentifier
-> Formula event ty -> Maybe HomogeneousFormula
go Set VariableIdentifier
forall a. Set a
Set.empty where
  go :: Set VariableIdentifier -> Formula event ty -> Maybe HomogeneousFormula
  go :: forall event ty.
Set VariableIdentifier
-> Formula event ty -> Maybe HomogeneousFormula
go Set VariableIdentifier
_     (F.ForallN {})                   = Maybe HomogeneousFormula
forall a. Maybe a
Nothing
  go Set VariableIdentifier
_     (F.ExistsN {})                   = Maybe HomogeneousFormula
forall a. Maybe a
Nothing
  go Set VariableIdentifier
_     (F.Forall {})                    = Maybe HomogeneousFormula
forall a. Maybe a
Nothing
  go Set VariableIdentifier
_     (F.NextN {})                     = Maybe HomogeneousFormula
forall a. Maybe a
Nothing
  go Set VariableIdentifier
_     (F.UntilN {})                    = Maybe HomogeneousFormula
forall a. Maybe a
Nothing
  go Set VariableIdentifier
_     (F.Atom {})                      = Maybe HomogeneousFormula
forall a. Maybe a
Nothing
  go Set VariableIdentifier
_     (F.Next Formula event ty
_)                       = Maybe HomogeneousFormula
forall a. Maybe a
Nothing
  go Set VariableIdentifier
bound (F.And Formula event ty
phi Formula event ty
psi)                  = HomogeneousFormula -> HomogeneousFormula -> HomogeneousFormula
And (HomogeneousFormula -> HomogeneousFormula -> HomogeneousFormula)
-> Maybe HomogeneousFormula
-> Maybe (HomogeneousFormula -> HomogeneousFormula)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set VariableIdentifier
-> Formula event ty -> Maybe HomogeneousFormula
forall event ty.
Set VariableIdentifier
-> Formula event ty -> Maybe HomogeneousFormula
go Set VariableIdentifier
bound Formula event ty
phi Maybe (HomogeneousFormula -> HomogeneousFormula)
-> Maybe HomogeneousFormula -> Maybe HomogeneousFormula
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Set VariableIdentifier
-> Formula event ty -> Maybe HomogeneousFormula
forall event ty.
Set VariableIdentifier
-> Formula event ty -> Maybe HomogeneousFormula
go Set VariableIdentifier
bound Formula event ty
psi
  go Set VariableIdentifier
bound (F.Or Formula event ty
phi Formula event ty
psi)                   = HomogeneousFormula -> HomogeneousFormula -> HomogeneousFormula
Or (HomogeneousFormula -> HomogeneousFormula -> HomogeneousFormula)
-> Maybe HomogeneousFormula
-> Maybe (HomogeneousFormula -> HomogeneousFormula)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set VariableIdentifier
-> Formula event ty -> Maybe HomogeneousFormula
forall event ty.
Set VariableIdentifier
-> Formula event ty -> Maybe HomogeneousFormula
go Set VariableIdentifier
bound Formula event ty
phi Maybe (HomogeneousFormula -> HomogeneousFormula)
-> Maybe HomogeneousFormula -> Maybe HomogeneousFormula
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Set VariableIdentifier
-> Formula event ty -> Maybe HomogeneousFormula
forall event ty.
Set VariableIdentifier
-> Formula event ty -> Maybe HomogeneousFormula
go Set VariableIdentifier
bound Formula event ty
psi
  go Set VariableIdentifier
bound (F.Implies Formula event ty
phi Formula event ty
psi)              = HomogeneousFormula -> HomogeneousFormula -> HomogeneousFormula
Implies (HomogeneousFormula -> HomogeneousFormula -> HomogeneousFormula)
-> Maybe HomogeneousFormula
-> Maybe (HomogeneousFormula -> HomogeneousFormula)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set VariableIdentifier
-> Formula event ty -> Maybe HomogeneousFormula
forall event ty.
Set VariableIdentifier
-> Formula event ty -> Maybe HomogeneousFormula
go Set VariableIdentifier
bound Formula event ty
phi Maybe (HomogeneousFormula -> HomogeneousFormula)
-> Maybe HomogeneousFormula -> Maybe HomogeneousFormula
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Set VariableIdentifier
-> Formula event ty -> Maybe HomogeneousFormula
forall event ty.
Set VariableIdentifier
-> Formula event ty -> Maybe HomogeneousFormula
go Set VariableIdentifier
bound Formula event ty
psi
  go Set VariableIdentifier
bound (F.Not Formula event ty
phi)                      = HomogeneousFormula -> HomogeneousFormula
Not (HomogeneousFormula -> HomogeneousFormula)
-> Maybe HomogeneousFormula -> Maybe HomogeneousFormula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set VariableIdentifier
-> Formula event ty -> Maybe HomogeneousFormula
forall event ty.
Set VariableIdentifier
-> Formula event ty -> Maybe HomogeneousFormula
go Set VariableIdentifier
bound Formula event ty
phi
  go Set VariableIdentifier
_     Formula event ty
F.Bottom                         = HomogeneousFormula -> Maybe HomogeneousFormula
forall a. a -> Maybe a
Just HomogeneousFormula
Bottom
  go Set VariableIdentifier
_     Formula event ty
F.Top                            = HomogeneousFormula -> Maybe HomogeneousFormula
forall a. a -> Maybe a
Just HomogeneousFormula
Top
  go Set VariableIdentifier
bound (F.PropIntBinRel BinRel
rel Relevance event ty
_ IntTerm
lhs IntTerm
rhs)
    | Set VariableIdentifier -> IntTerm -> Bool
groundTerm Set VariableIdentifier
bound IntTerm
lhs Bool -> Bool -> Bool
&& Set VariableIdentifier -> IntTerm -> Bool
groundTerm Set VariableIdentifier
bound IntTerm
rhs = HomogeneousFormula -> Maybe HomogeneousFormula
forall a. a -> Maybe a
Just (BinRel -> IntTerm -> IntTerm -> HomogeneousFormula
PropIntBinRel BinRel
rel IntTerm
lhs IntTerm
rhs)
  go Set VariableIdentifier
_     F.PropIntBinRel {}               = Maybe HomogeneousFormula
forall a. Maybe a
Nothing
  go Set VariableIdentifier
_     (F.PropTextEq Relevance event ty
_ (TextConst VariableIdentifier
c) VariableIdentifier
v) = HomogeneousFormula -> Maybe HomogeneousFormula
forall a. a -> Maybe a
Just (TextTerm -> VariableIdentifier -> HomogeneousFormula
PropTextEq (VariableIdentifier -> TextTerm
TextConst VariableIdentifier
c) VariableIdentifier
v)
  go Set VariableIdentifier
bound (F.PropTextEq Relevance event ty
_ (TextVar VariableIdentifier
x) VariableIdentifier
v)
                | VariableIdentifier -> Set VariableIdentifier -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member VariableIdentifier
x Set VariableIdentifier
bound        = HomogeneousFormula -> Maybe HomogeneousFormula
forall a. a -> Maybe a
Just (TextTerm -> VariableIdentifier -> HomogeneousFormula
PropTextEq (VariableIdentifier -> TextTerm
TextVar VariableIdentifier
x) VariableIdentifier
v)
  go Set VariableIdentifier
_     (F.PropTextEq Relevance event ty
_ (TextVar VariableIdentifier
_) VariableIdentifier
_)   = Maybe HomogeneousFormula
forall a. Maybe a
Nothing
  go Set VariableIdentifier
bound (F.PropIntForall VariableIdentifier
x Formula event ty
phi)           = VariableIdentifier -> HomogeneousFormula -> HomogeneousFormula
PropIntForall VariableIdentifier
x   (HomogeneousFormula -> HomogeneousFormula)
-> Maybe HomogeneousFormula -> Maybe HomogeneousFormula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set VariableIdentifier
-> Formula event ty -> Maybe HomogeneousFormula
forall event ty.
Set VariableIdentifier
-> Formula event ty -> Maybe HomogeneousFormula
go (VariableIdentifier
-> Set VariableIdentifier -> Set VariableIdentifier
forall a. Ord a => a -> Set a -> Set a
Set.insert VariableIdentifier
x Set VariableIdentifier
bound) Formula event ty
phi
  go Set VariableIdentifier
bound (F.PropTextForall VariableIdentifier
x Formula event ty
phi)          = VariableIdentifier -> HomogeneousFormula -> HomogeneousFormula
PropTextForall VariableIdentifier
x  (HomogeneousFormula -> HomogeneousFormula)
-> Maybe HomogeneousFormula -> Maybe HomogeneousFormula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set VariableIdentifier
-> Formula event ty -> Maybe HomogeneousFormula
forall event ty.
Set VariableIdentifier
-> Formula event ty -> Maybe HomogeneousFormula
go (VariableIdentifier
-> Set VariableIdentifier -> Set VariableIdentifier
forall a. Ord a => a -> Set a -> Set a
Set.insert VariableIdentifier
x Set VariableIdentifier
bound) Formula event ty
phi
  go Set VariableIdentifier
bound (F.PropIntForallN VariableIdentifier
x Set IntValue
dom Formula event ty
phi)      = VariableIdentifier
-> Set IntValue -> HomogeneousFormula -> HomogeneousFormula
PropIntForallN  VariableIdentifier
x Set IntValue
dom (HomogeneousFormula -> HomogeneousFormula)
-> Maybe HomogeneousFormula -> Maybe HomogeneousFormula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set VariableIdentifier
-> Formula event ty -> Maybe HomogeneousFormula
forall event ty.
Set VariableIdentifier
-> Formula event ty -> Maybe HomogeneousFormula
go (VariableIdentifier
-> Set VariableIdentifier -> Set VariableIdentifier
forall a. Ord a => a -> Set a -> Set a
Set.insert VariableIdentifier
x Set VariableIdentifier
bound) Formula event ty
phi
  go Set VariableIdentifier
bound (F.PropTextForallN VariableIdentifier
x Set VariableIdentifier
dom Formula event ty
phi)     = VariableIdentifier
-> Set VariableIdentifier
-> HomogeneousFormula
-> HomogeneousFormula
PropTextForallN VariableIdentifier
x Set VariableIdentifier
dom (HomogeneousFormula -> HomogeneousFormula)
-> Maybe HomogeneousFormula -> Maybe HomogeneousFormula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set VariableIdentifier
-> Formula event ty -> Maybe HomogeneousFormula
forall event ty.
Set VariableIdentifier
-> Formula event ty -> Maybe HomogeneousFormula
go (VariableIdentifier
-> Set VariableIdentifier -> Set VariableIdentifier
forall a. Ord a => a -> Set a -> Set a
Set.insert VariableIdentifier
x Set VariableIdentifier
bound) Formula event ty
phi
  go Set VariableIdentifier
bound (F.PropIntExists VariableIdentifier
x Formula event ty
phi)           = VariableIdentifier -> HomogeneousFormula -> HomogeneousFormula
PropIntExists VariableIdentifier
x   (HomogeneousFormula -> HomogeneousFormula)
-> Maybe HomogeneousFormula -> Maybe HomogeneousFormula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set VariableIdentifier
-> Formula event ty -> Maybe HomogeneousFormula
forall event ty.
Set VariableIdentifier
-> Formula event ty -> Maybe HomogeneousFormula
go (VariableIdentifier
-> Set VariableIdentifier -> Set VariableIdentifier
forall a. Ord a => a -> Set a -> Set a
Set.insert VariableIdentifier
x Set VariableIdentifier
bound) Formula event ty
phi
  go Set VariableIdentifier
bound (F.PropTextExists VariableIdentifier
x Formula event ty
phi)          = VariableIdentifier -> HomogeneousFormula -> HomogeneousFormula
PropTextExists VariableIdentifier
x  (HomogeneousFormula -> HomogeneousFormula)
-> Maybe HomogeneousFormula -> Maybe HomogeneousFormula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set VariableIdentifier
-> Formula event ty -> Maybe HomogeneousFormula
forall event ty.
Set VariableIdentifier
-> Formula event ty -> Maybe HomogeneousFormula
go (VariableIdentifier
-> Set VariableIdentifier -> Set VariableIdentifier
forall a. Ord a => a -> Set a -> Set a
Set.insert VariableIdentifier
x Set VariableIdentifier
bound) Formula event ty
phi
  go Set VariableIdentifier
bound (F.PropIntExistsN VariableIdentifier
x Set IntValue
dom Formula event ty
phi)      = VariableIdentifier
-> Set IntValue -> HomogeneousFormula -> HomogeneousFormula
PropIntExistsN  VariableIdentifier
x Set IntValue
dom (HomogeneousFormula -> HomogeneousFormula)
-> Maybe HomogeneousFormula -> Maybe HomogeneousFormula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set VariableIdentifier
-> Formula event ty -> Maybe HomogeneousFormula
forall event ty.
Set VariableIdentifier
-> Formula event ty -> Maybe HomogeneousFormula
go (VariableIdentifier
-> Set VariableIdentifier -> Set VariableIdentifier
forall a. Ord a => a -> Set a -> Set a
Set.insert VariableIdentifier
x Set VariableIdentifier
bound) Formula event ty
phi
  go Set VariableIdentifier
bound (F.PropTextExistsN VariableIdentifier
x Set VariableIdentifier
dom Formula event ty
phi)     = VariableIdentifier
-> Set VariableIdentifier
-> HomogeneousFormula
-> HomogeneousFormula
PropTextExistsN VariableIdentifier
x Set VariableIdentifier
dom (HomogeneousFormula -> HomogeneousFormula)
-> Maybe HomogeneousFormula -> Maybe HomogeneousFormula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set VariableIdentifier
-> Formula event ty -> Maybe HomogeneousFormula
forall event ty.
Set VariableIdentifier
-> Formula event ty -> Maybe HomogeneousFormula
go (VariableIdentifier
-> Set VariableIdentifier -> Set VariableIdentifier
forall a. Ord a => a -> Set a -> Set a
Set.insert VariableIdentifier
x Set VariableIdentifier
bound) Formula event ty
phi
  groundTerm :: Set VariableIdentifier -> IntTerm -> Bool
  groundTerm :: Set VariableIdentifier -> IntTerm -> Bool
groundTerm Set VariableIdentifier
_      (IntConst IntValue
_)   = Bool
True
  groundTerm Set VariableIdentifier
bound' (IntVar IntValue
_ VariableIdentifier
x)   = VariableIdentifier -> Set VariableIdentifier -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member VariableIdentifier
x Set VariableIdentifier
bound'
  groundTerm Set VariableIdentifier
bound' (IntSum IntTerm
a IntTerm
b)   = Set VariableIdentifier -> IntTerm -> Bool
groundTerm Set VariableIdentifier
bound' IntTerm
a Bool -> Bool -> Bool
&& Set VariableIdentifier -> IntTerm -> Bool
groundTerm Set VariableIdentifier
bound' IntTerm
b

normaliseHomogeneous :: Formula event ty -> Maybe (Formula event ty)
normaliseHomogeneous :: forall event ty. Formula event ty -> Maybe (Formula event ty)
normaliseHomogeneous Formula event ty
phi =
  HomogeneousFormula -> Formula event ty
forall event ty. HomogeneousFormula -> Formula event ty
toFormula (HomogeneousFormula -> Formula event ty)
-> (HomogeneousFormula -> HomogeneousFormula)
-> HomogeneousFormula
-> Formula event ty
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> HomogeneousFormula
quote (Bool -> HomogeneousFormula)
-> (HomogeneousFormula -> Bool)
-> HomogeneousFormula
-> HomogeneousFormula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HomogeneousFormula -> Bool
eval (HomogeneousFormula -> Formula event ty)
-> Maybe HomogeneousFormula -> Maybe (Formula event ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula event ty -> Maybe HomogeneousFormula
forall event ty. Formula event ty -> Maybe HomogeneousFormula
retract Formula event ty
phi