{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}

-- | A simple, but complete, tutorial for  how to use "Logic.Ltl". This does
-- not cover
--
-- - using higher-order effects in the LTL setting, and
--
-- - combining several different effects in one test scenario.
--
-- If you're reading the Haddock documentation, consider reading the source,
-- it'll make more sense.
module Examples.Ltl.Simple where

import Control.Applicative
import Control.Monad
import Control.Monad.Except
import Control.Monad.State
import Data.Map (Map)
import qualified Data.Map as Map
import Effect.Error
import Effect.Error.Passthrough ()
import Effect.TH
import Logic.Ltl
import Logic.SingleStep

-- * Example domain specification

-- $doc
-- To use this library, you need a type class of monads that captures the
-- behaviour you want to test. For the sake of this tutorial, let's take a
-- key-value-store where the keys are 'String's and the values are 'Integer's.

class (Monad m) => MonadKeyValue m where
  storeValue :: String -> Integer -> m ()
  getValue :: String -> m Integer
  deleteValue :: String -> m ()

-- $doc
-- We'll assume a number of /traces/ written using this type class. These will
-- most likely be manually written test cases that cover (some part of) the
-- normal usage of the system you're testing.
--
-- Here, we'll only write two slightly silly examples. The more different
-- scenarios you cover in these "seed" traces, the more interesting variations
-- will be generated later on.

swapTrace :: (MonadKeyValue m) => m (Integer, Integer)
swapTrace :: forall (m :: * -> *). MonadKeyValue m => m (Integer, Integer)
swapTrace = do
  String -> Integer -> m ()
forall (m :: * -> *). MonadKeyValue m => String -> Integer -> m ()
storeValue String
"a" Integer
1
  String -> Integer -> m ()
forall (m :: * -> *). MonadKeyValue m => String -> Integer -> m ()
storeValue String
"b" Integer
2
  Integer
a <- String -> m Integer
forall (m :: * -> *). MonadKeyValue m => String -> m Integer
getValue String
"a"
  Integer
b <- String -> m Integer
forall (m :: * -> *). MonadKeyValue m => String -> m Integer
getValue String
"b"
  String -> Integer -> m ()
forall (m :: * -> *). MonadKeyValue m => String -> Integer -> m ()
storeValue String
"a" Integer
b
  String -> Integer -> m ()
forall (m :: * -> *). MonadKeyValue m => String -> Integer -> m ()
storeValue String
"b" Integer
a
  Integer
a' <- String -> m Integer
forall (m :: * -> *). MonadKeyValue m => String -> m Integer
getValue String
"a"
  Integer
b' <- String -> m Integer
forall (m :: * -> *). MonadKeyValue m => String -> m Integer
getValue String
"b"
  (Integer, Integer) -> m (Integer, Integer)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer
a', Integer
b')

deleteTrace :: (MonadKeyValue m) => m Integer
deleteTrace :: forall (m :: * -> *). MonadKeyValue m => m Integer
deleteTrace = do
  String -> Integer -> m ()
forall (m :: * -> *). MonadKeyValue m => String -> Integer -> m ()
storeValue String
"a" Integer
1
  String -> Integer -> m ()
forall (m :: * -> *). MonadKeyValue m => String -> Integer -> m ()
storeValue String
"b" Integer
2
  String -> m ()
forall (m :: * -> *). MonadKeyValue m => String -> m ()
deleteValue String
"a"
  String -> Integer -> m ()
forall (m :: * -> *). MonadKeyValue m => String -> Integer -> m ()
storeValue String
"a" Integer
2
  String -> m Integer
forall (m :: * -> *). MonadKeyValue m => String -> m Integer
getValue String
"a"

-- $doc
-- What we'll test is an implementation of 'MonadKeyValue'. We'll
-- implement it very simply, but note that the implementation of
-- 'deleteValue' is wrong: we never delete anything from the
-- store. We'll "find" this mistake later on.

newtype KeyValueError = NoSuchKey String deriving (Int -> KeyValueError -> ShowS
[KeyValueError] -> ShowS
KeyValueError -> String
(Int -> KeyValueError -> ShowS)
-> (KeyValueError -> String)
-> ([KeyValueError] -> ShowS)
-> Show KeyValueError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> KeyValueError -> ShowS
showsPrec :: Int -> KeyValueError -> ShowS
$cshow :: KeyValueError -> String
show :: KeyValueError -> String
$cshowList :: [KeyValueError] -> ShowS
showList :: [KeyValueError] -> ShowS
Show)

type KeyValueT m = ExceptT KeyValueError (StateT (Map String Integer) m)

runKeyValueT :: Map String Integer -> KeyValueT m a -> m (Either KeyValueError a, Map String Integer)
runKeyValueT :: forall (m :: * -> *) a.
Map String Integer
-> KeyValueT m a -> m (Either KeyValueError a, Map String Integer)
runKeyValueT Map String Integer
s0 = (StateT (Map String Integer) m (Either KeyValueError a)
 -> Map String Integer
 -> m (Either KeyValueError a, Map String Integer))
-> Map String Integer
-> StateT (Map String Integer) m (Either KeyValueError a)
-> m (Either KeyValueError a, Map String Integer)
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT (Map String Integer) m (Either KeyValueError a)
-> Map String Integer
-> m (Either KeyValueError a, Map String Integer)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT Map String Integer
s0 (StateT (Map String Integer) m (Either KeyValueError a)
 -> m (Either KeyValueError a, Map String Integer))
