-- | This module applies the `Cooked.Tweak.Common.Tweak` effect for the purpose
-- of modifying transaction skeleton before sending them for validation.
module Cooked.MockChain.Tweak
  ( -- * Modifying mockchain runs using tweaks
    reinterpretMockChainWriteWithTweak,

    -- * Typed and Untyped tweaks geared for `Cooked.Skeleton.TxSkel`

    --   modifications
    TypedTweak,
    UntypedTweak (..),

    -- * Modalities to deploy `UntypedTweak`s on time
    somewhere,
    everywhere,
    nowhere,
    whenAble,
    there,
    withTweak,
  )
where

import Control.Monad
import Cooked.Ltl
import Cooked.MockChain.Write
import Cooked.Tweak.Common
import Data.Coerce
import Polysemy
import Polysemy.Internal
import Polysemy.NonDet

-- | A stack of effects starting with `Tweak` and `NonDet`
type TypedTweak tweakEffs a = Sem (Tweak : NonDet : tweakEffs) a

-- | Wrapping up typed tweaks to existentially quantify on their return type
data UntypedTweak tweakEffs where
  UntypedTweak :: TypedTweak tweakEffs a -> UntypedTweak tweakEffs

fromTweak ::
  TypedTweak tweakEffs a ->
  Ltl (UntypedTweak tweakEffs)
