{-# LANGUAGE FlexibleContexts #-}
{-# OPTIONS_GHC -Wno-missing-signatures #-}

module Examples.Account.Scenarios where

import Control.Monad
import Examples.Account.AbstractDomain
import Examples.Account.PaymentMod
import Logic.Ltl

-- * Some policies, some of them purposely bugged

-- Expectations: "policyAlwaysReceives" will only accept payments
-- that increase the balance of "me"
--
-- Reality: since it is possible to exchange negative amounts, being
-- the actual recipient of payments is not sufficient.
policyAlwaysReceives :: Policy
policyAlwaysReceives :: Policy
policyAlwaysReceives (String
_, Integer
_, String
recipient) Integer
_ String
me = String
recipient String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
me

-- Expectations: "policyNeverNegative" will never accept payments
-- that leave the balance negative.
--
-- Reality: balance should be checked to be positive after the payment
-- has been made, not before.
policyNeverNegative :: Policy
policyNeverNegative :: Policy
policyNeverNegative (String, Integer, String)
_ Integer
bal String
_ = Integer
bal Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0

policyOtherNeverNegative :: Policy
policyOtherNeverNegative :: Policy
policyOtherNeverNegative (String
_, Integer
amount, String
_) Integer
bal String
_ = Integer
bal Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
amount Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0

-- This policy ensures that the exchange of money cannot be negative
policyPositivePayments :: Policy
policyPositivePayments :: Policy
policyPositivePayments (String
_, Integer
amount, String
_) Integer
_ String
_ = Integer
amount Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0

-- * A few scenarios helpers and scenarios

registerPolicies :: (MonadAccounts m) => m ()
registerPolicies :: forall (m :: * -> *). MonadAccounts m => m ()
registerPolicies = do
  String -> Policy -> m ()
forall (m :: * -> *). MonadAccounts m => String -> Policy -> m ()
addPolicy String
"alwaysReceives" Policy
policyAlwaysReceives
  String -> Policy -> m ()
forall (m :: * -> *). MonadAccounts m => String -> Policy -> m ()
addPolicy String
"neverNegative" Policy
policyNeverNegative
  String -> Policy -> m ()
forall (m :: * -> *). MonadAccounts m => String -> Policy -> m ()
addPolicy String
"positiveAmount" Policy
policyPositivePayments
  String -> Policy -> m ()
forall (m :: * -> *). MonadAccounts m => String -> Policy -> m ()
addPolicy String
"realAlwaysPositive" Policy
policyOtherNeverNegative

addAndSubscribe :: (MonadAccounts m) => String -> Integer -> [String] -> m ()
addAndSubscribe :: forall (m :: * -> *).
MonadAccounts m =>
String -> Integer -> [String] -> m ()
addAndSubscribe String
user Integer
bal = (String -> Integer -> m ()
forall (m :: * -> *). MonadAccounts m => String -> Integer -> m ()
addUser String
user Integer
bal m () -> m () -> m ()
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>) (m () -> m ()) -> ([String] -> m ()) -> [String] -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> m ()) -> [String] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (String -> String -> m ()
forall (m :: * -> *). MonadAccounts m => String -> String -> m ()
subscribeToPolicy String
user)

registerUsers :: (MonadAccounts m) => m ()
registerUsers :: forall (m :: * -> *). MonadAccounts m => m ()
registerUsers = do
  String -> Integer -> [String] -> m ()
forall (m :: * -> *).
MonadAccounts m =>
String -> Integer -> [String] -> m ()
addAndSubscribe String
"alice" Integer
0 [String
"alwaysReceives"]
  String -> Integer -> [String] -> m ()
forall (m :: * -> *).
MonadAccounts m =>
String -> Integer -> [String] -> m ()
addAndSubscribe String
"bob" Integer
1000 []
  String -> Integer -> [String] -> m ()
forall (m :: * -> *).
MonadAccounts m =>
String -> Integer -> [String] -> m ()
addAndSubscribe String
"judith" Integer
500 [String
"neverNegative"]

firstPayments :: (MonadAccounts m) => m ()
firstPayments :: forall (m :: * -> *). MonadAccounts m => m ()
firstPayments = do
  (String, Integer, String) -> m ()
forall (m :: * -> *).
MonadAccounts m =>
(String, Integer, String) -> m ()
issuePayment (String
"bob", Integer
400, String
"judith")
  (String, Integer, String) -> m ()
forall (m :: * -> *).
MonadAccounts m =>
(String, Integer, String) -> m ()
issuePayment (String
"bob", Integer
600, String
"alice")
  (String, Integer, String) -> m ()
forall (m :: * -> *).
MonadAccounts m =>
(String, Integer, String) -> m ()
issuePayment (String
"judith", Integer
600, String
"alice")

scenario1 :: (MonadAccounts m) => String -> m Integer
scenario1 :: forall (m :: * -> *). MonadAccounts m => String -> m Integer
scenario1 String
user = do
  m ()
forall (m :: * -> *). MonadAccounts m => m ()
registerPolicies
  m ()
forall (m :: * -> *). MonadAccounts m => m ()
registerUsers
  m ()
forall (m :: * -> *). MonadAccounts m => m ()
firstPayments
  String -> m Integer
forall (m :: * -> *). MonadAccounts m => String -> m Integer
getUserBalance String
user

-- >>> [(Right -1200]
negateScenario1 :: [Either AccountsError Integer]
negateScenario1 = LtlAST
  AccountsMod
  '[MonadAccountsEffect, MonadErrorEffect AccountsError]
  Integer
-> [Either AccountsError Integer]
forall a.
LtlAST
  AccountsMod
  '[MonadAccountsEffect, MonadErrorEffect AccountsError]
  a
-> [Either AccountsError a]
interpretAndRun (LtlAST
   AccountsMod
   '[MonadAccountsEffect, MonadErrorEffect AccountsError]
   Integer
 -> [Either AccountsError Integer])
-> LtlAST
     AccountsMod
     '[MonadAccountsEffect, MonadErrorEffect AccountsError]
     Integer
-> [Either AccountsError Integer]
forall a b. (a -> b) -> a -> b
$ Ltl AccountsMod
-> LtlAST
     AccountsMod
     '[MonadAccountsEffect, MonadErrorEffect AccountsError]
     Integer
-> LtlAST
     AccountsMod
     '[MonadAccountsEffect, MonadErrorEffect AccountsError]
     Integer
forall mod (ops :: [(* -> *) -> * -> *]) a.
Ltl mod -> LtlAST mod ops a -> LtlAST mod ops a
modifyLtl (AccountsMod -> Ltl AccountsMod
forall a. a -> Ltl a
everywhere AccountsMod
negatePaymentsMod) (LtlAST
   AccountsMod
   '[MonadAccountsEffect, MonadErrorEffect AccountsError]
   Integer
 -> LtlAST
      AccountsMod
      '[MonadAccountsEffect, MonadErrorEffect AccountsError]
      Integer)
-> LtlAST
     AccountsMod
     '[MonadAccountsEffect, MonadErrorEffect AccountsError]
     Integer
-> LtlAST
     AccountsMod
     '[MonadAccountsEffect, MonadErrorEffect AccountsError]
     Integer
forall a b. (a -> b) -> a -> b
$ String
-> LtlAST
     AccountsMod
     '[MonadAccountsEffect, MonadErrorEffect AccountsError]
     Integer
forall (m :: * -> *). MonadAccounts m => String -> m Integer
scenario1 String
"alice"

scenario2 :: (MonadAccounts m) => m ()
scenario2 :: forall (m :: * -> *). MonadAccounts m => m ()
scenario2 = do
  m ()
forall (m :: * -> *). MonadAccounts m => m ()
registerPolicies
  m ()
forall (m :: * -> *). MonadAccounts m => m ()
registerUsers
  [String] -> (String -> m ()) -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [String
"alice", String
"bob", String
"judith"] (String -> String -> m ()
forall (m :: * -> *). MonadAccounts m => String -> String -> m ()
`subscribeToPolicy` String
"positiveAmount")
  m ()
forall (m :: * -> *). MonadAccounts m => m ()
firstPayments

-- >>> [Left PolicyError,Left PolicyError,Left PolicyError]
negateScenario2 :: [Either AccountsError ()]
negateScenario2 = LtlAST
  AccountsMod
  '[MonadAccountsEffect, MonadErrorEffect AccountsError]
  ()
-> [Either AccountsError ()]
forall a.
LtlAST
  AccountsMod
  '[MonadAccountsEffect, MonadErrorEffect AccountsError]
  a
-> [Either AccountsError a]
interpretAndRun (LtlAST
   AccountsMod
   '[MonadAccountsEffect, MonadErrorEffect AccountsError]
   ()
 -> [Either AccountsError ()])
-> LtlAST
     AccountsMod
     '[MonadAccountsEffect, MonadErrorEffect AccountsError]
     ()
-> [Either AccountsError ()]
forall a b. (a -> b) -> a -> b
$ Ltl AccountsMod
-> LtlAST
     AccountsMod
     '[MonadAccountsEffect, MonadErrorEffect AccountsError]
     ()
-> LtlAST
     AccountsMod
     '[MonadAccountsEffect, MonadErrorEffect AccountsError]
     ()
forall mod (ops :: [(* -> *) -> * -> *]) a.
Ltl mod -> LtlAST mod ops a -> LtlAST mod ops a
modifyLtl (AccountsMod -> Ltl AccountsMod
forall a. a -> Ltl a
somewhere AccountsMod
negatePaymentsMod) LtlAST
  AccountsMod
  '[MonadAccountsEffect, MonadErrorEffect AccountsError]
  ()
forall (m :: * -> *). MonadAccounts m => m ()
scenario2

-- >>> [Right (-200)]
increaseJudithPaymentsScenario1 :: [Either AccountsError Integer]
increaseJudithPaymentsScenario1 = LtlAST
  AccountsMod
  '[MonadAccountsEffect, MonadErrorEffect AccountsError]
  Integer
-> [Either AccountsError Integer]
forall a.
LtlAST
  AccountsMod
  '[MonadAccountsEffect, MonadErrorEffect AccountsError]
  a
-> [Either AccountsError a]
interpretAndRun (LtlAST
   AccountsMod
   '[MonadAccountsEffect, MonadErrorEffect AccountsError]
   Integer
 -> [Either AccountsError Integer])
-> LtlAST
     AccountsMod
     '[MonadAccountsEffect, MonadErrorEffect AccountsError]
     Integer
-> [Either AccountsError Integer]
forall a b. (a -> b) -> a -> b
$ Ltl AccountsMod
-> LtlAST
     AccountsMod
     '[MonadAccountsEffect, MonadErrorEffect AccountsError]
     Integer
-> LtlAST
     AccountsMod
     '[MonadAccountsEffect, MonadErrorEffect AccountsError]
     Integer
forall mod (ops :: [(* -> *) -> * -> *]) a.
Ltl mod -> LtlAST mod ops a -> LtlAST mod ops a
modifyLtl (Integer -> Ltl AccountsMod -> Ltl AccountsMod
forall a. Integer -> Ltl a -> Ltl a
there Integer
2 (Ltl AccountsMod -> Ltl AccountsMod)
-> Ltl AccountsMod -> Ltl AccountsMod
forall a b. (a -> b) -> a -> b
$ AccountsMod -> Ltl AccountsMod
forall a. a -> Ltl a
LtlAtom (AccountsMod -> Ltl AccountsMod) -> AccountsMod -> Ltl AccountsMod
forall a b. (a -> b) -> a -> b
$ Integer -> AccountsMod
increaseJudithPaymentsMod Integer
500) (LtlAST
   AccountsMod
   '[MonadAccountsEffect, MonadErrorEffect AccountsError]
   Integer
 -> LtlAST
      AccountsMod
      '[MonadAccountsEffect, MonadErrorEffect AccountsError]
      Integer)
-> LtlAST
     AccountsMod
     '[MonadAccountsEffect, MonadErrorEffect AccountsError]
     Integer
-> LtlAST
     AccountsMod
     '[MonadAccountsEffect, MonadErrorEffect AccountsError]
     Integer
forall a b. (a -> b) -> a -> b
$ String
-> LtlAST
     AccountsMod
     '[MonadAccountsEffect, MonadErrorEffect AccountsError]
     Integer
forall (m :: * -> *). MonadAccounts m => String -> m Integer
scenario1 String
"judith"

scenario3 :: (MonadAccounts m) => m ()
scenario3 :: forall (m :: * -> *). MonadAccounts m => m ()
scenario3 = do
  m ()
forall (m :: * -> *). MonadAccounts m => m ()
registerPolicies
  m ()
forall (m :: * -> *). MonadAccounts m => m ()
registerUsers
  String -> String -> m ()
forall (m :: * -> *). MonadAccounts m => String -> String -> m ()
subscribeToPolicy String
"judith" String
"realAlwaysPositive"
  m ()
forall (m :: * -> *). MonadAccounts m => m ()
firstPayments

-- >>> [Left PolicyError]
increaseJudithPaymentsScenario3 :: [Either AccountsError ()]
increaseJudithPaymentsScenario3 = LtlAST
  AccountsMod
  '[MonadAccountsEffect, MonadErrorEffect AccountsError]
  ()
-> [Either AccountsError ()]
forall a.
LtlAST
  AccountsMod
  '[MonadAccountsEffect, MonadErrorEffect AccountsError]
  a
-> [Either AccountsError a]
interpretAndRun (LtlAST
   AccountsMod
   '[MonadAccountsEffect, MonadErrorEffect AccountsError]
   ()
 -> [Either AccountsError ()])
-> LtlAST
     AccountsMod
     '[MonadAccountsEffect, MonadErrorEffect AccountsError]
     ()
-> [Either AccountsError ()]
forall a b. (a -> b) -> a -> b
$ Ltl AccountsMod
-> LtlAST
     AccountsMod
     '[MonadAccountsEffect, MonadErrorEffect AccountsError]
     ()
-> LtlAST
     AccountsMod
     '[MonadAccountsEffect, MonadErrorEffect AccountsError]
     ()
forall mod (ops :: [(* -> *) -> * -> *]) a.
Ltl mod -> LtlAST mod ops a -> LtlAST mod ops a
modifyLtl (Integer -> Ltl AccountsMod -> Ltl AccountsMod
forall a. Integer -> Ltl a -> Ltl a
there Integer
2 (Ltl AccountsMod -> Ltl AccountsMod)
-> Ltl AccountsMod -> Ltl AccountsMod
forall a b. (a -> b) -> a -> b
$ AccountsMod -> Ltl AccountsMod
forall a. a -> Ltl a
LtlAtom (AccountsMod -> Ltl AccountsMod) -> AccountsMod -> Ltl AccountsMod
forall a b. (a -> b) -> a -> b
$ Integer -> AccountsMod
increaseJudithPaymentsMod Integer
500) LtlAST
  AccountsMod
  '[MonadAccountsEffect, MonadErrorEffect AccountsError]
  ()
forall (m :: * -> *). MonadAccounts m => m ()
scenario3