module Cooked.Ltl
( Ltl (..),
nowLater,
nowLaterList,
LtlOp (..),
Staged (..),
interpLtl,
interpLtlAndPruneUnfinished,
InterpLtl (..),
MonadModal (..),
)
where
import Control.Monad
import Control.Monad.State
import Data.Kind
data Ltl a
=
LtlTruth
|
LtlFalsity
|
LtlAtom a
|
LtlOr (Ltl a) (Ltl a)
|
LtlAnd (Ltl a) (Ltl a)
|
LtlNext (Ltl a)
|
LtlUntil (Ltl a) (Ltl a)
|
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)
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))
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 (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
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
]
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)
data LtlOp (modification :: Type) (builtin :: Type -> Type) :: Type -> Type where
StartLtl :: Ltl modification -> LtlOp modification builtin ()
StopLtl :: LtlOp modification builtin ()
Builtin :: builtin a -> LtlOp modification builtin 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)
class (MonadPlus m) => InterpLtl modification builtin m where
interpBuiltin :: builtin a -> StateT [Ltl modification] m a
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
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
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