{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}

module Examples.Account.PaymentMod where

import Control.Applicative
import Control.Monad
import Data.Map qualified as Map
import Effect.Error
import Effect.Error.Passthrough ()
import Examples.Account.AbstractDomain
import Examples.Account.SimpleDomain
import Logic.Ltl
import Logic.SingleStep

data AccountsMod where
  AccountsMod :: (Payment -> Maybe Payment) -> AccountsMod

instance Semigroup AccountsMod where
  (AccountsMod Payment -> Maybe Payment
f1) <> :: AccountsMod -> AccountsMod -> AccountsMod
<> (AccountsMod Payment -> Maybe Payment
f2) =
    (Payment -> Maybe Payment) -> AccountsMod
AccountsMod
      (\Payment
x -> (Payment -> Maybe Payment
f1 (Payment -> Maybe Payment)
-> (Payment -> Maybe Payment) -> Payment -> Maybe Payment
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Payment -> Maybe Payment
f2) Payment
x Maybe Payment -> Maybe Payment -> Maybe Payment
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Payment -> Maybe Payment
f1 Payment
x Maybe Payment -> Maybe Payment -> Maybe Payment
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Payment -> Maybe Payment
f2 Payment
x)

instance
  (MonadAccounts m) =>
  InterpretMod AccountsMod m MonadAccountsEffect
  where
  interpretMod :: forall (dummy :: [Effect]) a.
MonadAccountsEffect (AST dummy) a -> ModInterp AccountsMod m a
interpretMod (IssuePayment Payment
payment) = (AccountsMod -> m (Maybe a)) -> ModInterp AccountsMod m a
forall mod (m :: * -> *) a.
(mod -> m (Maybe a)) -> ModInterp mod m a
Visible ((AccountsMod -> m (Maybe a)) -> ModInterp AccountsMod m a)
-> (AccountsMod -> m (Maybe a)) -> ModInterp AccountsMod m a
forall a b. (a -> b) -> a -> b
$ \(AccountsMod Payment -> Maybe Payment
modif) ->
    m (Maybe a)
