-- | This modules provides the infrastructure to modify sequences of
-- transactions using LTL formulaes with atomic modifications. This idea is to
-- describe when to apply certain modifications within a trace.
module Cooked.Ltl
  ( -- * LTL formulas
    Ltl (..),

    -- * LTL combinators
    ltlNot',
    ltlOr',
    ltlAnd',
    ltlNext',
    ltlAny,
    ltlAny',
    ltlAll,
    ltlAll',
    ltlDelay,
    ltlDelay',
    ltlEventually,
    ltlEventually',
    ltlAlways,
    ltlAlways',
    ltlWhenPossible,
    ltlWhenPossible',
    ltlIfPossible,
    ltlIfPossible',
    ltlImplies,
    ltlImplies',
    ltlNever,
    ltlNever',

    -- * Using LTL formulas to modify computations
    Requirement (..),
    LtlOp (..),
    StagedLtl,
    singletonBuiltin,
    MonadLtl (..),
    ModInterpBuiltin (..),
    interpStagedLtl,
  )
where

import Control.Monad
import Control.Monad.State
import Cooked.Staged
import Data.Functor
import Data.Kind

-- | Type of LTL formulas with atomic formulas of type @a@. Think of @a@ as a
-- type of "modifications", then a value of type @Ltl a@ describes where to
-- apply `Requirement`s in a trace.
data Ltl a
  = -- | The modification that always applies but does nothing.
    LtlTruth
  | -- | The modification that never applies (i.e. always fails).
    LtlFalsity
  | -- | The atomic modification, applying at the current time step.
    LtlAtom a
  | -- | Assert that the given formula must not hold at the current time step
    -- i.e. that the appropriate modifications fail.
    LtlNot (Ltl a)
  | -- | Disjunction will be interpreted in an "intuitionistic" way, i.e. as
    -- branching into the "timeline" where the left disjunct holds and the one
    -- where the right disjunct holds. In that sense, it is an exclusive or, as
    -- it does not introduce the branch where both disjuncts hold.
    LtlOr (Ltl a) (Ltl a)
  | -- | Conjunction will be interpreted as "apply both modifications".
    -- Attention: The "apply both" operation will be user-defined for atomic
    -- modifications, so that conjunction may for example fail to be commutative
    -- if the operation on atomic modification is not commutative. In
    -- particular, this is the case for tweaks, where the second modification
    -- will be applied first, to be consistent with nested modifications.
    LtlAnd (Ltl a) (Ltl a)
  | -- | Assert that the given formula holds at the next time step.
    LtlNext (Ltl a)
  | -- | Assert that the first formula holds at least until the second one
    -- begins to hold, which must happen ltlEventually. The following holds:
    --
    -- > a `LtlUntil` b <=> b `LtlOr` (a `LtlAnd` LtlNext (a `LtlUntil` b))
    --
    -- `LtlUntil` could technically be defined as the above formula using
    -- Haskell's laziness, but is left as a constructor to have a counterpart
    -- for `LtlRelease`, which cannot.
    LtlUntil (Ltl a) (Ltl a)
  | -- | Assert that the second formula has to hold up to and including the
    -- point when the first begins to hold; if that ltlNever happens, the second
    -- formula has to remain true forever. View this as dual to 'LtlUntil'. The
    -- following holds:
    --
    -- > a `LtlRelease` b <=> b `LtlAnd` (a `LtlOr` LtlNext (a `LtlRelease` b))
    --
    -- `LtlRelease` needs it own constructor, as it is considered valid on an
    -- empty computation, which the above formula is not in most cases.
    LtlRelease (Ltl a) (Ltl a)
  deriving (Int -> Ltl a -> ShowS
[Ltl a] -> ShowS
Ltl a -> String
(Int -> Ltl a -> ShowS)
-> (Ltl a -> String) -> ([Ltl a] -> ShowS) -> Show (Ltl a)
forall a. Show a => Int -> Ltl a -> ShowS
forall a. Show a => [Ltl a] -> ShowS
forall a. Show a => Ltl a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Ltl a -> ShowS
showsPrec :: Int -> Ltl a -> ShowS
$cshow :: forall a. Show a => Ltl a -> String
show :: Ltl a -> String
$cshowList :: forall a. Show a => [Ltl a] -> ShowS
showList :: [Ltl a] -> ShowS
Show, Ltl a -> Ltl a -> Bool
(Ltl a -> Ltl a -> Bool) -> (Ltl a -> Ltl a -> Bool) -> Eq (Ltl a)
forall a. Eq a => Ltl a -> Ltl a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Ltl a -> Ltl a -> Bool
== :: Ltl a -> Ltl a -> Bool
$c/= :: forall a. Eq a => Ltl a -> Ltl a -> Bool
/= :: Ltl a -> Ltl a -> Bool
Eq, (forall a b. (a -> b) -> Ltl a -> Ltl b)
-> (forall a b. a -> Ltl b -> Ltl a) -> Functor Ltl
forall a b. a -> Ltl b -> Ltl a
forall a b. (a -> b) -> Ltl a -> Ltl b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Ltl a -> Ltl b
fmap :: forall a b. (a -> b) -> Ltl a -> Ltl b
$c<$ :: forall a b. a -> Ltl b -> Ltl a
<$ :: forall a b. a -> Ltl b -> Ltl a
Functor)

