{-# LANGUAGE TemplateHaskell #-}

-- | 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',

    -- * `Ltl` helpers,
    nowLaterList,
    finished,

    -- * Laying out modifications on time using `Ltl`
    ModifyGlobally,
    modifyLtl,
    runModifyGlobally,

    -- * Locally applying laid out modifications
    Requirement (..),
    ModifyLocally,
    getRequirements,
    runModifyLocally,
  )
where

import Control.Monad
import Data.Functor
import Polysemy
import Polysemy.NonDet
import Polysemy.State

-- | 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
  deriving (Int -> Requirement a -> ShowS
[Requirement a] -> ShowS
Requirement a -> String
(Int -> Requirement a -> ShowS)
-> (Requirement a -> String)
-> ([Requirement a] -> ShowS)
-> Show (Requirement a)
forall a. Show a => Int -> Requirement a -> ShowS
forall a. Show a => [Requirement a] -> ShowS
forall a. Show a => Requirement a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Requirement a -> ShowS
showsPrec :: Int -> Requirement a -> ShowS
$cshow :: forall a. Show a => Requirement a -> String
show :: Requirement a -> String
$cshowList :: forall a. Show a => [Requirement a] -> ShowS
showList :: [Requirement a] -> ShowS
Show, Requirement a -> Requirement a -> Bool
(Requirement a -> Requirement a -> Bool)
-> (Requirement a -> Requirement a -> Bool) -> Eq (Requirement a)
forall a. Eq a => Requirement a -> Requirement a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Requirement a -> Requirement a -> Bool
== :: Requirement a -> Requirement a -> Bool
$c/= :: forall a. Eq a => Requirement a -> Requirement a -> Bool
/= :: Requirement a -> Requirement a -> Bool
Eq)

-- | 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

-- | An effect to modify a computation with an `Ltl` formula. The idea is that
-- the formula pinpoints locations where `Requirement`s should be enforced.
data ModifyGlobally a :: Effect where
  ModifyLtl :: Ltl a -> m b -> ModifyGlobally a m b

makeSem_ ''ModifyGlobally

-- | Lays out an `Ltl` formula to be used for modification within the execution
-- of the wrapped computation. See `ModifyLocally` for how to consume and use
-- the laid out modifications.
modifyLtl :: forall a r b. (Member (ModifyGlobally a) r) => Ltl a -> Sem r b -> Sem r b

