{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- | Generate state-aware modifications of sequences of stateful actions. The
-- approach is to use an LTL-inspired language to build /composite/
-- modifications that apply /atomic/ modifications to specific steps. Each
-- atomic modification's applicability and parameters may depend on the state
-- reached so far, and there will be zero or more possibilities to apply each
-- composite modification.
--
-- The workflow is to
--
-- - write effect types for all actions that you want to apply atomic
--   modifications to,
--
-- - write an abstract type describing your atomic modifications, together with
--   a 'Semigroup' instance that describes how they combine,
--
-- - write instances of 'InterpretLtl' (or 'InterpretLtlHigherOrder' for
--   higher-order effects) that explain how your atomic modifications apply to
--   your effects,
-- Last reply today at 4:00 PM
-- - use 'modifyLtl' to apply composite modifications to your trace, and
--
-- - use 'interpretLtlAST' to run all modified versions of your trace.
--
-- The module "Examples.Ltl.Simple" contains a tutorial.
--
-- For historic context, this is a re-implementation of the "LTL" module from
-- cooked-validators. The version this is based upon is:
-- https://github.com/tweag/cooked-validators/blob/a460c1718d8d21bada510d83b705b24b0f8d36e0/src/Cooked/Ltl.hs
module Logic.Ltl
  ( -- * 'Ltl' formulas
    Ltl (..),
    somewhere,
    everywhere,
    there,

    -- * Deploying 'Ltl' formulas
    LtlAST,
    modifyLtl,

    -- * Higher-order effects
    InterpretLtlHigherOrder (..),
    LtlInterpHigherOrder (..),
    nowLaterList,
    nowLaterSplit,

    -- * Interpreting 'Ltl' modifications
    LtlInstanceKind (..),
    InterpretEffectsLtl (..),
    interpretLtlAST,
    interpretLtlASTWithInitialFormulas,
  )
where

import Control.Arrow
import Control.Monad
import Data.Functor.Const
import Data.Kind
import Effect
import Effect.Internal
import Logic.SingleStep

-- | Type of \"LTL\" formulas. Think of @a@ as a type of atomic
-- \"modifications\", then a value of type @Ltl a@ describes a composite
-- modification that describes where to apply these 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 is always applicable
    LtlTruth
  | -- | The modification that never applies
    LtlFalsity
  | -- | The modification that applies a given atomic modification at the
    -- current step
    LtlAtom a
  | -- | Branch into the \"timeline\" where the left modification is applied
    -- and the one where the right modification is applied. (In a sense, this
    -- is an exclusive or, as we do not introduce the branch where both
    -- modifications are applied.)
    LtlOr (Ltl a) (Ltl a)
  | -- | Apply both the left and the right modification. Attention: The \"apply
    -- both\" operation for  atomic modifications of type @a@ will be
    -- user-defined through a @'Semigroup'@ instance. If that operation
    -- isn't commutative, this conjunction may also fail to be commutative.
    LtlAnd (Ltl a) (Ltl a)
  | -- | Apply the given modification at the next step.
    LtlNext (Ltl a)
  | -- | Apply the first modification at least until the second one begins to
    -- be applicable (and is applied), 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)
  | -- | Apply the second modification up to and including the step when the
    -- first one becomes applicable (and is applied); if that never happens,
    -- the second formula will be applied forever. View this as a 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)

-- | Apply an atomic modification to some action.
somewhere :: a -> Ltl a
somewhere :: forall a. a -> Ltl a
somewhere a
a = Ltl a
forall a. Ltl a
LtlTruth Ltl a -> Ltl a -> Ltl a
forall a. Ltl a -> Ltl a -> Ltl a
`LtlUntil` a -> Ltl a
forall a. a -> Ltl a
LtlAtom a
a

-- | Apply an atomic modification to all actions.
everywhere :: a -> Ltl a
everywhere :: forall a. a -> Ltl a
everywhere a
a = Ltl a
forall a. Ltl a
LtlFalsity Ltl a -> Ltl a -> Ltl a
forall a. Ltl a -> Ltl a -> Ltl a
`LtlRelease` a -> Ltl a
forall a. a -> Ltl a
LtlAtom a
a

-- | Apply a modification from the n-th step in the trace (0-indexed).
there :: Integer -> Ltl a -> Ltl a
there :: forall a. Integer -> Ltl a -> Ltl a
there Integer
0 = Ltl a -> Ltl a
forall a. a -> a
id
there 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
there (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)

-- | Internal: The effect type corresponding to 'modifyLtl'.
data LtlEffect mod (m :: Type -> Type) a where
  ModifyLtl :: Ltl mod -> m a -> LtlEffect mod m a