-- | Same as `LtlNot`, but first wraps the input in an atomic formula.
ltlNot' :: a -> Ltl a
ltlNot' :: forall a. a -> Ltl a
ltlNot' = Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
LtlNot (Ltl a -> Ltl a) -> (a -> Ltl a) -> a -> Ltl a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Ltl a
forall a. a -> Ltl a
LtlAtom

-- | Same as `LtlOr`, but first wraps the inputs in atomic formulas.
ltlOr' :: a -> a -> Ltl a
ltlOr' :: forall a. a -> a -> Ltl a
ltlOr' a
f1 a
f2 = Ltl a -> Ltl a -> Ltl a
forall a. Ltl a -> Ltl a -> Ltl a
LtlOr (a -> Ltl a
forall a. a -> Ltl a
LtlAtom a
f1) (a -> Ltl a
forall a. a -> Ltl a
LtlAtom a
f2)

-- | Same as `LtlAnd`, but first wraps the inputs in atomic formulas.
ltlAnd' :: a -> a -> Ltl a
ltlAnd' :: forall a. a -> a -> Ltl a
ltlAnd' a
f1 a
f2 = Ltl a -> Ltl a -> Ltl a
forall a. Ltl a -> Ltl a -> Ltl a
LtlAnd (a -> Ltl a
forall a. a -> Ltl a
LtlAtom a
f1) (a -> Ltl a
forall a. a -> Ltl a
LtlAtom a
f2)

-- | Same as `LtlNext`, but first wraps the input in an atomic formula.
ltlNext' :: a -> Ltl a
ltlNext' :: forall a. a -> Ltl a
ltlNext' = Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
LtlNext (Ltl a -> Ltl a) -> (a -> Ltl a) -> a -> Ltl a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Ltl a
forall a. a -> Ltl a
LtlAtom

-- | Produces an Ltl formula which consists of the disjunction of all the
-- formulas in the input list.
ltlAny :: [Ltl a] -> Ltl a
ltlAny :: forall a. [Ltl a] -> Ltl a
ltlAny = (Ltl a -> Ltl a -> Ltl a) -> Ltl a -> [Ltl a] -> Ltl a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Ltl a -> Ltl a -> Ltl a
forall a. Ltl a -> Ltl a -> Ltl a
LtlOr Ltl a
forall a. Ltl a
LtlFalsity

-- | Same as `ltlAny`, but first wraps the elements in the input list in atomic
-- formulas.
ltlAny' :: [a] -> Ltl a
ltlAny' :: forall a. [a] -> Ltl a
ltlAny' = [Ltl a] -> Ltl a
forall a. [Ltl a] -> Ltl a
ltlAny ([Ltl a] -> Ltl a) -> ([a] -> [Ltl a]) -> [a] -> Ltl a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Ltl a) -> [a] -> [Ltl a]
forall a b. (a -> b) -> [a] -> [b]
map a -> Ltl a
forall a. a -> Ltl a
LtlAtom

-- | Produces an Ltl formula which consists of the conjunction of all the
-- formulas in the input list.
ltlAll :: [Ltl a] -> Ltl a
ltlAll :: forall a. [Ltl a] -> Ltl a
ltlAll = (Ltl a -> Ltl a -> Ltl a) -> Ltl a -> [Ltl a] -> Ltl a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Ltl a -> Ltl a -> Ltl a
forall a. Ltl a -> Ltl a -> Ltl a
LtlAnd Ltl a
forall a. Ltl a
LtlTruth

-- | Same as `ltlAll`, but first wraps the elements in the input list in atomic
-- formulas.
ltlAll' :: [a] -> Ltl a
ltlAll' :: forall a. [a] -> Ltl a
ltlAll' = [Ltl a] -> Ltl a
forall a. [Ltl a] -> Ltl a
ltlAll ([Ltl a] -> Ltl a) -> ([a] -> [Ltl a]) -> [a] -> Ltl a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Ltl a) -> [a] -> [Ltl a]
forall a b. (a -> b) -> [a] -> [b]
map a -> Ltl a
forall a. a -> Ltl a
LtlAtom

-- | Produces an Ltl formula which consists of the delay of the input formula by
-- @n@ time steps, if @n > 0@.
ltlDelay :: Integer -> Ltl a -> Ltl a
ltlDelay :: forall a. Integer -> Ltl a -> Ltl a
ltlDelay Integer
n | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
0 = Ltl a -> Ltl a
forall a. a -> a
id
ltlDelay Integer
n = Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
LtlNext (Ltl a -> Ltl a) -> (Ltl a -> Ltl a) -> Ltl a -> Ltl a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Ltl a -> Ltl a
forall a. Integer -> Ltl a -> Ltl a
ltlDelay (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)