-- | Running the `ModifyGlobally` effect requires to have access of the current
-- list of `Ltl` formulas, and to have access to an empty computation.
--
-- A new formula is appended at the head of the current list of formula. Then,
-- the actual computation is run, after which the newly added formula must be
-- finished, otherwise the empty computation is returned.
runModifyGlobally ::
  forall mod effs a.
  ( Members
      '[ State [Ltl mod],
         NonDet
       ]
      effs
  ) =>
  Sem (ModifyGlobally mod ': effs) a ->
  Sem effs a
runModifyGlobally :: forall mod (effs :: EffectRow) a.
Members '[State [Ltl mod], NonDet] effs =>
Sem (ModifyGlobally mod : effs) a -> Sem effs a
runModifyGlobally =
  (forall (rInitial :: EffectRow) x.
 ModifyGlobally mod (Sem rInitial) x
 -> Tactical (ModifyGlobally mod) (Sem rInitial) effs x)
-> Sem (ModifyGlobally mod : effs) a -> Sem effs a
forall (e :: Effect) (r :: EffectRow) a.
(forall (rInitial :: EffectRow) x.
 e (Sem rInitial) x -> Tactical e (Sem rInitial) r x)
-> Sem (e : r) a -> Sem r a
interpretH ((forall (rInitial :: EffectRow) x.
  ModifyGlobally mod (Sem rInitial) x
  -> Tactical (ModifyGlobally mod) (Sem rInitial) effs x)
 -> Sem (ModifyGlobally mod : effs) a -> Sem effs a)
-> (forall (rInitial :: EffectRow) x.
    ModifyGlobally mod (Sem rInitial) x
    -> Tactical (ModifyGlobally mod) (Sem rInitial) effs x)
-> Sem (ModifyGlobally mod : effs) a
-> Sem effs a
forall a b. (a -> b) -> a -> b
$ \case
    ModifyLtl Ltl mod
formula Sem rInitial x
comp -> do
      ([Ltl mod] -> [Ltl mod])
-> Sem (WithTactics (ModifyGlobally mod) f (Sem rInitial) effs) ()
forall s (r :: EffectRow).
Member (State s) r =>
(s -> s) -> Sem r ()
modify (Ltl mod
formula Ltl mod -> [Ltl mod] -> [Ltl mod]
forall a. a -> [a] -> [a]
:)
      Sem (ModifyGlobally mod : effs) (f x)
comp' <- Sem rInitial x
-> Sem
     (WithTactics (ModifyGlobally mod) f (Sem rInitial) effs)
     (Sem (ModifyGlobally mod : effs) (f x))
forall (m :: * -> *) a (e :: Effect) (f :: * -> *)
       (r :: EffectRow).
m a -> Sem (WithTactics e f m r) (Sem (e : r) (f a))
runT Sem rInitial x
comp
      f x
res <- Sem effs (f x)
-> Sem
     (WithTactics (ModifyGlobally mod) f (Sem rInitial) effs) (f x)
forall (e :: Effect) (r :: EffectRow) a. Sem r a -> Sem (e : r) a
raise (Sem effs (f x)
 -> Sem
      (WithTactics (ModifyGlobally mod) f (Sem rInitial) effs) (f x))
-> Sem effs (f x)
-> Sem
     (WithTactics (ModifyGlobally mod) f (Sem rInitial) effs) (f x)
forall a b. (a -> b) -> a -> b
$ Sem (ModifyGlobally mod : effs) (f x) -> Sem effs (f x)
forall mod (effs :: EffectRow) a.
Members '[State [Ltl mod], NonDet] effs =>
Sem (ModifyGlobally mod : effs) a -> Sem effs a
runModifyGlobally Sem (ModifyGlobally mod : effs) (f x)
comp'
      [Ltl mod]
formulas <- Sem
  (WithTactics (ModifyGlobally mod) f (Sem rInitial) effs) [Ltl mod]
forall s (r :: EffectRow). Member (State s) r => Sem r s
get
      Bool
-> Sem (WithTactics (ModifyGlobally mod) f (Sem rInitial) effs) ()
-> Sem (WithTactics (ModifyGlobally mod) f (Sem rInitial) effs) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Ltl mod] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ltl mod]
formulas) (Sem (WithTactics (ModifyGlobally mod) f (Sem rInitial) effs) ()
 -> Sem (WithTactics (ModifyGlobally mod) f (Sem rInitial) effs) ())
-> Sem (WithTactics (ModifyGlobally mod) f (Sem rInitial) effs) ()
-> Sem (WithTactics (ModifyGlobally mod) f (Sem rInitial) effs) ()
forall a b. (a -> b) -> a -> b
$ do
        Bool
-> Sem (WithTactics (ModifyGlobally mod) f (Sem rInitial) effs) ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Ltl mod -> Bool
forall a. Ltl a -> Bool
finished ([Ltl mod] -> Ltl mod
forall a. HasCallStack => [a] -> a
head [Ltl mod]
formulas))
        [Ltl mod]
-> Sem (WithTactics (ModifyGlobally mod) f (Sem rInitial) effs) ()
forall s (r :: EffectRow). Member (State s) r => s -> Sem r ()
put ([Ltl mod] -> [Ltl mod]
forall a. HasCallStack => [a] -> [a]
tail [Ltl mod]
formulas)
      f x
-> Sem
     (WithTactics (ModifyGlobally mod) f (Sem rInitial) effs) (f x)
forall a.
a -> Sem (WithTactics (ModifyGlobally mod) f (Sem rInitial) effs) a
forall (m :: * -> *) a. Monad m => a -> m a
return f x
res

