-- | 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. This is to be
-- replaced later on with a dependency to https://github.com/tweag/graft.
module Cooked.Ltl
  ( Ltl (..),
    nowLater,
    nowLaterList,
    LtlOp (..),
    Staged (..),
    interpLtl,
    interpLtlAndPruneUnfinished,
    InterpLtl (..),
    MonadModal (..),
  )
where

import Control.Monad
import Control.Monad.State
import Data.Kind

-- * LTL formulas and operations on them

-- | 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 modifications. Since it does not make (obvious) sense to talk of a
-- negated modification or of one modification (possibly in the future) to imply
-- another modification, implication and negation are absent.
data Ltl a
  = -- | The "do nothing" modification that never fails
    LtlTruth
  | -- | The modification that never applies (i.e. always fails)
    LtlFalsity
  | -- | The modification that applies a given atomic modification at the
    -- | current time step
    LtlAtom 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.
    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 eventually. The formulas
    --
    -- > a `LtlUntil` b
    -- and
    -- > b `LtlOr` (a `LtlAnd` LtlNext (a `LtlUntil` b))
    --
    -- are equivalent.
    LtlUntil (Ltl a) (Ltl a)
  | -- | Assert that the second formula has to be true up to and including the
    -- point when the first one becomes true; if that never happens, the second
    -- formula has to remain true forever. View this as dual to 'LtlUntil'. The
    -- formulas
    --
    -- > a `LtlRelease` b
    -- and
    -- > b `LtlAnd` (a `LtlOr` LtlNext (a `LtlRelease` b))
    --
    -- are equivalent.
    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)

-- | Split an LTL formula that describes a modification of a computation into a
-- list of @(doNow, doLater)@ pairs, where
--
-- * @doNow@ is the modification to be applied to the current time step,
--
-- * @doLater@ is an LTL formula describing the modification that should be
--   applied from the next time step onwards, and
--
-- 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.
--
-- Modifications should form a 'Monoid', where 'mempty' is the do-nothing
-- modification, and '<>' is the composition of modifications. We interpret @a
-- <> b@ as the modification that first applies @b@ and then @a@. Attention:
-- Since we use '<>' to define conjunction, if '<>' is not commutative,
-- conjunction will also fail to be commutative!
nowLater :: (Monoid a) => Ltl a -> [(a, Ltl a)]
nowLater :: forall a. Monoid a => Ltl a -> [(a, Ltl a)]
nowLater Ltl a
LtlTruth = [(a
forall a. Monoid a => a
mempty, Ltl a
forall a. Ltl a
LtlTruth)]
nowLater Ltl a
LtlFalsity = []
nowLater (LtlAtom a
g) = [(a
g, Ltl a
forall a. Ltl a
LtlTruth)]
nowLater (Ltl a
a `LtlOr` Ltl a
b) = Ltl a -> [(a, Ltl a)]
forall a. Monoid a => Ltl a -> [(a, Ltl a)]
nowLater Ltl a
a [(a, Ltl a)] -> [(a, Ltl a)] -> [(a, Ltl a)]
forall a. [a] -> [a] -> [a]
++ Ltl a -> [(a, Ltl a)]
forall a. Monoid a => Ltl a -> [(a, Ltl a)]
nowLater Ltl a
b
nowLater (Ltl a
a `LtlAnd` Ltl a
b) =
  [ (a
f a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
g, 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
c Ltl a -> Ltl a -> Ltl a
forall a. Ltl a -> Ltl a -> Ltl a
`LtlAnd` Ltl a
d)
    | (a
f, Ltl a
c) <- Ltl a -> [(a, Ltl a)]
forall a. Monoid a => Ltl a -> [(a, Ltl a)]
nowLater Ltl a
a,
      (a
g, Ltl a
d) <- Ltl a -> [(a, Ltl a)]
forall a. Monoid a => Ltl a -> [(a, Ltl a)]
nowLater Ltl a
b
  ]
nowLater (LtlNext Ltl a
a) = [(a
forall a. Monoid a => a
mempty, Ltl a
a)]
nowLater (Ltl a
a `LtlUntil` Ltl a
b) =
  Ltl a -> [(a, Ltl a)]
