module Hermod.ReCon.LTL.Formula (
    PropName
  , VariableIdentifier
  , IntValue
  , TextValue
  , IntTerm(..)
  , TextTerm(..)
  , BinRel(..)
  , PropConstraint(..)
  , Formula(..)
  , unfoldForall
  , unfoldForallN
  , unfoldExistsN
  , unfoldNextN
  , unfoldUntilN
  , relevance
  , Relevance
  , and
  , interpTimeunit
  , OnMissingKey(..)
  , Event(..)) where

import           Prelude hiding (and)

import           Hermod.ReCon.Common.Types (BinRel (..), IntValue, VariableIdentifier)
import           Hermod.ReCon.Integer.Polynomial.Term (IntTerm (..))

import           Data.Map.Strict (Map)
import           Data.Set (Set, union)
import           Data.Text (Text)
import           Data.Word (Word64)

-- | A property name (e.g. "thread", "node", etc.).
type PropName = Text

-- | Text event property value.
type TextValue = Text

-- | Text term: a constant string or a variable ranging over strings.
data TextTerm = TextConst TextValue | TextVar VariableIdentifier deriving (Int -> TextTerm -> ShowS
[TextTerm] -> ShowS
TextTerm -> String
(Int -> TextTerm -> ShowS)
-> (TextTerm -> String) -> ([TextTerm] -> ShowS) -> Show TextTerm
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TextTerm -> ShowS
showsPrec :: Int -> TextTerm -> ShowS
$cshow :: TextTerm -> String
show :: TextTerm -> String
$cshowList :: [TextTerm] -> ShowS
showList :: [TextTerm] -> ShowS
Show, TextTerm -> TextTerm -> Bool
(TextTerm -> TextTerm -> Bool)
-> (TextTerm -> TextTerm -> Bool) -> Eq TextTerm
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TextTerm -> TextTerm -> Bool
== :: TextTerm -> TextTerm -> Bool
$c/= :: TextTerm -> TextTerm -> Bool
/= :: TextTerm -> TextTerm -> Bool
Eq, Eq TextTerm
Eq TextTerm =>
(TextTerm -> TextTerm -> Ordering)
-> (TextTerm -> TextTerm -> Bool)
-> (TextTerm -> TextTerm -> Bool)
-> (TextTerm -> TextTerm -> Bool)
-> (TextTerm -> TextTerm -> Bool)
-> (TextTerm -> TextTerm -> TextTerm)
-> (TextTerm -> TextTerm -> TextTerm)
-> Ord TextTerm
TextTerm -> TextTerm -> Bool
TextTerm -> TextTerm -> Ordering
TextTerm -> TextTerm -> TextTerm
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 :: TextTerm -> TextTerm -> Ordering
compare :: TextTerm -> TextTerm -> Ordering
$c< :: TextTerm -> TextTerm -> Bool
< :: TextTerm -> TextTerm -> Bool
$c<= :: TextTerm -> TextTerm -> Bool
<= :: TextTerm -> TextTerm -> Bool
$c> :: TextTerm -> TextTerm -> Bool
> :: TextTerm -> TextTerm -> Bool
$c>= :: TextTerm -> TextTerm -> Bool
>= :: TextTerm -> TextTerm -> Bool
$cmax :: TextTerm -> TextTerm -> TextTerm
max :: TextTerm -> TextTerm -> TextTerm
$cmin :: TextTerm -> TextTerm -> TextTerm
min :: TextTerm -> TextTerm -> TextTerm
Ord)

-- | Default name: c.
--   A constraint inside an `Atom`, matching an event property against a term.
data PropConstraint
  = IntPropConstraint  PropName IntTerm
  | TextPropConstraint PropName TextTerm
  deriving (Int -> PropConstraint -> ShowS
[PropConstraint] -> ShowS
PropConstraint -> String
(Int -> PropConstraint -> ShowS)
-> (PropConstraint -> String)
-> ([PropConstraint] -> ShowS)
-> Show PropConstraint
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PropConstraint -> ShowS
showsPrec :: Int -> PropConstraint -> ShowS
$cshow :: PropConstraint -> String
show :: PropConstraint -> String
$cshowList :: [PropConstraint] -> ShowS
showList :: [PropConstraint] -> ShowS
Show, PropConstraint -> PropConstraint -> Bool
(PropConstraint -> PropConstraint -> Bool)
-> (PropConstraint -> PropConstraint -> Bool) -> Eq PropConstraint
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PropConstraint -> PropConstraint -> Bool
== :: PropConstraint -> PropConstraint -> Bool
$c/= :: PropConstraint -> PropConstraint -> Bool
/= :: PropConstraint -> PropConstraint -> Bool
Eq, Eq PropConstraint
Eq PropConstraint =>
(PropConstraint -> PropConstraint -> Ordering)
-> (PropConstraint -> PropConstraint -> Bool)
-> (PropConstraint -> PropConstraint -> Bool)
-> (PropConstraint -> PropConstraint -> Bool)
-> (PropConstraint -> PropConstraint -> Bool)
-> (PropConstraint -> PropConstraint -> PropConstraint)
-> (PropConstraint -> PropConstraint -> PropConstraint)
-> Ord PropConstraint
PropConstraint -> PropConstraint -> Bool
PropConstraint -> PropConstraint -> Ordering
PropConstraint -> PropConstraint -> PropConstraint
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 :: PropConstraint -> PropConstraint -> Ordering
compare :: PropConstraint -> PropConstraint -> Ordering
$c< :: PropConstraint -> PropConstraint -> Bool
< :: PropConstraint -> PropConstraint -> Bool
$c<= :: PropConstraint -> PropConstraint -> Bool
<= :: PropConstraint -> PropConstraint -> Bool
$c> :: PropConstraint -> PropConstraint -> Bool
> :: PropConstraint -> PropConstraint -> Bool
$c>= :: PropConstraint -> PropConstraint -> Bool
>= :: PropConstraint -> PropConstraint -> Bool
$cmax :: PropConstraint -> PropConstraint -> PropConstraint
max :: PropConstraint -> PropConstraint -> PropConstraint
$cmin :: PropConstraint -> PropConstraint -> PropConstraint
min :: PropConstraint -> PropConstraint -> PropConstraint
Ord)

