module Hermod.ReCon.LTL.Internal.Progress(next, terminate) where

import           Hermod.ReCon.LTL.Formula
import qualified Hermod.ReCon.LTL.Formula as F
import           Hermod.ReCon.LTL.Internal.IR.HomogeneousFormula (HomogeneousFormula)
import qualified Hermod.ReCon.LTL.Internal.IR.HomogeneousFormula as H

import           Prelude hiding (lookup)

import           Control.Monad.Reader (Reader, asks)
import           Data.Map.Strict (lookup)
import qualified Data.Set as Set
import qualified Data.Text as Text

-- This file concerns algorithmically checking formula satisfiability.
--  There are two parts:
--    *) (t t̄ ⊧ φ) for producing a new formula φ' such that the two are equi-satisfiable,
--          but the new one operates on the suffix of the original context: (t̄ ⊧ φ')
--    *) (∅ ⊧ φ) for checking satisfiability against the empty context.

-- | This is an algorithm for representing
--   (t t̄ ⊧ φ) in terms of ∃φ'. (t̄ ⊧ φ')
next :: (Event event ty, Eq ty) => Formula event ty -> event -> Reader OnMissingKey (Formula event ty)
next :: forall event ty.
(Event event ty, Eq ty) =>
Formula event ty -> event -> Reader OnMissingKey (Formula event ty)
next (Forall Word
k Formula event ty
phi) event
s = Formula event ty -> event -> Reader OnMissingKey (Formula event ty)
forall event ty.
(Event event ty, Eq ty) =>
Formula event ty -> event -> Reader OnMissingKey (Formula event ty)
next (Word -> Formula event ty -> Formula event ty
forall event ty. Word -> Formula event ty -> Formula event ty
unfoldForall Word
k Formula event ty
phi) event
s
next (ForallN Word
k Formula event ty
phi) event
s = Formula event ty -> event -> Reader OnMissingKey (Formula event ty)
forall event ty.
(Event event ty, Eq ty) =>
Formula event ty -> event -> Reader OnMissingKey (Formula event ty)
next (Word -> Formula event ty -> Formula event ty
forall event ty. Word -> Formula event ty -> Formula event ty
unfoldForallN Word
k Formula event ty
phi) event
s
next (ExistsN Word
k Formula event ty
phi) event
s = Formula event ty -> event -> Reader OnMissingKey (Formula event ty)
forall event ty.
(Event event ty, Eq ty) =>
Formula event ty -> event -> Reader OnMissingKey (Formula event ty)
next (Word -> Formula event ty -> Formula event ty
forall event ty. Word -> Formula event ty -> Formula event ty
unfoldExistsN Word
k Formula event ty
phi) event
s
next (NextN Word
k Formula event ty
phi) event
s = Formula event ty -> event -> Reader OnMissingKey (Formula event ty)
forall event ty.
(Event event ty, Eq ty) =>
Formula event ty -> event -> Reader OnMissingKey (Formula event ty)
next (Word -> Formula event ty -> Formula event ty
forall event ty. Word -> Formula event ty -> Formula event ty
unfoldNextN Word
k Formula event ty
phi) event
s
next (UntilN Word
k Formula event ty
phi Formula event ty
psi) event
s = Formula event ty -> event -> Reader OnMissingKey (Formula event ty)
forall event ty.
(Event event ty, Eq ty) =>
Formula event ty -> event -> Reader OnMissingKey (Formula event ty)
next (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
k Formula event ty
phi Formula event ty
psi) event
s
next (Next Formula event ty
phi) event
_ = Formula event ty -> Reader OnMissingKey (Formula event ty)
forall a. a -> ReaderT OnMissingKey Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Formula event ty
phi
next (And Formula event ty
phi Formula event ty
psi) event
s = 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 -> Formula event ty -> Formula event ty)
-> Reader OnMissingKey (Formula event ty)
-> ReaderT
     OnMissingKey Identity (Formula event ty -> Formula event ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula event ty -> event -> Reader OnMissingKey (Formula event ty)
forall event ty.
(Event event ty, Eq ty) =>
Formula event ty -> event -> Reader OnMissingKey (Formula event ty)
next Formula event ty
phi event
s ReaderT
  OnMissingKey Identity (Formula event ty -> Formula event ty)
-> Reader OnMissingKey (Formula event ty)
-> Reader OnMissingKey (Formula event ty)
forall a b.
ReaderT OnMissingKey Identity (a -> b)
-> ReaderT OnMissingKey Identity a
-> ReaderT OnMissingKey Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Formula event ty -> event -> Reader OnMissingKey (Formula event ty)
forall event ty.
(Event event ty, Eq ty) =>
Formula event ty -> event -> Reader OnMissingKey (Formula event ty)
next Formula event ty
psi event
s
next (Or Formula event ty
phi Formula event ty
psi) event
s = 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 -> Formula event ty -> Formula event ty)
-> Reader OnMissingKey (Formula event ty)
-> ReaderT
     OnMissingKey Identity (Formula event ty -> Formula event ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula event ty -> event -> Reader OnMissingKey (Formula event ty)
forall event ty.
(Event event ty, Eq ty) =>
Formula event ty -> event -> Reader OnMissingKey (Formula event ty)
next Formula event ty
phi event
s ReaderT
  OnMissingKey Identity (Formula event ty -> Formula event ty)
-> Reader OnMissingKey (Formula event ty)
-> Reader OnMissingKey (Formula event ty)
forall a b.
ReaderT OnMissingKey Identity (a -> b)
-> ReaderT OnMissingKey Identity a
-> ReaderT OnMissingKey Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Formula event ty -> event -> Reader OnMissingKey (Formula event ty)
forall event ty.
(Event event ty, Eq ty) =>
Formula event ty -> event -> Reader OnMissingKey (Formula event ty)
next Formula event ty
psi event
s
next (Implies Formula event ty
phi Formula event ty
psi) event
s = 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 -> Formula event ty -> Formula event ty)
-> Reader OnMissingKey (Formula event ty)
-> ReaderT
     OnMissingKey Identity (Formula event ty -> Formula event ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula event ty -> event -> Reader OnMissingKey (Formula event ty)
forall event ty.
(Event event ty, Eq ty) =>
Formula event ty -> event -> Reader OnMissingKey (Formula event ty)
next Formula event ty
phi event
s ReaderT
  OnMissingKey Identity (Formula event ty -> Formula event ty)
-> Reader OnMissingKey (Formula event ty)
-> Reader OnMissingKey (Formula event ty)
forall a b.
ReaderT OnMissingKey Identity (a -> b)
-> ReaderT OnMissingKey Identity a
-> ReaderT OnMissingKey Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Formula event ty -> event -> Reader OnMissingKey (Formula event ty)
forall event ty.
(Event event ty, Eq ty) =>
Formula event ty -> event -> Reader OnMissingKey (Formula event ty)
next Formula event ty
psi event
s
next (Not Formula event ty
phi) event
s = Formula event ty -> Formula event ty
forall event ty. Formula event ty -> Formula event ty
Not (Formula event ty -> Formula event ty)
-> Reader OnMissingKey (Formula event ty)
-> Reader OnMissingKey (Formula event ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula event ty -> event -> Reader OnMissingKey (Formula event ty)
forall event ty.
(Event event ty, Eq ty) =>
Formula event ty -> event -> Reader OnMissingKey (Formula event ty)
next Formula event ty
phi event
s
next Formula event ty
Bottom event
_ = Formula event ty -> Reader OnMissingKey (Formula event ty)
forall a. a -> ReaderT OnMissingKey Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Formula event ty
forall event ty. Formula event ty
Bottom
next Formula event ty
Top event
_ = Formula event ty -> Reader OnMissingKey (Formula event ty)
forall a. a -> ReaderT OnMissingKey Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Formula event ty
forall event ty. Formula event ty
Top
next (Atom ty
c Set PropConstraint
is) event
s | event -> ty -> Bool
forall a ty. Event a ty => a -> ty -> Bool
ofTy event
s ty
c =
  [Formula event ty] -> Formula event ty
forall event ty. [Formula event ty] -> Formula event ty
F.and ([Formula event ty] -> Formula event ty)
-> ReaderT OnMissingKey Identity [Formula event ty]
-> Reader OnMissingKey (Formula event ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (PropConstraint -> Reader OnMissingKey (Formula event ty))
-> [PropConstraint]
-> ReaderT OnMissingKey Identity [Formula event ty]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse PropConstraint -> Reader OnMissingKey (Formula event ty)
forall {f :: * -> *}.
MonadReader OnMissingKey f =>
PropConstraint -> f (Formula event ty)
missingKey' (Set PropConstraint -> [PropConstraint]
forall a. Set a -> [a]
Set.toList Set PropConstraint
is)
  where
    missingKey' :: PropConstraint -> f (Formula event ty)
missingKey' (IntPropConstraint PropName
key IntTerm
t) =
      case PropName -> Map PropName IntValue -> Maybe IntValue
forall k a. Ord k => k -> Map k a -> Maybe a
lookup PropName
key (event -> ty -> Map PropName IntValue
forall a ty. Event a ty => a -> ty -> Map PropName IntValue
intProps event
s ty
c) of
        Just IntValue
v  -> Formula event ty -> f (Formula event ty)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Formula event ty -> f (Formula event ty))
-> Formula event ty -> f (Formula event ty)
forall a b. (a -> b) -> a -> b
$ BinRel
-> Relevance event ty -> IntTerm -> IntTerm -> Formula event ty
forall event ty.
BinRel
-> Relevance event ty -> IntTerm -> IntTerm -> Formula event ty
PropIntBinRel BinRel
Eq ((event, ty) -> Relevance event ty
forall a. a -> Set a
Set.singleton (event
s, ty
c)) IntTerm
t (IntValue -> IntTerm
IntConst IntValue
v)
        Maybe IntValue
