{- |
Module     : Agora.Effect
Maintainer : emi@haskell.fyi
Description: Helpers for constructing effects

Helpers for constructing effects.
-}
module Agora.Effect (makeEffect) where

import Agora.AuthorityToken (singleAuthorityTokenBurned)
import Plutarch.Api.V1 (PCurrencySymbol, PScriptPurpose (PSpending), PTxInfo, PTxOutRef, PValidator, PValue)
import Plutarch.Extra.TermCont (pguardC, pletC, pmatchC, ptryFromC)
import Plutarch.TryFrom ()
import PlutusLedgerApi.V1.Value (CurrencySymbol)

{- | Helper "template" for creating effect validator.

     In some situations, it may be the case that we need more control over how
     an effect is implemented. In such situations, it's okay to not use this
     helper.

     @since 0.1.0
-}
makeEffect ::
  forall (datum :: PType).
  (PIsData datum, PTryFrom PData (PAsData datum)) =>
  CurrencySymbol ->
  (forall (s :: S). Term s PCurrencySymbol -> Term s datum -> Term s PTxOutRef -> Term s (PAsData PTxInfo) -> Term s POpaque) ->
  ClosedTerm PValidator
makeEffect :: forall (datum :: PType).
(PIsData datum, PTryFrom PData (PAsData datum)) =>
CurrencySymbol
-> (forall (s :: S).
    Term s PCurrencySymbol
    -> Term s datum
    -> Term s PTxOutRef
    -> Term s (PAsData PTxInfo)
    -> Term s POpaque)
-> ClosedTerm PValidator
makeEffect CurrencySymbol
gatCs' forall (s :: S).
Term s PCurrencySymbol
-> Term s datum
-> Term s PTxOutRef
-> Term s (PAsData PTxInfo)
-> Term s POpaque
f =
  (Term s PData
 -> Term s PData -> Term s PScriptContext -> Term s POpaque)
-> Term s PValidator
forall a (b :: PType) (s :: S) (c :: PType).
PLamN a b s =>
(Term s c -> a) -> Term s (c :--> b)
plam ((Term s PData
  -> Term s PData -> Term s PScriptContext -> Term s POpaque)
 -> Term s PValidator)
-> (Term s PData
    -> Term s PData -> Term s PScriptContext -> Term s POpaque)
