-- SPDX-FileCopyrightText: 2022 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA

{-# OPTIONS_HADDOCK not-home #-}

-- | Machinery for the variadic 'transfer' function.
module Test.Cleveland.Internal.Actions.Transfer
  ( module Test.Cleveland.Internal.Actions.Transfer
  ) where

import Data.Constraint (Bottom(..))
import Data.Singletons.TH (SingI(..), genSingletons)
import GHC.TypeLits (ErrorMessage(..), TypeError)

import Lorentz
import Morley.Client.Types
import Morley.Michelson.Typed (Dict(..))
import Morley.Michelson.Untyped qualified as U
import Morley.Tezos.Address
import Test.Cleveland.Internal.Abstract
import Test.Cleveland.Internal.Actions.MonadOps
import Test.Cleveland.Lorentz.Types

-- $setup
-- >>> :m Lorentz.Constraints.Scopes Lorentz.Entrypoints.Core Test.Cleveland

----------------------------------------------------------------------------
-- TransferResult and its singletons
----------------------------------------------------------------------------

-- | Simple flag to track whether we want to return list of emitted events.
data TransferResult = TransferIgnoreResult | TransferWithEmits

-- | Type family encoding the actual 'transfer' result depending on
-- 'TransferResult'
type family FTransferResult emit :: Type where
  FTransferResult 'TransferWithEmits = [ContractEvent]
  FTransferResult 'TransferIgnoreResult = ()

genSingletons [''TransferResult]

{-
Note [TransferResult singletons]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~

If you're wondering why this complicated song and dance with singletons and not
just multiple terminating instances for each 'TransferWithEmits' value, if we
want to keep 'MonadTransfer', we need terminating instances work for any @emit@,
possibly constrained; if we have instances for a specific value, it's ambiguous
which one to choose in 'MonadTransfer'.

They're declared at the top of the file because of TH staging rules.

-- @lierdakil
-}

----------------------------------------------------------------------------
-- transfer
----------------------------------------------------------------------------

{- | Base method for making a transfer.

You can specify additional arguments after the destination address to modify
optional transfer arguments. Those can either be 'Mutez' to specify transfer
amount (0 by default), or a specially constructed call descriptor. The order
is arbitrary, but it is usually more convenient to specify transfer amount
first. For example:

> transfer addr [tz|123u|] $ calling (ep @"Entrypoint") ()
> transfer addr [tz|123u|]

If the call isn't specified, then the default entrypoint will be called with
@()@, i.e.

> transfer addr

is functionally the same as

> transfer addr $ calling def ()

If the address in the first argument is untyped, the transfer is unchecked.
Unchecked transfers must use 'unsafeCalling' for the call specification. You
can also use 'unsafeCalling' with typed address to force an unchecked
transfer.

See "Test.Cleveland.Internal.Actions.Transfer" for further explanation of the
interface.

By default, the sender is the account associated with the @moneybag@ alias.
This can be overridden with the @--cleveland-moneybag-alias@ command line
option, the @TASTY_CLEVELAND_MONEYBAG_ALIAS@ env var, or @withSender@.

In some polymorphic cases, you may need to add 'HasEntrypointArg' constraint:

>>> :{
example
  :: (MonadCleveland caps m, NiceParameter cp)
  => ContractHandle cp st vd -> m ()
example ch = transfer ch (123 :: Mutez)
:}
...
... Can not look up entrypoints in type
...   cp
... The most likely reason it is ambiguous, or you need
...   HasEntrypointArg cp (EntrypointRef 'Nothing) ()
... constraint
...

You can fix this by adding the constraint:

>>> :{
example
  :: ( MonadCleveland caps m, NiceParameter cp
     , HasEntrypointArg cp (EntrypointRef 'Nothing) ())
  => ContractHandle cp st vd -> m ()
example ch = transfer ch (123 :: Mutez)
:}

GHC may not always figure out the type of the entrypoint parameter. In that
case, it'll show unbound type variable, usually @arg0@:

>>> :{
example
  :: (MonadCleveland caps m, NiceParameter cp, NiceParameter arg)
  => ContractHandle cp st vd -> arg -> m ()
example ch x = transfer ch (123 :: Mutez) $ calling def x
:}
...
... Can not look up entrypoints in type
...   cp
... The most likely reason it is ambiguous, or you need
...   HasEntrypointArg cp (EntrypointRef 'Nothing) arg0
... constraint
...

Either specifying a concrete type in the constraint, or leaving it polymorphic,
fixes this:

>>> :{
example
  :: ( MonadCleveland caps m, NiceParameter cp, NiceParameter arg
     , HasEntrypointArg cp (EntrypointRef 'Nothing) Integer)
  => ContractHandle cp st vd -> Integer -> m ()
example ch x = transfer ch (123 :: Mutez) $ calling def x
:}

>>> :{
example
  :: ( MonadCleveland caps m, NiceParameter cp, NiceParameter arg
     , HasEntrypointArg cp (EntrypointRef 'Nothing) arg)
  => ContractHandle cp st vd -> arg -> m ()
example ch x = transfer ch (123 :: Mutez) $ calling def x
:}
-}
transfer :: forall addr r.
            ( HasCallStack
            , TransferFunc ('Incomplete (InitialTransferMode addr))
                'TransferIgnoreResult 'HasNoAmount r
            , ToL1Address addr )
         => addr -> r
transfer = transfer'r @_ @'TransferIgnoreResult @'HasNoAmount . initialData @addr

----------------------------------------------------------------------------
-- Initial transfer data and wrappers
----------------------------------------------------------------------------

-- | Data-kind for tracking what type of call we're making.
data TransferMode = Checked Type | Unchecked | Incomplete TransferMode

-- | Data-kind for call specification.
data GenericCall mode where
  CheckedCall
    :: (NiceParameter epArg, HasEntrypointArg param epRef epArg)
    => epRef -> epArg -> GenericCall ('Checked param)
  UncheckedCall :: NiceParameter epArg => U.EpName -> epArg -> GenericCall 'Unchecked
  UnspecifiedCall :: GenericCall ('Incomplete param)

-- | Generic version of 'TransferData'
data GenericTransferData mode =
  GenericTransferData
  { gtdAddr :: L1Address
  , gtdCall :: GenericCall mode
  , gtdAmount :: Mutez
  }

-- | Choose the initial 'TransferMode' based on the type of destination address.
type family InitialTransferMode addr :: TransferMode where
  InitialTransferMode ContractAddress = 'Unchecked
  InitialTransferMode ImplicitAddress = 'Unchecked
  InitialTransferMode L1Address = 'Unchecked
  InitialTransferMode (L1TAddress param _) = 'Checked param
  InitialTransferMode (ContractHandle param _ _) = 'Checked param
  InitialTransferMode Address = TypeError (
    'Text "'Address' can not be used as the first argument of 'transfer'." ':$$:
    'Text "Perhaps you meant to use 'L1Address'?")
  InitialTransferMode (TAddress _ _) = TypeError (
    'Text "'TAddress' can not be used as the first argument of 'transfer'." ':$$:
    'Text "Perhaps you meant to use 'L1TAddress'?")
  InitialTransferMode x = TypeError (
    'Text "Address type '" ':<>: 'ShowType x ':<>: 'Text "' is unsupported or ambiguous." ':$$:
    'Text "The supported address types are" ':$$:
    'Text "'ContractAddress', 'ImplicitAddress', 'L1Address', 'L1TAddress', and 'ContractHandle'")

-- | Construct initial 'GenericTransferData' for a given address.
initialData
  :: ToL1Address addr
  => addr -> GenericTransferData ('Incomplete (InitialTransferMode addr))
initialData addr = GenericTransferData
  { gtdAddr = toL1Address addr
  , gtdAmount = zeroMutez
  , gtdCall = UnspecifiedCall
  }

----------------------------------------------------------------------------
-- "The printf trick" for transfer
----------------------------------------------------------------------------

-- | Simple flag to track duplicate amount specification.
data HasAmount = HasAmount | HasNoAmount

-- | The class implementing a guarded "printf trick" for the 'transfer' function.
--
-- If you see GHC asking for this constraint, you most likely need to add
-- 'MonadTransfer' constraint on the return monad instead.
class TransferFunc (mode :: TransferMode) (emit :: TransferResult) (hasAmount :: HasAmount) r where
  transfer'r :: HasCallStack => GenericTransferData mode -> r

-- | Type family raising a type error on 'HasAmount' argument. Used to improve
-- error reporting for 'TransferFunc' instances with equality constraints.
type family NoDuplicateAmount am :: Constraint where
  NoDuplicateAmount 'HasAmount = TypeError ('Text "Amount is specified more than once.")
  NoDuplicateAmount 'HasNoAmount = ()

instance (TransferFunc mode emit 'HasAmount r, NoDuplicateAmount am, am ~ 'HasNoAmount)
  => TransferFunc mode emit am (Mutez -> r) where
  transfer'r initData x = transfer'r @_ @emit @'HasAmount initData{gtdAmount = x}

-- | Type family raising a type error on 'TransferWithEmits' argument. Used to
-- improve error reporting for 'TransferFunc' instances with equality
-- constraints.
type family NoDuplicateEmit am :: Constraint where
  NoDuplicateEmit 'TransferWithEmits =
    TypeError ('Text "WithContractEvents is specified more than once.")
  NoDuplicateEmit 'TransferIgnoreResult = ()

instance (TransferFunc mode 'TransferWithEmits am r
  , NoDuplicateEmit emit, emit ~ 'TransferIgnoreResult)
  => TransferFunc mode emit am (WithContractEvents -> r) where
  transfer'r initData _ = transfer'r @_ @'TransferWithEmits @am initData

-- | Type family that defines possible mode conversions in 'TransferFunc'.
-- Basically, we don't allow unchecked calls to become checked, and we require
-- that checked calls do not change the parameter type mid-way.
type family MatchModes from to :: Constraint where
  MatchModes ('Incomplete _) 'Unchecked = ()
  MatchModes ('Incomplete ('Checked param1)) ('Checked param2) = param1 ~ param2
  MatchModes ('Incomplete 'Unchecked) _ = TypeError (
    'Text "Can not use this type of call with an untyped address."
    ':$$: 'Text "Try using 'unsafeCalling' instead."
    )
  MatchModes _ _ = TypeError ('Text "Call is specified more than once.")

instance (TransferFunc modeTo emit am r, MatchModes modeFrom modeTo)
  => TransferFunc modeFrom emit am (GenericCall modeTo -> r) where
  transfer'r GenericTransferData{..} x =
    transfer'r @_ @emit @am $ GenericTransferData{gtdCall = x, ..}

-- | The terminating case for batched transfer
instance ( SingI emit, DoTransfer mode, a ~ FTransferResult emit)
  => TransferFunc mode emit am (ClevelandOpsBatch a) where
  transfer'r = case sing @emit of
    STransferWithEmits -> doTransfer
    STransferIgnoreResult -> void . doTransfer

-- | The terminating case for Cleveland monads
instance ( SingI emit, DoTransfer mode, HasClevelandCaps cap
  , base ~ ClevelandBaseMonad cap, a ~ FTransferResult emit )
  => TransferFunc mode emit am (ReaderT cap base a) where
  transfer'r = case sing @emit of
    STransferWithEmits -> doTransfer
    STransferIgnoreResult -> void . doTransfer

-- | A convenient synonym class to require the terminating instance for a given
-- monad without leaking too much implementation detail.
class (
  forall mod am emit a. (SingI emit, DoTransfer mod, a ~ FTransferResult emit)
    => TransferFunc mod emit am (m a)
  ) => MonadTransfer m
instance (
  forall mod am emit a. (SingI emit, DoTransfer mod, a ~ FTransferResult emit)
    => TransferFunc mod emit am (m a)
  ) => MonadTransfer m

-- | Catchall incoherent instance to report argument errors.
instance {-# INCOHERENT #-}
     ( Bottom
     , TypeError ('Text "Incorrect argument for the 'transfer' function: " ':<>: 'ShowType x ':$$:
                  'Text "If in doubt, try adding a type annotation."))
  => TransferFunc mode emit am (x -> r) where
  transfer'r = no

----------------------------------------------------------------------------
-- Making the actual transfer
----------------------------------------------------------------------------

-- | Typeclass abstracting making the actual transfer.
class DoTransfer mode where
  doTransfer :: (HasCallStack, MonadOpsInternal m) => GenericTransferData mode -> m [ContractEvent]

-- | Make the transfer given 'TransferData'
runTransfer :: (HasCallStack, MonadOpsInternal m) => TransferData -> m [ContractEvent]
runTransfer td = withOpsCap \opsCap ->
  runSingleOperation opsCap "transfer" (OpTransfer td) \case
    OpTransfer ops -> Just ops
    _ -> Nothing

instance DoTransfer 'Unchecked where
  doTransfer GenericTransferData
    { gtdAddr = tdTo
    , gtdAmount = tdAmount
    , gtdCall = UncheckedCall tdEntrypoint tdParameter
    } = runTransfer TransferData{..}

instance DoTransfer ('Checked param) where
  doTransfer GenericTransferData
    { gtdAddr = tdTo
    , gtdAmount = tdAmount
    , gtdCall = CheckedCall (epRef :: epRef) (tdParameter :: epArg)
    } | (Dict, tdEntrypoint) <- useHasEntrypointArg @param @epRef @epArg epRef
      = runTransfer TransferData{..}

instance HasEntrypointArg param (EntrypointRef 'Nothing) ()
  => DoTransfer ('Incomplete ('Checked param)) where
  doTransfer GenericTransferData{..} =
    doTransfer GenericTransferData {gtdCall = calling CallDefault @_ @param (), ..}

instance DoTransfer ('Incomplete 'Unchecked) where
  doTransfer GenericTransferData{..} =
    doTransfer GenericTransferData {gtdCall = unsafeCalling U.DefEpName (), ..}

----------------------------------------------------------------------------
-- Call specification
----------------------------------------------------------------------------

-- | Safely call an entrypoint specified by the first argument with the
-- provided parameter.
--
-- The first character of the entrypoint name must be capitalized.
--
-- This is "safe" in the sense that the contract is checked if it indeed has the
-- specified entrypoint and the entrypoint in question accepts the argument
-- provided, a type error is raised otherwise.
--
-- > transfer addr $ calling (ep @"Entrypoint") ()
--
-- Use 'CallDefault' or @def@ to call the default entrypoint.
--
-- > transfer addr $ calling def ()
--
-- Notice that type variables for entrypoint argument and full parameter are
-- specified after the entrypoint. This is done so more for readability. F. ex.:
--
-- > transfer addr $ calling def @Integer 123
--
-- This does also marginally simplify type inference in the case of partial
-- application.
calling
  :: forall mname.
      EntrypointRef mname
  -> forall epArg param. (NiceParameter epArg, HasEntrypointArg param (EntrypointRef mname) epArg)
  => epArg -> GenericCall ('Checked param)
calling arg = CheckedCall arg

-- | Unsafely call an entrypoint specified by the first argument with the
-- provided parameter.
--
-- This is "unsafe" in the sense that there is no check that the contract
-- indeed has the specified entrypoint or that the entrypoint in question
-- accepts the argument provided.
--
-- Also, no compile-time checks are performed on the entrypoint name, so it
-- can be malformed.
--
-- > transfer addr $ unsafeCalling (ep @"Entrypoint") ()
--
-- Overloaded labels are supported with 'unsafeCalling', so you can specify the
-- entrypoint as an overloaded label:
--
-- > transfer addr $ unsafeCalling #entrypoint ()
--
-- Use 'U.DefEpName' or @def@ to call the default entrypoint.
--
-- Notice that the type variable for the entrypoint argument is specified after
-- the entrypoint. This is done so more for readability. F. ex.:
--
-- > transfer addr $ calling def @Integer 123
--
-- This does also marginally simplify type inference in the case of partial
-- application.
unsafeCalling :: U.EpName -> forall epArg. NiceParameter epArg => epArg -> GenericCall 'Unchecked
unsafeCalling arg = UncheckedCall arg

----------------------------------------------------------------------------
-- Return value specification
----------------------------------------------------------------------------

-- | 'transfer' flag to signal we want contract events emitted by @EMIT@
-- returned. Passed in the variadic part of 'transfer', e.g.
--
-- > transfer addr [tz|123u|] WithContractEvents $ calling (ep @"Entrypoint") ()
data WithContractEvents = WithContractEvents