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

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

import Cardano.Ledger.Conway (ConwayEra)
import Cardano.Ledger.Conway.Core (EraPParams (..))
import Cardano.Ledger.Conway.Governance
import Cardano.Ledger.Conway.Rules
import Control.State.Transition.Extended (TRC (..))
import Lens.Micro ((&), (.~), (^.))
import qualified MAlonzo.Code.Ledger.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base ()
import Test.Cardano.Ledger.Conway.Arbitrary ()

instance ExecSpecRule "GOV" ConwayEra where
  type ExecContext "GOV" ConwayEra = EnactState ConwayEra

  runAgdaRule :: HasCallStack =>
SpecTRC "GOV" ConwayEra -> Either Text (SpecState "GOV" ConwayEra)
runAgdaRule (SpecTRC SpecEnvironment "GOV" ConwayEra
env SpecState "GOV" ConwayEra
st SpecSignal "GOV" ConwayEra
sig) = ComputationResult Text GovState -> Either Text GovState
forall a. ComputationResult Text a -> Either Text a
unComputationResult (ComputationResult Text GovState -> Either Text GovState)
-> ComputationResult Text GovState -> Either Text GovState
forall a b. (a -> b) -> a -> b
$ GovEnv
-> GovState
-> [Either GovVote GovProposal]
-> ComputationResult Text GovState
Agda.govStep GovEnv
SpecEnvironment "GOV" ConwayEra
env GovState
SpecState "GOV" ConwayEra
st [Either GovVote GovProposal]
SpecSignal "GOV" ConwayEra
sig

  translateInputs :: HasCallStack =>
ExecContext "GOV" ConwayEra
-> TRC (EraRule "GOV" ConwayEra)
-> Either Text (SpecTRC "GOV" ConwayEra)
translateInputs ExecContext "GOV" ConwayEra
enactState (TRC (env :: Environment (EraRule "GOV" ConwayEra)
env@GovEnv {PParams ConwayEra
gePParams :: PParams ConwayEra
gePParams :: forall era. GovEnv era -> PParams era
gePParams}, State (EraRule "GOV" ConwayEra)
st, Signal (EraRule "GOV" ConwayEra)
sig)) = do
    EnactState ConwayEra
-> SpecTransM (EnactState ConwayEra) (SpecTRC "GOV" ConwayEra)
-> Either Text (SpecTRC "GOV" ConwayEra)
forall ctx a. ctx -> SpecTransM ctx a -> Either Text a
runSpecTransM EnactState ConwayEra
ctx (SpecTransM (EnactState ConwayEra) (SpecTRC "GOV" ConwayEra)
 -> Either Text (SpecTRC "GOV" ConwayEra))
-> SpecTransM (EnactState ConwayEra) (SpecTRC "GOV" ConwayEra)
-> Either Text (SpecTRC "GOV" ConwayEra)
forall a b. (a -> b) -> a -> b
$
      GovEnv
-> GovState
-> [Either GovVote GovProposal]
-> SpecTRC "GOV" ConwayEra
SpecEnvironment "GOV" ConwayEra
-> SpecState "GOV" ConwayEra
-> SpecSignal "GOV" ConwayEra
-> SpecTRC "GOV" ConwayEra
forall (rule :: Symbol) era.
SpecEnvironment rule era
-> SpecState rule era -> SpecSignal rule era -> SpecTRC rule era
SpecTRC
        (GovEnv
 -> GovState
 -> [Either GovVote GovProposal]
 -> SpecTRC "GOV" ConwayEra)
-> SpecTransM (EnactState ConwayEra) GovEnv
-> SpecTransM
     (EnactState ConwayEra)
     (GovState
      -> [Either GovVote GovProposal] -> SpecTRC "GOV" ConwayEra)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GovEnv ConwayEra
-> SpecTransM (EnactState ConwayEra) (SpecRep (GovEnv ConwayEra))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep GovEnv ConwayEra
Environment (EraRule "GOV" ConwayEra)
env
        SpecTransM
  (EnactState ConwayEra)
  (GovState
   -> [Either GovVote GovProposal] -> SpecTRC "GOV" ConwayEra)
