{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Test.Cardano.Ledger.Conformance.ExecSpecRule.Dijkstra.NewEpoch () where

import Cardano.Ledger.BaseTypes (Globals (networkId), Network)
import Cardano.Ledger.Binary (EncCBOR (..))
import Cardano.Ledger.Binary.Coders (Encode (..), encode, (!>))
import Cardano.Ledger.Dijkstra (DijkstraEra)
import Control.State.Transition.Extended (TRC (..))
import GHC.Generics (Generic)
import qualified MAlonzo.Code.Ledger.Dijkstra.Foreign.API as Agda
import Test.Cardano.Ledger.Common (NFData, ToExpr (..))
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Core (
  ExecSpecRule (..),
  ExecSpecTopLevelRule (..),
  SpecTRC (..),
 )
import Test.Cardano.Ledger.Conformance.SpecTranslate.Base (
  SpecTranslate (..),
  askSpecTransM,
  unComputationResult_,
  withCtxSpecTransM,
  withSpecTransM,
 )
import Test.Cardano.Ledger.Conformance.SpecTranslate.Dijkstra ()
import Test.Cardano.Ledger.Dijkstra.ImpTest ()

newtype DijkstraNewEpochExecContext era
  = DijkstraNewEpochExecContext
  {forall era. DijkstraNewEpochExecContext era -> Network
dneecNetworkId :: Network}
  deriving ((forall x.
 DijkstraNewEpochExecContext era
 -> Rep (DijkstraNewEpochExecContext era) x)
-> (forall x.
    Rep (DijkstraNewEpochExecContext era) x
    -> DijkstraNewEpochExecContext era)
-> Generic (DijkstraNewEpochExecContext era)
forall x.
Rep (DijkstraNewEpochExecContext era) x
-> DijkstraNewEpochExecContext era
forall x.
DijkstraNewEpochExecContext era
-> Rep (DijkstraNewEpochExecContext era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (DijkstraNewEpochExecContext era) x
-> DijkstraNewEpochExecContext era
forall era x.
DijkstraNewEpochExecContext era
-> Rep (DijkstraNewEpochExecContext era) x
$cfrom :: forall era x.
DijkstraNewEpochExecContext era
-> Rep (DijkstraNewEpochExecContext era) x
from :: forall x.
DijkstraNewEpochExecContext era
-> Rep (DijkstraNewEpochExecContext era) x
$cto :: forall era x.
Rep (DijkstraNewEpochExecContext era) x
-> DijkstraNewEpochExecContext era
to :: forall x.
Rep (DijkstraNewEpochExecContext era) x
-> DijkstraNewEpochExecContext era
Generic)

instance NFData (DijkstraNewEpochExecContext era)

instance ToExpr (DijkstraNewEpochExecContext era)

instance EncCBOR (DijkstraNewEpochExecContext era) where
  encCBOR :: DijkstraNewEpochExecContext era -> Encoding
encCBOR DijkstraNewEpochExecContext {Network
dneecNetworkId :: forall era. DijkstraNewEpochExecContext era -> Network
dneecNetworkId :: Network
..} =
    Encode (Closed Dense) (DijkstraNewEpochExecContext (ZonkAny 0))
-> Encoding
forall (w :: Wrapped) t. Encode w t -> Encoding
encode (Encode (Closed Dense) (DijkstraNewEpochExecContext (ZonkAny 0))
 -> Encoding)
-> Encode (Closed Dense) (DijkstraNewEpochExecContext (ZonkAny 0))
-> Encoding
forall a b. (a -> b) -> a -> b
$
      (Network -> DijkstraNewEpochExecContext (ZonkAny 0))
-> Encode
     (Closed Dense) (Network -> DijkstraNewEpochExecContext (ZonkAny 0))
forall t. t -> Encode (Closed Dense) t
Rec Network -> DijkstraNewEpochExecContext (ZonkAny 0)
forall era. Network -> DijkstraNewEpochExecContext era
DijkstraNewEpochExecContext
        Encode
  (Closed Dense) (Network -> DijkstraNewEpochExecContext (ZonkAny 0))
-> Encode (Closed Dense) Network
-> Encode (Closed Dense) (DijkstraNewEpochExecContext (ZonkAny 0))
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> Network -> Encode (Closed Dense) Network
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To Network
dneecNetworkId

instance ExecSpecRule "NEWEPOCH" DijkstraEra where
  type ExecContext "NEWEPOCH" DijkstraEra = DijkstraNewEpochExecContext DijkstraEra

  translateInputs :: HasCallStack =>
TRC (EraRule "NEWEPOCH" DijkstraEra)
-> SpecTransM
     DijkstraEra
     (ExecContext "NEWEPOCH" DijkstraEra)
     (SpecTRC "NEWEPOCH" DijkstraEra)
translateInputs (TRC (Environment (EraRule "NEWEPOCH" DijkstraEra)
env, State (EraRule "NEWEPOCH" DijkstraEra)
st, Signal (EraRule "NEWEPOCH" DijkstraEra)
sig)) = do
    DijkstraNewEpochExecContext {..} <- SpecTransM
  DijkstraEra
  (DijkstraNewEpochExecContext DijkstraEra)
  (DijkstraNewEpochExecContext DijkstraEra)
forall era ctx. SpecTransM era ctx ctx
askSpecTransM
    agdaEnv <- withCtxSpecTransM () $ toSpecRep env
    agdaSt <- withCtxSpecTransM dneecNetworkId $ toSpecRep st
    agdaSig <- withCtxSpecTransM () $ toSpecRep sig
    pure $ SpecTRC agdaEnv agdaSt agdaSig

  translateOutput :: TRC (EraRule "NEWEPOCH" DijkstraEra)
-> State (EraRule "NEWEPOCH" DijkstraEra)
-> SpecTransM
     DijkstraEra
     (ExecContext "NEWEPOCH" DijkstraEra)
     (SpecState "NEWEPOCH" DijkstraEra)
translateOutput TRC (EraRule "NEWEPOCH" DijkstraEra)
_ = (DijkstraNewEpochExecContext DijkstraEra -> Network)
-> SpecTransM DijkstraEra Network NewEpochState
-> SpecTransM
     DijkstraEra (DijkstraNewEpochExecContext DijkstraEra) NewEpochState
forall ctx ctx' era a.
(ctx -> ctx') -> SpecTransM era ctx' a -> SpecTransM era ctx a
withSpecTransM DijkstraNewEpochExecContext DijkstraEra -> Network
forall era. DijkstraNewEpochExecContext era -> Network
dneecNetworkId (SpecTransM DijkstraEra Network NewEpochState
 -> SpecTransM
      DijkstraEra
      (DijkstraNewEpochExecContext DijkstraEra)
      NewEpochState)
-> (NewEpochState DijkstraEra
    -> SpecTransM DijkstraEra Network NewEpochState)
-> NewEpochState DijkstraEra
-> SpecTransM
     DijkstraEra (DijkstraNewEpochExecContext DijkstraEra) NewEpochState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NewEpochState DijkstraEra
-> SpecTransM DijkstraEra Network NewEpochState
NewEpochState DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (NewEpochState DijkstraEra))
     (SpecRep DijkstraEra (NewEpochState DijkstraEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep

  runAgdaRule :: HasCallStack =>
SpecTRC "NEWEPOCH" DijkstraEra
-> Either Text (SpecState "NEWEPOCH" DijkstraEra)
runAgdaRule (SpecTRC SpecEnvironment "NEWEPOCH" DijkstraEra
env SpecState "NEWEPOCH" DijkstraEra
st SpecSignal "NEWEPOCH" DijkstraEra
sig) = ComputationResult Void NewEpochState -> Either Text NewEpochState
forall a e. ComputationResult Void a -> Either e a
unComputationResult_ (ComputationResult Void NewEpochState -> Either Text NewEpochState)
-> ComputationResult Void NewEpochState
-> Either Text NewEpochState
forall a b. (a -> b) -> a -> b
$ ()
-> NewEpochState -> Integer -> ComputationResult Void NewEpochState
Agda.newEpochStep ()
SpecEnvironment "NEWEPOCH" DijkstraEra
env NewEpochState
SpecState "NEWEPOCH" DijkstraEra
st Integer
SpecSignal "NEWEPOCH" DijkstraEra
sig

instance ExecSpecTopLevelRule "NEWEPOCH" DijkstraEra where
  mkRuleExecContext :: Globals
-> TRC (EraRule "NEWEPOCH" DijkstraEra)
-> ExecContext "NEWEPOCH" DijkstraEra
mkRuleExecContext Globals
globals TRC (EraRule "NEWEPOCH" DijkstraEra)
_ =
    DijkstraNewEpochExecContext
      { dneecNetworkId :: Network
dneecNetworkId = Globals -> Network
networkId Globals
globals
      }