-- | This module exposes the certificate constructs used in a
-- 'Cooked.Skeleton.TxSkel' and their associated utilities. To emit certificates
-- in a skeleton, the usual way is to invoke @txSkelCertificates =
-- [pubKeyCertificate pk action, scriptCertificate script redeemer action ...]@
module Cooked.Skeleton.Certificate
  ( -- * Data types
    CertificateAction (..),
    TxSkelCertificate (..),

    -- * Optics
    txSkelCertificateOwnerAT,
    txSkelCertificateActionAT,

    -- * Smart constructors
    pubKeyCertificate,
    scriptCertificate,
  )
where

import Cooked.Skeleton.Families
import Cooked.Skeleton.Redeemer
import Cooked.Skeleton.User
import Data.Kind (Type)
import Data.Typeable (Typeable, cast)
import Ledger.Slot qualified as Ledger
import Optics.Core
import Plutus.Script.Utils.Address qualified as Script
import PlutusLedgerApi.V3 qualified as Api

-- | The depiction of the possible actions in a certificate. Each actions
-- exposes, in its types, the possible owners it can have.
data CertificateAction :: UserKind -> Type where
  StakingRegister :: CertificateAction IsEither
  StakingUnRegister :: CertificateAction IsEither
  StakingDelegate :: Api.Delegatee -> CertificateAction IsEither
  StakingRegisterDelegate :: Api.Delegatee -> CertificateAction IsEither
  DRepRegister :: CertificateAction IsEither
  DRepUpdate :: CertificateAction IsEither
  DRepUnRegister :: CertificateAction IsEither
  PoolRegister :: Api.PubKeyHash -> CertificateAction IsPubKey
  PoolRetire :: Ledger.Slot -> CertificateAction IsPubKey
  CommitteeRegisterHot :: Api.Credential -> CertificateAction IsEither
  CommitteeResign :: CertificateAction IsEither

deriving instance (Show (CertificateAction req))

deriving instance (Eq (CertificateAction req))

-- | Certificates used in 'Cooked.Skeleton.TxSkel'. The types ensure that each
-- certificate action is associated with a proper owner.
data TxSkelCertificate where
  TxSkelCertificate ::
    (Typeable kind) =>
    { -- | All owners of certificates must be in 'Redemption' mode
      ()
txSkelCertificateOwner :: User kind Redemption,
      -- | The certificate itself does impose a 'UserKind'
      ()
txSkelCertificateAction :: CertificateAction kind
    } ->
    TxSkelCertificate

deriving instance (Show TxSkelCertificate)

instance Eq TxSkelCertificate where
  (TxSkelCertificate User kind 'Redemption
owner CertificateAction kind
action) == :: TxSkelCertificate -> TxSkelCertificate -> Bool
== (TxSkelCertificate User kind 'Redemption
owner' CertificateAction kind
action') =
    User kind 'Redemption -> Maybe (User kind 'Redemption)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast User kind 'Redemption