-- | An 'AST' that allows modifying parts of its contents with 'Ltl'
-- modifications, using 'modifyLtl'.
type LtlAST mod ops = AST (LtlEffect mod ': ops)

-- | Apply an 'Ltl' modification to an 'LtlAST'. Think of @modifyLtl x acts@ as
-- "try all ways to apply @x@ to the actions given in @acts@".
modifyLtl :: Ltl mod -> LtlAST mod ops a -> LtlAST mod ops a
modifyLtl :: forall mod (ops :: [(* -> *) -> * -> *]) a.
Ltl mod -> LtlAST mod ops a -> LtlAST mod ops a
modifyLtl Ltl mod
x LtlAST mod ops a
acts = LtlEffect mod (AST (LtlEffect mod : ops)) a -> LtlAST mod ops a
forall (op :: (* -> *) -> * -> *) (ops :: [(* -> *) -> * -> *]) a.
EffectInject op ops =>
op (AST ops) a -> AST ops a
astInject (LtlEffect mod (AST (LtlEffect mod : ops)) a -> LtlAST mod ops a)
-> LtlEffect mod (AST (LtlEffect mod : ops)) a -> LtlAST mod ops a
forall a b. (a -> b) -> a -> b
$ Ltl mod
-> LtlAST mod ops a -> LtlEffect mod (AST (LtlEffect mod : ops)) a
forall mod (m :: * -> *) a. Ltl mod -> m a -> LtlEffect mod m a
ModifyLtl Ltl mod
x LtlAST mod ops a
acts

-- | Internal: We pass around a list of 'Ltl' modifications, with the intended
-- meaning that the first formula in the one that was added by the "innermost"
-- 'modifyLtl' (See 'nowLaterList' for how the list modification is applied
-- from step to step). Thus, what we have to do is to add the new formula upon
-- entering the block wrapped by 'ModifyLtl', and check that it's 'finished'
-- upon exiting.
instance
  {-# OVERLAPPING #-}
  (MonadPlus m) =>
  InterpretEffectStateful (Const [Ltl mod]) m (LtlEffect mod)
  where
  interpretEffectStateful :: forall (ops :: [(* -> *) -> * -> *]) x a.
(forall b y.
 Const [Ltl mod] y -> AST ops b -> m (b, Const [Ltl mod] y))
-> Const [Ltl mod] x
-> LtlEffect mod (AST ops) a
-> m (a, Const [Ltl mod] x)
interpretEffectStateful forall b y.
Const [Ltl mod] y -> AST ops b -> m (b, Const [Ltl mod] y)
evalActs Const [Ltl mod] x
ltls (ModifyLtl Ltl mod
ltl AST ops a
acts) = do
    (a
a, Const [Ltl mod]
ltls') <- Const [Ltl mod] Any -> AST ops a -> m (a, Const [Ltl mod] Any)
forall b y.
Const [Ltl mod] y -> AST ops b -> m (b, Const [Ltl mod] y)
evalActs ([Ltl mod] -> Const [Ltl mod] Any
forall {k} a (b :: k). a -> Const a b
Const ([Ltl mod] -> Const [Ltl mod] Any)
-> [Ltl mod] -> Const [Ltl mod] Any
forall a b. (a -> b) -> a -> b
$ Ltl mod
ltl Ltl mod -> [Ltl mod] -> [Ltl mod]
forall a. a -> [a] -> [a]
: Const [Ltl mod] x -> [Ltl mod]
forall {k} a (b :: k). Const a b -> a
getConst Const [Ltl mod] x
ltls) AST ops a
acts
    if Ltl mod -> Bool
forall a. Ltl a -> Bool
finished (Ltl mod -> Bool) -> ([Ltl mod] -> Ltl mod) -> [Ltl mod] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Ltl mod] -> Ltl mod
forall a. HasCallStack => [a] -> a
head ([Ltl mod] -> Bool) -> [Ltl mod] -> Bool
forall a b. (a -> b) -> a -> b
$ [Ltl mod]
ltls'
      then (a, Const [Ltl mod] x) -> m (a, Const [Ltl mod] x)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (a
a, [Ltl mod] -> Const [Ltl mod] x
forall {k} a (b :: k). a -> Const a b
Const ([Ltl mod] -> Const [Ltl mod] x) -> [Ltl mod] -> Const [Ltl mod] x
forall a b. (a -> b) -> a -> b
$ [Ltl mod] -> [Ltl mod]
forall a. HasCallStack => [a] -> [a]
tail [Ltl mod]
ltls')
      else m (a, Const [Ltl mod] x)
forall a. m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero

-- | Explain how to interpret an 'Ltl' modification, in the presence of
-- higher-order effects. The type parameters have the same meaning as for
-- 'InterpretLtl'.
class InterpretLtlHigherOrder (mod :: Type) (m :: Type -> Type) (op :: Effect) where
  -- | Given an operation of type @op a@, there are two possibilities,
  -- corresponding the two constructors of 'LtlInterpHigherOrder'.
  --
  -- For simple operations that don't \"nest\" other 'AST's, use the
  -- 'Direct' constructor. Its meaning corresponds precisely to the
  -- 'interpretMod' function.
  --
  -- For operations that /do/ nest, use the 'Nested' constructor. It needs some
  -- explanation: the stepwise approach based on applying atomic modifications
  -- to single operations breaks down for higher-order operations, since a
  -- single higher-order operation may contain 'AST's of operations. We'll
  -- likely want to use a composite modification while evaluating such nested
  -- 'AST's.
  --
  -- Composite modifications in the current setting are lists of 'Ltl'
  -- formulas, which are evaluated in parallel to the interpretation of the
  -- 'AST'. (Each 'modifyLtl' adds another formula to the head of that list. If
  -- you don't nest 'modifyLtl's, the list will only ever contain one element.
  -- If you nest 'modifyLtl's, the head of the list will be the formula that
  -- was introduced by the innermost 'modifyLtl')
  --
  -- The 'Nested' constructor proposes the following approach: It'll just give
  -- you a function
  --
  -- > evalAST :: forall b. [Ltl mod] -> AST ops b -> m (b, [Ltl mod])
  --
  -- which you can call on the nested 'AST's, which it'll evaluate with the
  -- list of 'Ltl' formulas you provide. To explain it by example, let's use
  -- 'ErrorEffect':
  --
  -- > instance (MonadError e m) => InterpretLtlHigherOrder x m (MonadErrorEffect e) where
  -- >   interpretLtlHigherOrder (CatchError acts handler) =
  -- >     Nested $ \evalAST ltls ->
  -- >       Just
  -- >         <$> catchError
  -- >           (evalAST ltls acts)
  -- >           ( \err ->
  -- >               do
  -- >                 (a, _) <- evalAST [] $ handler err
  -- >                 return (a, ltls)
  -- >           )
  -- >   interpretLtlHigherOrder (ThrowError err) = ...
  --
  -- The equation for 'CatchError' means that you'll interpret the body @acts@
  -- with the composite modification currently in place. If any error is
  -- thrown, you'll run the @handler@, without any modifications at all, and
  -- restore the original composite modification. There might be other ways to
  -- implement this nesting behaviour, depending on your use case, and the
  -- 'Nested' constructor should hopefully be general enough to accommodate
  -- most of them. In particular, you can also return 'Nothing' from the
  -- 'Nested' constructor to signal that with the current composite modification,
  -- the operation can't be evaluated.
  interpretLtlHigherOrder :: op (AST ops) a -> LtlInterpHigherOrder mod m ops a

-- | codomain of 'interpretLtlHigherOrder'. See the explanation there.
data LtlInterpHigherOrder (mod :: Type) (m :: Type -> Type) (ops :: [Effect]) (a :: Type) where
  Direct :: ModInterp mod m a -> LtlInterpHigherOrder mod m ops a
  Nested ::
    ( (forall b. [Ltl mod] -> AST ops b -> m (b, [Ltl mod])) ->
      [Ltl mod] ->
      m (Maybe (a, [Ltl mod]))
    ) ->
    LtlInterpHigherOrder mod m ops a

-- | Used to signify which instance is to be used for a specific effect in the
-- 'InterpretEffectsLtl' class.
data LtlInstanceKind = InterpretModTag | InterpretLtlHigherOrderTag | InterpretEffectStatefulTag

-- | Internal: A reification of the 'InterpretEffectsLtl' constraint. This
-- works, because matching on the constructors will bring the constraint on the
-- constructor in scope. (This is what happens in the function
-- 'interpretJoinedEffectsLtl'.)
data InterpretEffectsLtlConstraintList (mod :: Type) (m :: Type -> Type) (tags :: [LtlInstanceKind]) (ops :: [Effect]) where
  InterpretEffectsLtlNil :: InterpretEffectsLtlConstraintList mod m '[] '[]
  InterpretEffectsLtlFirstorder ::
    (InterpretEffect m op, InterpretMod mod m op) =>
    InterpretEffectsLtlConstraintList mod m tags ops ->
    InterpretEffectsLtlConstraintList mod m (InterpretModTag ': tags) (op ': ops)
  InterpretEffectsLtlHigherorder ::
    (InterpretEffect m op, InterpretLtlHigherOrder mod m op) =>
    InterpretEffectsLtlConstraintList mod m tags ops ->
    InterpretEffectsLtlConstraintList mod m (InterpretLtlHigherOrderTag ': tags) (op ': ops)
  InterpretEffectsLtlEffectStateful ::
    (InterpretEffectStateful (Const [Ltl mod]) m op) =>
    InterpretEffectsLtlConstraintList mod m tags ops ->
    InterpretEffectsLtlConstraintList mod m (InterpretEffectStatefulTag ': tags) (op ': ops)

-- | The constraint used by 'interpretLtlASt' and similar functions. See the documentation there.
--
-- Users of the library will /never/ have to write instances of this class.
class InterpretEffectsLtl (mod :: Type) (m :: Type -> Type) (tags :: [LtlInstanceKind]) (ops :: [Effect]) where
  -- | A witness of the constraint.
  interpretEffectsLtl :: InterpretEffectsLtlConstraintList mod m tags ops

instance InterpretEffectsLtl mod m '[] '[] where
  interpretEffectsLtl :: InterpretEffectsLtlConstraintList mod m '[] '[]
interpretEffectsLtl = InterpretEffectsLtlConstraintList mod m '[] '[]
forall mod (m :: * -> *).
InterpretEffectsLtlConstraintList mod m '[] '[]
InterpretEffectsLtlNil

instance (InterpretEffect m op, InterpretMod mod m op, InterpretEffectsLtl mod m tags ops) => InterpretEffectsLtl mod m (InterpretModTag ': tags) (op ': ops) where
  interpretEffectsLtl :: InterpretEffectsLtlConstraintList
  mod m ('InterpretModTag : tags) (op : ops)
interpretEffectsLtl = InterpretEffectsLtlConstraintList mod m tags ops
-> InterpretEffectsLtlConstraintList
     mod m ('InterpretModTag : tags) (op : ops)
forall (m :: * -> *) (op :: (* -> *) -> * -> *) mod
       (tags :: [LtlInstanceKind]) (ops :: [(* -> *) -> * -> *]).
(InterpretEffect m op, InterpretMod mod m op) =>
InterpretEffectsLtlConstraintList mod m tags ops
-> InterpretEffectsLtlConstraintList
     mod m ('InterpretModTag : tags) (op : ops)
InterpretEffectsLtlFirstorder InterpretEffectsLtlConstraintList mod m tags ops
forall mod (m :: * -> *) (tags :: [LtlInstanceKind])
       (ops :: [(* -> *) -> * -> *]).
InterpretEffectsLtl mod m tags ops =>
InterpretEffectsLtlConstraintList mod m tags ops
interpretEffectsLtl

instance (InterpretEffect m op, InterpretLtlHigherOrder mod m op, InterpretEffectsLtl mod m tags ops) => InterpretEffectsLtl mod m (InterpretLtlHigherOrderTag ': tags) (op ': ops) where
  interpretEffectsLtl :: InterpretEffectsLtlConstraintList
  mod m ('InterpretLtlHigherOrderTag : tags) (op : ops)
interpretEffectsLtl = InterpretEffectsLtlConstraintList mod m tags ops
-> InterpretEffectsLtlConstraintList
     mod m ('InterpretLtlHigherOrderTag : tags) (op : ops)
forall (m :: * -> *) (op :: (* -> *) -> * -> *) mod
       (tags :: [LtlInstanceKind]) (ops :: [(* -> *) -> * -> *]).
(InterpretEffect m op, InterpretLtlHigherOrder mod m op) =>
InterpretEffectsLtlConstraintList mod m tags ops
-> InterpretEffectsLtlConstraintList
     mod m ('InterpretLtlHigherOrderTag : tags) (op : ops)
InterpretEffectsLtlHigherorder InterpretEffectsLtlConstraintList mod m tags ops
forall mod (m :: * -> *) (tags :: [LtlInstanceKind])
       (ops :: [(* -> *) -> * -> *]).
InterpretEffectsLtl mod m tags ops =>
InterpretEffectsLtlConstraintList mod m tags ops
interpretEffectsLtl

instance (InterpretEffectStateful (Const [Ltl mod]) m op, InterpretEffectsLtl mod m tags ops) => InterpretEffectsLtl mod m (InterpretEffectStatefulTag ': tags) (op ': ops) where
  interpretEffectsLtl :: InterpretEffectsLtlConstraintList
  mod m ('InterpretEffectStatefulTag : tags) (op : ops)
interpretEffectsLtl = InterpretEffectsLtlConstraintList mod m tags ops
-> InterpretEffectsLtlConstraintList
     mod m ('InterpretEffectStatefulTag : tags) (op : ops)
forall mod (m :: * -> *) (op :: (* -> *) -> * -> *)
       (tags :: [LtlInstanceKind]) (ops :: [(* -> *) -> * -> *]).
InterpretEffectStateful (Const [Ltl mod]) m op =>
InterpretEffectsLtlConstraintList mod m tags ops
-> InterpretEffectsLtlConstraintList
     mod m ('InterpretEffectStatefulTag : tags) (op : ops)
InterpretEffectsLtlEffectStateful InterpretEffectsLtlConstraintList mod m tags ops
forall mod (m :: * -> *) (tags :: [LtlInstanceKind])
       (ops :: [(* -> *) -> * -> *]).
InterpretEffectsLtl mod m tags ops =>
InterpretEffectsLtlConstraintList mod m tags ops
interpretEffectsLtl

-- | Interpret an 'LtlAST' into a suitable domain.
--
-- Each effect @op@ in the list @ops@ must have one of the following instances:
--
-- - @InterpretLtl mod m op@
--
-- - @InterpretLtlHigherOrder mod m op@
--
-- - @InterpretEffectStateful (Const [Ltl mod]) m op@
--
-- Which instance is expected is declared through the @tags@. Since this type
-- variable is ambiguous, you will have to type-apply this function to a list
-- @tags :: ['LtlInstanceKind']@, which declare, in order, what instance you
-- want to use for the operations in @ops@.
interpretLtlAST ::
  forall tags mod m ops a.
  (Semigroup mod, MonadPlus m, InterpretEffectsLtl mod m tags ops) =>
  LtlAST mod ops a ->
  m a
interpretLtlAST :: forall (tags :: [LtlInstanceKind]) mod (m :: * -> *)
       (ops :: [(* -> *) -> * -> *]) a.
(Semigroup mod, MonadPlus m, InterpretEffectsLtl mod m tags ops) =>
LtlAST mod ops a -> m a
interpretLtlAST = forall (tags :: [LtlInstanceKind]) mod (m :: * -> *)
       (ops :: [(* -> *) -> * -> *]) a.
(Semigroup mod, MonadPlus m, InterpretEffectsLtl mod m tags ops) =>
[Ltl mod] -> LtlAST mod ops a -> m a
interpretLtlASTWithInitialFormulas @tags []

-- | Like 'interpretLtlAST', just with an initial list of 'Ltl' formulas that
-- will be evaluated throughout the interpretation, even when there are no
-- 'modifyLtl's. Prunes all branches that end with incompletely applied 'Ltl'
-- formulas.
--
-- You'll also have to type-apply this to a list of 'LtlInstanceKind's, as described ad
-- 'interpretLtlAST'.
--
-- internal note: This function is the same as 'interpretASTStateful', just for
-- an 'InterpretEffectsLtl' constraint instead of 'InterpretEffectsStateful'.
interpretLtlASTWithInitialFormulas ::
  forall tags mod m ops a.
  (Semigroup mod, MonadPlus m, InterpretEffectsLtl mod m tags ops) =>
  [Ltl mod] ->
  LtlAST mod ops a ->
  m a
interpretLtlASTWithInitialFormulas :: forall (tags :: [LtlInstanceKind]) mod (m :: * -> *)
       (ops :: [(* -> *) -> * -> *]) a.
(Semigroup mod, MonadPlus m, InterpretEffectsLtl mod m tags ops) =>
[Ltl mod] -> LtlAST mod ops a -> m a
interpretLtlASTWithInitialFormulas [Ltl mod]
ltls LtlAST mod ops a
acts = do
  (a
a, [Ltl mod]
finals) <- (Const [Ltl mod] Any -> [Ltl mod])
-> (a, Const [Ltl mod] Any) -> (a, [Ltl mod])
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second Const [Ltl mod] Any -> [Ltl mod]
forall {k} a (b :: k). Const a b -> a
getConst ((a, Const [Ltl mod] Any) -> (a, [Ltl mod]))
-> m (a, Const [Ltl mod] Any) -> m (a, [Ltl mod])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InterpretEffectsLtlConstraintList
  mod m ('InterpretEffectStatefulTag : tags) (LtlEffect mod : ops)
-> Const [Ltl mod] Any
-> LtlAST mod ops a
-> m (a, Const [Ltl mod] Any)
forall mod (m :: * -> *) (tags :: [LtlInstanceKind])
       (ops :: [(* -> *) -> * -> *]) x a.
(Semigroup mod, MonadPlus m) =>
InterpretEffectsLtlConstraintList mod m tags ops
-> Const [Ltl mod] x -> AST ops a -> m (a, Const [Ltl mod] x)
interpretASTLtlInternal InterpretEffectsLtlConstraintList
  mod m ('InterpretEffectStatefulTag : tags) (LtlEffect mod : ops)
constraintList ([Ltl mod] -> Const [Ltl mod] Any
forall {k} a (b :: k). a -> Const a b
Const [Ltl mod]
ltls) LtlAST mod ops a
acts
  if (Ltl mod -> Bool) -> [Ltl mod] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Ltl mod -> Bool
forall a. Ltl a -> Bool
finished [Ltl mod]
finals
    then a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a
    else m a
forall a. m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  where
    constraintList :: InterpretEffectsLtlConstraintList
  mod m ('InterpretEffectStatefulTag : tags) (LtlEffect mod : ops)
constraintList = forall mod (m :: * -> *) (tags :: [LtlInstanceKind])
       (ops :: [(* -> *) -> * -> *]).
InterpretEffectsLtl mod m tags ops =>
InterpretEffectsLtlConstraintList mod m tags ops
interpretEffectsLtl @mod @m @(InterpretEffectStatefulTag ': tags)

-- | Internal: The function that recursively interprets the 'AST' in
-- 'interpretLtlASTWithInitialFormulas'.
interpretASTLtlInternal ::
  (Semigroup mod, MonadPlus m) =>
  InterpretEffectsLtlConstraintList mod m tags ops ->
  Const [Ltl mod] x ->
  AST ops a ->
  m (a, Const [Ltl mod] x)
interpretASTLtlInternal :: forall mod (m :: * -> *) (tags :: [LtlInstanceKind])
       (ops :: [(* -> *) -> * -> *]) x a.
(Semigroup mod, MonadPlus m) =>
InterpretEffectsLtlConstraintList mod m tags ops
-> Const [Ltl mod] x -> AST ops a -> m (a, Const [Ltl mod] x)
interpretASTLtlInternal InterpretEffectsLtlConstraintList mod m tags ops
cs Const [Ltl mod] x
x =
  (forall b.
 Const [Ltl mod] x
 -> Fixpoint (JoinedEffects ops) Freer b
 -> m (b, Const [Ltl mod] x))
-> Const [Ltl mod] x
-> Freer (Fixpoint (JoinedEffects ops) Freer) a
-> m (a, Const [Ltl mod] x)
forall a.
(forall b.
 Const [Ltl mod] x
 -> Fixpoint (JoinedEffects ops) Freer b
 -> m (b, Const [Ltl mod] x))
-> Const [Ltl mod] x
-> Freer (Fixpoint (JoinedEffects ops) Freer) a
-> m (a, Const [Ltl mod] x)
forall x (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
       (m :: * -> *) a.
InterpretOneLayerState x f g m =>
(forall b. x -> Fixpoint g f b -> m (b, x))
-> x -> f (Fixpoint g f) a -> m (a, x)
interpretOneLayerState
    ( \Const [Ltl mod] x
x' Fixpoint (JoinedEffects ops) Freer b
acts ->
        InterpretEffectsLtlConstraintList mod m tags ops
-> (forall b y.
    Const [Ltl mod] y -> AST ops b -> m (b, Const [Ltl mod] y))
-> Const [Ltl mod] x
-> JoinedEffects ops (AST ops) b
-> m (b, Const [Ltl mod] x)
forall mod (m :: * -> *) (tags :: [LtlInstanceKind])
       (ops :: [(* -> *) -> * -> *]) (allOps :: [(* -> *) -> * -> *]) x a.
(Semigroup mod, MonadPlus m) =>
InterpretEffectsLtlConstraintList mod m tags ops
-> (forall b y.
    Const [Ltl mod] y -> AST allOps b -> m (b, Const [Ltl mod] y))
-> Const [Ltl mod] x
-> JoinedEffects ops (AST allOps) a
-> m (a, Const [Ltl mod] x)
interpretJoinedEffectsLtl
          InterpretEffectsLtlConstraintList mod m tags ops
cs
          (InterpretEffectsLtlConstraintList mod m tags ops
-> Const [Ltl mod] y -> AST ops b -> m (b, Const [Ltl mod] y)
forall mod (m :: * -> *) (tags :: [LtlInstanceKind])
       (ops :: [(* -> *) -> * -> *]) x a.
(Semigroup mod, MonadPlus m) =>
InterpretEffectsLtlConstraintList mod m tags ops
-> Const [Ltl mod] x -> AST ops a -> m (a, Const [Ltl mod] x)
interpretASTLtlInternal InterpretEffectsLtlConstraintList mod m tags ops
cs)
          Const [Ltl mod] x
x'
          (Fixpoint (JoinedEffects ops) Freer b
-> JoinedEffects ops (AST ops) b
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *) a.
Fixpoint f g a -> f (Fixpoint g f) a
unFixpoint Fixpoint (JoinedEffects ops) Freer b
acts)
    )
    Const [Ltl mod] x
x
    (Freer (Fixpoint (JoinedEffects ops) Freer) a
 -> m (a, Const [Ltl mod] x))
-> (AST ops a -> Freer (Fixpoint (JoinedEffects ops) Freer) a)
-> AST ops a
-> m (a, Const [Ltl mod] x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AST ops a -> Freer (Fixpoint (JoinedEffects ops) Freer) a
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *) a.
Fixpoint f g a -> f (Fixpoint g f) a
unFixpoint

-- | Internal: For 'interpretLtlASTWithInitialFormulas', we need a function
-- that takes a 'JoinedEffects', where each effect has one of the three relevant
-- instances, and returns the effect's interpretation.
--
-- This function is called in a mutually recursive fashion with 'interpretASTLtlInternal'.
interpretJoinedEffectsLtl ::
  (Semigroup mod, MonadPlus m) =>
  InterpretEffectsLtlConstraintList mod m tags ops ->
  (forall b y. Const [Ltl mod] y -> AST allOps b -> m (b, Const [Ltl mod] y)) ->
  Const [Ltl mod] x ->
  JoinedEffects ops (AST allOps) a ->
  m (a, Const [Ltl mod] x)
interpretJoinedEffectsLtl :: forall mod (m :: * -> *) (tags :: [LtlInstanceKind])
       (ops :: [(* -> *) -> * -> *]) (allOps :: [(* -> *) -> * -> *]) x a.
(Semigroup mod, MonadPlus m) =>
InterpretEffectsLtlConstraintList mod m tags ops
-> (forall b y.
    Const [Ltl mod] y -> AST allOps b -> m (b, Const [Ltl mod] y))
-> Const [Ltl mod] x
-> JoinedEffects ops (AST allOps) a
-> m (a, Const [Ltl mod] x)
interpretJoinedEffectsLtl InterpretEffectsLtlConstraintList mod m tags ops
InterpretEffectsLtlNil forall b y.
Const [Ltl mod] y -> AST allOps b -> m (b, Const [Ltl mod] y)
_ Const [Ltl mod] x
_ JoinedEffects ops (AST allOps) a
op = case JoinedEffects ops (AST allOps) a
op of {}
interpretJoinedEffectsLtl (InterpretEffectsLtlFirstorder InterpretEffectsLtlConstraintList mod m tags ops
_) forall b y.
Const [Ltl mod] y -> AST allOps b -> m (b, Const [Ltl mod] y)
evalAST Const [Ltl mod] x
x (JoinedEffectsHere op (AST allOps) a
op) =
  (forall b y.
 Const [Ltl mod] y -> AST allOps b -> m (b, Const [Ltl mod] y))
-> Const [Ltl mod] x
-> op (AST allOps) a
-> m (a, Const [Ltl mod] x)
forall mod (m :: * -> *) (op :: (* -> *) -> * -> *)
       (ops :: [(* -> *) -> * -> *]) x a.
(Semigroup mod, MonadPlus m, InterpretEffect m op,
 InterpretMod mod m op) =>
(forall b y.
 Const [Ltl mod] y -> AST ops b -> m (b, Const [Ltl mod] y))
-> Const [Ltl mod] x -> op (AST ops) a -> m (a, Const [Ltl mod] x)
interpretEffectStatefulFromLtl Const [Ltl mod] y -> AST allOps b -> m (b, Const [Ltl mod] y)
forall b y.
Const [Ltl mod] y -> AST allOps b -> m (b, Const [Ltl mod] y)
evalAST Const [Ltl mod] x
x op (AST allOps) a
op
interpretJoinedEffectsLtl (InterpretEffectsLtlFirstorder InterpretEffectsLtlConstraintList mod m tags ops
cs) forall b y.
Const [Ltl mod] y -> AST allOps b -> m (b, Const [Ltl mod] y)
evalAST Const [Ltl mod] x
x (JoinedEffectsThere JoinedEffects ops1 (AST allOps) a
op) =
  InterpretEffectsLtlConstraintList mod m tags ops
-> (forall b y.
    Const [Ltl mod] y -> AST allOps b -> m (b, Const [Ltl mod] y))
-> Const [Ltl mod] x
-> JoinedEffects ops (AST allOps) a
-> m (a, Const [Ltl mod] x)
forall mod (m :: * -> *) (tags :: [LtlInstanceKind])
       (ops :: [(* -> *) -> * -> *]) (allOps :: [(* -> *) -> * -> *]) x a.
(Semigroup mod, MonadPlus m) =>
InterpretEffectsLtlConstraintList mod m tags ops
-> (forall b y.
    Const [Ltl mod] y -> AST allOps b -> m (b, Const [Ltl mod] y))
-> Const [Ltl mod] x
-> JoinedEffects ops (AST allOps) a
-> m (a, Const [Ltl mod] x)
interpretJoinedEffectsLtl InterpretEffectsLtlConstraintList mod m tags ops
cs Const [Ltl mod] y -> AST allOps b -> m (b, Const [Ltl mod] y)
forall b y.
Const [Ltl mod] y -> AST allOps b -> m (b, Const [Ltl mod] y)
evalAST Const [Ltl mod] x
x JoinedEffects ops (AST allOps) a
JoinedEffects ops1 (AST allOps) a
op
interpretJoinedEffectsLtl (InterpretEffectsLtlHigherorder InterpretEffectsLtlConstraintList mod m tags ops
_) forall b y.
Const [Ltl mod] y -> AST allOps b -> m (b, Const [Ltl mod] y)
evalAST Const [Ltl mod] x
x (JoinedEffectsHere op (AST allOps) a
op) =
  (forall b y.
 Const [Ltl mod] y -> AST allOps b -> m (b, Const [Ltl mod] y))
-> Const [Ltl mod] x
-> op (AST allOps) a
-> m (a, Const [Ltl mod] x)
forall mod (m :: * -> *) (op :: (* -> *) -> * -> *)
       (ops :: [(* -> *) -> * -> *]) x a.
(Semigroup mod, MonadPlus m, InterpretEffect m op,
 InterpretLtlHigherOrder mod m op) =>
(forall b y.
 Const [Ltl mod] y -> AST ops b -> m (b, Const [Ltl mod] y))
-> Const [Ltl mod] x -> op (AST ops) a -> m (a, Const [Ltl mod] x)
interpretEffectStatefulFromLtlHigherOrder Const [Ltl mod] y -> AST allOps b -> m (b, Const [Ltl mod] y)
forall b y.
Const [Ltl mod] y -> AST allOps b -> m (b, Const [Ltl mod] y)
evalAST Const [Ltl mod] x
x op (AST allOps) a
op
interpretJoinedEffectsLtl (InterpretEffectsLtlHigherorder InterpretEffectsLtlConstraintList mod m tags ops
cs) forall b y.
Const [Ltl mod] y -> AST allOps b -> m (b, Const [Ltl mod] y)
evalAST Const [Ltl mod] x
x (JoinedEffectsThere JoinedEffects ops1 (AST allOps) a
op) =
  InterpretEffectsLtlConstraintList mod m tags ops
-> (forall b y.
    Const [Ltl mod] y -> AST allOps b -> m (b, Const [Ltl mod] y))
-> Const [Ltl mod] x
-> JoinedEffects ops (AST allOps) a
-> m (a, Const [Ltl mod] x)
forall mod (m :: * -> *) (tags :: [LtlInstanceKind])
       (ops :: [(* -> *) -> * -> *]) (allOps :: [(* -> *) -> * -> *]) x a.
(Semigroup mod, MonadPlus m) =>
InterpretEffectsLtlConstraintList mod m tags ops
-> (forall b y.
    Const [Ltl mod] y -> AST allOps b -> m (b, Const [Ltl mod] y))
-> Const [Ltl mod] x
-> JoinedEffects ops (AST allOps) a
-> m (a, Const [Ltl mod] x)
interpretJoinedEffectsLtl InterpretEffectsLtlConstraintList mod m tags ops
cs Const [Ltl mod] y -> AST allOps b -> m (b, Const [Ltl mod] y)
forall b y.
Const [Ltl mod] y -> AST allOps b -> m (b, Const [Ltl mod] y)
evalAST Const [Ltl mod] x
x JoinedEffects ops (AST allOps) a
JoinedEffects ops1 (AST allOps) a
op
interpretJoinedEffectsLtl (InterpretEffectsLtlEffectStateful InterpretEffectsLtlConstraintList mod m tags ops
_) forall b y.
Const [Ltl mod] y -> AST allOps b -> m (b, Const [Ltl mod] y)
evalAST Const [Ltl mod] x
x (JoinedEffectsHere op (AST allOps) a
op) =
  (forall b y.
 Const [Ltl mod] y -> AST allOps b -> m (b, Const [Ltl mod] y))
-> Const [Ltl mod] x
-> op (AST allOps) a
-> m (a, Const [Ltl mod] x)
forall (ops :: [(* -> *) -> * -> *]) x a.
(forall b y.
 Const [Ltl mod] y -> AST ops b -> m (b, Const [Ltl mod] y))
-> Const [Ltl mod] x -> op (AST ops) a -> m (a, Const [Ltl mod] x)
forall (t :: * -> *) (m :: * -> *) (op :: (* -> *) -> * -> *)
       (ops :: [(* -> *) -> * -> *]) x a.
InterpretEffectStateful t m op =>
(forall b y. t y -> AST ops b -> m (b, t y))
-> t x -> op (AST ops) a -> m (a, t x)
interpretEffectStateful Const [Ltl mod] y -> AST allOps b -> m (b, Const [Ltl mod] y)
forall b y.
Const [Ltl mod] y -> AST allOps b -> m (b, Const [Ltl mod] y)
evalAST Const [Ltl mod] x
x op (AST allOps) a
op
interpretJoinedEffectsLtl (InterpretEffectsLtlEffectStateful InterpretEffectsLtlConstraintList mod m tags ops
cs) forall b y.
Const [Ltl mod] y -> AST allOps b -> m (b, Const [Ltl mod] y)
evalAST Const [Ltl mod] x
x (JoinedEffectsThere JoinedEffects ops1 (AST allOps) a
op) =
  InterpretEffectsLtlConstraintList mod m tags ops
-> (forall b y.
    Const [Ltl mod] y -> AST allOps b -> m (b, Const [Ltl mod] y))
-> Const [Ltl mod] x
-> JoinedEffects ops (AST allOps) a
-> m (a, Const [Ltl mod] x)
forall mod (m :: * -> *) (tags :: [LtlInstanceKind])
       (ops :: [(* -> *) -> * -> *]) (allOps :: [(* -> *) -> * -> *]) x a.
(Semigroup mod, MonadPlus m) =>
InterpretEffectsLtlConstraintList mod m tags ops
-> (forall b y.
    Const [Ltl mod] y -> AST allOps b -> m (b, Const [Ltl mod] y))
-> Const [Ltl mod] x
-> JoinedEffects ops (AST allOps) a
-> m (a, Const [Ltl mod] x)
interpretJoinedEffectsLtl InterpretEffectsLtlConstraintList mod m tags ops
cs Const [Ltl mod] y -> AST allOps b -> m (b, Const [Ltl mod] y)
forall b y.
Const [Ltl mod] y -> AST allOps b -> m (b, Const [Ltl mod] y)
evalAST Const [Ltl mod] x
x JoinedEffects ops (AST allOps) a
JoinedEffects ops1 (AST allOps) a
op

-- | Internal: For 'interpretJoinedEffectsLtl', we'll need a function that
-- behaves like 'interpretEffectStateful', in the setting where we only have an
-- 'InterpretMod' instance. This is that function.
interpretEffectStatefulFromLtl ::
  ( Semigroup mod,
    MonadPlus m,
    InterpretEffect m op,
    InterpretMod mod m op
  ) =>
  (forall b y. Const [Ltl mod] y -> AST ops b -> m (b, Const [Ltl mod] y)) ->
  Const [Ltl mod] x ->
  op (AST ops) a ->
  m (a, Const [Ltl mod] x)
interpretEffectStatefulFromLtl :: forall mod (m :: * -> *) (op :: (* -> *) -> * -> *)
       (ops :: [(* -> *) -> * -> *]) x a.
(Semigroup mod, MonadPlus m, InterpretEffect m op,
 InterpretMod mod m op) =>
(forall b y.
 Const [Ltl mod] y -> AST ops b -> m (b, Const [Ltl mod] y))
-> Const [Ltl mod] x -> op (AST ops) a -> m (a, Const [Ltl mod] x)
interpretEffectStatefulFromLtl forall b y.
Const [Ltl mod] y -> AST ops b -> m (b, Const [Ltl mod] y)
evalActs (Const [Ltl mod]
ltls) op (AST ops) a
op =
  case op (AST ops) a -> ModInterp mod m a
forall (dummy :: [(* -> *) -> * -> *]) a.
op (AST dummy) a -> ModInterp mod m a
forall mod (m :: * -> *) (op :: (* -> *) -> * -> *)
       (dummy :: [(* -> *) -> * -> *]) a.
InterpretMod mod m op =>
op (AST dummy) a -> ModInterp mod m a
interpretMod op (AST ops) a
op of
    ModInterp mod m a
Invisible -> [Ltl mod] -> op (AST ops) a -> m (a, Const [Ltl mod] x)
interpretUnmodified [Ltl mod]
ltls op (AST ops) a
op
    Visible mod -> m (Maybe a)
attempt ->
      [m (a, Const [Ltl mod] x)] -> m (a, Const [Ltl mod] x)
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ([m (a, Const [Ltl mod] x)] -> m (a, Const [Ltl mod] x))
-> [m (a, Const [Ltl mod] x)] -> m (a, Const [Ltl mod] x)
forall a b. (a -> b) -> a -> b
$
        ((Maybe mod, [Ltl mod]) -> m (a, Const [Ltl mod] x))
-> [(Maybe mod, [Ltl mod])] -> [m (a, Const [Ltl mod] x)]
forall a b. (a -> b) -> [a] -> [b]
map
          ( \(Maybe mod
now, [Ltl mod]
later) ->
              case Maybe mod
now of
                Maybe mod
Nothing -> [Ltl mod] -> op (AST ops) a -> m (a, Const [Ltl mod] x)
interpretUnmodified [Ltl mod]
later op (AST ops) a
op
                Just mod
now' -> do
                  Maybe a
mA <- mod -> m (Maybe a)
attempt mod
now'
                  case Maybe a
mA of
                    Just a
a -> (a, Const [Ltl mod] x) -> m (a, Const [Ltl mod] x)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (a
a, [Ltl mod] -> Const [Ltl mod] x
forall {k} a (b :: k). a -> Const a b
Const [Ltl mod]
later)
                    Maybe a
Nothing -> m (a, Const [Ltl mod] x)
forall a. m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
          )
          ([Ltl mod] -> [(Maybe mod, [Ltl mod])]
forall a. Semigroup a => [Ltl a] -> [(Maybe a, [Ltl a])]
nowLaterList [Ltl mod]
ltls)
  where
    interpretUnmodified :: [Ltl mod] -> op (AST ops) a -> m (a, Const [Ltl mod] x)
interpretUnmodified [Ltl mod]
later op (AST ops) a
x =
      (,[Ltl mod] -> Const [Ltl mod] x
forall {k} a (b :: k). a -> Const a b
Const [Ltl mod]
later)
        (a -> (a, Const [Ltl mod] x)) -> m a -> m (a, Const [Ltl mod] x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall b. AST ops b -> m b) -> op (AST ops) a -> m a
forall (ops :: [(* -> *) -> * -> *]) a.
(forall b. AST ops b -> m b) -> op (AST ops) a -> m a
forall (m :: * -> *) (op :: (* -> *) -> * -> *)
       (ops :: [(* -> *) -> * -> *]) a.
InterpretEffect m op =>
(forall b. AST ops b -> m b) -> op (AST ops) a -> m a
interpretEffect
          (((b, Const [Ltl mod] Any) -> b)
-> m (b, Const [Ltl mod] Any) -> m b
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (b, Const [Ltl mod] Any) -> b
forall a b. (a, b) -> a
fst (m (b, Const [Ltl mod] Any) -> m b)
-> (AST ops b -> m (b, Const [Ltl mod] Any)) -> AST ops b -> m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const [Ltl mod] Any -> AST ops b -> m (b, Const [Ltl mod] Any)
forall b y.
Const [Ltl mod] y -> AST ops b -> m (b, Const [Ltl mod] y)
evalActs ([Ltl mod] -> Const [Ltl mod] Any
forall {k} a (b :: k). a -> Const a b
Const []))
          op (AST ops) a
x

-- | Internal: Like 'interpretEffectStatefulFromLtl', just for the higher-order
-- instance.
interpretEffectStatefulFromLtlHigherOrder ::
  ( Semigroup mod,
    MonadPlus m,
    InterpretEffect m op,
    InterpretLtlHigherOrder mod m op
  ) =>
  (forall b y. Const [Ltl mod] y -> AST ops b -> m (b, Const [Ltl mod] y)) ->
  Const [Ltl mod] x ->
  op (AST ops) a ->
  m (a, Const [Ltl mod] x)
interpretEffectStatefulFromLtlHigherOrder :: forall mod (m :: * -> *) (op :: (* -> *) -> * -> *)
       (ops :: [(* -> *) -> * -> *]) x a.
(Semigroup mod, MonadPlus m, InterpretEffect m op,
 InterpretLtlHigherOrder mod m op) =>
(forall b y.
 Const [Ltl mod] y -> AST ops b -> m (b, Const [Ltl mod] y))
-> Const [Ltl mod] x -> op (AST ops) a -> m (a, Const [Ltl mod] x)
interpretEffectStatefulFromLtlHigherOrder forall b y.
Const [Ltl mod] y -> AST ops b -> m (b, Const [Ltl mod] y)
evalActs (Const [Ltl mod]
ltls) op (AST ops) a
op =
  case op (AST ops) a -> LtlInterpHigherOrder mod m ops a
forall (ops :: [(* -> *) -> * -> *]) a.
op (AST ops) a -> LtlInterpHigherOrder mod m ops a
forall mod (m :: * -> *) (op :: (* -> *) -> * -> *)
       (ops :: [(* -> *) -> * -> *]) a.
InterpretLtlHigherOrder mod m op =>
op (AST ops) a -> LtlInterpHigherOrder mod m ops a
interpretLtlHigherOrder op (AST ops) a
op of
    Direct ModInterp mod m a
inner -> case ModInterp mod m a
inner of
      ModInterp mod m a
Invisible -> [Ltl mod] -> op (AST ops) a -> m (a, Const [Ltl mod] x)
interpretUnmodified [Ltl mod]
ltls op (AST ops) a
op
      Visible mod -> m (Maybe a)
attempt ->
        [m (a, Const [Ltl mod] x)] -> m (a, Const [Ltl mod] x)
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ([m (a, Const [Ltl mod] x)] -> m (a, Const [Ltl mod] x))
-> [m (a, Const [Ltl mod] x)] -> m (a, Const [Ltl mod] x)
forall a b. (a -> b) -> a -> b
$
          ((Maybe mod, [Ltl mod]) -> m (a, Const [Ltl mod] x))
-> [(Maybe mod, [Ltl mod])] -> [m (a, Const [Ltl mod] x)]
forall a b. (a -> b) -> [a] -> [b]
map
            ( \(Maybe mod
now, [Ltl mod]
later) ->
                case Maybe mod
now of
                  Maybe mod
Nothing -> [Ltl mod] -> op (AST ops) a -> m (a, Const [Ltl mod] x)
interpretUnmodified [Ltl mod]
later op (AST ops) a
op
                  Just mod
now' -> do
                    Maybe a
mA <- mod -> m (Maybe a)
attempt mod
now'
                    case Maybe a
mA of
                      Just a
a -> (a, Const [Ltl mod] x) -> m (a, Const [Ltl mod] x)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (a
a, [Ltl mod] -> Const [Ltl mod] x
forall {k} a (b :: k). a -> Const a b
Const [Ltl mod]
later)
                      Maybe a
Nothing -> m (a, Const [Ltl mod] x)
forall a. m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
            )
            ([Ltl mod] -> [(Maybe mod, [Ltl mod])]
forall a. Semigroup a => [Ltl a] -> [(Maybe a, [Ltl a])]
nowLaterList [Ltl mod]
ltls)
    Nested (forall b. [Ltl mod] -> AST ops b -> m (b, [Ltl mod]))
-> [Ltl mod] -> m (Maybe (a, [Ltl mod]))
nestFun -> do
      Maybe (a, [Ltl mod])
mA <- (forall b. [Ltl mod] -> AST ops b -> m (b, [Ltl mod]))
-> [Ltl mod] -> m (Maybe (a, [Ltl mod]))
nestFun (\[Ltl mod]
x' AST ops b
ast -> (Const [Ltl mod] Any -> [Ltl mod])
-> (b, Const [Ltl mod] Any) -> (b, [Ltl mod])
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second Const [Ltl mod] Any -> [Ltl mod]
forall {k} a (b :: k). Const a b -> a
getConst ((b, Const [Ltl mod] Any) -> (b, [Ltl mod]))
-> m (b, Const [Ltl mod] Any) -> m (b, [Ltl mod])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Const [Ltl mod] Any -> AST ops b -> m (b, Const [Ltl mod] Any)
forall b y.
Const [Ltl mod] y -> AST ops b -> m (b, Const [Ltl mod] y)
evalActs ([Ltl mod] -> Const [Ltl mod] Any
forall {k} a (b :: k). a -> Const a b
Const [Ltl mod]
x') AST ops b
ast) [Ltl mod]
ltls
      case Maybe (a, [Ltl mod])
mA of
        Maybe (a, [Ltl mod])
Nothing -> m (a, Const [Ltl mod] x)
forall a. m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
        Just (a
a, [Ltl mod]
ltls') -> (a, Const [Ltl mod] x) -> m (a, Const [Ltl mod] x)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (a
a, [Ltl mod] -> Const [Ltl mod] x
forall {k} a (b :: k). a -> Const a b
Const [Ltl mod]
ltls')
  where
    interpretUnmodified :: [Ltl mod] -> op (AST ops) a -> m (a, Const [Ltl mod] x)
interpretUnmodified [Ltl mod]
later op (AST ops) a
x =
      (,[Ltl mod] -> Const [Ltl mod] x
forall {k} a (b :: k). a -> Const a b
Const [Ltl mod]
later)
        (a -> (a, Const [Ltl mod] x)) -> m a -> m (a, Const [Ltl mod] x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall b. AST ops b -> m b) -> op (AST ops) a -> m a
forall (ops :: [(* -> *) -> * -> *]) a.
(forall b. AST ops b -> m b) -> op (AST ops) a -> m a
forall (m :: * -> *) (op :: (* -> *) -> * -> *)
       (ops :: [(* -> *) -> * -> *]) a.
InterpretEffect m op =>
(forall b. AST ops b -> m b) -> op (AST ops) a -> m a
interpretEffect
          (((b, Const [Ltl mod] Any) -> b)
-> m (b, Const [Ltl mod] Any) -> m b
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (b, Const [Ltl mod] Any) -> b
forall a b. (a, b) -> a
fst (m (b, Const [Ltl mod] Any) -> m b)
-> (AST ops b -> m (b, Const [Ltl mod] Any)) -> AST ops b -> m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const [Ltl mod] Any -> AST ops b -> m (b, Const [Ltl mod] Any)
forall b y.
Const [Ltl mod] y -> AST ops b -> m (b, Const [Ltl mod] y)
evalActs ([Ltl mod] -> Const [Ltl mod] Any
forall {k} a (b :: k). a -> Const a b
Const []))
          op (AST ops) a
x

-- | Internal: Split an LTL formula that describes a modification of a
-- computation into a list of @(doNow, doLater)@ pairs. This is used mostly to
-- implement 'nowLaterList', so see the comment there.
nowLater :: (Semigroup a) => Ltl a -> [(Maybe a, Ltl a)]
nowLater :: forall a. Semigroup a => Ltl a -> [(Maybe a, Ltl a)]
nowLater Ltl a
LtlTruth = [(Maybe a
forall a. Maybe a
Nothing, Ltl a
forall a. Ltl a
LtlTruth)]
nowLater Ltl a
LtlFalsity = []
nowLater (LtlAtom a
g) = [(a -> Maybe a
forall a. a -> Maybe a
Just a
g, Ltl a
forall a. Ltl a
LtlTruth)]
nowLater (Ltl a
a `LtlOr` Ltl a
b) = Ltl a -> [(Maybe a, Ltl a)]
forall a. Semigroup a => Ltl a -> [(Maybe a, Ltl a)]
nowLater Ltl a
a [(Maybe a, Ltl a)] -> [(Maybe a, Ltl a)] -> [(Maybe a, Ltl a)]
forall a. [a] -> [a] -> [a]
++ Ltl a -> [(Maybe a, Ltl a)]
forall a. Semigroup a => Ltl a -> [(Maybe a, Ltl a)]
nowLater Ltl a
b
nowLater (Ltl a
a `LtlAnd` Ltl a
b) =
  [ ( Maybe a
f Maybe a -> Maybe a -> Maybe a
forall a. Semigroup a => a -> a -> a
<> Maybe 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
    )
    | (Maybe a
f, Ltl a
c) <- Ltl a -> [(Maybe a, Ltl a)]
forall a. Semigroup a => Ltl a -> [(Maybe a, Ltl a)]
nowLater Ltl a
a,
      (Maybe a
g, Ltl a
d) <- Ltl a -> [(Maybe a, Ltl a)]
forall a. Semigroup a => Ltl a -> [(Maybe a, Ltl a)]
nowLater Ltl a
b
  ]
nowLater (LtlNext Ltl a
a) = [(Maybe a
forall a. Maybe a
Nothing, Ltl a
a)]
nowLater (Ltl a
a `LtlUntil` Ltl a
b) =
  Ltl a -> [(Maybe a, Ltl a)]
forall a. Semigroup a => Ltl a -> [(Maybe a, Ltl a)]
nowLater (Ltl a -> [(Maybe a, Ltl a)]) -> Ltl a -> [(Maybe 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 -> [(Maybe a, Ltl a)]
forall a. Semigroup a => Ltl a -> [(Maybe a, Ltl a)]
nowLater (Ltl a -> [(Maybe a, Ltl a)]) -> Ltl a -> [(Maybe 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))

-- | Internal: 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 (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

-- | We're passing around a list of 'Ltl' formulas from each time
-- step to the next.
--
-- This function returns computes a list of @(doNow, doLater)@ pairs, where
--
-- * @doNow@ is @Just@ the modification to be applied to the current time step,
--   or @Nothing@, if no modification needs to be applied, and
--
-- * @doLater@ is again a list of 'Ltl' formulas describing the composite 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.
--
-- Atomic modifications of type @a@ should form a 'Semigroup', where '<>' is
-- the composition of modifications. We interpret @x <> y@ as the modification
-- that first applies @y@ and then @x@. Attention: Since we use '<>' to define
-- conjunction, if '<>' is not commutative, conjunction will also fail to be
-- commutative!
nowLaterList :: (Semigroup a) => [Ltl a] -> [(Maybe a, [Ltl a])]
nowLaterList :: forall a. Semigroup a => [Ltl a] -> [(Maybe a, [Ltl a])]
nowLaterList = [[(Maybe a, Ltl a)]] -> [(Maybe a, [Ltl a])]
forall {a} {a}. Monoid a => [[(a, a)]] -> [(a, [a])]
joinNowLaters ([[(Maybe a, Ltl a)]] -> [(Maybe a, [Ltl a])])
-> ([Ltl a] -> [[(Maybe a, Ltl a)]])
-> [Ltl a]
-> [(Maybe a, [Ltl a])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Ltl a -> [(Maybe a, Ltl a)]) -> [Ltl a] -> [[(Maybe a, Ltl a)]]
forall a b. (a -> b) -> [a] -> [b]
map Ltl a -> [(Maybe a, Ltl a)]
forall a. Semigroup a => Ltl a -> [(Maybe 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
      ]

nowLaterSplit ::
  (Semigroup x, MonadPlus m) =>
  m a ->
  (x -> m (Maybe a)) ->
  [Ltl x] ->
  m (a, [Ltl x])
nowLaterSplit :: forall x (m :: * -> *) a.
(Semigroup x, MonadPlus m) =>
m a -> (x -> m (Maybe a)) -> [Ltl x] -> m (a, [Ltl x])
nowLaterSplit m a
defaultBehaviour x -> m (Maybe a)
applyMod [Ltl x]
formulas =
  [m (a, [Ltl x])] -> m (a, [Ltl x])
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ([m (a, [Ltl x])] -> m (a, [Ltl x]))
-> [m (a, [Ltl x])] -> m (a, [Ltl x])
forall a b. (a -> b) -> a -> b
$
    ((Maybe x, [Ltl x]) -> m (a, [Ltl x]))
-> [(Maybe x, [Ltl x])] -> [m (a, [Ltl x])]
forall a b. (a -> b) -> [a] -> [b]
map
      ( \(Maybe x
now, [Ltl x]
later) -> case Maybe x
now of
          Maybe x
Nothing -> (,[Ltl x]
later) (a -> (a, [Ltl x])) -> m a -> m (a, [Ltl x])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m a
defaultBehaviour
          Just x
x -> do
            Maybe a
mA <- x -> m (Maybe a)
applyMod x
x
            case Maybe a
mA of
              Maybe a
Nothing -> m (a, [Ltl x])
forall a. m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
              Just a
a -> (a, [Ltl x]) -> m (a, [Ltl x])
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (a
a, [Ltl x]
later)
      )
      ([Ltl x] -> [(Maybe x, [Ltl x])]
forall a. Semigroup a => [Ltl a] -> [(Maybe a, [Ltl a])]
nowLaterList [Ltl x]
formulas)

-- | Internal: 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)