-- | Same as `ltlDelay`, but first wraps the input in an atomic formula.
ltlDelay' :: Integer -> a -> Ltl a
ltlDelay' :: forall a. Integer -> a -> Ltl a
ltlDelay' Integer
n = Integer -> Ltl a -> Ltl a
forall a. Integer -> Ltl a -> Ltl a
ltlDelay Integer
n (Ltl a -> Ltl a) -> (a -> Ltl a) -> a -> Ltl a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Ltl a
forall a. a -> Ltl a
LtlAtom

-- | Produces an Ltl formula which ensures the input formula eventually holds.
ltlEventually :: Ltl a -> Ltl a
ltlEventually :: forall a. Ltl a -> Ltl a
ltlEventually = Ltl a -> Ltl a -> Ltl a
forall a. Ltl a -> Ltl a -> Ltl a
LtlUntil Ltl a
forall a. Ltl a
LtlTruth

-- | Same as `ltlEventually`, but first wraps the input in an atomic formula.
ltlEventually' :: a -> Ltl a
ltlEventually' :: forall a. a -> Ltl a
ltlEventually' = Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
ltlEventually (Ltl a -> Ltl a) -> (a -> Ltl a) -> a -> Ltl a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Ltl a
forall a. a -> Ltl a
LtlAtom

-- | Produces an Ltl formula which ensures the input formula always holds.
ltlAlways :: Ltl a -> Ltl a
ltlAlways :: forall a. Ltl a -> Ltl a
ltlAlways = Ltl a -> Ltl a -> Ltl a
forall a. Ltl a -> Ltl a -> Ltl a
LtlRelease Ltl a
forall a. Ltl a
LtlFalsity

-- | Same as `ltlAlways`, but first wraps the input in an atomic formula.
ltlAlways' :: a -> Ltl a
ltlAlways' :: forall a. a -> Ltl a
ltlAlways' = Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
ltlAlways (Ltl a -> Ltl a) -> (a -> Ltl a) -> a -> Ltl a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Ltl a
forall a. a -> Ltl a
LtlAtom

-- | Produces an Ltl formula which either ensure the given formula does not
-- hold, or apply its modifications.
ltlIfPossible :: Ltl a -> Ltl a
ltlIfPossible :: forall a. Ltl a -> Ltl a
ltlIfPossible Ltl a
f = Ltl a
f Ltl a -> Ltl a -> Ltl a
forall a. Ltl a -> Ltl a -> Ltl a
`LtlOr` Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
LtlNot Ltl a
f

-- | Same as `ltlIfPossible`, but first wraps the input in an atomic formula.
ltlIfPossible' :: a -> Ltl a
ltlIfPossible' :: forall a. a -> Ltl a
ltlIfPossible' = Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
ltlIfPossible (Ltl a -> Ltl a) -> (a -> Ltl a) -> a -> Ltl a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Ltl a
forall a. a -> Ltl a
LtlAtom

-- | Produces an Ltl formula which applies a formula whenever possible, while
-- ignoring steps when it is not.
ltlWhenPossible :: Ltl a -> Ltl a
ltlWhenPossible :: forall a. Ltl a -> Ltl a
ltlWhenPossible = Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
ltlAlways (Ltl a -> Ltl a) -> (Ltl a -> Ltl a) -> Ltl a -> Ltl a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
ltlIfPossible

-- | Same as `ltlWhenPossible`, but first wraps the input in an atomic formula.
ltlWhenPossible' :: a -> Ltl a
ltlWhenPossible' :: forall a. a -> Ltl a
ltlWhenPossible' = Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
ltlWhenPossible (Ltl a -> Ltl a) -> (a -> Ltl a) -> a -> Ltl a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Ltl a
forall a. a -> Ltl a
LtlAtom

-- | Produces an Ltl formula ensuring the given formula always fails.
ltlNever :: Ltl a -> Ltl a
ltlNever :: forall a. Ltl a -> Ltl a
ltlNever = Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
ltlAlways (Ltl a -> Ltl a) -> (Ltl a -> Ltl a) -> Ltl a -> Ltl a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
LtlNot

-- | Same as `ltlNever`, but first wraps the input in an atomic formula.
ltlNever' :: a -> Ltl a
ltlNever' :: forall a. a -> Ltl a
ltlNever' = Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
ltlNever (Ltl a -> Ltl a) -> (a -> Ltl a) -> a -> Ltl a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Ltl a
forall a. a -> Ltl a
LtlAtom

-- | Produces a formula that succeeds if the first formula does not hold, or if
-- both formulas hold.
ltlImplies :: Ltl a -> Ltl a -> Ltl a
ltlImplies :: forall a. Ltl a -> Ltl a -> Ltl a
ltlImplies Ltl a
f1 Ltl a
f2 = (Ltl a
f2 Ltl a -> Ltl a -> Ltl a
forall a. Ltl a -> Ltl a -> Ltl a
`LtlAnd` Ltl a
f1) Ltl a -> Ltl a -> Ltl a
forall a. Ltl a -> Ltl a -> Ltl a
`LtlOr` Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
LtlNot Ltl a
f1