forall a. Monoid a => Ltl a -> [(a, Ltl a)]
nowLater (Ltl a -> [(a, Ltl a)]) -> Ltl a -> [(a, Ltl a)]
forall a b. (a -> b) -> a -> b
$ Ltl a
b Ltl a -> Ltl a -> Ltl a
forall a. Ltl a -> Ltl a -> Ltl a
`LtlOr` (Ltl a
a 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
a Ltl a -> Ltl a -> Ltl a
forall a. Ltl a -> Ltl a -> Ltl a
`LtlUntil` Ltl a
b))
nowLater (Ltl a
a `LtlRelease` Ltl a
b) =
  Ltl a -> [(a, Ltl a)]
forall a. Monoid a => Ltl a -> [(a, Ltl a)]
nowLater (Ltl a -> [(a, Ltl a)]) -> Ltl a -> [(a, Ltl a)]
forall a b. (a -> b) -> a -> b
$ Ltl a
b Ltl a -> Ltl a -> Ltl a
forall a. Ltl a -> Ltl a -> Ltl a
`LtlAnd` (Ltl a
a 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
a Ltl a -> Ltl a -> Ltl a
forall a. Ltl a -> Ltl a -> Ltl a
`LtlRelease` Ltl a
b))

-- | 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 --  we want falsity to fail always, even on the empty computation
finished (LtlAtom a
_) = Bool
False
finished (Ltl a
a `LtlAnd` Ltl a
b) = Ltl a -> Bool
forall a. Ltl a -> Bool
finished Ltl a
a Bool -> Bool -> Bool
&& Ltl a -> Bool
forall a. Ltl a -> Bool
finished Ltl a
b
finished (Ltl a
a `LtlOr` Ltl a
b) = Ltl a -> Bool
forall a. Ltl a -> Bool
finished Ltl a
a Bool -> Bool -> Bool
|| Ltl a -> Bool
forall a. Ltl a -> Bool
finished Ltl a
b
finished (LtlNext Ltl a
_) = Bool
False
finished (LtlUntil Ltl a
_ Ltl a
_) = Bool
False
finished (LtlRelease Ltl a
_ Ltl a
_) = Bool
True

-- | Say we're passing around more than one formula from each time step to the
-- next, where the intended meaning of a list of formulas is the modification
-- that applies the first formula in the list first, then the second formula,
-- then the third and so on. We'd still like to compute a list of @(doNow,
-- doLater)@ pairs as in 'nowLater', only that the @doLater@ should again be a
-- list of formulas.
nowLaterList :: (Monoid a) => [Ltl a] -> [(a, [Ltl a])]
nowLaterList :: forall a. Monoid a => [Ltl a] -> [(a, [Ltl a])]
nowLaterList = [[(a, Ltl a)]] -> [(a, [Ltl a])]
forall {a} {a}. Monoid a => [[(a, a)]] -> [(a, [a])]
joinNowLaters ([[(a, Ltl a)]] -> [(a, [Ltl a])])
-> ([Ltl a] -> [[(a, Ltl a)]]) -> [Ltl a] -> [(a, [Ltl a])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Ltl a -> [(a, Ltl a)]) -> [Ltl a] -> [[(a, Ltl a)]]
forall a b. (a -> b) -> [a] -> [b]
map Ltl a -> [(a, Ltl a)]
forall a. Monoid a => Ltl a -> [(a, Ltl a)]
nowLater
  where
    joinNowLaters :: [[(a, a)]] -> [(a, [a])]
joinNowLaters [] = [(a
forall a. Monoid a => a
mempty, [])]
    joinNowLaters ([(a, a)]
l : [[(a, a)]]
ls) =
      [ (a
g a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
f, a
c a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
cs)
        | (a
f, a
c) <- [(a, a)]
l,
          (a
g, [a]
cs) <- [[(a, a)]] -> [(a, [a])]
joinNowLaters [[(a, a)]]
ls
      ]