-- | Set of relevant events.
type Relevance event ty = Set (event, ty)

-- | Default name: φ.
--
--   Formulas of a discrete-time Linear Temporal Logic (LTL) enriched with
--   first-order quantification over event properties.
--
--   __Time model.__
--   Time is a sequence of abstract /units/ indexed by natural numbers.
--   Each unit carries a finite multiset of typed events (see 'Event').
--   The temporal connectives advance through this sequence:
--
--   * @◯ φ@ — next unit
--   * @☐ ᪲ₖ φ@ — every @(k+1)@-th unit from now, forever
--   * @☐ⁿ φ@ — for each of the next @n@ units
--   * @♢ⁿ φ@ — for some unit within the next @n@
--   * @φ |ⁿ ψ@ — @φ@ until @ψ@, within @n@ units
--
--   __Parameterisation.__
--   The type parameter @ty@ is the vocabulary of /event types/; @event@ is the
--   concrete event representation (see 'Event').  Atoms (@'Atom' ty cs@) assert
--   that the current unit contains an event of type @ty@ whose properties
--   satisfy the constraints @cs@.
--
--   __First-order layer.__
--   Quantifiers @∀x ∈ ℤ@, @∃x ∈ ℤ@, @∀x ∈ Text@, @∃x ∈ Text@, and their
--   finite-domain variants, bind variables that can appear in property
--   constraints, integer comparison atoms (@'PropIntBinRel'@), and text
--   equality atoms (@'PropTextEq'@).  The resulting fragment is decidable:
--   integer arithmetic is handled by Cooper's quantifier elimination;
--   text quantifiers are decided by finite enumeration (see
--   "Hermod.ReCon.LTL.Internal.IR.HomogeneousFormula.FinFree").
data Formula event ty =
   ------------ Temporal -------------
     -- | ☐ ᪲ₖ φ ≡ φ ∧ ◯ (◯ᵏ (☐ ᪲ₖ))
     --   For every (k+1)-th unit of time from now, φ
     --   For example:
     --     ☐ ᪲₁ φ means for every other unit of time from now, φ
     --     ☐ ᪲₃ φ means for every 4-th unit of time from now, φ
     --     ☐ ᪲₀ φ means for every unit of time from now, φ
     Forall Word (Formula event ty)
     -- | ☐ⁿ φ
     --   ☐⁰ φ ≡ ⊤
     --   ☐¹⁺ᵏ φ ≡ φ ∧ ◯ (☐ᵏ φ)
     --   For each of the n units of time from now, φ
   | ForallN Word (Formula event ty)
     -- | ♢ⁿ φ
     --   ♢⁰ φ ≡ ⊥
     --   ♢¹⁺ᵏ φ ≡ φ ∨ ◯ (♢ᵏ φ)
     --   For one of the n units of time from now, φ
   | ExistsN Word (Formula event ty)
     -- | ◯ φ
     --   For the next unit of time from now, φ.
   | Next (Formula event ty)
     -- | ◯ⁿ φ
     --   ◯⁰ φ ≡ φ
     --   ◯¹⁺ᵏ φ ≡ ◯ (◯ᵏ φ)
     --   For the n-th unit of time from now, φ
   | NextN Word (Formula event ty)
     -- | φ |ⁿ ψ
     --   φ |⁰ ψ ≡ ⊤
     --   φ |¹⁺ᵏ ψ ≡ ψ ∨ ¬ ψ ∧ φ ∧ (φ |ᵏ ψ)
     --   φ until ψ in the n units of time from now
   | UntilN Word (Formula event ty) (Formula event ty)
   -------------------------------------

   -------------- Atomic ---------------
     -- | ty c̄
   | Atom ty (Set PropConstraint)
   -------------------------------------


   ------------ Connective -------------
     -- | φ ∨ ψ
   | Or (Formula event ty) (Formula event ty)
     -- | φ ∧ ψ
   | And (Formula event ty) (Formula event ty)
     -- | ¬ φ
   | Not (Formula event ty)
     -- | φ ⇒ ψ
   | Implies (Formula event ty) (Formula event ty)
     -- | T
   | Top
     -- | ⊥
   | Bottom
   -------------------------------------


   ----------- Event property ----------
     -- | ∀x ∈ ℤ. φ  —  x ranges over all integers
   | PropIntForall  VariableIdentifier (Formula event ty)
     -- | ∀x ∈ Text. φ  —  x ranges over all strings
   | PropTextForall VariableIdentifier (Formula event ty)
     -- | ∀x ∈ v̄. φ  —  x ranges over the given integers
   | PropIntForallN  VariableIdentifier (Set IntValue)  (Formula event ty)
     -- | ∀x ∈ v̄. φ  —  x ranges over the given strings
   | PropTextForallN VariableIdentifier (Set TextValue) (Formula event ty)
     -- | ∃x ∈ ℤ. φ  —  x ranges over all integers
   | PropIntExists  VariableIdentifier (Formula event ty)
     -- | ∃x ∈ Text. φ  —  x ranges over all strings
   | PropTextExists VariableIdentifier (Formula event ty)
     -- | ∃x ∈ v̄. φ  —  x ranges over the given integers
   | PropIntExistsN  VariableIdentifier (Set IntValue)  (Formula event ty)
     -- | ∃x ∈ v̄. φ  —  x ranges over the given strings
   | PropTextExistsN VariableIdentifier (Set TextValue) (Formula event ty)
     -- | t rel t  (integer)
   | PropIntBinRel BinRel (Relevance event ty) IntTerm  IntTerm
     -- | t = v  (text)
   | PropTextEq (Relevance event ty) TextTerm TextValue
   -------------------------------------
   deriving (Int -> Formula event ty -> ShowS
[Formula event ty] -> ShowS
Formula event ty -> String
(Int -> Formula event ty -> ShowS)
-> (Formula event ty -> String)
-> ([Formula event ty] -> ShowS)
-> Show (Formula event ty)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall event ty.
(Show ty, Show event) =>
Int -> Formula event ty -> ShowS
forall event ty.
(Show ty, Show event) =>
[Formula event ty] -> ShowS
forall event ty.
(Show ty, Show event) =>
Formula event ty -> String
$cshowsPrec :: forall event ty.
(Show ty, Show event) =>
Int -> Formula event ty -> ShowS
showsPrec :: Int -> Formula event ty -> ShowS
$cshow :: forall event ty.
(Show ty, Show event) =>
Formula event ty -> String
show :: Formula event ty -> String
$cshowList :: forall event ty.
(Show ty, Show event) =>
[Formula event ty] -> ShowS
showList :: [Formula event ty] -> ShowS
Show, Formula event ty -> Formula event ty -> Bool
(Formula event ty -> Formula event ty -> Bool)
-> (Formula event ty -> Formula event ty -> Bool)
-> Eq (Formula event ty)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall event ty.
(Eq ty, Eq event) =>
Formula event ty -> Formula event ty -> Bool
$c== :: forall event ty.
(Eq ty, Eq event) =>
Formula event ty -> Formula event ty -> Bool
== :: Formula event ty -> Formula event ty -> Bool
$c/= :: forall event ty.
(Eq ty, Eq event) =>
Formula event ty -> Formula event ty -> Bool
/= :: Formula event ty -> Formula event ty -> Bool
Eq, Eq (Formula event ty)
Eq (Formula event ty) =>
(Formula event ty -> Formula event ty -> Ordering)
-> (Formula event ty -> Formula event ty -> Bool)
-> (Formula event ty -> Formula event ty -> Bool)
-> (Formula event ty -> Formula event ty -> Bool)
-> (Formula event ty -> Formula event ty -> Bool)
-> (Formula event ty -> Formula event ty -> Formula event ty)
-> (Formula event ty -> Formula event ty -> Formula event ty)
-> Ord (Formula event ty)
Formula event ty -> Formula event ty -> Bool
Formula event ty -> Formula event ty -> Ordering
Formula event ty -> Formula event ty -> Formula event ty
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
forall event ty. (Ord ty, Ord event) => Eq (Formula event ty)
forall event ty.
(Ord ty, Ord event) =>
Formula event ty -> Formula event ty -> Bool
forall event ty.
(Ord ty, Ord event) =>
Formula event ty -> Formula event ty -> Ordering
forall event ty.
(Ord ty, Ord event) =>
Formula event ty -> Formula event ty -> Formula event ty
$ccompare :: forall event ty.
(Ord ty, Ord event) =>
Formula event ty -> Formula event ty -> Ordering
compare :: Formula event ty -> Formula event ty -> Ordering
$c< :: forall event ty.
(Ord ty, Ord event) =>
Formula event ty -> Formula event ty -> Bool
< :: Formula event ty -> Formula event ty -> Bool
$c<= :: forall event ty.
(Ord ty, Ord event) =>
Formula event ty -> Formula event ty -> Bool
<= :: Formula event ty -> Formula event ty -> Bool
$c> :: forall event ty.
(Ord ty, Ord event) =>
Formula event ty -> Formula event ty -> Bool
> :: Formula event ty -> Formula event ty -> Bool
$c>= :: forall event ty.
(Ord ty, Ord event) =>
Formula event ty -> Formula event ty -> Bool
>= :: Formula event ty -> Formula event ty -> Bool
$cmax :: forall event ty.
(Ord ty, Ord event) =>
Formula event ty -> Formula event ty -> Formula event ty
max :: Formula event ty -> Formula event ty -> Formula event ty
$cmin :: forall event ty.
(Ord ty, Ord event) =>
Formula event ty -> Formula event ty -> Formula event ty
min :: Formula event ty -> Formula event ty -> Formula event ty
Ord)