Nothing -> PropName -> f (Formula event ty)
forall {m :: * -> *} {event} {ty}.
MonadReader OnMissingKey m =>
PropName -> m (Formula event ty)
missingKey PropName
key
    missingKey' (TextPropConstraint PropName
key TextTerm
t) =
      case PropName -> Map PropName PropName -> Maybe PropName
forall k a. Ord k => k -> Map k a -> Maybe a
lookup PropName
key (event -> ty -> Map PropName PropName
forall a ty. Event a ty => a -> ty -> Map PropName PropName
textProps event
s ty
c) of
        Just PropName
v  -> Formula event ty -> f (Formula event ty)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Formula event ty -> f (Formula event ty))
-> Formula event ty -> f (Formula event ty)
forall a b. (a -> b) -> a -> b
$ Relevance event ty -> TextTerm -> PropName -> Formula event ty
forall event ty.
Relevance event ty -> TextTerm -> PropName -> Formula event ty
PropTextEq ((event, ty) -> Relevance event ty
forall a. a -> Set a
Set.singleton (event
s, ty
c)) TextTerm
t PropName
v
        Maybe PropName
Nothing -> PropName -> f (Formula event ty)
forall {m :: * -> *} {event} {ty}.
MonadReader OnMissingKey m =>
PropName -> m (Formula event ty)
missingKey PropName
key
    missingKey :: PropName -> m (Formula event ty)