-> (Payment -> m (Maybe a)) -> Maybe Payment -> m (Maybe a)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (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) ((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
<$>) (m a -> m (Maybe a)) -> (Payment -> m a) -> Payment -> m (Maybe a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Payment -> m a
Payment -> m ()
forall (m :: * -> *). MonadAccounts m => Payment -> m ()
issuePayment) (Maybe Payment -> m (Maybe a)) -> Maybe Payment -> m (Maybe a)
forall a b. (a -> b) -> a -> b
$ Payment -> Maybe Payment
modif Payment
payment
  interpretMod MonadAccountsEffect (AST dummy) a
_ = ModInterp AccountsMod m a
forall mod (m :: * -> *) a. ModInterp mod m a
Invisible

instance
  (MonadAccounts m) =>
  InterpretLtlHigherOrder AccountsMod m MonadAccountsEffect
  where
  interpretLtlHigherOrder :: forall (ops :: [Effect]) a.
MonadAccountsEffect (AST ops) a
-> LtlInterpHigherOrder AccountsMod m ops a
interpretLtlHigherOrder (Simulate AST ops a1
comp) = ((forall b.
  [Ltl AccountsMod] -> AST ops b -> m (b, [Ltl AccountsMod]))
 -> [Ltl AccountsMod] -> m (Maybe (a, [Ltl AccountsMod])))
-> LtlInterpHigherOrder AccountsMod m ops a
forall mod (ops :: [Effect]) (m :: * -> *) a.
((forall b. [Ltl mod] -> AST ops b -> m (b, [Ltl mod]))
 -> [Ltl mod] -> m (Maybe (a, [Ltl mod])))
-> LtlInterpHigherOrder mod m ops a
Nested (((forall b.
   [Ltl AccountsMod] -> AST ops b -> m (b, [Ltl AccountsMod]))
  -> [Ltl AccountsMod] -> m (Maybe (a, [Ltl AccountsMod])))
 -> LtlInterpHigherOrder AccountsMod m ops a)
-> ((forall b.
     [Ltl AccountsMod] -> AST ops b -> m (b, [Ltl AccountsMod]))
    -> [Ltl AccountsMod] -> m (Maybe (a, [Ltl AccountsMod])))
-> LtlInterpHigherOrder AccountsMod m ops a
forall a b. (a -> b) -> a -> b
$ \forall b.
[Ltl AccountsMod] -> AST ops b -> m (b, [Ltl AccountsMod])
evalAST [Ltl AccountsMod]
ltls ->
    (a, [Ltl AccountsMod]) -> Maybe (a, [Ltl AccountsMod])
forall a. a -> Maybe a
Just ((a, [Ltl AccountsMod]) -> Maybe (a, [Ltl AccountsMod]))
-> (Maybe (a1, [Ltl AccountsMod]) -> (a, [Ltl AccountsMod]))
-> Maybe (a1, [Ltl AccountsMod])
-> Maybe (a, [Ltl AccountsMod])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,[Ltl AccountsMod]
ltls) (a -> (a, [Ltl AccountsMod]))
-> (Maybe (a1, [Ltl AccountsMod]) -> a)
-> Maybe (a1, [Ltl AccountsMod])
-> (a, [Ltl AccountsMod])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((a1, [Ltl AccountsMod]) -> a1
forall a b. (a, b) -> a
fst ((a1, [Ltl AccountsMod]) -> a1)
-> Maybe (a1, [Ltl AccountsMod]) -> Maybe a1
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (Maybe (a1, [Ltl AccountsMod]) -> Maybe (a, [Ltl AccountsMod]))
-> m (Maybe (a1, [Ltl AccountsMod]))
-> m (Maybe (a, [Ltl AccountsMod]))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (a1, [Ltl AccountsMod]) -> m (Maybe (a1, [Ltl AccountsMod]))
forall a. m a -> m (Maybe a)
forall (m :: * -> *) a. MonadAccounts m => m a -> m (Maybe a)
simulate ([Ltl AccountsMod] -> AST ops a1 -> m (a1, [Ltl AccountsMod])
forall b.
[Ltl AccountsMod] -> AST ops b -> m (b, [Ltl AccountsMod])
evalAST [Ltl AccountsMod]
ltls AST ops a1
comp)
  interpretLtlHigherOrder MonadAccountsEffect (AST ops) a
p = ModInterp AccountsMod m a
-> LtlInterpHigherOrder AccountsMod m ops a
forall mod (m :: * -> *) a (ops :: [Effect]).
ModInterp mod m a -> LtlInterpHigherOrder mod m ops a
Direct (ModInterp AccountsMod m a
 -> LtlInterpHigherOrder AccountsMod m ops a)
-> ModInterp AccountsMod m a
-> LtlInterpHigherOrder AccountsMod m ops a
forall a b. (a -> b) -> a -> b
$ MonadAccountsEffect (AST ops) a -> ModInterp AccountsMod m a
forall (dummy :: [Effect]) a.
MonadAccountsEffect (AST dummy) a -> ModInterp AccountsMod m a
forall mod (m :: * -> *) (op :: Effect) (dummy :: [Effect]) a.
InterpretMod mod m op =>
op (AST dummy) a -> ModInterp mod m a
interpretMod MonadAccountsEffect (AST ops) a
p

conditionalPaymentMod :: (String -> Bool) -> (String -> Bool) -> (Integer -> Maybe Integer) -> AccountsMod
conditionalPaymentMod :: (String -> Bool)
-> (String -> Bool) -> (Integer -> Maybe Integer) -> AccountsMod
conditionalPaymentMod String -> Bool
condSender String -> Bool
condRecipient Integer -> Maybe Integer
change =
  (Payment -> Maybe Payment) -> AccountsMod
AccountsMod ((Payment -> Maybe Payment) -> AccountsMod)
-> (Payment -> Maybe Payment) -> AccountsMod
forall a b. (a -> b) -> a -> b
$
    \(String
sender, Integer
amount, String
recipient) -> case (Integer -> Maybe Integer
change Integer
amount, String -> Bool
condSender String
sender Bool -> Bool -> Bool
&& String -> Bool
condRecipient String
recipient) of
      (Maybe Integer
Nothing, Bool
_) -> Maybe Payment
forall a. Maybe a
Nothing
      (Maybe Integer
_, Bool
False) -> Maybe Payment
forall a. Maybe a
Nothing
      (Just Integer
newAmount, Bool
True) -> Payment -> Maybe Payment
forall a. a -> Maybe a
Just (String
sender, Integer
newAmount, String
recipient)

increaseJudithPaymentsMod :: Integer -> AccountsMod
increaseJudithPaymentsMod :: Integer -> AccountsMod
increaseJudithPaymentsMod Integer
n = (String -> Bool)
-> (String -> Bool) -> (Integer -> Maybe Integer) -> AccountsMod
conditionalPaymentMod (String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"judith") (Bool -> String -> Bool
forall a b. a -> b -> a
const Bool
True) (Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer -> Maybe Integer)
-> (Integer -> Integer) -> Integer -> Maybe Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
n))