-- | Compute the total `Relevance` of the formula.
relevance :: (Ord event, Ord ty) => Formula event ty -> Relevance event ty
relevance :: forall event ty.
(Ord event, Ord ty) =>
Formula event ty -> Relevance event ty
relevance = Relevance event ty -> Formula event ty -> Relevance event ty
forall event ty.
(Ord event, Ord ty) =>
Relevance event ty -> Formula event ty -> Relevance event ty
go Relevance event ty
forall a. Monoid a => a
mempty where
  go :: (Ord event, Ord ty) => Relevance event ty -> Formula event ty -> Relevance event ty
  go :: forall event ty.
(Ord event, Ord ty) =>
Relevance event ty -> Formula event ty -> Relevance event ty
go Relevance event ty
acc (Forall Word
_ Formula event ty
phi)          = Relevance event ty -> Formula event ty -> Relevance event ty
forall event ty.
(Ord event, Ord ty) =>
Relevance event ty -> Formula event ty -> Relevance event ty
go Relevance event ty
acc Formula event ty
phi
  go Relevance event ty
acc (ForallN Word
_ Formula event ty
phi)         = Relevance event ty -> Formula event ty -> Relevance event ty
forall event ty.
(Ord event, Ord ty) =>
Relevance event ty -> Formula event ty -> Relevance event ty
go Relevance event ty
acc Formula event ty
phi
  go Relevance event ty