missingKey PropName
key = (OnMissingKey -> Formula event ty) -> m (Formula event ty)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ((OnMissingKey -> Formula event ty) -> m (Formula event ty))
-> (OnMissingKey -> Formula event ty) -> m (Formula event ty)
forall a b. (a -> b) -> a -> b
$ \case
      OnMissingKey
BottomOnMissingKey -> Formula event ty
forall event ty. Formula event ty
Bottom
      OnMissingKey
CrashOnMissingKey  -> [Char] -> Formula event ty
forall a. HasCallStack => [Char] -> a
error ([Char] -> Formula event ty) -> [Char] -> Formula event ty
forall a b. (a -> b) -> a -> b
$ [Char]
"Missing key: " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> PropName -> [Char]
Text.unpack PropName
key
next (Atom {}) event
_ = Formula event ty -> Reader OnMissingKey (Formula event ty)
forall a. a -> ReaderT OnMissingKey Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Formula event ty
forall event ty. Formula event ty
Bottom
next (PropIntForall  PropName
x Formula event ty
phi) event
s = PropName -> Formula event ty -> Formula event ty
forall event ty. PropName -> Formula event ty -> Formula event ty
PropIntForall  PropName
x (Formula event ty -> Formula event ty)
-> Reader OnMissingKey (Formula event ty)
-> Reader OnMissingKey (Formula event ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula event ty -> event -> Reader OnMissingKey (Formula event ty)
forall event ty.
(Event event ty, Eq ty) =>
Formula event ty -> event -> Reader OnMissingKey (Formula event ty)
next Formula event ty
phi event
s
next (PropTextForall PropName
x Formula event ty
phi) event
s = PropName -> Formula event ty -> Formula event ty
forall event ty. PropName -> Formula event ty -> Formula event ty
PropTextForall PropName
x (Formula event ty -> Formula event ty)
-> Reader OnMissingKey (Formula event ty)
-> Reader OnMissingKey (Formula event ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula event ty -> event -> Reader OnMissingKey (Formula event ty)
forall event ty.
(Event event ty, Eq ty) =>
Formula event ty -> event -> Reader OnMissingKey (Formula event ty)
next Formula event ty
phi event
s
next (PropIntForallN  PropName
x Set IntValue
dom Formula event ty
phi) event
s = PropName -> Set IntValue -> Formula event ty -> Formula event ty
forall event ty.
PropName -> Set IntValue -> Formula event ty -> Formula event ty
PropIntForallN  PropName
x Set IntValue
dom (Formula event ty -> Formula event ty)
-> Reader OnMissingKey (Formula event ty)
-> Reader OnMissingKey (Formula event ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula event ty -> event -> Reader OnMissingKey (Formula event ty)
forall event ty.
(Event event ty, Eq ty) =>
Formula event ty -> event -> Reader OnMissingKey (Formula event ty)
next Formula event ty
phi event
s
next (PropTextForallN PropName
x Set PropName
dom Formula event ty
phi) event
s = PropName -> Set PropName -> Formula event ty -> Formula event ty
forall event ty.
PropName -> Set PropName -> Formula event ty -> Formula event ty
PropTextForallN PropName
x Set PropName
dom (Formula event ty -> Formula event ty)
-> Reader OnMissingKey (Formula event ty)
-> Reader OnMissingKey (Formula event ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula event ty -> event -> Reader OnMissingKey (Formula event ty)
forall event ty.
(Event event ty, Eq ty) =>
Formula event ty -> event -> Reader OnMissingKey (Formula event ty)
next Formula event ty
phi event
s
next (PropIntExists  PropName
x Formula event ty
phi) event
s = PropName -> Formula event ty -> Formula event ty
forall event ty. PropName -> Formula event ty -> Formula event ty
PropIntExists  PropName
x (Formula event ty -> Formula event ty)
-> Reader OnMissingKey (Formula event ty)
-> Reader OnMissingKey (Formula event ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula event ty -> event -> Reader OnMissingKey (Formula event ty)
forall event ty.
(Event event ty, Eq ty) =>
Formula event ty -> event -> Reader OnMissingKey (Formula event ty)
next Formula event ty
phi event
s
next (PropTextExists PropName
x Formula event ty
phi) event
s = PropName -> Formula event ty -> Formula event ty
forall event ty. PropName -> Formula event ty -> Formula event ty
PropTextExists PropName
x (Formula event ty -> Formula event ty)
-> Reader OnMissingKey (Formula event ty)
-> Reader OnMissingKey (Formula event ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula event ty -> event -> Reader OnMissingKey (Formula event ty)
forall event ty.
(Event event ty, Eq ty) =>
Formula event ty -> event -> Reader OnMissingKey (Formula event ty)
next Formula event ty
phi event
s
next (PropIntExistsN  PropName
x Set IntValue
dom Formula event ty
phi) event
s = PropName -> Set IntValue -> Formula event ty -> Formula event ty
forall event ty.
PropName -> Set IntValue -> Formula event ty -> Formula event ty
PropIntExistsN  PropName
x Set IntValue
dom (Formula event ty -> Formula event ty)
-> Reader OnMissingKey (Formula event ty)
-> Reader OnMissingKey (Formula event ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula event ty -> event -> Reader OnMissingKey (Formula event ty)
forall event ty.
(Event event ty, Eq ty) =>
Formula event ty -> event -> Reader OnMissingKey (Formula event ty)
next Formula event ty
phi event
s
next (PropTextExistsN PropName
x Set PropName
dom Formula event ty
phi) event
s = PropName -> Set PropName -> Formula event ty -> Formula event ty
forall event ty.
PropName -> Set PropName -> Formula event ty -> Formula event ty
PropTextExistsN PropName
x Set PropName
dom (Formula event ty -> Formula event ty)
-> Reader OnMissingKey (Formula event ty)
-> Reader OnMissingKey (Formula event ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula event ty -> event -> Reader OnMissingKey (Formula event ty)
forall event ty.
(Event event ty, Eq ty) =>
Formula event ty -> event -> Reader OnMissingKey (Formula event ty)
next Formula event ty
phi event
s
next (PropIntBinRel BinRel
rel Relevance event ty
r IntTerm
a IntTerm
b) event
_ = Formula event ty -> Reader OnMissingKey (Formula event ty)
forall a. a -> ReaderT OnMissingKey Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Formula event ty -> Reader OnMissingKey (Formula event ty))
-> Formula event ty -> Reader OnMissingKey (Formula event ty)
forall a b. (a -> b) -> a -> b
$ BinRel
-> Relevance event ty -> IntTerm -> IntTerm -> Formula event ty
forall event ty.
BinRel
-> Relevance event ty -> IntTerm -> IntTerm -> Formula event ty
PropIntBinRel BinRel
rel Relevance event ty
r IntTerm
a IntTerm
b
next (PropTextEq Relevance event ty
rel TextTerm
a PropName
b)      event
_ = Formula event ty -> Reader OnMissingKey (Formula event ty)
forall a. a -> ReaderT OnMissingKey Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Formula event ty -> Reader OnMissingKey (Formula event ty))
-> Formula event ty -> Reader OnMissingKey (Formula event ty)
forall a b. (a -> b) -> a -> b
$ Relevance event ty -> TextTerm -> PropName -> Formula event ty
forall event ty.
Relevance event ty -> TextTerm -> PropName -> Formula event ty
PropTextEq Relevance event ty
rel TextTerm
a PropName
b

-- | This is an algorithm for (∅ ⊧ ◯ φ)
terminateNext :: Formula event a -> HomogeneousFormula
terminateNext :: forall event a. Formula event a -> HomogeneousFormula
terminateNext (Next Formula event a
phi) = Formula event a -> HomogeneousFormula
forall event a. Formula event a -> HomogeneousFormula
terminateNext Formula event a
phi
terminateNext (Forall Word
_ Formula event a
phi)  = Formula event a -> HomogeneousFormula
forall event a. Formula event a -> HomogeneousFormula
terminateNext Formula event a
phi
terminateNext (Or Formula event a
phi Formula event a
psi) = Formula event a -> HomogeneousFormula
forall event a. Formula event a -> HomogeneousFormula
terminateNext Formula event a
phi HomogeneousFormula -> HomogeneousFormula -> HomogeneousFormula
`H.Or` Formula event a -> HomogeneousFormula
forall event a. Formula event a -> HomogeneousFormula
terminateNext Formula event a
psi
terminateNext (And Formula event a
phi Formula event a
psi) = Formula event a -> HomogeneousFormula
forall event a. Formula event a -> HomogeneousFormula
terminateNext Formula event a
phi HomogeneousFormula -> HomogeneousFormula -> HomogeneousFormula
`H.And` Formula event a -> HomogeneousFormula
forall event a. Formula event a -> HomogeneousFormula
terminateNext Formula event a
psi
terminateNext (Implies Formula event a
phi Formula event a
psi) = Formula event a -> HomogeneousFormula
forall event a. Formula event a -> HomogeneousFormula
terminateNext Formula event a
phi HomogeneousFormula -> HomogeneousFormula -> HomogeneousFormula
`H.Implies` Formula event a -> HomogeneousFormula
forall event a. Formula event a -> HomogeneousFormula
terminateNext Formula event a
psi
terminateNext (Not Formula event a
phi) = HomogeneousFormula -> HomogeneousFormula
H.Not (Formula event a -> HomogeneousFormula
forall event a. Formula event a -> HomogeneousFormula
terminateNext Formula event a
phi)
terminateNext (PropIntForall  PropName
x Formula event a
phi) = PropName -> HomogeneousFormula -> HomogeneousFormula
H.PropIntForall  PropName
x (Formula event a -> HomogeneousFormula
forall event a. Formula event a -> HomogeneousFormula
terminateNext Formula event a
phi)
terminateNext (PropTextForall PropName
x Formula event a
phi) = PropName -> HomogeneousFormula -> HomogeneousFormula
H.PropTextForall PropName
x (Formula event a -> HomogeneousFormula
forall event a. Formula event a -> HomogeneousFormula
terminateNext Formula event a
phi)
terminateNext (PropIntForallN  PropName
x Set IntValue
dom Formula event a
phi) = PropName
-> Set IntValue -> HomogeneousFormula -> HomogeneousFormula
H.PropIntForallN  PropName
x Set IntValue
dom (Formula event a -> HomogeneousFormula
forall event a. Formula event a -> HomogeneousFormula
terminateNext Formula event a
phi)
terminateNext (PropTextForallN PropName
x Set PropName
dom Formula event a
phi) = PropName
-> Set PropName -> HomogeneousFormula -> HomogeneousFormula
H.PropTextForallN PropName
x Set PropName
dom (Formula event a -> HomogeneousFormula
forall event a. Formula event a -> HomogeneousFormula
terminateNext Formula event a
phi)
terminateNext (PropIntExists  PropName
x Formula event a
phi) = PropName -> HomogeneousFormula -> HomogeneousFormula
H.PropIntExists  PropName
x (Formula event a -> HomogeneousFormula
forall event a. Formula event a -> HomogeneousFormula
terminateNext Formula event a
phi)
terminateNext (PropTextExists PropName
x Formula event a
phi) = PropName -> HomogeneousFormula -> HomogeneousFormula
H.PropTextExists PropName
x (Formula event a -> HomogeneousFormula
forall event a. Formula event a -> HomogeneousFormula
terminateNext Formula event a
phi)
terminateNext (PropIntExistsN  PropName
x Set IntValue
dom Formula event a
phi) = PropName
-> Set IntValue -> HomogeneousFormula -> HomogeneousFormula
H.PropIntExistsN  PropName
x Set IntValue
dom (Formula event a -> HomogeneousFormula
forall event a. Formula event a -> HomogeneousFormula
terminateNext Formula event a
phi)
terminateNext (PropTextExistsN PropName
x Set PropName
dom Formula event a
phi) = PropName
-> Set PropName -> HomogeneousFormula -> HomogeneousFormula
H.PropTextExistsN PropName
x Set PropName
dom (Formula event a -> HomogeneousFormula
forall event a. Formula event a -> HomogeneousFormula
terminateNext Formula event a
phi)
terminateNext (PropIntBinRel BinRel
rel Relevance event a
_ IntTerm
t IntTerm
v) = BinRel -> IntTerm -> IntTerm -> HomogeneousFormula
H.PropIntBinRel BinRel
rel IntTerm
t IntTerm
v
terminateNext (PropTextEq Relevance event a
_ TextTerm
t PropName
v)        = TextTerm -> PropName -> HomogeneousFormula
H.PropTextEq TextTerm
t PropName
v
terminateNext (NextN Word
_ Formula event a
phi) = Formula event a -> HomogeneousFormula
forall event a. Formula event a -> HomogeneousFormula
terminateNext Formula event a
phi
terminateNext (Atom a
ty Set PropConstraint
cs) = Formula Any a -> HomogeneousFormula
forall event a. Formula event a -> HomogeneousFormula
terminate (a -> Set PropConstraint -> Formula Any a
forall event ty. ty -> Set PropConstraint -> Formula event ty
Atom a
ty Set PropConstraint
cs)
terminateNext Formula event a
Bottom = Formula Any Any -> HomogeneousFormula
forall event a. Formula event a -> HomogeneousFormula
terminate Formula Any Any
forall event ty. Formula event ty
Bottom
terminateNext Formula event a
Top = Formula Any Any -> HomogeneousFormula
forall event a. Formula event a -> HomogeneousFormula
terminate Formula Any Any
forall event ty. Formula event ty
Top
terminateNext (ExistsN Word
k Formula event a
phi) = Formula event a -> HomogeneousFormula
forall event a. Formula event a -> HomogeneousFormula
terminateNext (Word -> Formula event a -> Formula event a
forall event ty. Word -> Formula event ty -> Formula event ty
unfoldExistsN Word
k Formula event a
phi)
terminateNext (ForallN Word
k Formula event a
phi) = Formula event a -> HomogeneousFormula
forall event a. Formula event a -> HomogeneousFormula
terminateNext (Word -> Formula event a -> Formula event a
forall event ty. Word -> Formula event ty -> Formula event ty
unfoldForallN Word
k Formula event a
phi)
terminateNext (UntilN Word
k Formula event a
phi Formula event a
psi) = Formula event a -> HomogeneousFormula
forall event a. Formula event a -> HomogeneousFormula
terminateNext (Word -> Formula event a -> Formula event a -> Formula event a
forall event ty.
Word -> Formula event ty -> Formula event ty -> Formula event ty
unfoldUntilN Word
k Formula event a
phi Formula event a
psi)

-- | This is an algorithm for (∅ ⊧ φ)
terminate :: Formula event a -> HomogeneousFormula
terminate :: forall event a. Formula event a -> HomogeneousFormula
terminate (Forall Word
k Formula event a
phi)          = Formula event a -> HomogeneousFormula
forall event a. Formula event a -> HomogeneousFormula
terminate (Word -> Formula event a -> Formula event a
forall event ty. Word -> Formula event ty -> Formula event ty
unfoldForall Word
k Formula event a
phi)
terminate (ForallN Word
k Formula event a
phi)         = Formula event a -> HomogeneousFormula
forall event a. Formula event a -> HomogeneousFormula
terminate (Word -> Formula event a -> Formula event a
forall event ty. Word -> Formula event ty -> Formula event ty
unfoldForallN Word
k Formula event a
phi)
terminate (ExistsN Word
k Formula event a
phi)         = Formula event a -> HomogeneousFormula
forall event a. Formula event a -> HomogeneousFormula
terminate (Word -> Formula event a -> Formula event a
forall event ty. Word -> Formula event ty -> Formula event ty
unfoldExistsN Word
k Formula event a
phi)
terminate (UntilN Word
k Formula event a
phi Formula event a
psi)      = Formula event a -> HomogeneousFormula
forall event a. Formula event a -> HomogeneousFormula
terminate (Word -> Formula event a -> Formula event a -> Formula event a
forall event ty.
Word -> Formula event ty -> Formula event ty -> Formula event ty
unfoldUntilN Word
k Formula event a
phi Formula event a
psi)
terminate (NextN Word
k Formula event a
phi)           = Formula event a -> HomogeneousFormula
forall event a. Formula event a -> HomogeneousFormula
terminate (Word -> Formula event a -> Formula event a
forall event ty. Word -> Formula event ty -> Formula event ty
unfoldNextN Word
k Formula event a
phi)
terminate (Atom a
_ Set PropConstraint
_)              = HomogeneousFormula
H.Bottom
terminate (Next Formula event a
phi)              = Formula event a -> HomogeneousFormula
forall event a. Formula event a -> HomogeneousFormula
terminateNext Formula event a
phi
terminate (And Formula event a
phi Formula event a
psi)           = HomogeneousFormula -> HomogeneousFormula -> HomogeneousFormula
H.And (Formula event a -> HomogeneousFormula
forall event a. Formula event a -> HomogeneousFormula
terminate Formula event a
phi) (Formula event a -> HomogeneousFormula
forall event a. Formula event a -> HomogeneousFormula
terminate Formula event a
psi)
terminate (Or Formula event a
phi Formula event a
psi)            = HomogeneousFormula -> HomogeneousFormula -> HomogeneousFormula
H.Or (Formula event a -> HomogeneousFormula
forall event a. Formula event a -> HomogeneousFormula
terminate Formula event a
phi) (Formula event a -> HomogeneousFormula
forall event a. Formula event a -> HomogeneousFormula
terminate Formula event a
psi)
terminate (Implies Formula event a
phi Formula event a
psi)       = HomogeneousFormula -> HomogeneousFormula -> HomogeneousFormula
H.Implies (Formula event a -> HomogeneousFormula
forall event a. Formula event a -> HomogeneousFormula
terminate Formula event a
phi) (Formula event a -> HomogeneousFormula
forall event a. Formula event a -> HomogeneousFormula
terminate Formula event a
psi)
terminate (Not Formula event a
phi)               = HomogeneousFormula -> HomogeneousFormula
H.Not (Formula event a -> HomogeneousFormula
forall event a. Formula event a -> HomogeneousFormula
terminate Formula event a
phi)
terminate Formula event a
Bottom                  = HomogeneousFormula
H.Bottom
terminate Formula event a
Top                     = HomogeneousFormula
H.Top
terminate (PropIntForall  PropName
x Formula event a
phi)       = PropName -> HomogeneousFormula -> HomogeneousFormula
H.PropIntForall  PropName
x (Formula event a -> HomogeneousFormula
forall event a. Formula event a -> HomogeneousFormula
terminate Formula event a
phi)
terminate (PropTextForall PropName
x Formula event a
phi)       = PropName -> HomogeneousFormula -> HomogeneousFormula
H.PropTextForall PropName
x (Formula event a -> HomogeneousFormula
forall event a. Formula event a -> HomogeneousFormula
terminate Formula event a
phi)
terminate (PropIntForallN  PropName
x Set IntValue
dom Formula event a
phi)  = PropName
-> Set IntValue -> HomogeneousFormula -> HomogeneousFormula
H.PropIntForallN  PropName
x Set IntValue
dom (Formula event a -> HomogeneousFormula
forall event a. Formula event a -> HomogeneousFormula
terminate Formula event a
phi)
terminate (PropTextForallN PropName
x Set PropName
dom Formula event a
phi)  = PropName
-> Set PropName -> HomogeneousFormula -> HomogeneousFormula
H.PropTextForallN PropName
x Set PropName
dom (Formula event a -> HomogeneousFormula
forall event a. Formula event a -> HomogeneousFormula
terminate Formula event a
phi)
terminate (PropIntExists  PropName
x Formula event a
phi)       = PropName -> HomogeneousFormula -> HomogeneousFormula
H.PropIntExists  PropName
x (Formula event a -> HomogeneousFormula
forall event a. Formula event a -> HomogeneousFormula
terminate Formula event a
phi)
terminate (PropTextExists PropName
x Formula event a
phi)       = PropName -> HomogeneousFormula -> HomogeneousFormula
H.PropTextExists PropName
x (Formula event a -> HomogeneousFormula
forall event a. Formula event a -> HomogeneousFormula
terminate Formula event a
phi)
terminate (PropIntExistsN  PropName
x Set IntValue
dom Formula event a
phi)  = PropName
-> Set IntValue -> HomogeneousFormula -> HomogeneousFormula
H.PropIntExistsN  PropName
x Set IntValue
dom (Formula event a -> HomogeneousFormula
forall event a. Formula event a -> HomogeneousFormula
terminate Formula event a
phi)
terminate (PropTextExistsN PropName
x Set PropName
dom Formula event a
phi)  = PropName
-> Set PropName -> HomogeneousFormula -> HomogeneousFormula
H.PropTextExistsN PropName
x Set PropName
dom (Formula event a -> HomogeneousFormula
forall event a. Formula event a -> HomogeneousFormula
terminate Formula event a
phi)
terminate (PropIntBinRel BinRel
rel Relevance event a
_ IntTerm
a IntTerm
b) = BinRel -> IntTerm -> IntTerm -> HomogeneousFormula
H.PropIntBinRel BinRel
rel IntTerm
a IntTerm
b
terminate (PropTextEq Relevance event a
_ TextTerm
a PropName
b)        = TextTerm -> PropName -> HomogeneousFormula
H.PropTextEq TextTerm
a PropName
b