content: -- SPDX-FileCopyrightText: 2021 Tezos Commons
  -- SPDX-License-Identifier: LicenseRef-MIT-TC
  
  {-# OPTIONS_GHC -Wno-orphans #-}
  {-# OPTIONS_GHC -Wno-missing-signatures #-}
  
  module SMT.Model.BaseDAO.Types
    ( ModelT (..)
    , ModelState (..)
    , SimpleContractType (..)
    , SimpleFA2Contract (..)
    , SimpleFA12Contract (..)
    , OtherContract (..)
    , SimpleOperation (..)
    , runModelT
    , getStore
    , getConfig
    , modifyStore
    , execOperation
  
    , ModelCall (..)
    , ModelSource (..)
    , ModelError (..)
    , contractErrorToModelError
    ) where
  
  import Universum hiding (show)
  
  import Control.Monad.Except (MonadError)
  import Data.Map qualified as Map
  import Fmt
  import Text.Show (show)
  
  import Lorentz hiding (cast, get, not, subMutez)
  import Lorentz.Contracts.Spec.AbstractLedgerInterface qualified as FA12
  import Lorentz.Contracts.Spec.FA2Interface qualified as FA2
  import Morley.Tezos.Address
  import Morley.Tezos.Core
  import Morley.Tezos.Crypto (HashTag)
  import Test.Cleveland (ImplicitAddressWithAlias)
  
  import Ligo.BaseDAO.ErrorCodes
  import Ligo.BaseDAO.Types
  
  -- | Transformer used in haskell implementation of BaseDAO
  newtype ModelT var a = ModelT
    { unModelT :: (ExceptT ModelError $ State (ModelState var)) a
    } deriving newtype (Functor, Applicative, Monad, MonadState (ModelState var), MonadError ModelError)
  
  -- | A type that keep track of blockchain state
  data ModelState var = ModelState
    { msStorage :: StorageSkeleton (VariantToExtra var)
    , msMutez :: Mutez
    -- ^ Dao balance
  
    , msLevel :: Natural
    , msChainId :: ChainId
    , msSelfAddress :: Address
    , msGovernanceTokenAddress :: Address
    , msContracts :: Map Address SimpleContractType
    -- ^ Keep track of originated contract in the blockchain.
    -- See `SimpleContractType` for detail.
  
    , msProposalCheck :: (ProposeParams, VariantToExtra var) -> ModelT var ()
    , msRejectedProposalSlashValue :: (Proposal, VariantToExtra var) -> ModelT var Natural
    , msDecisionCallback :: DecisionCallbackInput' (VariantToExtra var) -> ModelT var ([SimpleOperation], VariantToExtra var, Maybe Address)
    , msCustomEps :: VariantToParam var -> ModelT var ()
    } deriving stock (Generic)
  
  -- Needed by `forall`
  --
  deriving stock instance Show (VariantToExtra var) => Show (ModelState var)
  
  instance Show ((ProposeParams, a) -> ModelT var ()) where
    show _ = "<callback>"
  instance Show ((Proposal, a) -> ModelT cep Natural) where
    show _ = "<msRejectedProposalSlashValue>"
  instance Show (DecisionCallbackInput' b -> ModelT var ([SimpleOperation], a, Maybe Address)) where
    show _ = "<msDecisionCallback>"
  instance {-# INCOHERENT #-} Show (a -> ModelT var ()) where
    show _ = "<callback>"
  
  runModelT :: ModelT cep a -> ModelState cep -> (Either ModelError (ModelState cep))
  runModelT (ModelT model) initState =
    runExceptT model
      & (`runState` initState)
      & (\(result, updatedMs) -> case result of
            Left err -> Left err
            Right _ -> Right updatedMs
        )
  
  execOperation :: SimpleOperation -> ModelT cep ()
  execOperation op = do
    contracts <- get <&> msContracts
  
    let (updatedContracts, minusBal) =
          case op of
            FA2TransferOperation addr param tez ->
              case Map.lookup addr contracts of
                Just (SimpleFA2ContractType sfc) ->
                  let updatedSc = sfc
                        { sfcStorage = param : (sfc & sfcStorage)
                        , sfcMutez = unsafeAddMutez tez (sfc & sfcMutez)
                        }
                  in (Map.insert addr (SimpleFA2ContractType updatedSc) contracts, tez)
                _ ->
                  (contracts, zeroMutez)
            FA12TransferOperation addr param tez ->
              case Map.lookup addr contracts of
                Just (SimpleFA12ContractType sfc) ->
                  let updatedSc = sfc
                        { sfclStorage = param : (sfc & sfclStorage)
                        , sfclMutez = unsafeAddMutez tez (sfc & sfclMutez)
                        }
                  in (Map.insert addr (SimpleFA12ContractType updatedSc) contracts, tez)
                _ ->
                  (contracts, zeroMutez)
            OtherOperation addr param tez ->
              case Map.lookup addr contracts of
                Just (OtherContractType oc) ->
                  let updatedSc = oc
                        { ocStorage = param : (oc & ocStorage)
                        , ocMutez = unsafeAddMutez tez (oc & ocMutez)
                        }
                  in (Map.insert addr (OtherContractType updatedSc) contracts, tez)
                _ ->
                  (contracts, zeroMutez)
  
    currentBal <- get <&> msMutez
    let newBal = case currentBal `subMutez` minusBal of
          Just b -> b
          Nothing -> error "Dao balance is negative."
  
    modify $ \ms -> ms { msContracts = updatedContracts, msMutez = newBal }
  
  getStore :: ModelT var (StorageSkeleton (VariantToExtra var))
  getStore = get <&> msStorage
  
  getConfig :: ModelT cep Config
  getConfig = get <&> msStorage <&> sConfig
  
  modifyStore :: (StorageSkeleton (VariantToExtra var) -> ModelT var (StorageSkeleton (VariantToExtra var))) -> ModelT var ()
  modifyStore f = do
    ms :: ModelState var <- get
    updatedStorage :: StorageSkeleton (VariantToExtra var) <- f (msStorage $ ms)
    put $ ms
      { msStorage =  updatedStorage
      }
  
  -- Simple operation that only allows transfering to `FA2.TransferItem` entrypoint
  data SimpleOperation
    = FA2TransferOperation Address [FA2.TransferItem] Mutez
    | FA12TransferOperation Address FA12.TransferParams Mutez
    | OtherOperation Address Text Mutez
    deriving stock (Eq, Show, Generic)
    deriving Buildable via GenericBuildable SimpleOperation
  
  -- | A simple contract type used to track originate contracts
  -- We mostly care about contract that has the FA2 transfer entrypont.
  -- Other contract call params will be convert to text.
  data SimpleContractType
    = SimpleFA2ContractType SimpleFA2Contract
    | SimpleFA12ContractType SimpleFA12Contract
    | OtherContractType OtherContract
    deriving stock (Eq, Show, Generic)
    deriving Buildable via GenericBuildable SimpleContractType
  
  data SimpleFA2Contract = SimpleFA2Contract
    { sfcStorage :: [FA2.TransferParams]
    , sfcMutez :: Mutez
    } deriving stock (Eq, Show, Generic)
      deriving Buildable via GenericBuildable SimpleFA2Contract
  
  data SimpleFA12Contract = SimpleFA12Contract
    { sfclStorage :: [FA12.TransferParams]
    , sfclMutez :: Mutez
    } deriving stock (Eq, Show, Generic)
      deriving Buildable via GenericBuildable SimpleFA12Contract
  
  data OtherContract = OtherContract
    { ocStorage :: [Text]
    , ocMutez :: Mutez
    } deriving stock (Eq, Show, Generic)
      deriving Buildable via GenericBuildable OtherContract
  
  -- | Definition of an entrypoint call to emulate in the SMTs
  data ModelCall var = ModelCall
    { mcAdvanceLevel :: Maybe Natural -- Advance level before calling the entrypoint
    , mcParameter :: Parameter' (VariantToParam var)
    , mcSource :: ModelSource
    } deriving stock (Generic)
  
  deriving stock instance Show (VariantToParam var) => Show (ModelCall var)
  
  instance Buildable (HashTag a) where
    build = build . show
  
  deriving via GenericBuildable ContractHash instance Buildable ContractHash
  
  deriving via GenericBuildable (ModelCall var)
    instance Buildable (Parameter' (VariantToParam var)) => Buildable (ModelCall var)
  
  -- | Definition of an @source@ and @sender@ for a call to emulate in the SMTs
  data ModelSource = ModelSource
    { msoSender :: ImplicitAddressWithAlias
    , msoSource :: ImplicitAddressWithAlias
    } deriving stock (Eq, Show, Generic)
      deriving Buildable via GenericBuildable ModelSource
  
  -- | The possible contract errors for the models
  data ModelError
    = NOT_DELEGATE
    | EMPTY_FLUSH
    | NOT_ENOUGH_FROZEN_TOKENS
    | NOT_PROPOSING_STAGE
    | PROPOSAL_NOT_UNIQUE
    | PROPOSAL_NOT_EXIST
    | EXPIRED_PROPOSAL
    | MISSIGNED
    | VOTING_STAGE_OVER
    | DROP_PROPOSAL_CONDITION_NOT_MET
    | NOT_ADMIN
    | NOT_PENDING_ADMIN
    | BAD_TOKEN_CONTRACT
    | FAIL_PROPOSAL_CHECK
    | UNSTAKE_INVALID_PROPOSAL
    | VOTER_DOES_NOT_EXIST
    deriving stock (Generic, Eq, Show)
    deriving Buildable via GenericBuildable ModelError
  
  contractErrorToModelError :: Integer -> ModelError
  contractErrorToModelError errorCode
    | (errorCode == toInteger notDelegate) = NOT_DELEGATE
    | (errorCode == toInteger emptyFlush) = EMPTY_FLUSH
    | (errorCode == toInteger notEnoughFrozenTokens) = NOT_ENOUGH_FROZEN_TOKENS
    | (errorCode == toInteger notProposingStage) = NOT_PROPOSING_STAGE
    | (errorCode == toInteger proposalNotUnique) = PROPOSAL_NOT_UNIQUE
    | (errorCode == toInteger proposalNotExist) = PROPOSAL_NOT_EXIST
    | (errorCode == toInteger expiredProposal) = EXPIRED_PROPOSAL
    | (errorCode == toInteger missigned) = MISSIGNED
    | (errorCode == toInteger votingStageOver) = VOTING_STAGE_OVER
    | (errorCode == toInteger dropProposalConditionNotMet) = DROP_PROPOSAL_CONDITION_NOT_MET
    | (errorCode == toInteger notAdmin) = NOT_ADMIN
    | (errorCode == toInteger notPendingAdmin) = NOT_PENDING_ADMIN
    | (errorCode == toInteger badTokenContract) = BAD_TOKEN_CONTRACT
    | (errorCode == toInteger failProposalCheck) = FAIL_PROPOSAL_CHECK
    | (errorCode == toInteger unstakeInvalidProposal) = UNSTAKE_INVALID_PROPOSAL
    | (errorCode == toInteger voterDoesNotExist) = VOTER_DOES_NOT_EXIST
    | otherwise = error $ toText $ show errorCode
  