-- | An effect to request and consume the list of requirements that should be
-- enforced at the current time step.
data ModifyLocally a :: Effect where
  GetRequirements :: ModifyLocally a m [Requirement a]

makeSem_ ''ModifyLocally

-- | Reads and consumes a modification from the context, typically laid out by
-- `ModifyGlobally` further up the stack of effects.
getRequirements :: (Member (ModifyLocally a) effs) => Sem effs [Requirement a]

-- | Running the `ModifyLocally` effect requires to have access to the current
-- list of `Ltl` formulas, and to be able to branch.
--
-- The function `nowLaterList` is invoked to fetch the various paths implied by
-- the current formulas, and a branching is performed to explore all of
-- them. The new formulas for next steps are stored, and each path is given the
-- requirements to enforce at the current time step.
runModifyLocally ::
  forall modification effs a.
  ( Members
      '[ State [Ltl modification],
         NonDet
       ]
      effs
  ) =>
  Sem (ModifyLocally modification : effs) a ->
  Sem effs a
runModifyLocally :: forall modification (effs :: EffectRow) a.
Members '[State [Ltl modification], NonDet] effs =>
Sem (ModifyLocally modification : effs) a -> Sem effs a
runModifyLocally =
  (forall (rInitial :: EffectRow) x.
 ModifyLocally modification (Sem rInitial) x -> Sem effs x)
-> Sem (ModifyLocally modification : effs) a -> Sem effs a
forall (e :: Effect) (r :: EffectRow) a.
FirstOrder e "interpret" =>
(forall (rInitial :: EffectRow) x. e (Sem rInitial) x -> Sem r x)
-> Sem (e : r) a -> Sem r a
interpret ((forall (rInitial :: EffectRow) x.
  ModifyLocally modification (Sem rInitial) x -> Sem effs x)
 -> Sem (ModifyLocally modification : effs) a -> Sem effs a)
-> (forall (rInitial :: EffectRow) x.
    ModifyLocally modification (Sem rInitial) x -> Sem effs x)
-> Sem (ModifyLocally modification : effs) a
-> Sem effs a
forall a b. (a -> b) -> a -> b
$ \ModifyLocally modification (Sem rInitial) x
GetRequirements -> do
    [([Requirement modification], [Ltl modification])]
modifications <- ([Ltl modification]
 -> [([Requirement modification], [Ltl modification])])
-> Sem effs [([Requirement modification], [Ltl modification])]
forall s a (r :: EffectRow).
Member (State s) r =>
(s -> a) -> Sem r a
gets [Ltl modification]
-> [([Requirement modification], [Ltl modification])]
forall a. [Ltl a] -> [([Requirement a], [Ltl a])]
nowLaterList
    [Sem effs x] -> Sem effs x
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ([Sem effs x] -> Sem effs x)
-> ((([Requirement modification], [Ltl modification])
     -> Sem effs x)
    -> [Sem effs x])
-> (([Requirement modification], [Ltl modification]) -> Sem effs x)
-> Sem effs x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([([Requirement modification], [Ltl modification])]
modifications [([Requirement modification], [Ltl modification])]
-> (([Requirement modification], [Ltl modification]) -> Sem effs x)
-> [Sem effs x]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>) ((([Requirement modification], [Ltl modification]) -> Sem effs x)
 -> Sem effs x)
-> (([Requirement modification], [Ltl modification]) -> Sem effs x)
-> Sem effs x
forall a b. (a -> b) -> a -> b
$ \([Requirement modification]
now, [Ltl modification]
later) -> [Ltl modification] -> Sem effs ()
forall s (r :: EffectRow). Member (State s) r => s -> Sem r ()
put [Ltl modification]
later Sem effs () -> Sem effs x -> Sem effs x
forall a b. Sem effs a -> Sem effs b -> Sem effs b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> x -> Sem effs x
forall a. a -> Sem effs a
forall (m :: * -> *) a. Monad m => a -> m a
return x
[Requirement modification]
now