-> (KeyValueT m a
    -> StateT (Map String Integer) m (Either KeyValueError a))
-> KeyValueT m a
-> m (Either KeyValueError a, Map String Integer)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. KeyValueT m a
-> StateT (Map String Integer) m (Either KeyValueError a)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT

instance (Monad m) => MonadKeyValue (KeyValueT m) where
  storeValue :: String -> Integer -> KeyValueT m ()
storeValue String
k Integer
v = (Map String Integer -> Map String Integer) -> KeyValueT m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Map String Integer -> Map String Integer) -> KeyValueT m ())
-> (Map String Integer -> Map String Integer) -> KeyValueT m ()
forall a b. (a -> b) -> a -> b
$ String -> Integer -> Map String Integer -> Map String Integer
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
k Integer
v
  getValue :: String -> KeyValueT m Integer
getValue String
k = do
    Map String Integer
m <- ExceptT
  KeyValueError (StateT (Map String Integer) m) (Map String Integer)
forall s (m :: * -> *). MonadState s m => m s
get
    case String -> Map String Integer -> Maybe Integer
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
k Map String Integer
m of
      Maybe Integer
Nothing -> KeyValueError -> KeyValueT m Integer
forall a.
KeyValueError
-> ExceptT KeyValueError (StateT (Map String Integer) m) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (KeyValueError -> KeyValueT m Integer)
-> KeyValueError -> KeyValueT m Integer
forall a b. (a -> b) -> a -> b
$ String -> KeyValueError
NoSuchKey String
k
      Just Integer
v -> Integer -> KeyValueT m Integer
forall a.
a -> ExceptT KeyValueError (StateT (Map String Integer) m) a
forall (m :: * -> *) a. Monad m => a -> m a
return Integer
v
  deleteValue :: String -> KeyValueT m ()
deleteValue String
_ = () -> KeyValueT m ()
forall a.
a -> ExceptT KeyValueError (StateT (Map String Integer) m) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- * Using the effect system