negatePaymentsMod :: AccountsMod
negatePaymentsMod :: AccountsMod
negatePaymentsMod = (String -> Bool)
-> (String -> Bool) -> (Integer -> Maybe Integer) -> AccountsMod
conditionalPaymentMod (Bool -> String -> Bool
forall a b. a -> b -> a
const Bool
True) (Bool -> String -> Bool
forall a b. a -> b -> a
const Bool
True) (Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer -> Maybe Integer)
-> (Integer -> Integer) -> Integer -> Maybe Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer
forall a. Num a => a -> a
negate)

interpretAndRun ::
  LtlAST AccountsMod '[MonadAccountsEffect, MonadErrorEffect AccountsError] a ->
  [Either AccountsError a]
interpretAndRun :: forall a.
LtlAST
  AccountsMod
  '[MonadAccountsEffect, MonadErrorEffect AccountsError]
  a
-> [Either AccountsError a]
interpretAndRun =
  ((Either AccountsError a, Map String Account)
-> Either AccountsError a
forall a b. (a, b) -> a
fst ((Either AccountsError a, Map String Account)
 -> Either AccountsError a)
-> [(Either AccountsError a, Map String Account)]
-> [Either AccountsError a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>)
    ([(Either AccountsError a, Map String Account)]
 -> [Either AccountsError a])
-> (LtlAST
      AccountsMod
      '[MonadAccountsEffect, MonadErrorEffect AccountsError]
      a
    -> [(Either AccountsError a, Map String Account)])
-> LtlAST
     AccountsMod
     '[MonadAccountsEffect, MonadErrorEffect AccountsError]
     a
-> [Either AccountsError a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Register
-> AccountsT [] a -> [(Either AccountsError a, Map String Account)]
forall (m :: * -> *) a.
Monad m =>
Register
-> AccountsT m a -> m (Either AccountsError a, Map String Account)
runAccountsT (Map String Policy -> Map String Account -> Register
Register Map String Policy
forall k a. Map k a
Map.empty Map String Account
forall k a. Map k a
Map.empty)
    (AccountsT [] a -> [(Either AccountsError a, Map String Account)])
-> (LtlAST
      AccountsMod
      '[MonadAccountsEffect, MonadErrorEffect AccountsError]
      a
    -> AccountsT [] a)
-> LtlAST
     AccountsMod
     '[MonadAccountsEffect, MonadErrorEffect AccountsError]
     a
-> [(Either AccountsError a, Map String Account)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (tags :: [LtlInstanceKind]) mod (m :: * -> *)
       (ops :: [Effect]) a.
(Semigroup mod, MonadPlus m, InterpretEffectsLtl mod m tags ops) =>
LtlAST mod ops a -> m a
interpretLtlAST
      @'[ InterpretLtlHigherOrderTag,
          InterpretEffectStatefulTag
        ]