-- | Same as `ltlImplies` but first wraps the inputs in atomic formulas.
ltlImplies' :: a -> a -> Ltl a
ltlImplies' :: forall a. a -> a -> Ltl a
ltlImplies' a
a1 a
a2 = a -> Ltl a
forall a. a -> Ltl a
LtlAtom a
a1 Ltl a -> Ltl a -> Ltl a
forall a. Ltl a -> Ltl a -> Ltl a
`ltlImplies` a -> Ltl a
forall a. a -> Ltl a
LtlAtom a
a2

-- | Simplification procedure for LTL formulas. This function knows how
-- `LtlTruth` and `LtlFalsity` play with negation, conjunction and disjunction
-- and recursively applies this knowledge; it is used to keep the formulas
-- `nowLaterList` generates from growing too wildly. While this function does
-- not compute a normal form per se (as it does not tamper with nested
-- conjunction and disjunction), it does ensure a few properties:
--
-- * `LtlNext` is left unchanged
--
-- * `LtlNot` only appears in the resulting formula wrapping up a `LtlAtom`
--
-- * `LtlUntil` and `LtlRelease` are interpreted in terms of other constructs,
--   and thus are never returned.
--
-- * Two `LtlNext` appearing in both sides of an `LtlAnd` and `LtlOr` are
--   merged. Thus a formula of shape @LtlAnd (LtlNext a) (LtlNext b)@ will never
--   be returned, and similarly with @LtlOr@.
ltlSimpl :: Ltl a -> Ltl a
ltlSimpl :: forall a. Ltl a -> Ltl a
ltlSimpl (LtlAtom a
a) = a -> Ltl a
forall a. a -> Ltl a
LtlAtom a
a
ltlSimpl Ltl a
LtlTruth = Ltl a
forall a. Ltl a
LtlTruth
ltlSimpl Ltl a
LtlFalsity = Ltl a
forall a. Ltl a
LtlFalsity
ltlSimpl (LtlNext Ltl a
f) = Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
LtlNext Ltl a
f
ltlSimpl (LtlRelease Ltl a
f1 Ltl a
f2) = Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
ltlSimpl (Ltl a -> Ltl a) -> Ltl a -> Ltl a
forall a b. (a -> b) -> a -> b
$ Ltl a
f2 Ltl a -> Ltl a -> Ltl a
forall a. Ltl a -> Ltl a -> Ltl a
`LtlAnd` (Ltl a
f1 Ltl a -> Ltl a -> Ltl a
forall a. Ltl a -> Ltl a -> Ltl a
`LtlOr` Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
LtlNext (Ltl a
f1 Ltl a -> Ltl a -> Ltl a
forall a. Ltl a -> Ltl a -> Ltl a
`LtlRelease` Ltl a
f2))
ltlSimpl (LtlUntil Ltl a
f1 Ltl a
f2) = Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
ltlSimpl (Ltl a -> Ltl a) -> Ltl a -> Ltl a
forall a b. (a -> b) -> a -> b
$ Ltl a
f2 Ltl a -> Ltl a -> Ltl a
forall a. Ltl a -> Ltl a -> Ltl a
`LtlOr` (Ltl a
f1 Ltl a -> Ltl a -> Ltl a
forall a. Ltl a -> Ltl a -> Ltl a
`LtlAnd` Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
LtlNext (Ltl a
f1 Ltl a -> Ltl a -> Ltl a
forall a. Ltl a -> Ltl a -> Ltl a
`LtlUntil` Ltl a
f2))
ltlSimpl (LtlNot (Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
ltlSimpl -> Ltl a
LtlTruth)) = Ltl a
forall a. Ltl a
LtlFalsity
ltlSimpl (LtlNot (Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
ltlSimpl -> Ltl a
LtlFalsity)) = Ltl a
forall a. Ltl a
LtlTruth
ltlSimpl (LtlNot (Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
ltlSimpl -> LtlNot Ltl a
f)) = Ltl a
f
ltlSimpl (LtlNot (Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
ltlSimpl -> LtlAnd Ltl a
f1 Ltl a
f2)) = Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
ltlSimpl (Ltl a -> Ltl a) -> Ltl a -> Ltl a
forall a b. (a -> b) -> a -> b
$ Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
LtlNot Ltl a
f1 Ltl a -> Ltl a -> Ltl a
forall a. Ltl a -> Ltl a -> Ltl a
`LtlOr` Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
LtlNot Ltl a
f2
ltlSimpl (LtlNot (Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
ltlSimpl -> LtlOr Ltl a
f1 Ltl a
f2)) = Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
ltlSimpl (Ltl a -> Ltl a) -> Ltl a -> Ltl a
forall a b. (a -> b) -> a -> b
$ Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
LtlNot Ltl a
f1 Ltl a -> Ltl a -> Ltl a
forall a. Ltl a -> Ltl a -> Ltl a
`LtlAnd` Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
LtlNot Ltl a
f2
ltlSimpl (LtlNot (Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
ltlSimpl -> LtlNext Ltl a
f)) = Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
LtlNext (Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
LtlNot Ltl a
f)
-- The following will never occur, as `ltlSimpl` never returns something of
-- the shape `LtlUntil` or `LtlRelease`
ltlSimpl (LtlNot (Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
ltlSimpl -> Ltl a
f)) = Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
LtlNot Ltl a
f
ltlSimpl (LtlAnd (Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
ltlSimpl -> Ltl a
LtlFalsity) Ltl a
_) = Ltl a
forall a. Ltl a
LtlFalsity
ltlSimpl (LtlAnd Ltl a
_ (Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
ltlSimpl -> Ltl a
LtlFalsity)) = Ltl a
forall a. Ltl a
LtlFalsity
ltlSimpl (LtlAnd (Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
ltlSimpl -> Ltl a
LtlTruth) (Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
ltlSimpl -> Ltl a
f2)) = Ltl a
f2
ltlSimpl (LtlAnd (Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
ltlSimpl -> Ltl a
f1) (Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
ltlSimpl -> Ltl a
LtlTruth)) = Ltl a
f1
ltlSimpl (LtlAnd (Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
ltlSimpl -> LtlNext Ltl a
f1) (Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
ltlSimpl -> LtlNext Ltl a
f2)) = Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
LtlNext (Ltl a -> Ltl a) -> Ltl a -> Ltl a
forall a b. (a -> b) -> a -> b
$ Ltl a
f1 Ltl a -> Ltl a -> Ltl a
forall a. Ltl a -> Ltl a -> Ltl a
`LtlAnd` Ltl a
f2
ltlSimpl (LtlAnd (Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
ltlSimpl -> Ltl a
f1) (Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
ltlSimpl -> Ltl a
f2)) = Ltl a -> Ltl a -> Ltl a
forall a. Ltl a -> Ltl a -> Ltl a
LtlAnd Ltl a
f1 Ltl a
f2
ltlSimpl (LtlOr (Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
ltlSimpl -> Ltl a
LtlFalsity) (Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
ltlSimpl -> Ltl a
f2)) = Ltl a
f2
ltlSimpl (LtlOr (Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
ltlSimpl -> Ltl a
f1) (Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
ltlSimpl -> Ltl a
LtlFalsity)) = Ltl a
f1
ltlSimpl (LtlOr (Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
ltlSimpl -> LtlNext Ltl a
f1) (Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
ltlSimpl -> LtlNext Ltl a
f2)) = Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
LtlNext (Ltl a -> Ltl a) -> Ltl a -> Ltl a
forall a b. (a -> b) -> a -> b
$ Ltl a
f1 Ltl a -> Ltl a -> Ltl a
forall a. Ltl a -> Ltl a -> Ltl a
`LtlOr` Ltl a
f2
-- We don't perform any reduction when `LtlOr` is applied to `LtlTruth` as
-- we still need to keep both branches, and certainly don't want to discard
-- the branch were potential meaningful modifications need to be applied.
ltlSimpl (LtlOr (Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
ltlSimpl -> Ltl a
f1) (Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
ltlSimpl -> Ltl a
f2)) = Ltl a -> Ltl a -> Ltl a
forall a. Ltl a -> Ltl a -> Ltl a
LtlOr Ltl a
f1 Ltl a
f2