acc (ExistsN Word
_ Formula event ty
phi)         = Relevance event ty -> Formula event ty -> Relevance event ty
forall event ty.
(Ord event, Ord ty) =>
Relevance event ty -> Formula event ty -> Relevance event ty
go Relevance event ty
acc Formula event ty
phi
  go Relevance event ty
acc (Next Formula event ty
phi)              = Relevance event ty -> Formula event ty -> Relevance event ty
forall event ty.
(Ord event, Ord ty) =>
Relevance event ty -> Formula event ty -> Relevance event ty
go Relevance event ty
acc Formula event ty
phi
  go Relevance event ty
acc (NextN Word
_ Formula event ty
phi)           = Relevance event ty -> Formula event ty -> Relevance event ty
forall event ty.
(Ord event, Ord ty) =>
Relevance event ty -> Formula event ty -> Relevance event ty
go Relevance event ty
acc Formula event ty
phi
  go Relevance event ty
acc (UntilN Word
_ Formula event ty
phi Formula event ty
psi)      = Relevance event ty -> Formula event ty -> Relevance event ty
forall event ty.
(Ord event, Ord ty) =>
Relevance event ty -> Formula event ty -> Relevance event ty
go (Relevance event ty -> Formula event ty -> Relevance event ty
forall event ty.
(Ord event, Ord ty) =>
Relevance event ty -> Formula event ty -> Relevance event ty
go Relevance event ty
acc Formula event ty
phi) Formula event ty
psi
  go Relevance event ty
acc (Or Formula event ty
phi Formula event ty
psi)            = Relevance event ty -> Formula event ty -> Relevance event ty
forall event ty.
(Ord event, Ord ty) =>
Relevance event ty -> Formula event ty -> Relevance event ty
go (Relevance event ty -> Formula event ty -> Relevance event ty
forall event ty.
(Ord event, Ord ty) =>
Relevance event ty -> Formula event ty -> Relevance event ty
go Relevance event ty
acc Formula event ty
phi) Formula event ty
psi
  go Relevance event ty
