graft-0.0.0
Safe HaskellSafe-Inferred
LanguageHaskell2010

Logic.Ltl

Description

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

Synopsis

Ltl formulas

data Ltl a Source #

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.

Constructors

LtlTruth

The "do nothing" modification that is always applicable

LtlFalsity

The modification that never applies

LtlAtom a

The modification that applies a given atomic modification at the current step

LtlOr (Ltl a) (Ltl 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.)

LtlAnd (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.

LtlNext (Ltl a)

Apply the given modification at the next step.

LtlUntil (Ltl a) (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.

LtlRelease (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.

Instances

Instances details
Show a => Show (Ltl a) Source # 
Instance details

Defined in Logic.Ltl

Methods

showsPrec :: Int -> Ltl a -> ShowS #

show :: Ltl a -> String #

showList :: [Ltl a] -> ShowS #

somewhere :: a -> Ltl a Source #

Apply an atomic modification to some action.

everywhere :: a -> Ltl a Source #

Apply an atomic modification to all actions.

there :: Integer -> Ltl a -> Ltl a Source #

Apply a modification from the n-th step in the trace (0-indexed).

Deploying Ltl formulas

type LtlAST mod ops = AST (LtlEffect mod ': ops) Source #

An AST that allows modifying parts of its contents with Ltl modifications, using modifyLtl.

modifyLtl :: Ltl mod -> LtlAST mod ops a -> LtlAST mod ops a Source #

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

Higher-order effects

class InterpretLtlHigherOrder (mod :: Type) (m :: Type -> Type) (op :: Effect) where Source #

Explain how to interpret an Ltl modification, in the presence of higher-order effects. The type parameters have the same meaning as for InterpretLtl.

Methods

interpretLtlHigherOrder :: op (AST ops) a -> LtlInterpHigherOrder mod m ops a Source #

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 ASTs, 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 ASTs of operations. We'll likely want to use a composite modification while evaluating such nested ASTs.

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 modifyLtls, the list will only ever contain one element. If you nest modifyLtls, 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 ASTs, 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.

Instances

Instances details
MonadAccounts m => InterpretLtlHigherOrder AccountsMod m MonadAccountsEffect Source # 
Instance details

Defined in Examples.Account.PaymentMod

Methods

interpretLtlHigherOrder :: forall (ops :: [Effect]) a. MonadAccountsEffect (AST ops) a -> LtlInterpHigherOrder AccountsMod m ops a Source #

(MonadPlus m, MonadError MiniLangError m, MonadMiniLang m) => InterpretLtlHigherOrder MiniLangMod m MonadMiniLangEffect Source # 
Instance details

Defined in Examples.Ltl.HigherOrder

Methods

interpretLtlHigherOrder :: forall (ops :: [Effect]) a. MonadMiniLangEffect (AST ops) a -> LtlInterpHigherOrder MiniLangMod m ops a Source #

data LtlInterpHigherOrder (mod :: Type) (m :: Type -> Type) (ops :: [Effect]) (a :: Type) where Source #

codomain of interpretLtlHigherOrder. See the explanation there.

Constructors

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 

nowLaterList :: Semigroup a => [Ltl a] -> [(Maybe a, [Ltl a])] Source #

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!

nowLaterSplit :: (Semigroup x, MonadPlus m) => m a -> (x -> m (Maybe a)) -> [Ltl x] -> m (a, [Ltl x]) Source #

Interpreting Ltl modifications

data LtlInstanceKind Source #

Used to signify which instance is to be used for a specific effect in the InterpretEffectsLtl class.

Constructors

InterpretModTag 
InterpretLtlHigherOrderTag 
InterpretEffectStatefulTag 

Instances

Instances details
InterpretEffectsLtl mod m ('[] :: [LtlInstanceKind]) ('[] :: [Effect]) Source # 
Instance details

Defined in Logic.Ltl

Methods

interpretEffectsLtl :: InterpretEffectsLtlConstraintList mod m '[] '[] Source #

(InterpretEffectStateful (Const [Ltl mod] :: Type -> Type) m op, InterpretEffectsLtl mod m tags ops) => InterpretEffectsLtl mod m ('InterpretEffectStatefulTag ': tags) (op ': ops) Source # 
Instance details

Defined in Logic.Ltl

Methods

interpretEffectsLtl :: InterpretEffectsLtlConstraintList mod m ('InterpretEffectStatefulTag ': tags) (op ': ops) Source #

(InterpretEffect m op, InterpretLtlHigherOrder mod m op, InterpretEffectsLtl mod m tags ops) => InterpretEffectsLtl mod m ('InterpretLtlHigherOrderTag ': tags) (op ': ops) Source # 
Instance details

Defined in Logic.Ltl

Methods

interpretEffectsLtl :: InterpretEffectsLtlConstraintList mod m ('InterpretLtlHigherOrderTag ': tags) (op ': ops) Source #

(InterpretEffect m op, InterpretMod mod m op, InterpretEffectsLtl mod m tags ops) => InterpretEffectsLtl mod m ('InterpretModTag ': tags) (op ': ops) Source # 
Instance details

Defined in Logic.Ltl

Methods

interpretEffectsLtl :: InterpretEffectsLtlConstraintList mod m ('InterpretModTag ': tags) (op ': ops) Source #

class InterpretEffectsLtl (mod :: Type) (m :: Type -> Type) (tags :: [LtlInstanceKind]) (ops :: [Effect]) where Source #

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.

Methods

interpretEffectsLtl :: InterpretEffectsLtlConstraintList mod m tags ops Source #

A witness of the constraint.

Instances

Instances details
InterpretEffectsLtl mod m ('[] :: [LtlInstanceKind]) ('[] :: [Effect]) Source # 
Instance details

Defined in Logic.Ltl

Methods

interpretEffectsLtl :: InterpretEffectsLtlConstraintList mod m '[] '[] Source #

(InterpretEffectStateful (Const [Ltl mod] :: Type -> Type) m op, InterpretEffectsLtl mod m tags ops) => InterpretEffectsLtl mod m ('InterpretEffectStatefulTag ': tags) (op ': ops) Source # 
Instance details

Defined in Logic.Ltl

Methods

interpretEffectsLtl :: InterpretEffectsLtlConstraintList mod m ('InterpretEffectStatefulTag ': tags) (op ': ops) Source #

(InterpretEffect m op, InterpretLtlHigherOrder mod m op, InterpretEffectsLtl mod m tags ops) => InterpretEffectsLtl mod m ('InterpretLtlHigherOrderTag ': tags) (op ': ops) Source # 
Instance details

Defined in Logic.Ltl

Methods

interpretEffectsLtl :: InterpretEffectsLtlConstraintList mod m ('InterpretLtlHigherOrderTag ': tags) (op ': ops) Source #

(InterpretEffect m op, InterpretMod mod m op, InterpretEffectsLtl mod m tags ops) => InterpretEffectsLtl mod m ('InterpretModTag ': tags) (op ': ops) Source # 
Instance details

Defined in Logic.Ltl

Methods

interpretEffectsLtl :: InterpretEffectsLtlConstraintList mod m ('InterpretModTag ': tags) (op ': ops) Source #

interpretLtlAST :: forall tags mod m ops a. (Semigroup mod, MonadPlus m, InterpretEffectsLtl mod m tags ops) => LtlAST mod ops a -> m a Source #

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.

interpretLtlASTWithInitialFormulas :: forall tags mod m ops a. (Semigroup mod, MonadPlus m, InterpretEffectsLtl mod m tags ops) => [Ltl mod] -> LtlAST mod ops a -> m a Source #

Like interpretLtlAST, just with an initial list of Ltl formulas that will be evaluated throughout the interpretation, even when there are no modifyLtls. Prunes all branches that end with incompletely applied Ltl formulas.

You'll also have to type-apply this to a list of LtlInstanceKinds, as described ad interpretLtlAST.

internal note: This function is the same as interpretASTStateful, just for an InterpretEffectsLtl constraint instead of InterpretEffectsStateful.