-- | Requirements implied by a given `Ltl` formula at a given time step
data Requirement a
  = -- | Apply this modification now
    Apply a
  | -- | Ensure this modification fails now
    EnsureFailure a

-- | For each LTL formula that describes a modification of a computation in a
-- list, split it into a list of @(doNow, doLater)@ pairs, and then
-- appropriately combine the results. The result of the splitting is bound to
-- the following semantics:
--
-- * @doNow@ is the list of modifications to be consecutively either applied to
-- the current time step (`Apply`), or that should fail at the current time step
-- (`EnsureFailure`)
--
-- * @doLater@ is an LTL formula describing the modification that should be
-- applied from the next time step onwards.
--
-- The return value is a list because a formula might be satisfied in different
-- ways. For example, the modification described by @a `LtlUntil` b@ might be
-- accomplished by applying the modification @b@ right now, or by applying @a@
-- right now and @a `LtlUntil` b@ from the next step onwards; the returned list
-- will contain these two options.
nowLaterList :: [Ltl a] -> [([Requirement a], [Ltl a])]
nowLaterList :: forall a. [Ltl a] -> [([Requirement a], [Ltl a])]
nowLaterList =
  (Ltl a
 -> [([Requirement a], [Ltl a])] -> [([Requirement a], [Ltl a])])
-> [([Requirement a], [Ltl a])]
-> [Ltl a]
-> [([Requirement a], [Ltl a])]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
    ( \Ltl a
el [([Requirement a], [Ltl a])]
acc -> do
        ([Requirement a]
now, Ltl a
next) <- Ltl a -> [([Requirement a], Ltl a)]
forall a. Ltl a -> [([Requirement a], Ltl a)]
nowLater (Ltl a -> [([Requirement a], Ltl a)])
-> Ltl a -> [([Requirement a], Ltl a)]
forall a b. (a -> b) -> a -> b
$ Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
ltlSimpl Ltl a
el
        ([Requirement a]
now', [Ltl a]
nexts) <- [([Requirement a], [Ltl a])]
acc
        ([Requirement a], [Ltl a]) -> [([Requirement a], [Ltl a])]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Requirement a]
