-- | Executor and typechecker of a contract in Morley language.

module Michelson.Runtime
  (
    -- * High level interface for end user
    originateContract
  , runContract
  , transfer

  -- * Other helpers
  , parseContract
  , parseExpandContract
  , readAndParseContract
  , prepareContract
  , typeCheckWithDb

  -- * Re-exports
  , ContractState (..)
  , AddressState (..)
  , TxData (..)

  -- * For testing
  , ExecutorOp (..)
  , ExecutorRes (..)
  , ExecutorError' (..)
  , ExecutorError
  , executorPure

  -- * To avoid warnings (can't generate lenses only for some fields)
  , erInterpretResults
  , erUpdates
  ) where

import Control.Lens (at, makeLenses, (%=))
import Control.Monad.Except (Except, runExcept, throwError)
import Data.Singletons (sing)
import Data.Text.IO (getContents)
import Fmt (Buildable(build), blockListF, fmt, fmtLn, nameF, pretty, (+|), (|+))
import Named ((:!), (:?), arg, argDef, defaults, (!))
import Text.Megaparsec (parse)

import Michelson.Interpret
  (ContractEnv(..), InterpretError(..), InterpretResult(..), InterpreterState(..), MorleyLogs(..),
  RemainingSteps(..), handleContractReturn, interpret)
import Michelson.Macro (ParsedOp, expandContract)
import qualified Michelson.Parser as P
import Michelson.Runtime.GState
import Michelson.Runtime.TxData
import Michelson.TypeCheck
  (SomeContract, TCError, typeCheckContract, typeCheckTopLevelType, typeVerifyTopLevelType)
import Michelson.Typed
  (CreateContract(..), EpName, Operation'(..), SomeValue'(..), TransferTokens(..), convertContract,
  untypeValue)
import qualified Michelson.Typed as T
import Michelson.Untyped (Contract, OriginationOperation(..), mkContractAddress)
import qualified Michelson.Untyped as U
import Tezos.Address (Address(..))
import Tezos.Core (Mutez, Timestamp(..), getCurrentTime, toMutez, unsafeAddMutez, unsafeSubMutez)
import Tezos.Crypto (parseKeyHash)
import Util.IO (readFileUtf8)

----------------------------------------------------------------------------
-- Auxiliary types
----------------------------------------------------------------------------

-- | Operations executed by interpreter.
-- In our model one Michelson's operation (`operation` type in Michelson)
-- corresponds to 0 or 1 interpreter operation.
--
-- Note: 'Address' is not part of 'TxData', because 'TxData' is
-- supposed to be provided by the user, while 'Address' can be
-- computed by our code.
data ExecutorOp
  = OriginateOp OriginationOperation
  -- ^ Originate a contract.
  | TransferOp Address TxData
  -- ^ Send a transaction to given address which is assumed to be the
  -- address of an originated contract.
  deriving stock (Show)

-- | Result of a single execution of interpreter.
data ExecutorRes = ExecutorRes
  { _erGState :: GState
  -- ^ New 'GState'.
  , _erOperations :: [ExecutorOp]
  -- ^ List of operations to be added to the operations queue.
  , _erUpdates :: [GStateUpdate]
  -- ^ Updates applied to 'GState'.
  , _erInterpretResults :: [(Address, InterpretResult)]
  -- ^ During execution a contract can print logs and in the end it returns
  -- a pair. All logs and returned values are kept until all called contracts
  -- are executed. In the end they are printed.
  , _erSourceAddress :: Maybe Address
  -- ^ As soon as transfer operation is encountered, this address is
  -- set to its input.
  , _erRemainingSteps :: RemainingSteps
  -- ^ Now much gas all remaining executions can consume.
  } deriving stock (Show)

makeLenses ''ExecutorRes

-- Note that it's not commutative.
-- It applies to the case when we have some ExecutorRes already
-- and get a new one after performing some operations.
instance Semigroup ExecutorRes where
  a <> b =
    b
      { _erUpdates = _erUpdates a <> _erUpdates b
      , _erInterpretResults = _erInterpretResults a <> _erInterpretResults b
      , _erSourceAddress = _erSourceAddress a <|> _erSourceAddress b
      }

-- | Errors that can happen during contract interpreting.
-- Type parameter @a@ determines how contracts will be represented
-- in these errors, e.g. @Address@
data ExecutorError' a
  = EEUnknownContract !a
  -- ^ The interpreted contract hasn't been originated.
  | EEInterpreterFailed !a
                        !InterpretError
  -- ^ Interpretation of Michelson contract failed.
  | EEAlreadyOriginated !a
                        !ContractState
  -- ^ A contract is already originated.
  | EEUnknownSender !a
  -- ^ Sender address is unknown.
  | EEUnknownManager !a
  -- ^ Manager address is unknown.
  | EENotEnoughFunds !a !Mutez
  -- ^ Sender doesn't have enough funds.
  | EEZeroTransaction !a
  -- ^ Sending 0tz towards an address.
  | EEFailedToApplyUpdates !GStateUpdateError
  -- ^ Failed to apply updates to GState.
  | EEIllTypedContract !TCError
  -- ^ A contract is ill-typed.
  | EEIllTypedStorage !TCError
  -- ^ Contract storage is ill-typed.
  | EEIllTypedParameter !TCError
  -- ^ Contract parameter is ill-typed.
  | EEUnknownEntrypoint EpName
  -- ^ Specified entrypoint to run is not found.
  deriving stock (Show)

instance (Buildable a) => Buildable (ExecutorError' a) where
  build =
    \case
      EEUnknownContract addr -> "The contract is not originated " +| addr |+ ""
      EEInterpreterFailed addr err ->
        "Michelson interpreter failed for contract " +| addr |+ ": " +| err |+ ""
      EEAlreadyOriginated addr cs ->
        "The following contract is already originated: " +| addr |+
        ", " +| cs |+ ""
      EEUnknownSender addr -> "The sender address is unknown " +| addr |+ ""
      EEUnknownManager addr -> "The manager address is unknown " +| addr |+ ""
      EENotEnoughFunds addr amount ->
        "The sender (" +| addr |+
        ") doesn't have enough funds (has only " +| amount |+ ")"
      EEZeroTransaction addr ->
        "Transaction of 0ꜩ towards a key address " +| addr |+ " which has no code is prohibited"
      EEFailedToApplyUpdates err -> "Failed to update GState: " +| err |+ ""
      EEIllTypedContract err -> "The contract is ill-typed: " +| err |+ ""
      EEIllTypedStorage err -> "The contract storage is ill-typed: " +| err |+ ""
      EEIllTypedParameter err -> "The contract parameter is ill-typed: " +| err |+ ""
      EEUnknownEntrypoint epName -> "The contract does not contain entrypoint '" +| epName |+ "'"

type ExecutorError = ExecutorError' Address

instance (Typeable a, Show a, Buildable a) => Exception (ExecutorError' a) where
  displayException = pretty

----------------------------------------------------------------------------
-- Interface
----------------------------------------------------------------------------

-- | Parse a contract from 'Text'.
parseContract ::
     Maybe FilePath -> Text -> Either P.ParserException (U.Contract' ParsedOp)
parseContract mFileName =
  first P.ParserException . parse P.program (fromMaybe "<stdin>" mFileName)

-- | Parse a contract from 'Text' and expand macros.
parseExpandContract ::
     Maybe FilePath -> Text -> Either P.ParserException Contract
parseExpandContract mFileName = fmap expandContract . parseContract mFileName

-- | Read and parse a contract from give path or `stdin` (if the
-- argument is 'Nothing'). The contract is not expanded.
readAndParseContract :: Maybe FilePath -> IO (U.Contract' ParsedOp)
readAndParseContract mFilename = do
  code <- readCode mFilename
  either throwM pure $ parseContract mFilename code
  where
    readCode :: Maybe FilePath -> IO Text
    readCode = maybe getContents readFileUtf8

-- | Read a contract using 'readAndParseContract', expand and
-- flatten. The contract is not type checked.
prepareContract :: Maybe FilePath -> IO Contract
prepareContract mFile = expandContract <$> readAndParseContract mFile

-- | Originate a contract. Returns the address of the originated
-- contract.
originateContract ::
     FilePath -> OriginationOperation -> "verbose" :! Bool -> IO Address
originateContract dbPath origination verbose =
  -- pass 100500 as maxSteps, because it doesn't matter for origination,
  -- as well as 'now'
  mkContractAddress origination <$
  executor Nothing 100500 dbPath [OriginateOp origination] verbose
  ! defaults

-- | Run a contract. The contract is originated first (if it's not
-- already) and then we pretend that we send a transaction to it.
runContract
  :: Maybe Timestamp
  -> Word64
  -> Mutez
  -> FilePath
  -> U.Value
  -> Contract
  -> TxData
  -> "verbose" :! Bool
  -> "dryRun" :! Bool
  -> IO ()
runContract maybeNow maxSteps initBalance dbPath storageValue contract txData
  verbose (arg #dryRun -> dryRun) =
  executor maybeNow maxSteps dbPath operations verbose ! #dryRun dryRun
  where
    -- We hardcode some random key hash here as delegate to make sure that:
    -- 1. Contract's address won't clash with already originated one (because
    -- it may have different storage value which may be confusing).
    -- 2. If one uses this functionality twice with the same contract and
    -- other data, the contract will have the same address.
    delegate =
      either (error . mappend "runContract can't parse delegate: " . pretty) id $
      parseKeyHash "tz1YCABRTa6H8PLKx2EtDWeCGPaKxUhNgv47"
    origination = OriginationOperation
      { ooOriginator = genesisAddress
      , ooDelegate = Just delegate
      , ooBalance = initBalance
      , ooStorage = storageValue
      , ooContract = contract
      }
    addr = mkContractAddress origination
    operations =
      [ OriginateOp origination
      , TransferOp addr txData
      ]

-- | Send a transaction to given address with given parameters.
transfer ::
     Maybe Timestamp
  -> Word64
  -> FilePath
  -> Address
  -> TxData
  -> "verbose" :! Bool -> "dryRun" :? Bool -> IO ()
transfer maybeNow maxSteps dbPath destination txData =
  executor maybeNow maxSteps dbPath [TransferOp destination txData]

----------------------------------------------------------------------------
-- Executor
----------------------------------------------------------------------------

-- | Execute a contract on some global state (read from file) and
-- transaction data (passed explicitly).
executor ::
     Maybe Timestamp
  -> Word64
  -> FilePath
  -> [ExecutorOp]
  -> "verbose" :! Bool -> "dryRun" :? Bool -> IO ()
executor maybeNow maxSteps dbPath operations
  (arg #verbose -> verbose)
  (argDef #dryRun False -> dryRun)
    = do
  now <- maybe getCurrentTime pure maybeNow
  gState <- readGState dbPath
  let eitherRes =
        executorPure now (RemainingSteps maxSteps) gState operations
  ExecutorRes {..} <- either throwM pure eitherRes
  mapM_ printInterpretResult _erInterpretResults
  when (verbose && not (null _erUpdates)) $ do
    fmtLn $ nameF "Updates:" (blockListF _erUpdates)
    putTextLn $ "Remaining gas: " <> pretty _erRemainingSteps
  unless dryRun $
    writeGState dbPath _erGState
  where
    printInterpretResult
      :: (Address, InterpretResult) -> IO ()
    printInterpretResult (addr, InterpretResult {..}) = do
      putTextLn $ "Executed contract " <> pretty addr
      case iurOps of
        [] -> putTextLn "It didn't return any operations"
        _ -> fmt $ nameF "It returned operations:" (blockListF iurOps)
      putTextLn $
        "It returned storage: " <> pretty (untypeValue iurNewStorage)
      let MorleyLogs logs = isMorleyLogs iurNewState
      unless (null logs) $
        mapM_ putTextLn logs
      putTextLn "" -- extra break line to separate logs from two sequence contracts

-- | Implementation of executor outside 'IO'.  It reads operations,
-- executes them one by one and updates state accordingly.
-- Each operation from the passed list is fully executed before
-- the next one is considered.
executorPure ::
  Timestamp -> RemainingSteps -> GState -> [ExecutorOp] -> Either ExecutorError ExecutorRes
executorPure now maxSteps gState =
  foldM step initialState
  where
    -- Note that we can't just put all operations into '_erOperations'
    -- and call 'statefulExecutor' once, because in this case the
    -- order of operations will be wrong. We need to consider
    -- top-level operations (passed to this function) and operations returned by contracts separatety.
    -- Specifically, suppose that we want to interpreter two 'TransferOp's: [t1, t2].
    -- If t1 returns an operation, it should be performed before t2, but if we just
    -- pass [t1, t2] as '_erOperations' then 't2' will done immediately after 't1'.
    initialState = ExecutorRes
      { _erGState = gState
      , _erOperations = []
      , _erUpdates = mempty
      , _erInterpretResults = []
      , _erSourceAddress = Nothing
      , _erRemainingSteps = maxSteps
      }

    step :: ExecutorRes -> ExecutorOp -> Either ExecutorError ExecutorRes
    step currentRes op =
      let start = currentRes { _erOperations = [op]
                             , _erUpdates = []
                             , _erInterpretResults = []
                             }
       in (currentRes <>) <$> runExcept (execStateT (statefulExecutor now) start)

statefulExecutor
  :: Timestamp
  -> StateT ExecutorRes (Except ExecutorError) ()
statefulExecutor now = do
  curGState <- use erGState
  mSourceAddr <- use erSourceAddress
  remainingSteps <- use erRemainingSteps
  use erOperations >>= \case
    [] -> pass
    (op:opsTail) ->
      either throwError (processIntRes opsTail) $
      executeOneOp now remainingSteps mSourceAddr curGState op
  where
    processIntRes opsTail ir = do
      -- Not using `<>=` because it requires `Monoid` for no reason.
      id %= (<> ir)
      erOperations %= (opsTail <>)
      statefulExecutor now

-- | Execute only one operation and update 'GState' accordingly.
executeOneOp
  :: Timestamp
  -> RemainingSteps
  -> Maybe Address
  -> GState
  -> ExecutorOp
  -> Either ExecutorError ExecutorRes
executeOneOp _ remainingSteps _ gs (OriginateOp origination) = do
  typedContract <- first EEIllTypedContract $
    typeCheckContract (extractAllContracts gs) (ooContract origination)
  typedStorage <- first EEIllTypedStorage $
    typeCheckTopLevelType
      (extractAllContracts gs) (U.stor $ ooContract origination) (ooStorage origination)
  let originatorAddress = ooOriginator origination
  originatorBalance <- case gsAddresses gs ^. at (originatorAddress) of
    Nothing -> Left (EEUnknownManager originatorAddress)
    Just (asBalance -> oldBalance)
      | oldBalance < ooBalance origination ->
        Left (EENotEnoughFunds originatorAddress oldBalance)
      | otherwise ->
        -- Subtraction is safe because we have checked its
        -- precondition in guard.
        Right (oldBalance `unsafeSubMutez` ooBalance origination)
  let
    updates =
      [ GSAddAddress address (ASContract $ mkContractState typedContract typedStorage)
      , GSSetBalance originatorAddress originatorBalance
      ]
  case applyUpdates updates gs of
    Left _ ->
      Left (EEAlreadyOriginated address $ mkContractState typedContract typedStorage)
    Right newGS -> Right $
      ExecutorRes
      { _erGState = newGS
      , _erOperations = mempty
      , _erUpdates = updates
      , _erInterpretResults = []
      , _erSourceAddress = Nothing
      , _erRemainingSteps = remainingSteps
      }
  where
    mkContractState typedContract typedStorage = ContractState
      { csBalance = ooBalance origination
      , csStorage = ooStorage origination
      , csContract = ooContract origination
      , csTypedContract = Just typedContract
      , csTypedStorage = Just typedStorage
      }
    address = mkContractAddress origination
executeOneOp now remainingSteps mSourceAddr gs (TransferOp addr txData) = do
    let sourceAddr = fromMaybe (tdSenderAddress txData) mSourceAddr
    let senderAddr = tdSenderAddress txData
    let isKeyAddress (KeyAddress _) = True
        isKeyAddress _  = False
    let isZeroTransfer = tdAmount txData == toMutez 0

    -- Transferring 0 XTZ to a key address is prohibited.
    when (isZeroTransfer && isKeyAddress addr) $
      Left (EEZeroTransaction addr)

    mDecreaseSenderBalance <- case (isZeroTransfer, addresses ^. at senderAddr) of
      (True, _) -> pure Nothing
      (False, Nothing) -> Left (EEUnknownSender senderAddr)
      (False, Just (asBalance -> balance))
        | balance < tdAmount txData ->
          Left (EENotEnoughFunds senderAddr balance)
        | otherwise ->
          -- Subtraction is safe because we have checked its
          -- precondition in guard.
          Right (Just $ GSSetBalance senderAddr (balance `unsafeSubMutez` tdAmount txData))
    let onlyUpdates updates = Right (updates, [], Nothing, remainingSteps)
    (otherUpdates, sideEffects, maybeInterpretRes, newRemSteps)
        <- case (addresses ^. at addr, addr) of
      (Nothing, ContractAddress _) ->
        Left (EEUnknownContract addr)
      (Nothing, KeyAddress _) -> do
        let
          transferAmount = tdAmount txData
          addrState = ASSimple transferAmount
          upd = GSAddAddress addr addrState
        onlyUpdates [upd]
      (Just (ASSimple oldBalance), _) -> do
        -- can't overflow if global state is correct (because we can't
        -- create money out of nowhere)
        let
          newBalance = oldBalance `unsafeAddMutez` tdAmount txData
          upd = GSSetBalance addr newBalance
        onlyUpdates [upd]
      (Just (ASContract cs), _) -> do
        let
          existingContracts = extractAllContracts gs
          contractEnv = ContractEnv
            { ceNow = now
            , ceMaxSteps = remainingSteps
            , ceBalance = csBalance cs
            , ceContracts = existingContracts
            , ceSelf = addr
            , ceSource = sourceAddr
            , ceSender = senderAddr
            , ceAmount = tdAmount txData
            , ceChainId = gsChainId gs
            }
          epName = tdEntrypoint txData

        SomeContractAndStorage typedContract typedStorage
          <- getTypedContractAndStorage EEIllTypedContract EEIllTypedStorage gs cs
        T.MkEntryPointCallRes _ epc
          <- T.mkEntryPointCall epName (sing, T.fcParamNotesSafe typedContract)
             & maybe (throwError $ EEUnknownEntrypoint epName) pure
        typedParameter <- first EEIllTypedParameter $
           typeVerifyTopLevelType existingContracts (tdParameter txData)
        iur@InterpretResult
          { iurOps = sideEffects
          , iurNewStorage = newValue
          , iurNewState = InterpreterState _ newRemainingSteps
          }
          <- first (EEInterpreterFailed addr) $
             handleContractReturn $
                interpret (T.fcCode typedContract) epc
                typedParameter typedStorage contractEnv
        let
          newValueU = untypeValue newValue
          -- can't overflow if global state is correct (because we can't
          -- create money out of nowhere)
          newBalance = csBalance cs `unsafeAddMutez` tdAmount txData
          updBalance
            | newBalance == csBalance cs = Nothing
            | otherwise = Just $ GSSetBalance addr newBalance
          updStorage
            | SomeValue newValue == SomeValue typedStorage = Nothing
            | otherwise = Just $ GSSetStorageValue addr newValueU (SomeValue newValue)
          updates = catMaybes
            [ updBalance
            , updStorage
            ]
        Right (updates, sideEffects, Just iur, newRemainingSteps)

    let
      updates = maybe id (:) mDecreaseSenderBalance otherUpdates

    newGState <- first EEFailedToApplyUpdates $ applyUpdates updates gs

    return ExecutorRes
      { _erGState = newGState
      , _erOperations = mapMaybe (convertOp addr) sideEffects
      , _erUpdates = updates
      , _erInterpretResults = maybe mempty (one . (addr,)) maybeInterpretRes
      , _erSourceAddress = Just sourceAddr
      , _erRemainingSteps = newRemSteps
      }
  where
    addresses :: Map Address AddressState
    addresses = gsAddresses gs

----------------------------------------------------------------------------
-- TypeCheck
----------------------------------------------------------------------------
typeCheckWithDb
  :: FilePath
  -> U.Contract
  -> IO (Either TCError SomeContract)
typeCheckWithDb dbPath morleyContract = do
  gState <- readGState dbPath
  pure . typeCheckContract (extractAllContracts gState) $ morleyContract

----------------------------------------------------------------------------
-- Simple helpers
----------------------------------------------------------------------------

-- The argument is the address of the contract that generation this operation.
convertOp :: Address -> T.Operation -> Maybe ExecutorOp
convertOp interpretedAddr =
  \case
    OpTransferTokens tt ->
      case ttContract tt of
        T.VContract destAddress sepc ->
          let txData =
                TxData
                  { tdSenderAddress = interpretedAddr
                  , tdEntrypoint = T.sepcName sepc
                  , tdParameter = untypeValue (ttTransferArgument tt)
                  , tdAmount = ttAmount tt
                  }
          in Just (TransferOp destAddress txData)
    OpSetDelegate {} -> Nothing
    OpCreateContract cc ->
      let origination = OriginationOperation
            { ooOriginator = ccOriginator cc
            , ooDelegate = ccDelegate cc
            , ooBalance = ccBalance cc
            , ooStorage = untypeValue (ccStorageVal cc)
            , ooContract = convertContract (ccContractCode cc)
            }
       in Just (OriginateOp origination)