-> SpecTransM (EnactState ConwayEra) GovState
-> SpecTransM
     (EnactState ConwayEra)
     ([Either GovVote GovProposal] -> SpecTRC "GOV" ConwayEra)
forall a b.
SpecTransM (EnactState ConwayEra) (a -> b)
-> SpecTransM (EnactState ConwayEra) a
-> SpecTransM (EnactState ConwayEra) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Proposals ConwayEra
-> SpecTransM
     (EnactState ConwayEra) (SpecRep (Proposals ConwayEra))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Proposals ConwayEra
State (EraRule "GOV" ConwayEra)
st
        SpecTransM
  (EnactState ConwayEra)
  ([Either GovVote GovProposal] -> SpecTRC "GOV" ConwayEra)
-> SpecTransM (EnactState ConwayEra) [Either GovVote GovProposal]
-> SpecTransM (EnactState ConwayEra) (SpecTRC "GOV" ConwayEra)
forall a b.
SpecTransM (EnactState ConwayEra) (a -> b)
-> SpecTransM (EnactState ConwayEra) a
-> SpecTransM (EnactState ConwayEra) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> GovSignal ConwayEra
-> SpecTransM
     (EnactState ConwayEra) (SpecRep (GovSignal ConwayEra))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep GovSignal ConwayEra
Signal (EraRule "GOV" ConwayEra)
sig
    where
      ctx :: EnactState ConwayEra
ctx =
        EnactState ConwayEra
ExecContext "GOV" ConwayEra
enactState
          EnactState ConwayEra
-> (EnactState ConwayEra -> EnactState ConwayEra)
-> EnactState ConwayEra
forall a b. a -> (a -> b) -> b
& (GovRelation StrictMaybe -> Identity (GovRelation StrictMaybe))
-> EnactState ConwayEra -> Identity (EnactState ConwayEra)
forall era (f :: * -> *).
Functor f =>
(GovRelation StrictMaybe -> f (GovRelation StrictMaybe))
-> EnactState era -> f (EnactState era)
ensPrevGovActionIdsL ((GovRelation StrictMaybe -> Identity (GovRelation StrictMaybe))
 -> EnactState ConwayEra -> Identity (EnactState ConwayEra))
-> GovRelation StrictMaybe
-> EnactState ConwayEra
-> EnactState ConwayEra
forall s t a b. ASetter s t a b -> b -> s -> t
.~ GovRelation PRoot -> GovRelation StrictMaybe
toPrevGovActionIds (Proposals ConwayEra
State (EraRule "GOV" ConwayEra)
st Proposals ConwayEra
-> Getting
     (GovRelation PRoot) (Proposals ConwayEra) (GovRelation PRoot)
-> GovRelation PRoot
forall s a. s -> Getting a s a -> a
^. Getting
  (GovRelation PRoot) (Proposals ConwayEra) (GovRelation PRoot)
forall era (f :: * -> *).
Functor f =>
(GovRelation PRoot -> f (GovRelation PRoot))
-> Proposals era -> f (Proposals era)
pRootsL)
          EnactState ConwayEra
-> (EnactState ConwayEra -> EnactState ConwayEra)
-> EnactState ConwayEra
forall a b. a -> (a -> b) -> b
& (ProtVer -> Identity ProtVer)
-> EnactState ConwayEra -> Identity (EnactState ConwayEra)
forall era. EraPParams era => Lens' (EnactState era) ProtVer
Lens' (EnactState ConwayEra) ProtVer
ensProtVerL ((ProtVer -> Identity ProtVer)
 -> EnactState ConwayEra -> Identity (EnactState ConwayEra))
-> ProtVer -> EnactState ConwayEra -> EnactState ConwayEra
forall s t a b. ASetter s t a b -> b -> s -> t
.~ (PParams ConwayEra
gePParams PParams ConwayEra
-> Getting ProtVer (PParams ConwayEra) ProtVer -> ProtVer
forall s a. s -> Getting a s a -> a
^. Getting ProtVer (PParams ConwayEra) ProtVer
forall era. EraPParams era => Lens' (PParams era) ProtVer
Lens' (PParams ConwayEra) ProtVer
ppProtocolVersionL)