now [Requirement a] -> [Requirement a] -> [Requirement a]
forall a. Semigroup a => a -> a -> a
<> [Requirement a]
now', Ltl a
next Ltl a -> [Ltl a] -> [Ltl a]
forall a. a -> [a] -> [a]
: [Ltl a]
nexts)
    )
    [([], [])]
  where
    nowLater :: Ltl a -> [([Requirement a], Ltl a)]
    nowLater :: forall a. Ltl a -> [([Requirement a], Ltl a)]
nowLater Ltl a
LtlTruth = [([], Ltl a
forall a. Ltl a
LtlTruth)]
    nowLater Ltl a
LtlFalsity = [([], Ltl a
forall a. Ltl a
LtlFalsity)]
    nowLater (LtlAtom a
now) = [([a -> Requirement a
forall a. a -> Requirement a
Apply a
now], Ltl a
forall a. Ltl a
LtlTruth)]
    nowLater (LtlNext Ltl a
f) = [([], Ltl a
f)]
    nowLater (LtlNot (LtlAtom a
now)) = [([a -> Requirement a
forall a. a -> Requirement a
EnsureFailure a
now], Ltl a
forall a. Ltl a
LtlTruth)]
    nowLater (Ltl a
f1 `LtlOr` Ltl a
f2) = Ltl a -> [([Requirement a], Ltl a)]
forall a. Ltl a -> [([Requirement a], Ltl a)]
nowLater Ltl a
f1 [([Requirement a], Ltl a)]
-> [([Requirement a], Ltl a)] -> [([Requirement a], Ltl a)]
forall a. [a] -> [a] -> [a]
++ Ltl a -> [([Requirement a], Ltl a)]
forall a. Ltl a -> [([Requirement a], Ltl a)]
nowLater Ltl a
f2
    nowLater (Ltl a
f1 `LtlAnd` Ltl a
f2) = do
      ([Requirement a]
now1, Ltl a
next1) <- Ltl a -> [([Requirement a], Ltl a)]
forall a. Ltl a -> [([Requirement a], Ltl a)]
nowLater Ltl a
f1
      ([Requirement a]
now2, Ltl a
next2) <- Ltl a -> [([Requirement a], Ltl a)]
forall a. Ltl a -> [([Requirement a], Ltl a)]
nowLater Ltl a
f2
      ([Requirement a], Ltl a) -> [([Requirement a], Ltl a)]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Requirement a]
now2 [Requirement a] -> [Requirement a] -> [Requirement a]
forall a. Semigroup a => a -> a -> a
<> [Requirement a]
now1, Ltl a
next2 Ltl a -> Ltl a -> Ltl a
forall a. Ltl a -> Ltl a -> Ltl a
`LtlAnd` Ltl a
next1)
    -- Only the above cases can occur, as they are outcomes of @ltlSimpl@. This
    -- is handy (and intended), as the remaining cases would lead to complicated
    -- interactions and hard to handle growth in the number of formulas.
    nowLater Ltl a
_ = String -> [([Requirement a], Ltl a)]
forall a. HasCallStack => String -> a
error String
"nowLater is always called after ltlSimpl which does not yield more cases."

-- | If there are no more steps and the next step should satisfy the given
-- formula: Are we finished, i.e. was the initial formula satisfied by now?
finished :: Ltl a -> Bool
finished :: forall a. Ltl a -> Bool
finished Ltl a
LtlTruth = Bool
True
finished Ltl a
LtlFalsity = Bool
False
finished (LtlAtom a
_) = Bool
False
finished (LtlAnd Ltl a
f1 Ltl a
f2) = Ltl a -> Bool
forall a. Ltl a -> Bool
finished Ltl a
f1 Bool -> Bool -> Bool
&& Ltl a -> Bool
forall a. Ltl a -> Bool
finished Ltl a
f2
finished (LtlOr Ltl a
f1 Ltl a
f2) = Ltl a -> Bool
forall a. Ltl a -> Bool
finished Ltl a
f1 Bool -> Bool -> Bool
|| Ltl a -> Bool
forall a. Ltl a -> Bool
finished Ltl a
f2
finished (LtlNext Ltl a
_) = Bool
False
finished (LtlUntil Ltl a
_ Ltl a
_) = Bool
False
finished (LtlRelease Ltl a
_ Ltl a
_) = Bool
True
finished (LtlNot Ltl a
f) = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Ltl a -> Bool
forall a. Ltl a -> Bool
finished Ltl a
f

-- | Operations that either allow to use a builtin, or to modify a computation
-- using an `Ltl` formula.
data LtlOp modification builtin :: Type -> Type where
  WrapLtl :: Ltl modification -> StagedLtl modification builtin a -> LtlOp modification builtin a
  Builtin :: builtin a -> LtlOp modification builtin a