owner Maybe (User kind 'Redemption)
-> Maybe (User kind 'Redemption) -> Bool
forall a. Eq a => a -> a -> Bool
== User kind 'Redemption -> Maybe (User kind 'Redemption)
forall a. a -> Maybe a
Just User kind 'Redemption
owner' Bool -> Bool -> Bool
&& CertificateAction kind -> Maybe (CertificateAction kind)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast CertificateAction kind
action Maybe (CertificateAction kind)
-> Maybe (CertificateAction kind) -> Bool
forall a. Eq a => a -> a -> Bool
== CertificateAction kind -> Maybe (CertificateAction kind)
forall a. a -> Maybe a
Just CertificateAction kind
action'

-- | Focuses on the owner of a 'TxSkelCertificate'
txSkelCertificateOwnerAT :: (Typeable user) => AffineTraversal' TxSkelCertificate (User user Redemption)
txSkelCertificateOwnerAT :: forall (user :: UserKind).
Typeable user =>
AffineTraversal' TxSkelCertificate (User user 'Redemption)
txSkelCertificateOwnerAT =
  (TxSkelCertificate
 -> Either TxSkelCertificate (User user 'Redemption))
-> (TxSkelCertificate
    -> User user 'Redemption -> TxSkelCertificate)
-> AffineTraversal
     TxSkelCertificate
     TxSkelCertificate
     (User user 'Redemption)
     (User user 'Redemption)
forall s t a b.
(s -> Either t a) -> (s -> b -> t) -> AffineTraversal s t a b
atraversal
    (\cert :: TxSkelCertificate
cert@(TxSkelCertificate {User kind 'Redemption
txSkelCertificateOwner :: ()
txSkelCertificateOwner :: User kind 'Redemption
txSkelCertificateOwner}) -> Either TxSkelCertificate (User user 'Redemption)
-> (User user 'Redemption
    -> Either TxSkelCertificate (User user 'Redemption))
-> Maybe (User user 'Redemption)
-> Either TxSkelCertificate (User user 'Redemption)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (TxSkelCertificate
-> Either TxSkelCertificate (User user 'Redemption)
forall a b. a -> Either a b
Left TxSkelCertificate
cert) User user 'Redemption
-> Either TxSkelCertificate (User user 'Redemption)
forall a b. b -> Either a b
Right (Maybe (User user 'Redemption)
 -> Either TxSkelCertificate (User user 'Redemption))
-> Maybe (User user 'Redemption)
-> Either TxSkelCertificate (User user 'Redemption)
forall a b. (a -> b) -> a -> b
$ User kind 'Redemption -> Maybe (User user 'Redemption)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast User kind 'Redemption
txSkelCertificateOwner)
    (\cert :: TxSkelCertificate
cert@(TxSkelCertificate @user' User kind 'Redemption
_ CertificateAction kind
action) -> TxSkelCertificate
-> (User kind 'Redemption -> TxSkelCertificate)
-> Maybe (User kind 'Redemption)
-> TxSkelCertificate
forall b a. b -> (a -> b) -> Maybe a -> b
maybe TxSkelCertificate
cert (User kind 'Redemption
-> CertificateAction kind -> TxSkelCertificate
forall (kind :: UserKind).
Typeable kind =>
User kind 'Redemption
-> CertificateAction kind -> TxSkelCertificate
`TxSkelCertificate` CertificateAction kind
action) (Maybe (User kind 'Redemption) -> TxSkelCertificate)
-> (User user 'Redemption -> Maybe (User kind 'Redemption))
-> User user 'Redemption
-> TxSkelCertificate
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast @_ @(User user' Redemption))

-- | Focuses on the action of a 'TxSkelCertificate'
txSkelCertificateActionAT :: (Typeable user) => AffineTraversal' TxSkelCertificate (CertificateAction user)
txSkelCertificateActionAT :: forall (user :: UserKind).
Typeable user =>
AffineTraversal' TxSkelCertificate (CertificateAction user)
txSkelCertificateActionAT =
  (TxSkelCertificate
 -> Either TxSkelCertificate (CertificateAction user))
-> (TxSkelCertificate
    -> CertificateAction user -> TxSkelCertificate)
-> AffineTraversal
     TxSkelCertificate
     TxSkelCertificate
     (CertificateAction user)
     (CertificateAction user)
forall s t a b.
(s -> Either t a) -> (s -> b -> t) -> AffineTraversal s t a b
atraversal
    (\cert :: TxSkelCertificate
cert@(TxSkelCertificate {CertificateAction kind
txSkelCertificateAction :: ()
txSkelCertificateAction :: CertificateAction kind
txSkelCertificateAction}) -> Either TxSkelCertificate (CertificateAction user)
-> (CertificateAction user
    -> Either TxSkelCertificate (CertificateAction user))
-> Maybe (CertificateAction user)
-> Either TxSkelCertificate (CertificateAction user)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (TxSkelCertificate
-> Either TxSkelCertificate (CertificateAction user)
forall a b. a -> Either a b
Left TxSkelCertificate
cert) CertificateAction user
-> Either TxSkelCertificate (CertificateAction user)
forall a b. b -> Either a b
Right (Maybe (CertificateAction user)
 -> Either TxSkelCertificate (CertificateAction user))
-> Maybe (CertificateAction user)
-> Either TxSkelCertificate (CertificateAction user)
forall a b. (a -> b) -> a -> b
$ CertificateAction kind -> Maybe (CertificateAction user)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast CertificateAction kind
txSkelCertificateAction)
    (\cert :: TxSkelCertificate
cert@(TxSkelCertificate @user' User kind 'Redemption
owner CertificateAction kind
_) -> TxSkelCertificate
-> (CertificateAction kind -> TxSkelCertificate)
-> Maybe (CertificateAction kind)
-> TxSkelCertificate
forall b a. b -> (a -> b) -> Maybe a -> b
maybe TxSkelCertificate
cert (User kind 'Redemption
-> CertificateAction kind -> TxSkelCertificate
forall (kind :: UserKind).
Typeable kind =>
User kind 'Redemption
-> CertificateAction kind -> TxSkelCertificate
TxSkelCertificate User kind 'Redemption
owner) (Maybe (CertificateAction kind) -> TxSkelCertificate)
-> (CertificateAction user -> Maybe (CertificateAction kind))
-> CertificateAction user
-> TxSkelCertificate
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast @_ @(CertificateAction user'))

-- | Smart constructor for a pubkey certificate
pubKeyCertificate :: (Script.ToPubKeyHash pkh, Typeable pkh, Typeable a, a ∈ '[IsPubKey, IsEither]) => pkh -> CertificateAction a -> TxSkelCertificate
pubKeyCertificate :: forall pkh (a :: UserKind).
(ToPubKeyHash pkh, Typeable pkh, Typeable a,
 a ∈ '[ 'IsPubKey, 'IsEither]) =>
pkh -> CertificateAction a -> TxSkelCertificate
pubKeyCertificate pkh
pkh = User a 'Redemption -> CertificateAction a -> TxSkelCertificate
forall (kind :: UserKind).
Typeable kind =>
User kind 'Redemption
-> CertificateAction kind -> TxSkelCertificate
TxSkelCertificate (pkh -> User a 'Redemption
forall pkh (a :: UserKind) (b :: UserMode).
(a ∈ '[ 'IsPubKey, 'IsEither], ToPubKeyHash pkh, Typeable pkh) =>
pkh -> User a b
UserPubKey pkh
pkh)

-- | Smart constructor for a script certificate
scriptCertificate :: (ToVScript script, Typeable script, RedeemerConstrs red) => script -> red -> CertificateAction IsEither -> TxSkelCertificate
scriptCertificate :: forall script red.
(ToVScript script, Typeable script, RedeemerConstrs red) =>
script -> red -> CertificateAction 'IsEither -> TxSkelCertificate
scriptCertificate script
script red
red = User 'IsEither 'Redemption
-> CertificateAction 'IsEither -> TxSkelCertificate
forall (kind :: UserKind).
Typeable kind =>
User kind 'Redemption
-> CertificateAction kind -> TxSkelCertificate
TxSkelCertificate (script -> TxSkelRedeemer -> User 'IsEither 'Redemption
forall script (a :: UserKind).
(a ∈ '[ 'IsScript, 'IsEither], ToVScript script,
 Typeable script) =>
script -> TxSkelRedeemer -> User a 'Redemption
UserRedeemedScript script
script (red -> TxSkelRedeemer
forall redeemer.
RedeemerConstrs redeemer =>
redeemer -> TxSkelRedeemer
someTxSkelRedeemer red
red))