-- $doc
-- This library is based on a custom effect system. There are a few macros that
-- will make using it more convenient. You'll at least need the following
-- language extensions (more extensions might be needed in more complex
-- scenarios than this tutorial):
--
-- > {-# LANGUAGE ConstraintKinds #-}
-- > {-# LANGUAGE FlexibleContexts #-}
-- > {-# LANGUAGE FlexibleInstances #-}
-- > {-# LANGUAGE KindSignatures #-}
-- > {-# LANGUAGE MultiParamTypeClasses #-}
-- > {-# LANGUAGE ScopedTypeVariables #-}
-- > {-# LANGUAGE TemplateHaskell #-}
-- > {-# LANGUAGE TypeApplications #-}
--
-- The first macro will write an /effect type/ corresponding to 'MonadKeyValue'
-- for us, and give it the name 'MonadKeyValueEffect':

defineEffectType ''MonadKeyValue

-- $doc
-- The type 'MonadKeyValueEffect' is an abstract representation of the class
-- 'MonadKeyValue'. This means that for each method of the class, there's a
-- constructor of the effect type:
--
-- - for @storeValue :: String -> Integer -> m ()@, there is @StoreValue :: String -> Integer -> MonadKeyValueEffect m ()@,
--
-- - for @getValue :: String -> m Integer@, there is @GetValue :: String -> MonadKeyValueEffect m Integer@, and
--
-- - for @deleteValue :: String -> m ()@, there is @DeleteValue :: String -> MonadKeyValueEffect m ()@.
--
-- We thus have a reification of computations in 'MonadKeyValue'. This
-- reification will be used to build 'AST's, which can then be interpreted in
-- flexible ways.
--
-- There's also a macro to define some instances that will make this
-- convenient.

makeEffect ''MonadKeyValue ''MonadKeyValueEffect

-- * Defining a type of single-step modifications

-- $doc
-- The testing method explained in this tutorial consists in deploying
-- single-step modifications while interpreting an 'AST'. The 'AST' will be
-- built from abstract representations of actions (i.e. the constructors of
-- effect types like 'MonadKeyValueEffect'), and we'll interpret it into some
-- suitable monad (here, that'll be @KeyValueT m@).
--
-- So, we'll first have to define a type of single-step modifications, and
-- explain how they should change the interpretation of actions. The
-- single-step modifications have no meaning in and of them themselves, as they
-- are only explained by how they apply to the constructors of
-- 'MonadKeyValueEffect'.

data KeyValueMod = KeyValueMod
  { KeyValueMod -> Bool
noOverwrite :: Bool,
    KeyValueMod -> ShowS
renameKey :: String -> String
  }

-- $doc
-- Our modification type 'KeyValueMod' captures two behaviours:
--
-- - When 'noOverwrite' is @True@, the intended meaning is that
--   'storeValue' should be ignored when it replaces the value (i.e., when the
--   key is already present in the store)
--
-- - 'renameKey' will change the keys used by any action with a prescribed
--   function.
--
-- The 'InterpretMod' instance now makes these intended meanings explicit. The
-- function 'interpretMod' describes, for each constructor of
-- 'MonadKeyValueEffect', how it should be interpreted under a modification:
--
-- - Whenever the there's a modification that might apply, we'll try to apply
--   it using the 'AttemptModification' constructor.
--
--   - When the modification applies, we signal that success by wrapping the
--     return value of the action in a 'Just'.
--
--   - When the modification doesn't apply, we return 'Nothing'.
--
-- - Whenever there's no modification, we have nothing to apply, so we return
--   'SkipModification'. This will mean that the operation will be performed as
--   usual.
--
-- - A third possibility, which is not shown here, is returning 'PassModification'
--   instead of 'AttemptModification' or 'SkipModification', which would mean
--   to do the operation without modification as usual, but remember the
--   modification for the next step. This can be thought of as making the
--   operation invisible to modifications.

instance (MonadError KeyValueError m, MonadKeyValue m) => InterpretMod KeyValueMod m MonadKeyValueEffect where
  interpretMod :: forall (dummy :: [(* -> *) -> * -> *]) a.
MonadKeyValueEffect (AST dummy) a -> ModInterp KeyValueMod m a
interpretMod (StoreValue String
key Integer
val) =
    (KeyValueMod -> m (Maybe a)) -> ModInterp KeyValueMod m a
forall mod (m :: * -> *) a.
(mod -> m (Maybe a)) -> ModInterp mod m a
Visible ((KeyValueMod -> m (Maybe a)) -> ModInterp KeyValueMod m a)
-> (KeyValueMod -> m (Maybe a)) -> ModInterp KeyValueMod m a
forall a b. (a -> b) -> a -> b
$ \KeyValueMod
modif -> do
      Maybe Integer
oldVal <- m (Maybe Integer)
-> (KeyValueError -> m (Maybe Integer)) -> m (Maybe Integer)
forall a. m a -> (KeyValueError -> m a) -> m a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
catchError (Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer -> Maybe Integer) -> m Integer -> m (Maybe Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> m Integer
forall (m :: * -> *). MonadKeyValue m => String -> m Integer
getValue String
key) (\NoSuchKey {} -> Maybe Integer -> m (Maybe Integer)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Integer
forall a. Maybe a
Nothing)
      case (Maybe Integer
oldVal, KeyValueMod -> Bool
noOverwrite KeyValueMod
modif) of
        (Just Integer
_, Bool
True) -> Maybe a -> m (Maybe a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Maybe a
forall a. a -> Maybe a
Just ())
        (Maybe Integer
Nothing, Bool
True) -> Maybe a -> m (Maybe a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
forall a. Maybe a
Nothing
        (Maybe Integer
_, Bool
False) -> a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> m a -> m (Maybe a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> Integer -> m ()
forall (m :: * -> *). MonadKeyValue m => String -> Integer -> m ()
storeValue (KeyValueMod -> ShowS
renameKey KeyValueMod
modif String
key) Integer
val
  interpretMod (DeleteValue String
key) =
    (KeyValueMod -> m (Maybe a)) -> ModInterp KeyValueMod m a
forall mod (m :: * -> *) a.
(mod -> m (Maybe a)) -> ModInterp mod m a
Visible ((KeyValueMod -> m (Maybe a)) -> ModInterp KeyValueMod m a)
-> (KeyValueMod -> m (Maybe a)) -> ModInterp KeyValueMod m a
forall a b. (a -> b) -> a -> b
$ \KeyValueMod
modif ->
      if KeyValueMod -> Bool
noOverwrite KeyValueMod
modif
        then Maybe a -> m (Maybe a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
forall a. Maybe a
Nothing
        else a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> m a -> m (Maybe a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> m ()
forall (m :: * -> *). MonadKeyValue m => String -> m ()
deleteValue (KeyValueMod -> ShowS
renameKey KeyValueMod
modif String
key)
  interpretMod (GetValue String
key) =
    (KeyValueMod -> m (Maybe a)) -> ModInterp KeyValueMod m a
forall mod (m :: * -> *) a.
(mod -> m (Maybe a)) -> ModInterp mod m a
Visible ((KeyValueMod -> m (Maybe a)) -> ModInterp KeyValueMod m a)
-> (KeyValueMod -> m (Maybe a)) -> ModInterp KeyValueMod m a
forall a b. (a -> b) -> a -> b
$ \KeyValueMod
modif ->
      if KeyValueMod -> Bool
noOverwrite KeyValueMod
modif
        then Maybe a -> m (Maybe a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
forall a. Maybe a
Nothing
        else a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> m a -> m (Maybe a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> m Integer
forall (m :: * -> *). MonadKeyValue m => String -> m Integer
getValue (KeyValueMod -> ShowS
renameKey KeyValueMod
modif String
key)

-- $doc
-- Here are two smart constructors for modifications, one for creating a
-- modification that transforms keys solely, the other that only ignores
-- overwrites:

renameKeys :: (String -> String) -> KeyValueMod
renameKeys :: ShowS -> KeyValueMod
renameKeys ShowS
f = KeyValueMod {noOverwrite :: Bool
noOverwrite = Bool
False, renameKey :: ShowS
renameKey = ShowS
f}

noStoreOverride :: KeyValueMod
noStoreOverride :: KeyValueMod
noStoreOverride = KeyValueMod {noOverwrite :: Bool
noOverwrite = Bool
True, renameKey :: ShowS
renameKey = ShowS
forall a. a -> a
id}

-- * Using "Logic.Ltl" to deploy single-step modifications

-- $doc
-- The module "Logic.Ltl" implements one way to combine single-step
-- modifications into composite modifications that apply to traces: a formula
-- in an LTL-like language determines when to apply the single-step
-- modifications.
--
-- The evaluation of such 'Ltl' formulas sometimes makes it necessary to try
-- applying two single-step modifications on the same step. The 'Semigroup'
-- instance describes how they should combine.

instance Semigroup KeyValueMod where
  KeyValueMod
mod1 <> :: KeyValueMod -> KeyValueMod -> KeyValueMod
<> KeyValueMod
mod2 =
    KeyValueMod
      { noOverwrite :: Bool
noOverwrite = KeyValueMod -> Bool
noOverwrite KeyValueMod
mod1 Bool -> Bool -> Bool
|| KeyValueMod -> Bool
noOverwrite KeyValueMod
mod2,
        renameKey :: ShowS
renameKey = KeyValueMod -> ShowS
renameKey KeyValueMod
mod1 ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. KeyValueMod -> ShowS
renameKey KeyValueMod
mod2
      }

-- $doc
-- The module "Logic.Ltl" provides the wrapper type @'LtlAST' mod ops@.
-- Here, @ops@ is the list of effect types related to our domain. In our case,
-- it will have to contain 'MonadKeyValueEffect' and @MonadErrorEffect
-- KeyValueError@. The Template Haskell macros we used above make it so that
--
-- > LtlAST mod '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
--
-- is an instance of 'MonadKeyValue' and @MonadError KeyValueError@. The
-- parameter @mod@ is the type of single-step modifications; here it is
-- 'KeyValueMod'.
--
-- In addition to all the 'MonadKeyValue' and 'MonadError' functions, the
-- 'LtlAST' also gives you access to the function
--
-- > modifyLtl :: Ltl mod -> LtlAST mod ops a -> LtlAST mod ops a
--
-- This is what makes it possible to deploy composite 'Ltl' modifications: wrap
-- the part of the computation you want to modify in 'modifyLtl' with the 'Ltl'
-- formula of your choice.
--
-- The module "Logic.Ltl" also provides
--
-- > interpretLtlAST :: forall mod m ops a. (Semigroup mod, MonadPlus m, InterpretEffectsLtl mod m tags ops) => LtlAST mod ops a -> m a
--
-- which interprets the @'LtlAST' mod ops@ into any suitable monad @m@. Here,
-- "suitable" means:
--
-- - All of the effects in @ops@ have one of the following three instances:
--
--     - @InterpretMod mod m@ (this is what we have here)
--
--     - @InterpretLtlHigherOrder mod m@ (this is for higher order effect
--       types, we're not interested in that here)
--
--     - @InterpretEffectStateful (Const [Ltl mod]) m@ (this is a low-level
--       class used to implement the LTL framework itself)
--
-- - @m@ is a 'MonadPlus'. This is necessary because there might be several
--   ways to satisfy an 'Ltl' formula. The whole point of using 'Ltl' do describe
--   modifications of a single trace is to try /all/ of the possible ways to
--   apply the formula. Sometimes, this requires defining a custom 'MonadPlus'
--   instance for the monad (or transformer) we're interested in.

instance {-# OVERLAPPING #-} (MonadPlus m) => Alternative (KeyValueT m) where
  empty :: forall a. KeyValueT m a
empty = StateT (Map String Integer) m a
-> ExceptT KeyValueError (StateT (Map String Integer) m) a
forall (m :: * -> *) a. Monad m => m a -> ExceptT KeyValueError m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (StateT (Map String Integer) m a
 -> ExceptT KeyValueError (StateT (Map String Integer) m) a)
-> StateT (Map String Integer) m a
-> ExceptT KeyValueError (StateT (Map String Integer) m) a
forall a b. (a -> b) -> a -> b
$ m a -> StateT (Map String Integer) m a
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (Map String Integer) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m a
forall a. m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  ExceptT (StateT Map String Integer
-> m (Either KeyValueError a, Map String Integer)
a) <|> :: forall a. KeyValueT m a -> KeyValueT m a -> KeyValueT m a
<|> (ExceptT (StateT Map String Integer
-> m (Either KeyValueError a, Map String Integer)
b)) = StateT (Map String Integer) m (Either KeyValueError a)
-> ExceptT KeyValueError (StateT (Map String Integer) m) a
forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT (StateT (Map String Integer) m (Either KeyValueError a)
 -> ExceptT KeyValueError (StateT (Map String Integer) m) a)
-> StateT (Map String Integer) m (Either KeyValueError a)
-> ExceptT KeyValueError (StateT (Map String Integer) m) a
forall a b. (a -> b) -> a -> b
$ (Map String Integer
 -> m (Either KeyValueError a, Map String Integer))
-> StateT (Map String Integer) m (Either KeyValueError a)
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT ((Map String Integer
  -> m (Either KeyValueError a, Map String Integer))
 -> StateT (Map String Integer) m (Either KeyValueError a))
-> (Map String Integer
    -> m (Either KeyValueError a, Map String Integer))
-> StateT (Map String Integer) m (Either KeyValueError a)
forall a b. (a -> b) -> a -> b
$ \Map String Integer
x -> Map String Integer
-> m (Either KeyValueError a, Map String Integer)
a Map String Integer
x m (Either KeyValueError a, Map String Integer)
-> m (Either KeyValueError a, Map String Integer)
-> m (Either KeyValueError a, Map String Integer)
forall a. m a -> m a -> m a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Map String Integer
-> m (Either KeyValueError a, Map String Integer)
b Map String Integer
x

instance {-# OVERLAPPING #-} (MonadPlus m) => MonadPlus (KeyValueT m)

-- $doc
-- Using 'interpretLtlAST', we can write a convenience function that will
-- interpret an 'LtlAST' of 'MonadKeyValueEffect's and return the final return value
-- and state of the store.
--
-- Note how we type-apply 'interpretLtlAST' to a list of "tags" of kind
-- 'LtlInstanceKind': These tags specify, in order, which of the three
-- instances described above we expect the effects to have.
--
-- The 'InterpretEffectStateful' instance for 'MonadErrorEffect' is imported
-- from "Effect.Error.Passthrough", and is implemented in a generic way so as
-- to ignore every modification: we only care about modifying 'MonadKeyValue'
-- actions.

interpretAndRun ::
  LtlAST KeyValueMod '[MonadKeyValueEffect, MonadErrorEffect KeyValueError] a ->
  [(Either KeyValueError a, Map String Integer)]
interpretAndRun :: forall a.
LtlAST
  KeyValueMod
  '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
  a
-> [(Either KeyValueError a, Map String Integer)]
interpretAndRun =
  Map String Integer
-> KeyValueT [] a -> [(Either KeyValueError a, Map String Integer)]
forall (m :: * -> *) a.
Map String Integer
-> KeyValueT m a -> m (Either KeyValueError a, Map String Integer)
runKeyValueT Map String Integer
forall a. Monoid a => a
mempty
    (KeyValueT [] a -> [(Either KeyValueError a, Map String Integer)])
-> (LtlAST
      KeyValueMod
      '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
      a
    -> KeyValueT [] a)
-> LtlAST
     KeyValueMod
     '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
     a
-> [(Either KeyValueError a, Map String Integer)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (tags :: [LtlInstanceKind]) mod (m :: * -> *)
       (ops :: [(* -> *) -> * -> *]) a.
(Semigroup mod, MonadPlus m, InterpretEffectsLtl mod m tags ops) =>
LtlAST mod ops a -> m a
interpretLtlAST
      @'[ InterpretModTag,
          InterpretEffectStatefulTag
        ]

-- * A few examples

-- ** 'somewhere'

-- $doc
-- By far the most commonly used 'Ltl' formula is 'somewhere'.
--
-- In our first example, we try applying the modification 'noStoreOverride' to
-- some action in the 'swapTrace'. There are two actions where the modification
-- applies, namely the third and fourth 'storeValue's:
--
-- > swapTrace = do
-- >   storeValue "a" 1
-- >   storeValue "b" 2
-- >   a <- getValue "a"
-- >   b <- getValue "b"
-- >   storeValue "a" b   -- replaced by no-op in branch 1
-- >   storeValue "b" a   -- replaced by no-op in branch 2
-- >   a' <- getValue "a"
-- >   b' <- getValue "b"
--
-- So, we expect to have two modified traces, where both "a" and "b" share the
-- same value, and that's indeed the case:
--
-- >>> exampleSomewhereSwap
-- [(Right (1,1),fromList [("a",1),("b",1)]),
--  (Right (2,2),fromList [("a",2),("b",2)])]

exampleSomewhereSwap :: [(Either KeyValueError (Integer, Integer), Map String Integer)]
exampleSomewhereSwap :: [(Either KeyValueError (Integer, Integer), Map String Integer)]
exampleSomewhereSwap = LtlAST
  KeyValueMod
  '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
  (Integer, Integer)
-> [(Either KeyValueError (Integer, Integer), Map String Integer)]
forall a.
LtlAST
  KeyValueMod
  '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
  a
-> [(Either KeyValueError a, Map String Integer)]
interpretAndRun (LtlAST
   KeyValueMod
   '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
   (Integer, Integer)
 -> [(Either KeyValueError (Integer, Integer), Map String Integer)])
-> LtlAST
     KeyValueMod
     '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
     (Integer, Integer)
-> [(Either KeyValueError (Integer, Integer), Map String Integer)]
forall a b. (a -> b) -> a -> b
$ Ltl KeyValueMod
-> LtlAST
     KeyValueMod
     '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
     (Integer, Integer)
-> LtlAST
     KeyValueMod
     '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
     (Integer, Integer)
forall mod (ops :: [(* -> *) -> * -> *]) a.
Ltl mod -> LtlAST mod ops a -> LtlAST mod ops a
modifyLtl (KeyValueMod -> Ltl KeyValueMod
forall a. a -> Ltl a
somewhere KeyValueMod
noStoreOverride) LtlAST
  KeyValueMod
  '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
  (Integer, Integer)
forall (m :: * -> *). MonadKeyValue m => m (Integer, Integer)
swapTrace

-- $doc
-- In the 'deleteTrace', we expect 'noStoreOverride' never to apply as
-- there should be no override. However, it applies because our
-- implementation of 'deleteKey' does not actually delete anything.
--
-- > deleteTrace = do
-- >   storeValue "a" 1
-- >   storeValue "b" 2
-- >   deleteValue "a"
-- >   storeValue "a" 2 -- replaced by no-op
-- >   getValue "a"
--
-- We have "discovered" the bug!
--
-- >>> exampleSomewhereDelete
-- [(Right 1,fromList [("a",1),("b",2)])]

exampleSomewhereDelete :: [(Either KeyValueError Integer, Map String Integer)]
exampleSomewhereDelete :: [(Either KeyValueError Integer, Map String Integer)]
exampleSomewhereDelete =
  LtlAST
  KeyValueMod
  '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
  Integer
-> [(Either KeyValueError Integer, Map String Integer)]
forall a.
LtlAST
  KeyValueMod
  '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
  a
-> [(Either KeyValueError a, Map String Integer)]
interpretAndRun (LtlAST
   KeyValueMod
   '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
   Integer
 -> [(Either KeyValueError Integer, Map String Integer)])
-> LtlAST
     KeyValueMod
     '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
     Integer
-> [(Either KeyValueError Integer, Map String Integer)]
forall a b. (a -> b) -> a -> b
$ Ltl KeyValueMod
-> LtlAST
     KeyValueMod
     '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
     Integer
-> LtlAST
     KeyValueMod
     '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
     Integer
forall mod (ops :: [(* -> *) -> * -> *]) a.
Ltl mod -> LtlAST mod ops a -> LtlAST mod ops a
modifyLtl (KeyValueMod -> Ltl KeyValueMod
forall a. a -> Ltl a
somewhere KeyValueMod
noStoreOverride) LtlAST
  KeyValueMod
  '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
  Integer
forall (m :: * -> *). MonadKeyValue m => m Integer
deleteTrace

-- ** 'everywhere'

-- $doc
-- Another very commonly used 'Ltl' formula is 'everywhere'. It must
-- apply the given single-step modification to every action in the
-- 'AST'. If it is not applicable somewhere, then there will be no
-- output trace.
--
-- So, when we apply @everywhere noStoreOverride@ to the swapTrace, we'll get
-- no results, because not all 'storeValue's in that trace replace the value at
-- a key.
--
-- >>> exampleEverywhereSwap
-- []

exampleEverywhereSwap :: [(Either KeyValueError (Integer, Integer), Map String Integer)]
exampleEverywhereSwap :: [(Either KeyValueError (Integer, Integer), Map String Integer)]
exampleEverywhereSwap =
  LtlAST
  KeyValueMod
  '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
  (Integer, Integer)
-> [(Either KeyValueError (Integer, Integer), Map String Integer)]
forall a.
LtlAST
  KeyValueMod
  '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
  a
-> [(Either KeyValueError a, Map String Integer)]
interpretAndRun (LtlAST
   KeyValueMod
   '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
   (Integer, Integer)
 -> [(Either KeyValueError (Integer, Integer), Map String Integer)])
-> LtlAST
     KeyValueMod
     '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
     (Integer, Integer)
-> [(Either KeyValueError (Integer, Integer), Map String Integer)]
forall a b. (a -> b) -> a -> b
$ Ltl KeyValueMod
-> LtlAST
     KeyValueMod
     '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
     (Integer, Integer)
-> LtlAST
     KeyValueMod
     '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
     (Integer, Integer)
forall mod (ops :: [(* -> *) -> * -> *]) a.
Ltl mod -> LtlAST mod ops a -> LtlAST mod ops a
modifyLtl (KeyValueMod -> Ltl KeyValueMod
forall a. a -> Ltl a
everywhere KeyValueMod
noStoreOverride) LtlAST
  KeyValueMod
  '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
  (Integer, Integer)
forall (m :: * -> *). MonadKeyValue m => m (Integer, Integer)
swapTrace

-- $doc
-- On the other hand, 'renameKeys' always applies, and hence we can
-- successfully apply it to, say the 'deleteTrace', and thus prove that its
-- behaviour is independent under renaming of keys.
--
-- >>> exampleEverywhereDelete
-- [(Right 2,fromList [("anew",2),("bnew",2)])]

exampleEverywhereDelete :: [(Either KeyValueError Integer, Map String Integer)]
exampleEverywhereDelete :: [(Either KeyValueError Integer, Map String Integer)]
exampleEverywhereDelete =
  LtlAST
  KeyValueMod
  '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
  Integer
-> [(Either KeyValueError Integer, Map String Integer)]
forall a.
LtlAST
  KeyValueMod
  '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
  a
-> [(Either KeyValueError a, Map String Integer)]
interpretAndRun (LtlAST
   KeyValueMod
   '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
   Integer
 -> [(Either KeyValueError Integer, Map String Integer)])
-> LtlAST
     KeyValueMod
     '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
     Integer
-> [(Either KeyValueError Integer, Map String Integer)]
forall a b. (a -> b) -> a -> b
$ Ltl KeyValueMod
-> LtlAST
     KeyValueMod
     '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
     Integer
-> LtlAST
     KeyValueMod
     '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
     Integer
forall mod (ops :: [(* -> *) -> * -> *]) a.
Ltl mod -> LtlAST mod ops a -> LtlAST mod ops a
modifyLtl (KeyValueMod -> Ltl KeyValueMod
forall a. a -> Ltl a
everywhere (KeyValueMod -> Ltl KeyValueMod) -> KeyValueMod -> Ltl KeyValueMod
forall a b. (a -> b) -> a -> b
$ ShowS -> KeyValueMod
renameKeys (String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"new")) LtlAST
  KeyValueMod
  '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
  Integer
forall (m :: * -> *). MonadKeyValue m => m Integer
deleteTrace

-- $doc
-- Note that, unlike 'somewhere', 'everywhere' doesn't imply that any
-- modification is applied. Applying 'everywhere' to an empty trace is
-- successful, and returns one result:
--
-- >>> exampleEverywhereEmpty
-- [((),fromList [])]

exampleEverywhereEmpty :: [(Either KeyValueError (), Map String Integer)]
exampleEverywhereEmpty :: [(Either KeyValueError (), Map String Integer)]
exampleEverywhereEmpty =
  LtlAST
  KeyValueMod
  '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
  ()
-> [(Either KeyValueError (), Map String Integer)]
forall a.
LtlAST
  KeyValueMod
  '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
  a
-> [(Either KeyValueError a, Map String Integer)]
interpretAndRun (LtlAST
   KeyValueMod
   '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
   ()
 -> [(Either KeyValueError (), Map String Integer)])
-> LtlAST
     KeyValueMod
     '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
     ()
-> [(Either KeyValueError (), Map String Integer)]
forall a b. (a -> b) -> a -> b
$ Ltl KeyValueMod
-> LtlAST
     KeyValueMod
     '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
     ()
-> LtlAST
     KeyValueMod
     '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
     ()
forall mod (ops :: [(* -> *) -> * -> *]) a.
Ltl mod -> LtlAST mod ops a -> LtlAST mod ops a
modifyLtl (KeyValueMod -> Ltl KeyValueMod
forall a. a -> Ltl a
everywhere KeyValueMod
noStoreOverride) (()
-> LtlAST
     KeyValueMod
     '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
     ()
forall a.
a
-> Fixpoint
     Freer
     (JoinedEffects
        '[LtlEffect KeyValueMod, MonadKeyValueEffect,
          MonadErrorEffect KeyValueError])
     a
forall (m :: * -> *) a. Monad m => a -> m a
return ())

-- ** 'there'

-- $doc
-- In addition to 'somewhere' and 'everywhere', it is also possible to
-- require the application of a modification starting from a specific position in
-- a trace using 'there'
--
-- >>> exampleThere
-- [(Right (),fromList [("a",1),("b",2),("cnew",3),("d",4)]),
--  (Right (),fromList [("a",1),("b",2),("c",3),("dnew",4)])]

exampleThere :: [(Either KeyValueError (), Map String Integer)]
exampleThere :: [(Either KeyValueError (), Map String Integer)]
exampleThere =
  LtlAST
  KeyValueMod
  '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
  ()
-> [(Either KeyValueError (), Map String Integer)]
forall a.
LtlAST
  KeyValueMod
  '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
  a
-> [(Either KeyValueError a, Map String Integer)]
interpretAndRun (LtlAST
   KeyValueMod
   '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
   ()
 -> [(Either KeyValueError (), Map String Integer)])
-> LtlAST
     KeyValueMod
     '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
     ()
-> [(Either KeyValueError (), Map String Integer)]
forall a b. (a -> b) -> a -> b
$ Ltl KeyValueMod
-> LtlAST
     KeyValueMod
     '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
     ()
-> LtlAST
     KeyValueMod
     '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
     ()
forall mod (ops :: [(* -> *) -> * -> *]) a.
Ltl mod -> LtlAST mod ops a -> LtlAST mod ops a
modifyLtl (Integer -> Ltl KeyValueMod -> Ltl KeyValueMod
forall a. Integer -> Ltl a -> Ltl a
there Integer
2 (Ltl KeyValueMod -> Ltl KeyValueMod)
-> Ltl KeyValueMod -> Ltl KeyValueMod
forall a b. (a -> b) -> a -> b
$ KeyValueMod -> Ltl KeyValueMod
forall a. a -> Ltl a
somewhere (KeyValueMod -> Ltl KeyValueMod) -> KeyValueMod -> Ltl KeyValueMod
forall a b. (a -> b) -> a -> b
$ ShowS -> KeyValueMod
renameKeys (String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"new")) (LtlAST
   KeyValueMod
   '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
   ()
 -> LtlAST
      KeyValueMod
      '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
      ())
-> LtlAST
     KeyValueMod
     '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
     ()
-> LtlAST
     KeyValueMod
     '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
     ()
forall a b. (a -> b) -> a -> b
$ do
    String
-> Integer
-> LtlAST
     KeyValueMod
     '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
     ()
forall (m :: * -> *). MonadKeyValue m => String -> Integer -> m ()
storeValue String
"a" Integer
1
    String
-> Integer
-> LtlAST
     KeyValueMod
     '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
     ()
forall (m :: * -> *). MonadKeyValue m => String -> Integer -> m ()
storeValue String
"b" Integer
2
    String
-> Integer
-> LtlAST
     KeyValueMod
     '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
     ()
forall (m :: * -> *). MonadKeyValue m => String -> Integer -> m ()
storeValue String
"c" Integer
3
    String
-> Integer
-> LtlAST
     KeyValueMod
     '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
     ()
forall (m :: * -> *). MonadKeyValue m => String -> Integer -> m ()
storeValue String
"d" Integer
4

-- $doc
-- Another idiom to accomplish the same without using 'there' is to only apply
-- 'modifyLtl' after the first few actions:
--
-- >>> exampleNotThere
-- [(Right (),fromList [("a",1),("b",2),("cnew",3),("d",4)]),
--  (Right (),fromList [("a",1),("b",2),("c",3),("dnew",4)])]

exampleNotThere :: [(Either KeyValueError (), Map String Integer)]
exampleNotThere :: [(Either KeyValueError (), Map String Integer)]
exampleNotThere =
  LtlAST
  KeyValueMod
  '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
  ()
-> [(Either KeyValueError (), Map String Integer)]
forall a.
LtlAST
  KeyValueMod
  '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
  a
-> [(Either KeyValueError a, Map String Integer)]
interpretAndRun (LtlAST
   KeyValueMod
   '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
   ()
 -> [(Either KeyValueError (), Map String Integer)])
-> LtlAST
     KeyValueMod
     '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
     ()
-> [(Either KeyValueError (), Map String Integer)]
forall a b. (a -> b) -> a -> b
$ do
    String
-> Integer
-> LtlAST
     KeyValueMod
     '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
     ()
forall (m :: * -> *). MonadKeyValue m => String -> Integer -> m ()
storeValue String
"a" Integer
1
    String
-> Integer
-> LtlAST
     KeyValueMod
     '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
     ()
forall (m :: * -> *). MonadKeyValue m => String -> Integer -> m ()
storeValue String
"b" Integer
2
    Ltl KeyValueMod
-> LtlAST
     KeyValueMod
     '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
     ()
-> LtlAST
     KeyValueMod
     '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
     ()
forall mod (ops :: [(* -> *) -> * -> *]) a.
Ltl mod -> LtlAST mod ops a -> LtlAST mod ops a
modifyLtl (KeyValueMod -> Ltl KeyValueMod
forall a. a -> Ltl a
somewhere (KeyValueMod -> Ltl KeyValueMod) -> KeyValueMod -> Ltl KeyValueMod
forall a b. (a -> b) -> a -> b
$ ShowS -> KeyValueMod
renameKeys (String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"new")) (LtlAST
   KeyValueMod
   '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
   ()
 -> LtlAST
      KeyValueMod
      '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
      ())
-> LtlAST
     KeyValueMod
     '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
     ()
-> LtlAST
     KeyValueMod
     '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
     ()
forall a b. (a -> b) -> a -> b
$ do
      String
-> Integer
-> LtlAST
     KeyValueMod
     '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
     ()
forall (m :: * -> *). MonadKeyValue m => String -> Integer -> m ()
storeValue String
"c" Integer
3
      String
-> Integer
-> LtlAST
     KeyValueMod
     '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
     ()
forall (m :: * -> *). MonadKeyValue m => String -> Integer -> m ()
storeValue String
"d" Integer
4

-- ** Custom 'Ltl' formulas

-- $doc
-- Finally, it is possible to create formulas by hand using the 'Ltl'
-- constructors. In this example, we add "new" to the key of the two
-- first instructions of @deleteTrace
--
-- >>> exampleCustom
-- [(Right (),fromList [("anew",1),("bnew",2),("c",3),("d",4)])]

exampleCustom :: [(Either KeyValueError (), Map String Integer)]
exampleCustom :: [(Either KeyValueError (), Map String Integer)]
exampleCustom =
  LtlAST
  KeyValueMod
  '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
  ()
-> [(Either KeyValueError (), Map String Integer)]
forall a.
LtlAST
  KeyValueMod
  '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
  a
-> [(Either KeyValueError a, Map String Integer)]
interpretAndRun
    (LtlAST
   KeyValueMod
   '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
   ()
 -> [(Either KeyValueError (), Map String Integer)])
-> LtlAST
     KeyValueMod
     '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
     ()
-> [(Either KeyValueError (), Map String Integer)]
forall a b. (a -> b) -> a -> b
$ Ltl KeyValueMod
-> LtlAST
     KeyValueMod
     '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
     ()
-> LtlAST
     KeyValueMod
     '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
     ()
forall mod (ops :: [(* -> *) -> * -> *]) a.
Ltl mod -> LtlAST mod ops a -> LtlAST mod ops a
modifyLtl
      ( Ltl KeyValueMod -> Ltl KeyValueMod -> Ltl KeyValueMod
forall a. Ltl a -> Ltl a -> Ltl a
LtlAnd
          (KeyValueMod -> Ltl KeyValueMod
forall a. a -> Ltl a
LtlAtom (KeyValueMod -> Ltl KeyValueMod) -> KeyValueMod -> Ltl KeyValueMod
forall a b. (a -> b) -> a -> b
$ ShowS -> KeyValueMod
renameKeys (String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"new"))
          (Ltl KeyValueMod -> Ltl KeyValueMod
forall a. Ltl a -> Ltl a
LtlNext (Ltl KeyValueMod -> Ltl KeyValueMod)
-> Ltl KeyValueMod -> Ltl KeyValueMod
forall a b. (a -> b) -> a -> b
$ KeyValueMod -> Ltl KeyValueMod
forall a. a -> Ltl a
LtlAtom (KeyValueMod -> Ltl KeyValueMod) -> KeyValueMod -> Ltl KeyValueMod
forall a b. (a -> b) -> a -> b
$ ShowS -> KeyValueMod
renameKeys (String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"new"))
      )
    (LtlAST
   KeyValueMod
   '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
   ()
 -> LtlAST
      KeyValueMod
      '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
      ())
-> LtlAST
     KeyValueMod
     '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
     ()
-> LtlAST
     KeyValueMod
     '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
     ()
forall a b. (a -> b) -> a -> b
$ do
      String
-> Integer
-> LtlAST
     KeyValueMod
     '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
     ()
forall (m :: * -> *). MonadKeyValue m => String -> Integer -> m ()
storeValue String
"a" Integer
1
      String
-> Integer
-> LtlAST
     KeyValueMod
     '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
     ()
forall (m :: * -> *). MonadKeyValue m => String -> Integer -> m ()
storeValue String
"b" Integer
2
      String
-> Integer
-> LtlAST
     KeyValueMod
     '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
     ()
forall (m :: * -> *). MonadKeyValue m => String -> Integer -> m ()
storeValue String
"c" Integer
3
      String
-> Integer
-> LtlAST
     KeyValueMod
     '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]
     ()
forall (m :: * -> *). MonadKeyValue m => String -> Integer -> m ()
storeValue String
"d" Integer
4