-- | An AST of builtins wrapped into an `Ltl` setting
type StagedLtl modification builtin = Staged (LtlOp modification builtin)

-- | Builds a singleton instruction in a `StagedLtl` monad
singletonBuiltin :: builtin a -> StagedLtl modification builtin a
singletonBuiltin :: forall (builtin :: * -> *) a modification.
builtin a -> StagedLtl modification builtin a
singletonBuiltin = (LtlOp modification builtin a
-> (a -> Staged (LtlOp modification builtin) a)
-> Staged (LtlOp modification builtin) a
forall (op :: * -> *) a1 a.
op a1 -> (a1 -> Staged op a) -> Staged op a
`Instr` a -> Staged (LtlOp modification builtin) a
forall a (op :: * -> *). a -> Staged op a
Return) (LtlOp modification builtin a
 -> Staged (LtlOp modification builtin) a)
-> (builtin a -> LtlOp modification builtin a)
-> builtin a
-> Staged (LtlOp modification builtin) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. builtin a -> LtlOp modification builtin a
forall (builtin :: * -> *) a modification.
builtin a -> LtlOp modification builtin a
Builtin

-- | Depicts the ability to modify a computation with an `Ltl` formula
class (Monad m) => MonadLtl modification m where
  modifyLtl :: Ltl modification -> m a -> m a

instance MonadLtl modification (StagedLtl modification builtin) where
  modifyLtl :: forall a.
Ltl modification
-> StagedLtl modification builtin a
-> StagedLtl modification builtin a
modifyLtl Ltl modification
formula StagedLtl modification builtin a
comp = LtlOp modification builtin a
-> (a -> StagedLtl modification builtin a)
-> StagedLtl modification builtin a
forall (op :: * -> *) a1 a.
op a1 -> (a1 -> Staged op a) -> Staged op a
Instr (Ltl modification
-> StagedLtl modification builtin a -> LtlOp modification builtin a
forall modification (builtin :: * -> *) a.
Ltl modification
-> StagedLtl modification builtin a -> LtlOp modification builtin a
WrapLtl Ltl modification
formula StagedLtl modification builtin a
comp) a -> StagedLtl modification builtin a
forall a (op :: * -> *). a -> Staged op a
Return

-- | Depicts the ability to modify and interpret builtins in a given
-- domain. Each builtin can either:
--
-- * be interpreted directly through @Left@, in which case it will not be
--   considered as a timestep in a trace.
--
-- * be modified and only then interpreted through @Right@, in which case it
--   will be considered as a timestep in a trace.
class ModInterpBuiltin modification builtin m where
  modifyAndInterpBuiltin :: builtin a -> Either (m a) ([Requirement modification] -> m a)

-- | Interprets a `StagedLtl` computation based on an interpretation of
-- @builtin@ with respect to possible modifications. This unfolds as follows:
--
-- * When a builtin is met, which is directly interpreted, we return the
--   associated computation, with no changes to the `Ltl` state.
--
-- * When a builtin is met, which requires a modification, we return the
--   modified interpretation, and consume the current modification requirements.
--
-- * When a wrapped computation is met, we store the new associated formula, and
--   ensure that when the computation ends, the formula is finished.
interpStagedLtl ::
  forall modification builtin m.
  ( MonadPlus m,
    ModInterpBuiltin modification builtin m
  ) =>
  forall a.
  -- | A staged computation `Ltl` compatible
  StagedLtl modification builtin a ->
  -- | Interpretation of the computation
  m a
interpStagedLtl :: forall modification (builtin :: * -> *) (m :: * -> *) a.
(MonadPlus m, ModInterpBuiltin modification builtin m) =>
StagedLtl modification builtin a -> m a
interpStagedLtl = (StateT [Ltl modification] m a -> [Ltl modification] -> m a)
-> [Ltl modification] -> StateT [Ltl modification] m a -> m a
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT [Ltl modification] m a -> [Ltl modification] -> m a
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT [] (StateT [Ltl modification] m a -> m a)
-> (StagedLtl modification builtin a
    -> StateT [Ltl modification] m a)
-> StagedLtl modification builtin a
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StagedLtl modification builtin a -> StateT [Ltl modification] m a
forall a.
Staged (LtlOp modification builtin) a
-> StateT [Ltl modification] m a
go
  where
    go :: forall a. Staged (LtlOp modification builtin) a -> StateT [Ltl modification] m a
    go :: forall a.
Staged (LtlOp modification builtin) a
-> StateT [Ltl modification] m a
go = (forall a.
 LtlOp modification builtin a -> StateT [Ltl modification] m a)
-> forall a.
   Staged (LtlOp modification builtin) a
   -> StateT [Ltl modification] m a
forall (m :: * -> *) (op :: * -> *).
Monad m =>
(forall a. op a -> m a) -> forall a. Staged op a -> m a
interpStaged ((forall a.
  LtlOp modification builtin a -> StateT [Ltl modification] m a)
 -> forall a.
    Staged (LtlOp modification builtin) a
    -> StateT [Ltl modification] m a)
