content: -- SPDX-FileCopyrightText: 2021 Tezos Commons
  -- SPDX-License-Identifier: LicenseRef-MIT-TC
  
  module SMT.Common.Types
    ( ModelInputArg (..)
    , ModelInput (..)
    , MkModelInput
    , MkGenPropose
    , MkGenCustomCalls
    , SmtOption (..)
  
    , GeneratorState (..)
    , GeneratorT
    , initGeneratorState
    , runGeneratorT
    , (<<&>>)
    ) where
  
  import Universum hiding (show)
  
  import Hedgehog
  import Text.Show (show)
  
  import Test.Cleveland.Lorentz.Types
  import Lorentz hiding (cast, not)
  import Morley.Tezos.Crypto (SecretKey)
  import Test.Cleveland (ImplicitAddressWithAlias)
  
  import Ligo.BaseDAO.Types
  import SMT.Model.BaseDAO.Types
  import Test.Ligo.BaseDAO.Common (ContractType(..))
  
  
  -- | A type that will be the inputs to the (Haskell) Model.
  -- This contains a list of entrypoint calls and the `ModelState`.
  newtype ModelInput var =
    ModelInput ([ModelCall var], ModelState var)
  
  deriving stock instance (Show (VariantToExtra var), Show (VariantToParam var)) => Show (ModelInput var)
  
  -- | A type needed to pass to `MkModelInput` to get `ModelInput`
  data ModelInputArg = ModelInputArg
    { miaGuardianAddr :: Address -- Used in `genPropose`, `genStorage`
    , miaGovAddr :: Address -- Used in `genPropose`, `genTransferContractTokens`
    , miaViewContractAddr :: ContractHandle (MText, Maybe MText) [(MText, Maybe MText)] () -- Used in registry dao `genLookupRegistryEntrypoint`
    }
  
  -- | The main type that will be generated by the generator.
  -- We cannot generate just the `ModelInput`, since it is not possible get the address of guardian
  -- and governance contract until they are originated in the nettest.
  -- As a result, we generate functions that accepts those addresses instead.
  type MkModelInput cep = ModelInputArg -> ModelInput cep
  
  -- | Instance Needed by Hedgehog `forall`
  instance Show (ModelInputArg -> ModelInput cep) where
    show _ = "<MkModelInput>"
  
  -- | A type for `genPropose` which is used by registry/treasury dao
  type MkGenPropose (var :: Variants) =
       Address
    -> Address
    -> Address
    -> GeneratorT var (Address -> Address -> (Parameter' (VariantToParam var), Natural, ProposalKey))
  
  type MkGenCustomCalls var = GeneratorT var ([ModelInputArg -> VariantToParam var])
  
  -- | A data type that is used to configure the generator, initial storage
  -- how the SMT behaves. Mostly used by Registry/Treasury SMT.
  data SmtOption (var :: Variants) = SmtOption
    { soMkPropose :: MkGenPropose var
    , soMkCustomCalls :: MkGenCustomCalls var
  
    , soModifyS :: (StorageSkeleton (VariantToExtra var) -> StorageSkeleton (VariantToExtra var))
      -- ^ Used by `registry/treasury` dao to add their configurations (sExtra, cProposalCheck ..)
      -- to the generated storage.
  
    , soContractType :: ContractType
      -- ^ Track which dao the smt used. Mainly needed to run some pre-cond (sendXtz when registry/treasury)
  
    , soProposalCheck :: (ProposeParams, VariantToExtra var) -> ModelT var ()
    , soRejectedProposalSlashValue :: (Proposal, VariantToExtra var) -> ModelT var Natural
    , soDecisionCallback :: DecisionCallbackInput' (VariantToExtra var) -> ModelT var ([SimpleOperation], VariantToExtra var, Maybe Address)
    , soCustomEps :: VariantToParam var -> ModelT var ()
    }
  
  -- | Generator state, contains commonly used value that shared between generators.
  data GeneratorState cep = GeneratorState
    { gsAddresses :: [(ImplicitAddressWithAlias, SecretKey)]
    , gsLevel :: Natural
    , gsMkGenPropose :: MkGenPropose cep
    , gsMkCustomCalls :: MkGenCustomCalls cep
    }
  
  -- | Generator transformer containing `GeneratorState`
  newtype GeneratorT cep a = GeneratorT
    { unGeneratorT :: StateT (GeneratorState cep) Gen a
    } deriving newtype (Functor, Applicative, Monad, MonadState (GeneratorState cep), MonadGen)
  
  initGeneratorState :: MkGenPropose cep -> GeneratorState cep
  initGeneratorState mkGenPropose = GeneratorState [] 0 mkGenPropose (pure [])
  
  runGeneratorT :: GeneratorT cep a -> GeneratorState cep -> Gen a
  runGeneratorT genAction st = do
    evalStateT (unGeneratorT genAction) st
  
  ------------------------------------------------------------------------------------
  -- Helper
  ------------------------------------------------------------------------------------
  
  -- | Fmap twice. Reverse of @<<$>>@
  (<<&>>) :: (Functor f1, Functor f2) => f1 (f2 a) -> (a -> b) -> f1 (f2 b)
  (<<&>>) a f =
    fmap (fmap f) a
  