acc (And Formula event ty
phi Formula event ty
psi)           = Relevance event ty -> Formula event ty -> Relevance event ty
forall event ty.
(Ord event, Ord ty) =>
Relevance event ty -> Formula event ty -> Relevance event ty
go (Relevance event ty -> Formula event ty -> Relevance event ty
forall event ty.
(Ord event, Ord ty) =>
Relevance event ty -> Formula event ty -> Relevance event ty
go Relevance event ty
acc Formula event ty
phi) Formula event ty
psi
  go Relevance event ty
acc (Not Formula event ty
phi)               = Relevance event ty -> Formula event ty -> Relevance event ty
forall event ty.
(Ord event, Ord ty) =>
Relevance event ty -> Formula event ty -> Relevance event ty
go Relevance event ty
acc Formula event ty
phi
  go Relevance event ty
acc (Implies Formula event ty
phi Formula event ty
psi)       = Relevance event ty -> Formula event ty -> Relevance event ty
forall event ty.
(Ord event, Ord ty) =>
Relevance event ty -> Formula event ty -> Relevance event ty
go (Relevance event ty -> Formula event ty -> Relevance event ty
forall event ty.
(Ord event, Ord ty) =>
Relevance event ty -> Formula event ty -> Relevance event ty
go Relevance event ty
acc Formula event ty
phi) Formula event ty
psi
  go Relevance event ty
acc Formula event ty
Top                     = Relevance event ty
acc
  go Relevance event ty
acc Formula event ty
Bottom                  = Relevance event ty
acc
  go Relevance event ty
acc (Atom {})               = Relevance event ty
acc
  go Relevance event ty
acc (PropIntForall TextValue
_ Formula event ty
phi)   = Relevance event ty -> Formula event ty -> Relevance event ty
forall event ty.
(Ord event, Ord ty) =>
Relevance event ty -> Formula event ty -> Relevance event ty
go Relevance event ty
acc Formula event ty
phi
  go Relevance event ty
acc (PropTextForall TextValue
_ Formula event ty
phi)  = Relevance event ty -> Formula event ty -> Relevance event ty
forall event ty.
(Ord event, Ord ty) =>
Relevance event ty -> Formula event ty -> Relevance event ty
go Relevance event ty
acc Formula event ty
phi
  go Relevance event ty
acc (PropIntForallN TextValue
_ Set IntValue
_ Formula event ty
phi)  = Relevance event ty -> Formula event ty -> Relevance event ty
forall event ty.
(Ord event, Ord ty) =>
Relevance event ty -> Formula event ty -> Relevance event ty
go Relevance event ty
acc Formula event ty
phi
  go Relevance event ty
acc (PropTextForallN TextValue
_ Set TextValue
_ Formula event ty
phi) = Relevance event ty -> Formula event ty -> Relevance event ty
forall event ty.
(Ord event, Ord ty) =>
Relevance event ty -> Formula event ty -> Relevance event ty
go Relevance event ty
acc Formula event ty
phi
  go Relevance event ty
acc (PropIntExists TextValue
_ Formula event ty
phi)   = Relevance event ty -> Formula event ty -> Relevance event ty
forall event ty.
(Ord event, Ord ty) =>
Relevance event ty -> Formula event ty -> Relevance event ty
go Relevance event ty
acc Formula event ty
phi
  go Relevance event ty
acc (PropTextExists TextValue
_ Formula event ty
phi)  = Relevance event ty -> Formula event ty -> Relevance event ty
forall event ty.
(Ord event, Ord ty) =>
Relevance event ty -> Formula event ty -> Relevance event ty
go Relevance event ty
acc Formula event ty
phi
  go Relevance event ty
acc (PropIntExistsN TextValue
_ Set IntValue
_ Formula event ty
phi)  = Relevance event ty -> Formula event ty -> Relevance event ty
forall event ty.
(Ord event, Ord ty) =>
Relevance event ty -> Formula event ty -> Relevance event ty
go Relevance event ty
acc Formula event ty
phi
  go Relevance event ty
acc (PropTextExistsN TextValue
_ Set TextValue
_ Formula event ty
phi) = Relevance event ty -> Formula event ty -> Relevance event ty
forall event ty.
(Ord event, Ord ty) =>
Relevance event ty -> Formula event ty -> Relevance event ty
go Relevance event ty
acc Formula event ty
phi
  go Relevance event ty
acc (PropIntBinRel BinRel
_ Relevance event ty
rel IntTerm
_ IntTerm
_) = Relevance event ty
rel Relevance event ty -> Relevance event ty -> Relevance event ty
forall a. Ord a => Set a -> Set a -> Set a
`union` Relevance event ty
acc
  go Relevance event ty
acc (PropTextEq Relevance event ty
rel TextTerm
_ TextValue
_)      = Relevance event ty
rel Relevance event ty -> Relevance event ty -> Relevance event ty
forall a. Ord a => Set a -> Set a -> Set a
`union` Relevance event ty
acc