-> (forall a.
    LtlOp modification builtin a -> StateT [Ltl modification] m a)
-> forall a.
   Staged (LtlOp modification builtin) a
   -> StateT [Ltl modification] m a
forall a b. (a -> b) -> a -> b
$ \case
      WrapLtl Ltl modification
formula StagedLtl modification builtin a
comp -> do
        ([Ltl modification] -> [Ltl modification])
-> StateT [Ltl modification] m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (Ltl modification
formula Ltl modification -> [Ltl modification] -> [Ltl modification]
forall a. a -> [a] -> [a]
:)
        a
res <- StagedLtl modification builtin a -> StateT [Ltl modification] m a
forall a.
Staged (LtlOp modification builtin) a
-> StateT [Ltl modification] m a
go StagedLtl modification builtin a
comp
        [Ltl modification]
formulas <- StateT [Ltl modification] m [Ltl modification]
forall s (m :: * -> *). MonadState s m => m s
get
        Bool
-> StateT [Ltl modification] m () -> StateT [Ltl modification] m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Ltl modification] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ltl modification]
formulas) (StateT [Ltl modification] m () -> StateT [Ltl modification] m ())
-> StateT [Ltl modification] m () -> StateT [Ltl modification] m ()
forall a b. (a -> b) -> a -> b
$ do
          Bool -> StateT [Ltl modification] m ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> StateT [Ltl modification] m ())
-> Bool -> StateT [Ltl modification] m ()
forall a b. (a -> b) -> a -> b
$ Ltl modification -> Bool
forall a. Ltl a -> Bool
finished (Ltl modification -> Bool) -> Ltl modification -> Bool
forall a b. (a -> b) -> a -> b
$ [Ltl modification] -> Ltl modification
forall a. HasCallStack => [a] -> a
head [Ltl modification]
formulas
          [Ltl modification] -> StateT [Ltl modification] m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ([Ltl modification] -> StateT [Ltl modification] m ())
-> [Ltl modification] -> StateT [Ltl modification] m ()
forall a b. (a -> b) -> a -> b
$ [Ltl modification] -> [Ltl modification]
forall a. HasCallStack => [a] -> [a]
tail [Ltl modification]
formulas
        a -> StateT [Ltl modification] m a
forall a. a -> StateT [Ltl modification] m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
res
      Builtin builtin a
builtin ->
        case builtin a -> Either (m a) ([Requirement modification] -> m a)
forall a.
builtin a -> Either (m a) ([Requirement modification] -> m a)
forall {k} modification (builtin :: k -> *) (m :: k -> *) (a :: k).
ModInterpBuiltin modification builtin m =>
builtin a -> Either (m a) ([Requirement modification] -> m a)
modifyAndInterpBuiltin builtin a
builtin of
          Left m a
comp -> m a -> StateT [Ltl modification] m a
forall (m :: * -> *) a.
Monad m =>
m a -> StateT [Ltl modification] m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m a
comp
          Right [Requirement modification] -> m a
applyMod -> do
            [([Requirement modification], [Ltl modification])]
modifications <- ([Ltl modification]
 -> [([Requirement modification], [Ltl modification])])
-> StateT
     [Ltl modification]
     m
     [([Requirement modification], [Ltl modification])]
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets [Ltl modification]
-> [([Requirement modification], [Ltl modification])]
forall a. [Ltl a] -> [([Requirement a], [Ltl a])]
nowLaterList
            [StateT [Ltl modification] m a] -> StateT [Ltl modification] m a
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ([StateT [Ltl modification] m a] -> StateT [Ltl modification] m a)
-> ((([Requirement modification], [Ltl modification])
     -> StateT [Ltl modification] m a)
    -> [StateT [Ltl modification] m a])
-> (([Requirement modification], [Ltl modification])
    -> StateT [Ltl modification] m a)
-> StateT [Ltl modification] m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([([Requirement modification], [Ltl modification])]
modifications [([Requirement modification], [Ltl modification])]
-> (([Requirement modification], [Ltl modification])
    -> StateT [Ltl modification] m a)
-> [StateT [Ltl modification] m a]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>) ((([Requirement modification], [Ltl modification])
  -> StateT [Ltl modification] m a)
 -> StateT [Ltl modification] m a)
-> (([Requirement modification], [Ltl modification])
    -> StateT [Ltl modification] m a)
-> StateT [Ltl modification] m a
forall a b. (a -> b) -> a -> b
$
              \([Requirement modification]
now, [Ltl modification]
later) -> do
                [Ltl modification] -> StateT [Ltl modification] m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put [Ltl modification]
later
                m a -> StateT [Ltl modification] m a
forall (m :: * -> *) a.
Monad m =>
m a -> StateT [Ltl modification] m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m a -> StateT [Ltl modification] m a)
-> m a -> StateT [Ltl modification] m a
forall a b. (a -> b) -> a -> b
$ [Requirement modification] -> m a
applyMod [Requirement modification]
now