-> Term s PValidator
forall a b. (a -> b) -> a -> b
$ \Term s PData
datum Term s PData
_redeemer Term s PScriptContext
ctx' -> TermCont @POpaque s (Term s POpaque) -> Term s POpaque
forall (a :: PType) (s :: S). TermCont @a s (Term s a) -> Term s a
unTermCont (TermCont @POpaque s (Term s POpaque) -> Term s POpaque)
-> TermCont @POpaque s (Term s POpaque) -> Term s POpaque
forall a b. (a -> b) -> a -> b
$ do
    HRec
  (BoundTerms
     (PFields PScriptContext)
     (Bindings
        (PFields PScriptContext)
        ((':) @Symbol "txInfo" ((':) @Symbol "purpose" ('[] @Symbol))))
     s)
ctx <- ((HRec
    (BoundTerms
       (PFields PScriptContext)
       (Bindings
          (PFields PScriptContext)
          ((':) @Symbol "txInfo" ((':) @Symbol "purpose" ('[] @Symbol))))
       s)
  -> Term s POpaque)
 -> Term s POpaque)
-> TermCont
     @POpaque
     s
     (HRec
        (BoundTerms
           (PFields PScriptContext)
           (Bindings
              (PFields PScriptContext)
              ((':) @Symbol "txInfo" ((':) @Symbol "purpose" ('[] @Symbol))))
           s))
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((HRec
     (BoundTerms
        (PFields PScriptContext)
        (Bindings
           (PFields PScriptContext)
           ((':) @Symbol "txInfo" ((':) @Symbol "purpose" ('[] @Symbol))))
        s)
   -> Term s POpaque)
  -> Term s POpaque)
 -> TermCont
      @POpaque
      s
      (HRec
         (BoundTerms
            (PFields PScriptContext)
            (Bindings
               (PFields PScriptContext)
               ((':) @Symbol "txInfo" ((':) @Symbol "purpose" ('[] @Symbol))))
            s)))
-> ((HRec
       (BoundTerms
          (PFields PScriptContext)
          (Bindings
             (PFields PScriptContext)
             ((':) @Symbol "txInfo" ((':) @Symbol "purpose" ('[] @Symbol))))
          s)
     -> Term s POpaque)
    -> Term s POpaque)
-> TermCont
     @POpaque
     s
     (HRec
        (BoundTerms
           (PFields PScriptContext)
           (Bindings
              (PFields PScriptContext)
              ((':) @Symbol "txInfo" ((':) @Symbol "purpose" ('[] @Symbol))))
           s))
forall a b. (a -> b) -> a -> b
$ forall (fs :: [Symbol]) (a :: PType) (s :: S) (b :: PType)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(PDataFields a,
 (ps :: [PLabeledType]) ~ (PFields a :: [PLabeledType]),
 (bs :: [ToBind]) ~ (Bindings ps fs :: [ToBind]),
 BindFields ps bs) =>
Term s a -> (HRecOf a fs s -> Term s b) -> Term s b
pletFields @'["txInfo", "purpose"] Term s PScriptContext
ctx'
    Term s (PAsData PTxInfo)
txInfo' <- Term s (PAsData PTxInfo)
-> TermCont @POpaque s (Term s (PAsData PTxInfo))
forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont @r s (Term s a)
pletC HRec
  (BoundTerms
     (PFields PScriptContext)
     (Bindings
        (PFields PScriptContext)
        ((':) @Symbol "txInfo" ((':) @Symbol "purpose" ('[] @Symbol))))
     s)
ctx.txInfo

    -- convert input datum, PData, into desierable type
    -- the way this conversion is performed should be defined
    -- by PTryFrom for each datum in effect script.
    (Term s (PAsData datum) -> Term s datum
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData -> Term s datum
datum', Reduce @Type (PTryFromExcess PData (PAsData datum) s)
_) <- Term s PData
-> TermCont
     @POpaque
     s
     (Term s (PAsData datum),
      Reduce @Type (PTryFromExcess PData (PAsData datum) s))
forall (b :: PType) (r :: PType) (a :: PType) (s :: S).
PTryFrom a b =>
Term s a
-> TermCont @r s (Term s b, Reduce @Type (PTryFromExcess a b s))
ptryFromC Term s PData
datum

    -- ensure purpose is Spending.
    PSpending Term
  s
  (PDataRecord
     ((':) @PLabeledType ("_0" ':= PTxOutRef) ('[] @PLabeledType)))
txOutRef <- Term s PScriptPurpose -> TermCont @POpaque s (PScriptPurpose s)
forall {r :: PType} (a :: PType) (s :: S).
PMatch a =>
Term s a -> TermCont @r s (a s)
pmatchC (Term s PScriptPurpose -> TermCont @POpaque s (PScriptPurpose s))
-> Term s PScriptPurpose -> TermCont @POpaque s (PScriptPurpose s)
forall a b. (a -> b) -> a -> b
$ Term s (PAsData PScriptPurpose) -> Term s PScriptPurpose
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData HRec
  (BoundTerms
     (PFields PScriptContext)
     (Bindings
        (PFields PScriptContext)
        ((':) @Symbol "txInfo" ((':) @Symbol "purpose" ('[] @Symbol))))
     s)
ctx.purpose
    Term s PTxOutRef
txOutRef' <- Term s PTxOutRef -> TermCont @POpaque s (Term s PTxOutRef)
forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont @r s (Term s a)
pletC (forall (name :: Symbol) (p :: PType) (s :: S) (a :: PType)
       (as :: [PLabeledType]) (n :: Nat) (b :: PType).
(PDataFields p,
 (as :: [PLabeledType]) ~ (PFields p :: [PLabeledType]),
 (n :: Nat) ~ (PLabelIndex name as :: Nat), KnownNat n,
 (a :: PType) ~ (PUnLabel (IndexList @PLabeledType n as) :: PType),
 PFromDataable a b) =>
Term s (p :--> b)
pfield @"_0" Term
  s
  (PDataRecord
     ((':) @PLabeledType ("_0" ':= PTxOutRef) ('[] @PLabeledType))
   :--> PTxOutRef)
-> Term
     s
     (PDataRecord
        ((':) @PLabeledType ("_0" ':= PTxOutRef) ('[] @PLabeledType)))
-> Term s PTxOutRef
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term
  s
  (PDataRecord
     ((':) @PLabeledType ("_0" ':= PTxOutRef) ('[] @PLabeledType)))
txOutRef)

    -- fetch minted values to ensure single GAT is burned
    HRec
  ((':)
     @(Symbol, Type)
     '("mint", Term s (PAsData (PValue 'Sorted 'NoGuarantees)))
     ('[] @(Symbol, Type)))
txInfo <- ((HRec
    ((':)
       @(Symbol, Type)
       '("mint", Term s (PAsData (PValue 'Sorted 'NoGuarantees)))
       ('[] @(Symbol, Type)))
  -> Term s POpaque)
 -> Term s POpaque)
-> TermCont
     @POpaque
     s
     (HRec
        ((':)
           @(Symbol, Type)
           '("mint", Term s (PAsData (PValue 'Sorted 'NoGuarantees)))
           ('[] @(Symbol, Type))))
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((HRec
     ((':)
        @(Symbol, Type)
        '("mint", Term s (PAsData (PValue 'Sorted 'NoGuarantees)))
        ('[] @(Symbol, Type)))
   -> Term s POpaque)
  -> Term s POpaque)
 -> TermCont
      @POpaque
      s
      (HRec
         ((':)
            @(Symbol, Type)
            '("mint", Term s (PAsData (PValue 'Sorted 'NoGuarantees)))
            ('[] @(Symbol, Type)))))
-> ((HRec
       ((':)
          @(Symbol, Type)
          '("mint", Term s (PAsData (PValue 'Sorted 'NoGuarantees)))
          ('[] @(Symbol, Type)))
     -> Term s POpaque)
    -> Term s POpaque)
-> TermCont
     @POpaque
     s
     (HRec
        ((':)
           @(Symbol, Type)
           '("mint", Term s (PAsData (PValue 'Sorted 'NoGuarantees)))
           ('[] @(Symbol, Type))))
forall a b. (a -> b) -> a -> b
$ forall (fs :: [Symbol]) (a :: PType) (s :: S) (b :: PType)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(PDataFields a,
 (ps :: [PLabeledType]) ~ (PFields a :: [PLabeledType]),
 (bs :: [ToBind]) ~ (Bindings ps fs :: [ToBind]),
 BindFields ps bs) =>
Term s a -> (HRecOf a fs s -> Term s b) -> Term s b
pletFields @'["mint"] Term s (PAsData PTxInfo)
txInfo'
    let mint :: Term _ (PValue _ _)
        mint :: Term s (PValue 'Sorted 'NoGuarantees)
mint = HRec
  ((':)
     @(Symbol, Type)
     '("mint", Term s (PAsData (PValue 'Sorted 'NoGuarantees)))
     ('[] @(Symbol, Type)))
txInfo.mint

    -- fetch script context
    Term s PCurrencySymbol
gatCs <- Term s PCurrencySymbol
-> TermCont @POpaque s (Term s PCurrencySymbol)
forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont @r s (Term s a)
pletC (Term s PCurrencySymbol
 -> TermCont @POpaque s (Term s PCurrencySymbol))
-> Term s PCurrencySymbol
-> TermCont @POpaque s (Term s PCurrencySymbol)
forall a b. (a -> b) -> a -> b
$ PLifted PCurrencySymbol -> Term s PCurrencySymbol
forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant PLifted PCurrencySymbol
CurrencySymbol
gatCs'

    Term s (PString @S) -> Term s PBool -> TermCont @POpaque s ()
forall {r :: PType} (s :: S).
Term s (PString @S) -> Term s PBool -> TermCont @r s ()
pguardC Term s (PString @S)
"A single authority token has been burned" (Term s PBool -> TermCont @POpaque s ())
-> Term s PBool -> TermCont @POpaque s ()
forall a b. (a -> b) -> a -> b
$ Term s PCurrencySymbol
-> Term s (PAsData PTxInfo)
-> Term s (PValue 'Sorted 'NoGuarantees)
-> Term s PBool
forall (keys :: KeyGuarantees) (amounts :: AmountGuarantees)
       (s :: S).
Term s PCurrencySymbol
-> Term s (PAsData PTxInfo)
-> Term s (PValue keys amounts)
-> Term s PBool
singleAuthorityTokenBurned Term s PCurrencySymbol
gatCs Term s (PAsData PTxInfo)
txInfo' Term s (PValue 'Sorted 'NoGuarantees)
mint

    -- run effect function
    Term s POpaque -> TermCont @POpaque s (Term s POpaque)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s POpaque -> TermCont @POpaque s (Term s POpaque))
-> Term s POpaque -> TermCont @POpaque s (Term s POpaque)
forall a b. (a -> b) -> a -> b
$ Term s PCurrencySymbol
-> Term s datum
-> Term s PTxOutRef
-> Term s (PAsData PTxInfo)
-> Term s POpaque
forall (s :: S).
Term s PCurrencySymbol
-> Term s datum
-> Term s PTxOutRef
-> Term s (PAsData PTxInfo)
-> Term s POpaque
f Term s PCurrencySymbol
gatCs Term s datum
datum' Term s PTxOutRef
txOutRef' Term s (PAsData PTxInfo)
txInfo'