unfoldForall :: Word -> Formula event ty -> Formula event ty
unfoldForall :: forall event ty. Word -> Formula event ty -> Formula event ty
unfoldForall Word
k Formula event ty
phi = 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 -> Formula event ty
forall event ty. Formula event ty -> Formula event ty
Next (Word -> Formula event ty -> Formula event ty
forall event ty. Word -> Formula event ty -> Formula event ty
NextN Word
k (Word -> Formula event ty -> Formula event ty
forall event ty. Word -> Formula event ty -> Formula event ty
Forall Word
k Formula event ty
phi)))

unfoldForallN :: Word -> Formula event ty -> Formula event ty
unfoldForallN :: forall event ty. Word -> Formula event ty -> Formula event ty
unfoldForallN Word
0 Formula event ty
_   = Formula event ty
forall event ty. Formula event ty
Top
unfoldForallN Word
k Formula event ty
phi = 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 -> Formula event ty
forall event ty. Formula event ty -> Formula event ty
Next (Word -> Formula event ty -> Formula event ty
forall event ty. Word -> Formula event ty -> Formula event ty
ForallN (Word
k Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
1) Formula event ty
phi))

unfoldExistsN :: Word -> Formula event ty -> Formula event ty
unfoldExistsN :: forall event ty. Word -> Formula event ty -> Formula event ty
unfoldExistsN Word
0 Formula event ty
_   = Formula event ty
forall event ty. Formula event ty
Bottom
unfoldExistsN Word
k Formula event ty
phi = 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 -> Formula event ty
forall event ty. Formula event ty -> Formula event ty
Next (Word -> Formula event ty -> Formula event ty
forall event ty. Word -> Formula event ty -> Formula event ty
ExistsN (Word
k Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
1) Formula event ty
phi))

unfoldNextN :: Word -> Formula event ty -> Formula event ty
unfoldNextN :: forall event ty. Word -> Formula event ty -> Formula event ty
unfoldNextN Word
0 Formula event ty
phi = Formula event ty
phi
unfoldNextN Word
k Formula event ty
phi = Formula event ty -> Formula event ty
forall event ty. Formula event ty -> Formula event ty
Next (Word -> Formula event ty -> Formula event ty
forall event ty. Word -> Formula event ty -> Formula event ty
NextN (Word
k Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
1) Formula event ty
phi)

unfoldUntilN :: Word -> Formula event ty -> Formula event ty -> Formula event ty
unfoldUntilN :: forall event ty.
Word -> Formula event ty -> Formula event ty -> Formula event ty
unfoldUntilN Word
0 Formula event ty
_ Formula event ty
_ = Formula event ty
forall event ty. Formula event ty
Top
unfoldUntilN Word
k 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
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 -> 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
forall event ty. Formula event ty -> Formula event ty
Not Formula event ty
psi)
         (Formula event ty -> Formula event ty
forall event ty. Formula event ty -> 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
UntilN (Word
k Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
1) Formula event ty
phi Formula event ty
psi))
       )
     )

and :: [Formula event ty] -> Formula event ty
and :: forall event ty. [Formula event ty] -> Formula event ty
and []           = Formula event ty
forall event ty. Formula event ty
Top
and [Formula event ty
phi]        = Formula event ty
phi
and (Formula event ty
phi : [Formula event ty]
phis) = 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] -> Formula event ty
forall event ty. [Formula event ty] -> Formula event ty
and [Formula event ty]
phis)