fromTweak :: forall (tweakEffs :: [(* -> *) -> * -> *]) a.
TypedTweak tweakEffs a -> Ltl (UntypedTweak tweakEffs)
fromTweak = UntypedTweak tweakEffs -> Ltl (UntypedTweak tweakEffs)
forall a. a -> Ltl a
LtlAtom (UntypedTweak tweakEffs -> Ltl (UntypedTweak tweakEffs))
-> (TypedTweak tweakEffs a -> UntypedTweak tweakEffs)
-> TypedTweak tweakEffs a
-> Ltl (UntypedTweak tweakEffs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedTweak tweakEffs a -> UntypedTweak tweakEffs
forall (tweakEffs :: [(* -> *) -> * -> *]) a.
TypedTweak tweakEffs a -> UntypedTweak tweakEffs
UntypedTweak

-- | Applies a 'Tweak' to every step in a trace where it is applicable,
-- branching at any such locations. The tweak must apply at least once.
somewhere ::
  (Members '[ModifyGlobally (UntypedTweak tweakEffs)] effs) =>
  TypedTweak tweakEffs b ->
  Sem effs a ->
  Sem effs a
somewhere :: forall (tweakEffs :: [(* -> *) -> * -> *])
       (effs :: [(* -> *) -> * -> *]) b a.
Members '[ModifyGlobally (UntypedTweak tweakEffs)] effs =>
TypedTweak tweakEffs b -> Sem effs a -> Sem effs a
somewhere = Ltl (UntypedTweak tweakEffs) -> Sem effs a -> Sem effs a
forall a (r :: [(* -> *) -> * -> *]) b.
Member (ModifyGlobally a) r =>
Ltl a -> Sem r b -> Sem r b
modifyLtl (Ltl (UntypedTweak tweakEffs) -> Sem effs a -> Sem effs a)
-> (TypedTweak tweakEffs b -> Ltl (UntypedTweak tweakEffs))
-> TypedTweak tweakEffs b
-> Sem effs a
-> Sem effs a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ltl (UntypedTweak tweakEffs) -> Ltl (UntypedTweak tweakEffs)
forall a. Ltl a -> Ltl a
ltlEventually (Ltl (UntypedTweak tweakEffs) -> Ltl (UntypedTweak tweakEffs))
-> (TypedTweak tweakEffs b -> Ltl (UntypedTweak tweakEffs))
-> TypedTweak tweakEffs b
-> Ltl (UntypedTweak tweakEffs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedTweak tweakEffs b -> Ltl (UntypedTweak tweakEffs)
forall (tweakEffs :: [(* -> *) -> * -> *]) a.
TypedTweak tweakEffs a -> Ltl (UntypedTweak tweakEffs)
fromTweak

-- | Applies a 'Tweak' to every transaction in a given trace. Fails if the tweak
-- fails anywhere in the trace.
everywhere ::
  (Members '[ModifyGlobally (UntypedTweak tweakEffs)] effs) =>
  TypedTweak tweakEffs b ->
  Sem effs a ->
  Sem effs a
everywhere :: forall (tweakEffs :: [(* -> *) -> * -> *])
       (effs :: [(* -> *) -> * -> *]) b a.
Members '[ModifyGlobally (UntypedTweak tweakEffs)] effs =>
TypedTweak tweakEffs b -> Sem effs a -> Sem effs a
everywhere = Ltl (UntypedTweak tweakEffs) -> Sem effs a -> Sem effs a
forall a (r :: [(* -> *) -> * -> *]) b.
Member (ModifyGlobally a) r =>
Ltl a -> Sem r b -> Sem r b
modifyLtl (Ltl (UntypedTweak tweakEffs) -> Sem effs a -> Sem effs a)
-> (TypedTweak tweakEffs b -> Ltl (UntypedTweak tweakEffs))
-> TypedTweak tweakEffs b
-> Sem effs a
-> Sem effs a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ltl (UntypedTweak tweakEffs) -> Ltl (UntypedTweak tweakEffs)
forall a. Ltl a -> Ltl a
ltlAlways (Ltl (UntypedTweak tweakEffs) -> Ltl (UntypedTweak tweakEffs))
-> (TypedTweak tweakEffs b -> Ltl (UntypedTweak tweakEffs))
-> TypedTweak tweakEffs b
-> Ltl (UntypedTweak tweakEffs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedTweak tweakEffs b -> Ltl (UntypedTweak tweakEffs)
forall (tweakEffs :: [(* -> *) -> * -> *]) a.
TypedTweak tweakEffs a -> Ltl (UntypedTweak tweakEffs)
fromTweak

-- | Ensures a given 'Tweak' can never successfully be applied in a computation,
-- and leaves the computation unchanged.
nowhere ::
  (Members '[ModifyGlobally (UntypedTweak tweakEffs)] effs) =>
  TypedTweak tweakEffs b ->
  Sem effs a ->
  Sem effs a
nowhere :: forall (tweakEffs :: [(* -> *) -> * -> *])
       (effs :: [(* -> *) -> * -> *]) b a.
Members '[ModifyGlobally (UntypedTweak tweakEffs)] effs =>
TypedTweak tweakEffs b -> Sem effs a -> Sem effs a
nowhere = Ltl (UntypedTweak tweakEffs) -> Sem effs a -> Sem effs a
forall a (r :: [(* -> *) -> * -> *]) b.
Member (ModifyGlobally a) r =>
Ltl a -> Sem r b -> Sem r b
modifyLtl (Ltl (UntypedTweak tweakEffs) -> Sem effs a -> Sem effs a)
-> (TypedTweak tweakEffs b -> Ltl (UntypedTweak tweakEffs))
-> TypedTweak tweakEffs b
-> Sem effs a
-> Sem effs a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ltl (UntypedTweak tweakEffs) -> Ltl (UntypedTweak tweakEffs)
forall a. Ltl a -> Ltl a
ltlNever (Ltl (UntypedTweak tweakEffs) -> Ltl (UntypedTweak tweakEffs))
-> (TypedTweak tweakEffs b -> Ltl (UntypedTweak tweakEffs))
-> TypedTweak tweakEffs b
-> Ltl (UntypedTweak tweakEffs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedTweak tweakEffs b -> Ltl (UntypedTweak tweakEffs)
forall (tweakEffs :: [(* -> *) -> * -> *]) a.
TypedTweak tweakEffs a -> Ltl (UntypedTweak tweakEffs)
fromTweak

-- | Apply a given 'Tweak' at every location in a computation where it does not
-- fail, which might never occur.
whenAble ::
  (Members '[ModifyGlobally (UntypedTweak tweakEffs)] effs) =>
  TypedTweak tweakEffs b ->
  Sem effs a ->
  Sem effs a
whenAble :: forall (tweakEffs :: [(* -> *) -> * -> *])
       (effs :: [(* -> *) -> * -> *]) b a.
Members '[ModifyGlobally (UntypedTweak tweakEffs)] effs =>
TypedTweak tweakEffs b -> Sem effs a -> Sem effs a
whenAble = Ltl (UntypedTweak tweakEffs) -> Sem effs a -> Sem effs a
forall a (r :: [(* -> *) -> * -> *]) b.
Member (ModifyGlobally a) r =>
Ltl a -> Sem r b -> Sem r b
modifyLtl (Ltl (UntypedTweak tweakEffs) -> Sem effs a -> Sem effs a)
-> (TypedTweak tweakEffs b -> Ltl (UntypedTweak tweakEffs))
-> TypedTweak tweakEffs b
-> Sem effs a
-> Sem effs a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ltl (UntypedTweak tweakEffs) -> Ltl (UntypedTweak tweakEffs)
forall a. Ltl a -> Ltl a
ltlWhenPossible (Ltl (UntypedTweak tweakEffs) -> Ltl (UntypedTweak tweakEffs))
-> (TypedTweak tweakEffs b -> Ltl (UntypedTweak tweakEffs))
-> TypedTweak tweakEffs b
-> Ltl (UntypedTweak tweakEffs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedTweak tweakEffs b -> Ltl (UntypedTweak tweakEffs)
forall (tweakEffs :: [(* -> *) -> * -> *]) a.
TypedTweak tweakEffs a -> Ltl (UntypedTweak tweakEffs)
fromTweak

-- | Apply a 'Tweak' to the (0-indexed) nth transaction in a given
-- trace. Successful when this transaction exists and can be modified.
--
-- See also `Cooked.Tweak.Labels.labelled` to select transactions based on
-- labels instead of their index.
there ::
  (Members '[ModifyGlobally (UntypedTweak tweakEffs)] effs) =>
  Integer ->
  TypedTweak tweakEffs b ->
  Sem effs a ->
  Sem effs a
there :: forall (tweakEffs :: [(* -> *) -> * -> *])
       (effs :: [(* -> *) -> * -> *]) b a.
Members '[ModifyGlobally (UntypedTweak tweakEffs)] effs =>
Integer -> TypedTweak tweakEffs b -> Sem effs a -> Sem effs a
there Integer
n = Ltl (UntypedTweak tweakEffs) -> Sem effs a -> Sem effs a
forall a (r :: [(* -> *) -> * -> *]) b.
Member (ModifyGlobally a) r =>
Ltl a -> Sem r b -> Sem r b
modifyLtl (Ltl (UntypedTweak tweakEffs) -> Sem effs a -> Sem effs a)
-> (TypedTweak tweakEffs b -> Ltl (UntypedTweak tweakEffs))
-> TypedTweak tweakEffs b
-> Sem effs a
-> Sem effs a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer
-> Ltl (UntypedTweak tweakEffs) -> Ltl (UntypedTweak tweakEffs)
forall a. Integer -> Ltl a -> Ltl a
ltlDelay Integer
n (Ltl (UntypedTweak tweakEffs) -> Ltl (UntypedTweak tweakEffs))
-> (TypedTweak tweakEffs b -> Ltl (UntypedTweak tweakEffs))
-> TypedTweak tweakEffs b
-> Ltl (UntypedTweak tweakEffs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedTweak tweakEffs b -> Ltl (UntypedTweak tweakEffs)
forall (tweakEffs :: [(* -> *) -> * -> *]) a.
TypedTweak tweakEffs a -> Ltl (UntypedTweak tweakEffs)
fromTweak

-- | Apply a 'Tweak' to the next transaction in the given trace. The order of
-- arguments enables an idiom like
--
-- > do ...
-- >    endpoint arguments `withTweak` someModification
-- >    ...
--
-- where @endpoint@ builds and validates a single transaction depending on the
-- given @arguments@. Then `withTweak` says "I want to modify the transaction
-- returned by this endpoint in the following way".
withTweak ::
  (Members '[ModifyGlobally (UntypedTweak tweakEffs)] effs) =>
  Sem effs a ->
  TypedTweak tweakEffs b ->
  Sem effs a
withTweak :: forall (tweakEffs :: [(* -> *) -> * -> *])
       (effs :: [(* -> *) -> * -> *]) a b.
Members '[ModifyGlobally (UntypedTweak tweakEffs)] effs =>
Sem effs a -> TypedTweak tweakEffs b -> Sem effs a
withTweak = (TypedTweak tweakEffs b -> Sem effs a -> Sem effs a)
-> Sem effs a -> TypedTweak tweakEffs b -> Sem effs a
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Integer -> TypedTweak tweakEffs b -> Sem effs a -> Sem effs a
forall (tweakEffs :: [(* -> *) -> * -> *])
       (effs :: [(* -> *) -> * -> *]) b a.
Members '[ModifyGlobally (UntypedTweak tweakEffs)] effs =>
Integer -> TypedTweak tweakEffs b -> Sem effs a -> Sem effs a
there Integer
0)

-- | Reinterpretes `MockChainWrite` in itself, when the `ModifyLocally` effect
-- exists in the stack, applying the relevant modifications in the process.
reinterpretMockChainWriteWithTweak ::
  forall tweakEffs effs a.
  ( Members
      '[ ModifyLocally (UntypedTweak tweakEffs),
         NonDet
       ]
      effs,
    Subsume tweakEffs effs
  ) =>
  Sem (MockChainWrite : effs) a ->
  Sem (MockChainWrite : effs) a
reinterpretMockChainWriteWithTweak :: forall (tweakEffs :: [(* -> *) -> * -> *])
       (effs :: [(* -> *) -> * -> *]) a.
(Members '[ModifyLocally (UntypedTweak tweakEffs), NonDet] effs,
 Subsume tweakEffs effs) =>
Sem (MockChainWrite : effs) a -> Sem (MockChainWrite : effs) a
reinterpretMockChainWriteWithTweak = forall (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *)
       (r :: [(* -> *) -> * -> *]) a.
FirstOrder e1 "reinterpret" =>
(forall (rInitial :: [(* -> *) -> * -> *]) x.
 e1 (Sem rInitial) x -> Sem (e2 : r) x)
-> Sem (e1 : r) a -> Sem (e2 : r) a
reinterpret @MockChainWrite ((forall (rInitial :: [(* -> *) -> * -> *]) x.
  MockChainWrite (Sem rInitial) x -> Sem (MockChainWrite : effs) x)
 -> Sem (MockChainWrite : effs) a -> Sem (MockChainWrite : effs) a)
-> (forall (rInitial :: [(* -> *) -> * -> *]) x.
    MockChainWrite (Sem rInitial) x -> Sem (MockChainWrite : effs) x)
-> Sem (MockChainWrite : effs) a
-> Sem (MockChainWrite : effs) a
forall a b. (a -> b) -> a -> b
$ \case
  ValidateTxSkel TxSkel
skel -> do
    [Requirement (UntypedTweak tweakEffs)]
requirements <- Sem (MockChainWrite : effs) [Requirement (UntypedTweak tweakEffs)]
forall a (effs :: [(* -> *) -> * -> *]).
Member (ModifyLocally a) effs =>
Sem effs [Requirement a]
getRequirements
    let TypedTweak tweakEffs ()
sumTweak :: TypedTweak tweakEffs () =
          (Requirement (UntypedTweak tweakEffs)
 -> TypedTweak tweakEffs () -> TypedTweak tweakEffs ())
-> TypedTweak tweakEffs ()
-> [Requirement (UntypedTweak tweakEffs)]
-> TypedTweak tweakEffs ()
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
            ( \Requirement (UntypedTweak tweakEffs)
req TypedTweak tweakEffs ()
acc -> case Requirement (UntypedTweak tweakEffs)
req of
                Apply (UntypedTweak TypedTweak tweakEffs a
tweak) -> TypedTweak tweakEffs a
tweak TypedTweak tweakEffs a
-> TypedTweak tweakEffs () -> TypedTweak tweakEffs ()
forall a b.
Sem (Tweak : NonDet : tweakEffs) a
-> Sem (Tweak : NonDet : tweakEffs) b
-> Sem (Tweak : NonDet : tweakEffs) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> TypedTweak tweakEffs ()
acc
                EnsureFailure (UntypedTweak TypedTweak tweakEffs a
tweak) -> do
                  TxSkel
txSkel' <- Sem (Tweak : NonDet : tweakEffs) TxSkel
forall (r :: [(* -> *) -> * -> *]). Member Tweak r => Sem r TxSkel
getTxSkel
                  [(TxSkel, a)]
results <- Sem tweakEffs [(TxSkel, a)]
-> Sem (Tweak : NonDet : tweakEffs) [(TxSkel, a)]
forall (r :: [(* -> *) -> * -> *]) (r' :: [(* -> *) -> * -> *]) a.
Raise r r' =>
Sem r a -> Sem r' a
raise_ (Sem tweakEffs [(TxSkel, a)]
 -> Sem (Tweak : NonDet : tweakEffs) [(TxSkel, a)])
-> Sem tweakEffs [(TxSkel, a)]
-> Sem (Tweak : NonDet : tweakEffs) [(TxSkel, a)]
forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) (r :: [(* -> *) -> * -> *]) a.
Alternative f =>
Sem (NonDet : r) a -> Sem r (f a)
runNonDet @[] (Sem (NonDet : tweakEffs) (TxSkel, a)
 -> Sem tweakEffs [(TxSkel, a)])
-> Sem (NonDet : tweakEffs) (TxSkel, a)
-> Sem tweakEffs [(TxSkel, a)]
forall a b. (a -> b) -> a -> b
$ TxSkel
-> TypedTweak tweakEffs a -> Sem (NonDet : tweakEffs) (TxSkel, a)
forall (effs :: [(* -> *) -> * -> *]) a.
TxSkel -> Sem (Tweak : effs) a -> Sem effs (TxSkel, a)
runTweak TxSkel
txSkel' TypedTweak tweakEffs a
tweak
                  Bool -> TypedTweak tweakEffs ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> TypedTweak tweakEffs ())
-> Bool -> TypedTweak tweakEffs ()
forall a b. (a -> b) -> a -> b
$ [(TxSkel, a)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(TxSkel, a)]
results
                  TypedTweak tweakEffs ()
acc
            )
            (() -> TypedTweak tweakEffs ()
forall a. a -> Sem (Tweak : NonDet : tweakEffs) a
forall (m :: * -> *) a. Monad m => a -> m a
return ())
            [Requirement (UntypedTweak tweakEffs)]
requirements
    TxSkel
newTxSkel <- Sem effs TxSkel -> Sem (MockChainWrite : effs) TxSkel
forall (e :: (* -> *) -> * -> *) (r :: [(* -> *) -> * -> *]) a.
Sem r a -> Sem (e : r) a
raise (Sem effs TxSkel -> Sem (MockChainWrite : effs) TxSkel)
-> Sem effs TxSkel -> Sem (MockChainWrite : effs) TxSkel
forall a b. (a -> b) -> a -> b
$ Sem (NonDet : tweakEffs) TxSkel -> Sem effs TxSkel
forall (r :: [(* -> *) -> * -> *]) (r' :: [(* -> *) -> * -> *]) a.
Subsume r r' =>
Sem r a -> Sem r' a
subsume_ (Sem (NonDet : tweakEffs) TxSkel -> Sem effs TxSkel)
-> Sem (NonDet : tweakEffs) TxSkel -> Sem effs TxSkel
forall a b. (a -> b) -> a -> b
$ (TxSkel, ()) -> TxSkel
forall a b. (a, b) -> a
fst ((TxSkel, ()) -> TxSkel)
-> Sem (NonDet : tweakEffs) (TxSkel, ())
-> Sem (NonDet : tweakEffs) TxSkel
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TxSkel
-> TypedTweak tweakEffs () -> Sem (NonDet : tweakEffs) (TxSkel, ())
forall (effs :: [(* -> *) -> * -> *]) a.
TxSkel -> Sem (Tweak : effs) a -> Sem effs (TxSkel, a)
runTweak TxSkel
skel TypedTweak tweakEffs ()
sumTweak
    TxSkel -> Sem (MockChainWrite : effs) (CardanoTx, Utxos)
forall (effs :: [(* -> *) -> * -> *]).
Member MockChainWrite effs =>
TxSkel -> Sem effs (CardanoTx, Utxos)
validateTxSkel TxSkel
newTxSkel
  MockChainWrite (Sem rInitial) x
a -> MockChainWrite (Sem (MockChainWrite : effs)) x
-> Sem (MockChainWrite : effs) x
forall (e :: (* -> *) -> * -> *) (r :: [(* -> *) -> * -> *]) a.
Member e r =>
e (Sem r) a -> Sem r a
send (MockChainWrite (Sem (MockChainWrite : effs)) x
 -> Sem (MockChainWrite : effs) x)
-> MockChainWrite (Sem (MockChainWrite : effs)) x
-> Sem (MockChainWrite : effs) x
forall a b. (a -> b) -> a -> b
$ MockChainWrite (Sem rInitial) x
-> MockChainWrite (Sem (MockChainWrite : effs)) x
forall a b. Coercible a b => a -> b
coerce MockChainWrite (Sem rInitial) x
a