-- | Straightforward simplification procedure for LTL formulas. This function
-- knows how 'LtlTruth' and 'LtlFalsity' play with conjunction and disjunction
-- and recursively applies this knowledge; it does not do anything "fancy" like
-- computing a normal form and is only used to keep the formulas 'nowLater'
-- generates from growing too wildly.
ltlSimpl :: Ltl a -> Ltl a
ltlSimpl :: forall a. Ltl a -> Ltl a
ltlSimpl Ltl a
expr =
  let (Ltl a
expr', Bool
progress) = Ltl a -> (Ltl a, Bool)
forall a. Ltl a -> (Ltl a, Bool)
simpl Ltl a
expr
   in if Bool
progress then Ltl a
expr' else Ltl a
expr
  where
    simpl :: Ltl a -> (Ltl a, Bool)
    simpl :: forall a. Ltl a -> (Ltl a, Bool)
simpl (LtlAnd Ltl a
a Ltl a
b) = Ltl a -> Ltl a -> (Ltl a, Bool)
forall a. Ltl a -> Ltl a -> (Ltl a, Bool)
simplAnd Ltl a
a Ltl a
b
    simpl (LtlOr Ltl a
a Ltl a
b) = Ltl a -> Ltl a -> (Ltl a, Bool)
forall a. Ltl a -> Ltl a -> (Ltl a, Bool)
simplOr Ltl a
a Ltl a
b
    simpl (LtlNext Ltl a
a) =
      let (Ltl a
a', Bool
pa) = Ltl a -> (Ltl a, Bool)
forall a. Ltl a -> (Ltl a, Bool)
simpl Ltl a
a
       in if Bool
pa
            then (Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
LtlNext Ltl a
a', Bool
True)
            else (Ltl a -> Ltl a
forall a. Ltl a -> Ltl a
LtlNext Ltl a
a, Bool
False)
    simpl (LtlUntil Ltl a
a Ltl a
b) = (Ltl a -> Ltl a -> Ltl a) -> Ltl a -> Ltl a -> (Ltl a, Bool)
forall a.
(Ltl a -> Ltl a -> Ltl a) -> Ltl a -> Ltl a -> (Ltl a, Bool)
recurse2 Ltl a -> Ltl a -> Ltl a
forall a. Ltl a -> Ltl a -> Ltl a
LtlUntil Ltl a
a Ltl a
b
    simpl (LtlRelease Ltl a
a Ltl a
b) = (Ltl a -> Ltl a -> Ltl a) -> Ltl a -> Ltl a -> (Ltl a, Bool)
forall a.
(Ltl a -> Ltl a -> Ltl a) -> Ltl a -> Ltl a -> (Ltl a, Bool)
recurse2 Ltl a -> Ltl a -> Ltl a
forall a. Ltl a -> Ltl a -> Ltl a
LtlRelease Ltl a
a Ltl a
b
    simpl Ltl a
x = (Ltl a
x, Bool
False)

    simplAnd :: Ltl a -> Ltl a -> (Ltl a, Bool)
    simplAnd :: forall a. Ltl a -> Ltl a -> (Ltl a, Bool)