-- | It's useful to express temporal aspect of the formulas in a familiar time unit (e.g milliseconds).
--   Yet, the LTL machinery works with nameless abstract time units.
--   This function can be used to convert one into the other.
interpTimeunit :: (Word -> Word) -> Formula event ty -> Formula event ty
interpTimeunit :: forall event ty.
(Word -> Word) -> Formula event ty -> Formula event ty
interpTimeunit Word -> Word
f (Forall Word
k Formula event ty
phi)   = Word -> Formula event ty -> Formula event ty
forall event ty. Word -> Formula event ty -> Formula event ty
Forall (Word -> Word
f Word
k) ((Word -> Word) -> Formula event ty -> Formula event ty
forall event ty.
(Word -> Word) -> Formula event ty -> Formula event ty
interpTimeunit Word -> Word
f Formula event ty
phi)
interpTimeunit Word -> Word
f (ForallN Word
k Formula event ty
phi)  = Word -> Formula event ty -> Formula event ty
forall event ty. Word -> Formula event ty -> Formula event ty
ForallN (Word -> Word
f Word
k) ((Word -> Word) -> Formula event ty -> Formula event ty
forall event ty.
(Word -> Word) -> Formula event ty -> Formula event ty
interpTimeunit Word -> Word
f Formula event ty
phi)
interpTimeunit Word -> Word
f (ExistsN Word
k Formula event ty
phi)  = Word -> Formula event ty -> Formula event ty
forall event ty. Word -> Formula event ty -> Formula event ty
ExistsN (Word -> Word
f Word
k) ((Word -> Word) -> Formula event ty -> Formula event ty
forall event ty.
(Word -> Word) -> Formula event ty -> Formula event ty
interpTimeunit Word -> Word
f Formula event ty
phi)
interpTimeunit Word -> Word
f (Next Formula event ty
phi)       = Formula event ty -> Formula event ty
forall event ty. Formula event ty -> Formula event ty
Next ((Word -> Word) -> Formula event ty -> Formula event ty
forall event ty.
(Word -> Word) -> Formula event ty -> Formula event ty
interpTimeunit Word -> Word
f Formula event ty
phi)
interpTimeunit Word -> Word
f (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 -> Word
f Word
k) ((Word -> Word) -> Formula event ty -> Formula event ty
forall event ty.
(Word -> Word) -> Formula event ty -> Formula event ty
interpTimeunit Word -> Word
f Formula event ty
phi)
interpTimeunit Word -> Word
f (UntilN Word
k Formula event ty
phi 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 -> Word
f Word
k) ((Word -> Word) -> Formula event ty -> Formula event ty
forall event ty.
(Word -> Word) -> Formula event ty -> Formula event ty
interpTimeunit Word -> Word
f Formula event ty
phi) ((Word -> Word) -> Formula event ty -> Formula event ty
forall event ty.
(Word -> Word) -> Formula event ty -> Formula event ty
interpTimeunit Word -> Word
f Formula event ty
psi)
interpTimeunit Word -> Word
f (Not Formula event ty
phi)        = Formula event ty -> Formula event ty
forall event ty. Formula event ty -> Formula event ty
Not ((Word -> Word) -> Formula event ty -> Formula event ty
forall event ty.
(Word -> Word) -> Formula event ty -> Formula event ty
interpTimeunit Word -> Word
f Formula event ty
phi)
interpTimeunit Word -> Word
f (Or 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 ((Word -> Word) -> Formula event ty -> Formula event ty
forall event ty.
(Word -> Word) -> Formula event ty -> Formula event ty
interpTimeunit Word -> Word
f Formula event ty
phi) ((Word -> Word) -> Formula event ty -> Formula event ty
forall event ty.
(Word -> Word) -> Formula event ty -> Formula event ty
interpTimeunit Word -> Word
f Formula event ty
psi)
interpTimeunit Word -> Word
f (And 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 ((Word -> Word) -> Formula event ty -> Formula event ty
forall event ty.
(Word -> Word) -> Formula event ty -> Formula event ty
interpTimeunit Word -> Word
f Formula event ty
phi) ((Word -> Word) -> Formula event ty -> Formula event ty
forall event ty.
(Word -> Word) -> Formula event ty -> Formula event ty
interpTimeunit Word -> Word
f Formula event ty
psi)
interpTimeunit Word -> Word
f (Implies 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 ((Word -> Word) -> Formula event ty -> Formula event ty
forall event ty.
(Word -> Word) -> Formula event ty -> Formula event ty
interpTimeunit Word -> Word
f Formula event ty
phi) ((Word -> Word) -> Formula event ty -> Formula event ty
forall event ty.
(Word -> Word) -> Formula event ty -> Formula event ty
interpTimeunit Word -> Word
f Formula event ty
psi)
interpTimeunit Word -> Word
_ Formula event ty
Top              = Formula event ty
forall event ty. Formula event ty
Top
interpTimeunit Word -> Word
_ Formula event ty
Bottom           = Formula event ty
forall event ty. Formula event ty
Bottom
interpTimeunit Word -> Word
_ phi :: Formula event ty
phi@Atom{}       = Formula event ty
phi
interpTimeunit Word -> Word
_ phi :: Formula event ty
phi@PropIntBinRel{} = Formula event ty
phi
interpTimeunit Word -> Word
_ phi :: Formula event ty
phi@PropTextEq{}    = Formula event ty
phi
interpTimeunit Word -> Word
f (PropIntForall TextValue
x Formula event ty
phi)    = TextValue -> Formula event ty -> Formula event ty
forall event ty. TextValue -> Formula event ty -> Formula event ty
PropIntForall TextValue
x ((Word -> Word) -> Formula event ty -> Formula event ty
forall event ty.
(Word -> Word) -> Formula event ty -> Formula event ty
interpTimeunit Word -> Word
f Formula event ty
phi)
interpTimeunit Word -> Word
f (PropTextForall TextValue
x Formula event ty
phi)   = TextValue -> Formula event ty -> Formula event ty
forall event ty. TextValue -> Formula event ty -> Formula event ty
PropTextForall TextValue
x ((Word -> Word) -> Formula event ty -> Formula event ty
forall event ty.
(Word -> Word) -> Formula event ty -> Formula event ty
interpTimeunit Word -> Word
f Formula event ty
phi)
interpTimeunit Word -> Word
f (PropIntForallN TextValue
x Set IntValue
dom Formula event ty
phi)  = TextValue -> Set IntValue -> Formula event ty -> Formula event ty
forall event ty.
TextValue -> Set IntValue -> Formula event ty -> Formula event ty
PropIntForallN TextValue
x Set IntValue
dom ((Word -> Word) -> Formula event ty -> Formula event ty
forall event ty.
(Word -> Word) -> Formula event ty -> Formula event ty
interpTimeunit Word -> Word
f Formula event ty
phi)
interpTimeunit Word -> Word
f (PropTextForallN TextValue
x Set TextValue
dom Formula event ty
phi) = TextValue -> Set TextValue -> Formula event ty -> Formula event ty
forall event ty.
TextValue -> Set TextValue -> Formula event ty -> Formula event ty
PropTextForallN TextValue
x Set TextValue
dom ((Word -> Word) -> Formula event ty -> Formula event ty
forall event ty.
(Word -> Word) -> Formula event ty -> Formula event ty
interpTimeunit Word -> Word
f Formula event ty
phi)
interpTimeunit Word -> Word
f (PropIntExists TextValue
x Formula event ty
phi)    = TextValue -> Formula event ty -> Formula event ty
forall event ty. TextValue -> Formula event ty -> Formula event ty
PropIntExists TextValue
x ((Word -> Word) -> Formula event ty -> Formula event ty
forall event ty.
(Word -> Word) -> Formula event ty -> Formula event ty
interpTimeunit Word -> Word
f Formula event ty
phi)
interpTimeunit Word -> Word
f (PropTextExists TextValue
x Formula event ty
phi)   = TextValue -> Formula event ty -> Formula event ty
forall event ty. TextValue -> Formula event ty -> Formula event ty
PropTextExists TextValue
x ((Word -> Word) -> Formula event ty -> Formula event ty
forall event ty.
(Word -> Word) -> Formula event ty -> Formula event ty
interpTimeunit Word -> Word
f Formula event ty
phi)
interpTimeunit Word -> Word
f (PropIntExistsN TextValue
x Set IntValue
dom Formula event ty
phi)  = TextValue -> Set IntValue -> Formula event ty -> Formula event ty
forall event ty.
TextValue -> Set IntValue -> Formula event ty -> Formula event ty
PropIntExistsN TextValue
x Set IntValue
dom ((Word -> Word) -> Formula event ty -> Formula event ty
forall event ty.
(Word -> Word) -> Formula event ty -> Formula event ty
interpTimeunit Word -> Word
f Formula event ty
phi)
interpTimeunit Word -> Word
f (PropTextExistsN TextValue
x Set TextValue
dom Formula event ty
phi) = TextValue -> Set TextValue -> Formula event ty -> Formula event ty
forall event ty.
TextValue -> Set TextValue -> Formula event ty -> Formula event ty
PropTextExistsN TextValue
x Set TextValue
dom ((Word -> Word) -> Formula event ty -> Formula event ty
forall event ty.
(Word -> Word) -> Formula event ty -> Formula event ty
interpTimeunit Word -> Word
f Formula event ty
phi)

-- | Controls evaluator behaviour when a formula atom references a property
--   key that is absent from the event being evaluated.
--
--   * 'BottomOnMissingKey' — treat the atom as unsatisfied (@⊥@); evaluation
--     continues silently.  Useful when events may legally omit optional fields.
--   * 'CrashOnMissingKey' — throw an exception.  Useful during development to
--     catch formula/event-schema mismatches early.
data OnMissingKey = BottomOnMissingKey | CrashOnMissingKey

-- | Default name: e.
--
--   Interface between a concrete event representation @a@ and the LTL
--   evaluator.  The functional dependency @a -> ty@ fixes the event-type
--   vocabulary once the event type is known.
--
--   __Semantics.__
--   Each time unit presents a sequence of events to the evaluator.  An
--   @'Atom' ty cs@ is satisfied by unit @t@ if there exists an event @e@ in
--   @t@ such that:
--
--   1. @'ofTy' e ty@ holds, and
--   2. every constraint @c ∈ cs@ matches @e@ against @'intProps' e ty@ or
--      @'textProps' e ty@ (see @satisfiability-semantics.txt@).
--
--   __Precondition.__
--   @'intProps'@ and @'textProps'@ are only called when @'ofTy' e ty@ is
--   @True@; their behaviour is unspecified otherwise.
class Event a ty | a -> ty where
  -- | @'ofTy' e ty@ — is event @e@ of type @ty@?
  ofTy :: a -> ty -> Bool
  -- | Integer-valued properties of @e@ relevant to type @ty@,
  --   keyed by property name.  Precondition: @'ofTy' e ty@.
  intProps  :: a -> ty -> Map VariableIdentifier IntValue
  -- | Text-valued properties of @e@ relevant to type @ty@,
  --   keyed by property name.  Precondition: @'ofTy' e ty@.
  textProps :: a -> ty -> Map VariableIdentifier TextValue
  -- | Timestamp of the event in microseconds.  Used for diagnostics only;
  --   the LTL evaluator does not reason about wall-clock time.
  beg :: a -> Word64