{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Deleg () where

import Cardano.Ledger.Conway
import Cardano.Ledger.Conway.Core (KeyRole (..))
import Cardano.Ledger.Credential (Credential)
import Control.State.Transition.Extended (TRC (..))
import Data.Bifunctor (second)
import Data.Set (Set)
import qualified MAlonzo.Code.Ledger.Conway.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base ()
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Core (
  ExecSpecRule (ExecContext, runAgdaRule, translateInputs),
  SpecTRC (SpecTRC),
 )
import Test.Cardano.Ledger.Conformance.SpecTranslate.Base (
  SpecTranslate (toSpecRep),
  unComputationResult,
  withCtxSpecTransM,
 )
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base ()
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Cert ()
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Deleg ()

instance ExecSpecRule "DELEG" ConwayEra where
  -- The context is the set of all DRep delegatees in the transaction
  type ExecContext "DELEG" ConwayEra = Set (Credential DRepRole)

  translateInputs :: HasCallStack =>
TRC (EraRule "DELEG" ConwayEra)
-> SpecTransM
     ConwayEra
     (ExecContext "DELEG" ConwayEra)
     (SpecTRC "DELEG" ConwayEra)
translateInputs (TRC (Environment (EraRule "DELEG" ConwayEra)
env, State (EraRule "DELEG" ConwayEra)
st, Signal (EraRule "DELEG" ConwayEra)
sig)) = do
    agdaEnv <- ConwayDelegEnv ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (ConwayDelegEnv ConwayEra))
     (SpecRep ConwayEra (ConwayDelegEnv ConwayEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep ConwayDelegEnv ConwayEra
Environment (EraRule "DELEG" ConwayEra)
env
    agdaSt <- withCtxSpecTransM () $ toSpecRep st
    agdaSig <- withCtxSpecTransM () $ toSpecRep sig
    pure $ SpecTRC agdaEnv agdaSt agdaSig

  runAgdaRule :: HasCallStack =>
SpecTRC "DELEG" ConwayEra
-> Either Text (SpecState "DELEG" ConwayEra)
runAgdaRule (SpecTRC SpecEnvironment "DELEG" ConwayEra
env (Agda.MkCertState DState
dState PState
pState GState
vState) SpecSignal "DELEG" ConwayEra
sig) =
    (DState -> CertState)
-> Either Text DState -> Either Text CertState
forall b c a. (b -> c) -> Either a b -> Either a c
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second
      (\DState
dState' -> DState -> PState -> GState -> CertState
Agda.MkCertState DState
dState' PState
pState GState
vState)
      (Either Text DState -> Either Text (SpecState "DELEG" ConwayEra))
-> (T_HSComputationResult_110 Text DState -> Either Text DState)
-> T_HSComputationResult_110 Text DState
-> Either Text (SpecState "DELEG" ConwayEra)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T_HSComputationResult_110 Text DState -> Either Text DState
forall a. ComputationResult Text a -> Either Text a
unComputationResult
      (T_HSComputationResult_110 Text DState
 -> Either Text (SpecState "DELEG" ConwayEra))
-> T_HSComputationResult_110 Text DState
-> Either Text (SpecState "DELEG" ConwayEra)
forall a b. (a -> b) -> a -> b
$ DelegEnv
-> DState -> DCert -> T_HSComputationResult_110 Text DState
Agda.delegStep DelegEnv
SpecEnvironment "DELEG" ConwayEra
env DState
dState DCert
SpecSignal "DELEG" ConwayEra
sig