simplAnd Ltl a
a Ltl a
b =
      let (Ltl a
a', Bool
pa) = Ltl a -> (Ltl a, Bool)
forall a. Ltl a -> (Ltl a, Bool)
simpl Ltl a
a
          (Ltl a
b', Bool
pb) = Ltl a -> (Ltl a, Bool)
forall a. Ltl a -> (Ltl a, Bool)
simpl Ltl a
b
       in case (Ltl a
a', Ltl a
b') of
            (Ltl a
LtlTruth, Ltl a
_) -> (Ltl a
b', Bool
True)
            (Ltl a
_, Ltl a
LtlTruth) -> (Ltl a
a', Bool
True)
            (Ltl a
LtlFalsity, Ltl a
_) -> (Ltl a
forall a. Ltl a
LtlFalsity, Bool
True)
            (Ltl a
_, Ltl a
LtlFalsity) -> (Ltl a
forall a. Ltl a
LtlFalsity, Bool
True)
            (Ltl a, Ltl a)
_ -> if Bool
pa Bool -> Bool -> Bool
|| Bool
pb then (Ltl a -> Ltl a -> Ltl a
forall a. Ltl a -> Ltl a -> Ltl a
LtlAnd Ltl a
a' Ltl a
b', Bool
True) else (Ltl a -> Ltl a -> Ltl a
forall a. Ltl a -> Ltl a -> Ltl a
LtlAnd Ltl a
a Ltl a
b, Bool
False)

    simplOr :: Ltl a -> Ltl a -> (Ltl a, Bool)
    simplOr :: forall a. Ltl a -> Ltl a -> (Ltl a, Bool)
simplOr Ltl a
a Ltl a
b =
      let (Ltl a
a', Bool
pa) = Ltl a -> (Ltl a, Bool)
forall a. Ltl a -> (Ltl a, Bool)
simpl Ltl a
a
          (Ltl a
b', Bool
pb) = Ltl a -> (Ltl a, Bool)
forall a. Ltl a -> (Ltl a, Bool)
simpl Ltl a
b
       in case (Ltl a
a', Ltl a
b') of
            (Ltl a
LtlTruth, Ltl a
_) -> (Ltl a
forall a. Ltl a
LtlTruth, Bool
True)
            (Ltl a
_, Ltl a
LtlTruth) -> (Ltl a
forall a. Ltl a
LtlTruth, Bool
True)
            (Ltl a
LtlFalsity, Ltl a
_) -> (Ltl a
b', Bool
True)
            (Ltl a
_, Ltl a
LtlFalsity) -> (Ltl a
a', Bool
True)
            (Ltl a, Ltl a)
_ -> if Bool
pa Bool -> Bool -> Bool
|| Bool
pb then (Ltl a -> Ltl a -> Ltl a
forall a. Ltl a -> Ltl a -> Ltl a
LtlOr Ltl a
a' Ltl a
b', Bool
True) else (Ltl a -> Ltl a -> Ltl a
forall a. Ltl a -> Ltl a -> Ltl a
LtlOr Ltl a
a Ltl a
b, Bool
False)

    recurse2 ::
      (Ltl a -> Ltl a -> Ltl a) ->
      Ltl a ->
      Ltl a ->
      (Ltl a, Bool)
    recurse2 :: forall a.
(Ltl a -> Ltl a -> Ltl a) -> Ltl a -> Ltl a -> (Ltl a, Bool)
recurse2 Ltl a -> Ltl a -> Ltl a
f Ltl a
a Ltl a
b =
      let (Ltl a
a', Bool
pa) = Ltl a -> (Ltl a, Bool)
forall a. Ltl a -> (Ltl a, Bool)
simpl Ltl a
a
          (Ltl a
b', Bool
pb) = Ltl a -> (Ltl a, Bool)
forall a. Ltl a -> (Ltl a, Bool)
simpl Ltl a
b
       in if Bool
pa Bool -> Bool -> Bool
|| Bool
pb
            then (Ltl a -> Ltl a -> Ltl a
f Ltl a
a' Ltl a
b', Bool
True)
            else (Ltl a -> Ltl a -> Ltl a
f Ltl a
a Ltl a
b, Bool
False)

-- * An AST for "reified computations"

-- | The idea is that a value of type @Staged (LtlOp modification builtin) a@
-- describes a set of (monadic) computations that return an @a@ such that
--
-- * every step of the computations that returns a @b@ is reified as a @builtin
--   b@, and
--
-- * every step can be modified by a @modification@.

-- | Operations for computations that can be modified using LTL formulas.
data LtlOp (modification :: Type) (builtin :: Type -> Type) :: Type -> Type where
  -- | The operation that introduces a new LTL formula that should be used to
  -- modify the following computations. Think of this operation as coming
  -- between time steps and adding a new formula to be applied before all of the
  -- formulas that should already be applied to the next time step.
  StartLtl :: Ltl modification -> LtlOp modification builtin ()
  -- | The operation that removes the last LTL formula that was introduced. If
  -- the formula is not yet finished, the current time line will fail.
  StopLtl :: LtlOp modification builtin ()
  Builtin :: builtin a -> LtlOp modification builtin a

-- | The freer monad on @op@. We think of this as the AST of a computation with
-- operations of types @op a@.
data Staged (op :: Type -> Type) :: Type -> Type where
  Return :: a -> Staged op a
  Instr :: op a -> (a -> Staged op b) -> Staged op b

instance Functor (Staged op) where
  fmap :: forall a b. (a -> b) -> Staged op a -> Staged op b
fmap a -> b
f (Return a
x) = b -> Staged op b
forall a (op :: * -> *). a -> Staged op a
Return (b -> Staged op b) -> b -> Staged op b
forall a b. (a -> b) -> a -> b
$ a -> b
f a
x
  fmap a -> b
f (Instr op a
op a -> Staged op a
cont) = op a -> (a -> Staged op b) -> Staged op b
forall (op :: * -> *) a b.
op a -> (a -> Staged op b) -> Staged op b
Instr op a
op ((a -> b) -> Staged op a -> Staged op b
forall a b. (a -> b) -> Staged op a -> Staged op b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f (Staged op a -> Staged op b)
-> (a -> Staged op a) -> a -> Staged op b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Staged op a
cont)

instance Applicative (Staged op) where
  pure :: forall a. a -> Staged op a
pure = a -> Staged op a
forall a (op :: * -> *). a -> Staged op a
Return
  <*> :: forall a b. Staged op (a -> b) -> Staged op a -> Staged op b
(<*>) = Staged op (a -> b) -> Staged op a -> Staged op b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance Monad (Staged op) where
  (Return a
x) >>= :: forall a b. Staged op a -> (a -> Staged op b) -> Staged op b
>>= a -> Staged op b
f = a -> Staged op b
f a
x
  (Instr op a
i a -> Staged op a
m) >>= a -> Staged op b
f = op a -> (a -> Staged op b) -> Staged op b
forall (op :: * -> *) a b.
op a -> (a -> Staged op b) -> Staged op b
Instr op a
i (a -> Staged op a
m (a -> Staged op a) -> (a -> Staged op b) -> a -> Staged op b
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> a -> Staged op b
f)

-- * Interpreting the AST

-- | To be a suitable semantic domain for computations modified by LTL formulas,
-- a monad @m@ has to
--
-- * have the right @builtin@ functions, which can be modified by the right
--   @modification@s,
--
-- * be a 'MonadPlus', because one LTL formula might yield different modified
--   versions of the computation, and
--
-- This type class only requires from the user to specify how to interpret the
-- (modified) builtins. In order to do so, it passes around the formulas that
-- are to be applied to the next time step in a @StateT@. A common idiom to
-- modify an operation should be this:
--
-- > interpBuiltin op =
-- >  get
-- >    >>= msum
-- >      . map (\(now, later) -> applyModification now op <* put later)
-- >      . nowLaterList
--
-- (But to write this, @modification@ has to be a 'Monoid' to make
-- 'nowLaterList' work!) Look at the tests for this module and at
-- "Cooked.MockChain.Monad.Staged" for examples of how to use this type class.
class (MonadPlus m) => InterpLtl modification builtin m where
  interpBuiltin :: builtin a -> StateT [Ltl modification] m a

-- | Interpret a 'Staged' computation into a suitable domain, using the function
-- 'interpBuiltin' to interpret the builtins.
interpLtl ::
  (InterpLtl modification builtin m) =>
  Staged (LtlOp modification builtin) a ->
  StateT [Ltl modification] m a
interpLtl :: forall modification (builtin :: * -> *) (m :: * -> *) a.
InterpLtl modification builtin m =>
Staged (LtlOp modification builtin) a
-> StateT [Ltl modification] m a
interpLtl (Return a
a) = a -> StateT [Ltl modification] m a
forall a. a -> StateT [Ltl modification] m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a
interpLtl (Instr (StartLtl Ltl modification
x) a -> Staged (LtlOp modification builtin) a
f) = StateT [Ltl modification] m [Ltl modification]
forall s (m :: * -> *). MonadState s m => m s
get StateT [Ltl modification] m [Ltl modification]
-> ([Ltl modification] -> StateT [Ltl modification] m ())
-> StateT [Ltl modification] m ()
forall a b.
StateT [Ltl modification] m a
-> (a -> StateT [Ltl modification] m b)
-> StateT [Ltl modification] m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [Ltl modification] -> StateT [Ltl modification] m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ([Ltl modification] -> StateT [Ltl modification] m ())
-> ([Ltl modification] -> [Ltl modification])
-> [Ltl modification]
-> StateT [Ltl modification] m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Ltl modification
x Ltl modification -> [Ltl modification] -> [Ltl modification]
forall a. a -> [a] -> [a]
:) StateT [Ltl modification] m ()
-> (() -> StateT [Ltl modification] m a)
-> StateT [Ltl modification] m a
forall a b.
StateT [Ltl modification] m a
-> (a -> StateT [Ltl modification] m b)
-> StateT [Ltl modification] m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Staged (LtlOp modification builtin) a
-> StateT [Ltl modification] m a
forall modification (builtin :: * -> *) (m :: * -> *) a.
InterpLtl modification builtin m =>
Staged (LtlOp modification builtin) a
-> StateT [Ltl modification] m a
interpLtl (Staged (LtlOp modification builtin) a
 -> StateT [Ltl modification] m a)
-> (() -> Staged (LtlOp modification builtin) a)
-> ()
-> StateT [Ltl modification] m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Staged (LtlOp modification builtin) a
() -> Staged (LtlOp modification builtin) a
f
interpLtl (Instr LtlOp modification builtin a
StopLtl a -> Staged (LtlOp modification builtin) a
f) = do
  [Ltl modification]
xs <- StateT [Ltl modification] m [Ltl modification]
forall s (m :: * -> *). MonadState s m => m s
get
  case [Ltl modification]
xs of
    [] -> String -> StateT [Ltl modification] m a
forall a. HasCallStack => String -> a
error String
"You called 'StopLtl' before 'StartLtl'. This is only possible if you're using internals."
    Ltl modification
x : [Ltl modification]
rest ->
      if Ltl modification -> Bool
forall a. Ltl a -> Bool
finished Ltl modification
x
        then do
          [Ltl modification] -> StateT [Ltl modification] m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put [Ltl modification]
rest
          Staged (LtlOp modification builtin) a
-> StateT [Ltl modification] m a
forall modification (builtin :: * -> *) (m :: * -> *) a.
InterpLtl modification builtin m =>
Staged (LtlOp modification builtin) a
-> StateT [Ltl modification] m a
interpLtl (Staged (LtlOp modification builtin) a
 -> StateT [Ltl modification] m a)
-> Staged (LtlOp modification builtin) a
-> StateT [Ltl modification] m a
forall a b. (a -> b) -> a -> b
$ a -> Staged (LtlOp modification builtin) a
f ()
        else StateT [Ltl modification] m a
forall a. StateT [Ltl modification] m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
interpLtl (Instr (Builtin builtin a
b) a -> Staged (LtlOp modification builtin) a
f) = builtin a -> StateT [Ltl modification] m a
forall a. builtin a -> StateT [Ltl modification] m a
forall modification (builtin :: * -> *) (m :: * -> *) a.
InterpLtl modification builtin m =>
builtin a -> StateT [Ltl modification] m a
interpBuiltin builtin a
b StateT [Ltl modification] m a
-> (a -> StateT [Ltl modification] m a)
-> StateT [Ltl modification] m a
forall a b.
StateT [Ltl modification] m a
-> (a -> StateT [Ltl modification] m b)
-> StateT [Ltl modification] m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Staged (LtlOp modification builtin) a
-> StateT [Ltl modification] m a
forall modification (builtin :: * -> *) (m :: * -> *) a.
InterpLtl modification builtin m =>
Staged (LtlOp modification builtin) a
-> StateT [Ltl modification] m a
interpLtl (Staged (LtlOp modification builtin) a
 -> StateT [Ltl modification] m a)
-> (a -> Staged (LtlOp modification builtin) a)
-> a
-> StateT [Ltl modification] m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Staged (LtlOp modification builtin) a
f

-- | Interpret a 'Staged' computation into a suitable domain, using the function
-- 'interpBuiltin' to interpret the builtins. At the end of the computation,
-- prune branches that still have unfinished modifications applied to them.  See
-- the discussion on the regression test case for PRs 110 and 131 in
-- 'StagedSpec.hs' for a discussion on why this function has to exist.
interpLtlAndPruneUnfinished ::
  (InterpLtl modification builtin m) =>
  Staged (LtlOp modification builtin) a ->
  StateT [Ltl modification] m a
interpLtlAndPruneUnfinished :: forall modification (builtin :: * -> *) (m :: * -> *) a.
InterpLtl modification builtin m =>
Staged (LtlOp modification builtin) a
-> StateT [Ltl modification] m a
interpLtlAndPruneUnfinished Staged (LtlOp modification builtin) a
f = do
  a
res <- Staged (LtlOp modification builtin) a
-> StateT [Ltl modification] m a
forall modification (builtin :: * -> *) (m :: * -> *) a.
InterpLtl modification builtin m =>
Staged (LtlOp modification builtin) a
-> StateT [Ltl modification] m a
interpLtl Staged (LtlOp modification builtin) a
f
  [Ltl modification]
mods <- StateT [Ltl modification] m [Ltl modification]
forall s (m :: * -> *). MonadState s m => m s
get
  if (Ltl modification -> Bool) -> [Ltl modification] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Ltl modification -> Bool
forall a. Ltl a -> Bool
finished [Ltl modification]
mods then 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 else StateT [Ltl modification] m a
forall a. StateT [Ltl modification] m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero

-- * Convenience functions

-- Users of this module should never use 'StartLtl' and 'StopLtl' explicitly.
-- Here are some safe-to-use functions that should be used instead. Most
-- functions like the ones below should be defined for the class 'MonadModal'
-- because there might be other possibilities to equip a monad with LTL
-- modifications beside the method above.

-- | Monads that allow modifications with LTL formulas.
class (Monad m) => MonadModal m where
  type Modification m :: Type
  modifyLtl :: Ltl (Modification m) -> m a -> m a

instance MonadModal (Staged (LtlOp modification builtin)) where
  type Modification (Staged (LtlOp modification builtin)) = modification
  modifyLtl :: forall a.
Ltl (Modification (Staged (LtlOp modification builtin)))
-> Staged (LtlOp modification builtin) a
-> Staged (LtlOp modification builtin) a
modifyLtl Ltl (Modification (Staged (LtlOp modification builtin)))
x Staged (LtlOp modification builtin) a
tr = LtlOp modification builtin ()
-> (() -> Staged (LtlOp modification builtin) ())
-> Staged (LtlOp modification builtin) ()
forall (op :: * -> *) a b.
op a -> (a -> Staged op b) -> Staged op b
Instr (Ltl modification -> LtlOp modification builtin ()
forall modification (builtin :: * -> *).
Ltl modification -> LtlOp modification builtin ()
StartLtl Ltl modification
Ltl (Modification (Staged (LtlOp modification builtin)))
x) () -> Staged (LtlOp modification builtin) ()
forall a (op :: * -> *). a -> Staged op a
Return Staged (LtlOp modification builtin) ()
-> Staged (LtlOp modification builtin) a
-> Staged (LtlOp modification builtin) a
forall a b.
Staged (LtlOp modification builtin) a
-> Staged (LtlOp modification builtin) b
-> Staged (LtlOp modification builtin) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Staged (LtlOp modification builtin) a
tr Staged (LtlOp modification builtin) a
-> (a -> Staged (LtlOp modification builtin) a)
-> Staged (LtlOp modification builtin) a
forall a b.
Staged (LtlOp modification builtin) a
-> (a -> Staged (LtlOp modification builtin) b)
-> Staged (LtlOp modification builtin) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
res -> LtlOp modification builtin ()
-> (() -> Staged (LtlOp modification builtin) ())
-> Staged (LtlOp modification builtin) ()
forall (op :: * -> *) a b.
op a -> (a -> Staged op b) -> Staged op b
Instr LtlOp modification builtin ()
forall modification (builtin :: * -> *).
LtlOp modification builtin ()
StopLtl () -> Staged (LtlOp modification builtin) ()
forall a (op :: * -> *). a -> Staged op a
Return Staged (LtlOp modification builtin) ()
-> Staged (LtlOp modification builtin) a
-> Staged (LtlOp modification builtin) a
forall a b.
Staged (LtlOp modification builtin) a
-> Staged (LtlOp modification builtin) b
-> Staged (LtlOp modification builtin) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> a -> Staged (LtlOp modification builtin) a
forall a. a -> Staged (LtlOp modification builtin) a
forall (m :: * -> *) a. Monad m => a -> m a
return a
res