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

module Test.Cardano.Ledger.Conformance.SpecTranslate.Dijkstra.Cert () where

import Cardano.Ledger.BaseTypes (Network)
import Cardano.Ledger.Conway.State (ConwayCertState (..))
import Cardano.Ledger.Dijkstra (DijkstraEra)
import Cardano.Ledger.Dijkstra.TxCert (DijkstraTxCert (..))
import qualified MAlonzo.Code.Ledger.Dijkstra.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance.SpecTranslate.Base (
  SpecTranslate (..),
  withCtxSpecTransM,
 )
import Test.Cardano.Ledger.Conformance.SpecTranslate.Dijkstra.Deleg ()
import Test.Cardano.Ledger.Conformance.SpecTranslate.Dijkstra.GovCert ()
import Test.Cardano.Ledger.Conformance.SpecTranslate.Dijkstra.Pool ()

instance SpecTranslate DijkstraEra (ConwayCertState DijkstraEra) where
  type SpecRep DijkstraEra (ConwayCertState DijkstraEra) = Agda.CertState

  type SpecContext DijkstraEra (ConwayCertState DijkstraEra) = Network

  toSpecRep :: ConwayCertState DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (ConwayCertState DijkstraEra))
     (SpecRep DijkstraEra (ConwayCertState DijkstraEra))
toSpecRep ConwayCertState {DState DijkstraEra
PState DijkstraEra
VState DijkstraEra
conwayCertVState :: VState DijkstraEra
conwayCertPState :: PState DijkstraEra
conwayCertDState :: DState DijkstraEra
conwayCertDState :: forall era. ConwayCertState era -> DState era
conwayCertPState :: forall era. ConwayCertState era -> PState era
conwayCertVState :: forall era. ConwayCertState era -> VState era
..} =
    DState -> PState -> GState -> CertState
Agda.MkCertState
      (DState -> PState -> GState -> CertState)
-> SpecTransM DijkstraEra Network DState
-> SpecTransM DijkstraEra Network (PState -> GState -> CertState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ()
-> SpecTransM DijkstraEra () DState
-> SpecTransM DijkstraEra Network DState
forall ctx era a ctx'.
ctx -> SpecTransM era ctx a -> SpecTransM era ctx' a
withCtxSpecTransM () (DState DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (DState DijkstraEra))
     (SpecRep DijkstraEra (DState DijkstraEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep DState DijkstraEra
conwayCertDState)
      SpecTransM DijkstraEra Network (PState -> GState -> CertState)
-> SpecTransM DijkstraEra Network PState
-> SpecTransM DijkstraEra Network (GState -> CertState)
forall a b.
SpecTransM DijkstraEra Network (a -> b)
-> SpecTransM DijkstraEra Network a
-> SpecTransM DijkstraEra Network b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> PState DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (PState DijkstraEra))
     (SpecRep DijkstraEra (PState DijkstraEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep PState DijkstraEra
conwayCertPState
      SpecTransM DijkstraEra Network (GState -> CertState)
-> SpecTransM DijkstraEra Network GState
-> SpecTransM DijkstraEra Network CertState
forall a b.
SpecTransM DijkstraEra Network (a -> b)
-> SpecTransM DijkstraEra Network a
-> SpecTransM DijkstraEra Network b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ()
-> SpecTransM DijkstraEra () GState
-> SpecTransM DijkstraEra Network GState
forall ctx era a ctx'.
ctx -> SpecTransM era ctx a -> SpecTransM era ctx' a
withCtxSpecTransM () (VState DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (VState DijkstraEra))
     (SpecRep DijkstraEra (VState DijkstraEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep VState DijkstraEra
conwayCertVState)

instance SpecTranslate DijkstraEra (DijkstraTxCert DijkstraEra) where
  type SpecRep DijkstraEra (DijkstraTxCert DijkstraEra) = Agda.DCert

  toSpecRep :: DijkstraTxCert DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (DijkstraTxCert DijkstraEra))
     (SpecRep DijkstraEra (DijkstraTxCert DijkstraEra))
toSpecRep (DijkstraTxCertPool PoolCert
p) = PoolCert
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra PoolCert)
     (SpecRep DijkstraEra PoolCert)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep PoolCert
p
  toSpecRep (DijkstraTxCertGov ConwayGovCert
c) = ConwayGovCert
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra ConwayGovCert)
     (SpecRep DijkstraEra ConwayGovCert)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep ConwayGovCert
c
  toSpecRep (DijkstraTxCertDeleg DijkstraDelegCert
x) = DijkstraDelegCert
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra DijkstraDelegCert)
     (SpecRep DijkstraEra DijkstraDelegCert)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep DijkstraDelegCert
x